Session Grothendieck_Schemes

Theory Set_Extras

text โ€นAuthors: Anthony Bordg and Lawrence Paulsonโ€บ

theory Set_Extras
  imports "Jacobson_Basic_Algebra.Set_Theory"

begin

text โ€นSome new notation for built-in primitivesโ€บ

section โ€นSetsโ€บ

abbreviation complement_in_of:: "'a set โ‡’ 'a set โ‡’ 'a set" ("_โˆ–_" [65,65]65)
  where "A โˆ– B โ‰ก A-B"

section โ€นFunctionsโ€บ

abbreviation preimage:: "('a โ‡’ 'b) โ‡’ 'a set โ‡’ 'b set โ‡’ 'a set" ("_ ยฏ _ _" [90,90,1000]90)
  where "fยฏ X V โ‰ก (vimage f V) โˆฉ X"

lemma preimage_of_inter:
  fixes f::"'a โ‡’ 'b" and X::"'a set" and V::"'b set" and V'::"'b set"
  shows "fยฏ X (V โˆฉ V') = (fยฏ X V) โˆฉ (fยฏ X V')"
  by blast

lemma preimage_identity_self: "identity A ยฏ A B = B โˆฉ A"
  by (simp add: vimage_inter_cong)

text โ€นSimplification actually replaces the RHS by the LHSโ€บ
lemma preimage_vimage_eq: "(f ยฏ (f -` U') U) โˆฉ X = fยฏ X (U โˆฉ U')"
  by simp

definition inverse_map:: "('a โ‡’ 'b) โ‡’ 'a set โ‡’ 'b set โ‡’ ('b โ‡’ 'a)"
  where "inverse_map f S T โ‰ก restrict (inv_into S f) T"

lemma bijective_map_preimage:
  assumes "bijective_map f S T"
  shows "bijective_map (inverse_map f S T) T S"
proof
  show "inverse_map f S T โˆˆ T โ†’E S"
    by (simp add: assms bij_betw_imp_funcset bij_betw_inv_into bijective.bijective bijective_map.axioms(2) inverse_map_def)
  show "bij_betw (inverse_map f S T) T S"
    using assms by (simp add: bij_betw_inv_into bijective_def bijective_map_def inverse_map_def)
qed

lemma inverse_map_identity [simp]:
  "inverse_map (identity S) S S = identity S"
  by (metis Id_compose compose_id_inv_into image_ident image_restrict_eq inv_into_funcset inverse_map_def restrict_extensional)

abbreviation composing ("_ โˆ˜ _ โ†“ _" [60,0,60]59)
  where "g โˆ˜ f โ†“ D โ‰ก compose D g f"

lemma comp_maps:
  assumes "Set_Theory.map ฮท A B" and "Set_Theory.map ฮธ B C"
  shows "Set_Theory.map (ฮธ โˆ˜ ฮท โ†“ A) A C"
proof-
  have "(ฮธ โˆ˜ ฮท โ†“ A) โˆˆ A โ†’E C"
    using assms by (metis Int_iff PiE_def compose_def funcset_compose map.graph restrict_extensional)
  thus ?thesis by (simp add: Set_Theory.map_def)
qed

lemma undefined_is_map_on_empty:
  fixes f:: "'a set โ‡’ 'b set"
  assumes "f = (ฮปx. undefined)"
  shows "map f {} {}"
  using assms by (simp add: map.intro)

lemma restrict_on_source:
  assumes "map f S T"
  shows "restrict f S = f"
  using assms by (meson PiE_restrict map.graph)

lemma restrict_further:
  assumes "map f S T" and "U โŠ† S" and "V โŠ† U"
  shows "restrict (restrict f U) V = restrict f V"
  using assms by (simp add: inf.absorb_iff2)

lemma map_eq:
  assumes "map f S T" and "map g S T" and "โ‹€x. x โˆˆ S โŸน f x = g x"
  shows "f = g"
  using assms by (metis restrict_ext restrict_on_source)

lemma image_subset_of_target:
  assumes "map f S T"
  shows "f ` S โŠ† T"
  using assms by (meson image_subsetI map.map_closed)

end

Theory Group_Extras

text โ€นAuthors: Anthony Bordg and Lawrence Paulsonโ€บ

theory Group_Extras
  imports Main
          "Jacobson_Basic_Algebra.Group_Theory"
          "Set_Extras"

begin

section โ€นFold operator with a subdomainโ€บ

inductive_set
  foldSetD :: "['a set, 'b โ‡’ 'a โ‡’ 'a, 'a] โ‡’ ('b set * 'a) set"
  for D :: "'a set" and f :: "'b โ‡’ 'a โ‡’ 'a" and e :: 'a
  where
    emptyI [intro]: "e โˆˆ D โŸน ({}, e) โˆˆ foldSetD D f e"
  | insertI [intro]: "โŸฆx โˆ‰ A; f x y โˆˆ D; (A, y) โˆˆ foldSetD D f eโŸง โŸน
                      (insert x A, f x y) โˆˆ foldSetD D f e"

inductive_cases empty_foldSetDE [elim!]: "({}, x) โˆˆ foldSetD D f e"

definition
  foldD :: "['a set, 'b โ‡’ 'a โ‡’ 'a, 'a, 'b set] โ‡’ 'a"
  where "foldD D f e A = (THE x. (A, x) โˆˆ foldSetD D f e)"

lemma foldSetD_closed: "(A, z) โˆˆ foldSetD D f e โŸน z โˆˆ D"
  by (erule foldSetD.cases) auto

lemma Diff1_foldSetD:
  "โŸฆ(A - {x}, y) โˆˆ foldSetD D f e; x โˆˆ A; f x y โˆˆ DโŸง โŸน
   (A, f x y) โˆˆ foldSetD D f e"
  by (metis Diff_insert_absorb foldSetD.insertI mk_disjoint_insert)

lemma foldSetD_imp_finite [simp]: "(A, x) โˆˆ foldSetD D f e โŸน finite A"
  by (induct set: foldSetD) auto

lemma finite_imp_foldSetD:
  "โŸฆfinite A; e โˆˆ D; โ‹€x y. โŸฆx โˆˆ A; y โˆˆ DโŸง โŸน f x y โˆˆ DโŸง
    โŸน โˆƒx. (A, x) โˆˆ foldSetD D f e"
proof (induct set: finite)
  case empty then show ?case by auto
next
  case (insert x F)
  then obtain y where y: "(F, y) โˆˆ foldSetD D f e" by auto
  with insert have "y โˆˆ D" by (auto dest: foldSetD_closed)
  with y and insert have "(insert x F, f x y) โˆˆ foldSetD D f e"
    by (intro foldSetD.intros) auto
  then show ?case ..
qed

lemma foldSetD_backwards:
  assumes "A โ‰  {}" "(A, z) โˆˆ foldSetD D f e"
  shows "โˆƒx y. x โˆˆ A โˆง (A - { x }, y) โˆˆ foldSetD D f e โˆง z = f x y"
  using assms(2) by (cases) (simp add: assms(1), metis Diff_insert_absorb insertI1)

subsection โ€นLeft-Commutative Operationsโ€บ

locale LCD =
  fixes B :: "'b set"
  and D :: "'a set"
  and f :: "'b โ‡’ 'a โ‡’ 'a"    (infixl "โ‹…" 70)
  assumes left_commute:
    "โŸฆx โˆˆ B; y โˆˆ B; z โˆˆ DโŸง โŸน x โ‹… (y โ‹… z) = y โ‹… (x โ‹… z)"
  and f_closed [simp, intro!]: "!!x y. โŸฆx โˆˆ B; y โˆˆ DโŸง โŸน f x y โˆˆ D"

lemma (in LCD) foldSetD_closed [dest]: "(A, z) โˆˆ foldSetD D f e โŸน z โˆˆ D"
  by (erule foldSetD.cases) auto

lemma (in LCD) Diff1_foldSetD:
  "โŸฆ(A - {x}, y) โˆˆ foldSetD D f e; x โˆˆ A; A โŠ† BโŸง โŸน
  (A, f x y) โˆˆ foldSetD D f e"
  by (meson Diff1_foldSetD f_closed local.foldSetD_closed subsetCE)

lemma (in LCD) finite_imp_foldSetD:
  "โŸฆfinite A; A โŠ† B; e โˆˆ DโŸง โŸน โˆƒx. (A, x) โˆˆ foldSetD D f e"
proof (induct set: finite)
  case empty then show ?case by auto
next
  case (insert x F)
  then obtain y where y: "(F, y) โˆˆ foldSetD D f e" by auto
  with insert have "y โˆˆ D" by auto
  with y and insert have "(insert x F, f x y) โˆˆ foldSetD D f e"
    by (intro foldSetD.intros) auto
  then show ?case ..
qed


lemma (in LCD) foldSetD_determ_aux:
  assumes "e โˆˆ D" and A: "card A < n" "A โŠ† B" "(A, x) โˆˆ foldSetD D f e" "(A, y) โˆˆ foldSetD D f e"
  shows "y = x"
  using A
proof (induction n arbitrary: A x y)
  case 0
  then show ?case
    by auto
next
  case (Suc n)
  then consider "card A = n" | "card A < n"
    by linarith
  then show ?case
  proof cases
    case 1
    show ?thesis
      using foldSetD.cases [OF โ€น(A,x) โˆˆ foldSetD D (โ‹…) eโ€บ]
    proof cases
      case 1
      then show ?thesis
        using โ€น(A,y) โˆˆ foldSetD D (โ‹…) eโ€บ by auto
    next
      case (2 x' A' y')
      note A' = this
      show ?thesis
        using foldSetD.cases [OF โ€น(A,y) โˆˆ foldSetD D (โ‹…) eโ€บ]
      proof cases
        case 1
        then show ?thesis
          using โ€น(A,x) โˆˆ foldSetD D (โ‹…) eโ€บ by auto
      next
        case (2 x'' A'' y'')
        note A'' = this
        show ?thesis
        proof (cases "x' = x''")
          case True
          show ?thesis
          proof (cases "y' = y''")
            case True
            then show ?thesis
              using A' A'' โ€นx' = x''โ€บ by (blast elim!: equalityE)
          next
            case False
            then show ?thesis
              using A' A'' โ€นx' = x''โ€บ
              by (metis โ€นcard A = nโ€บ Suc.IH Suc.prems(2) card_insert_disjoint foldSetD_imp_finite insert_eq_iff insert_subset lessI)
          qed
        next
          case False
          then have *: "A' - {x''} = A'' - {x'}" "x'' โˆˆ A'" "x' โˆˆ A''"
            using A' A'' by fastforce+
          then have "A' = insert x'' A'' - {x'}"
            using โ€นx' โˆ‰ A'โ€บ by blast
          then have card: "card A' โ‰ค card A''"
            using A' A'' * by (metis card_Suc_Diff1 eq_refl foldSetD_imp_finite)
          obtain u where u: "(A' - {x''}, u) โˆˆ foldSetD D (โ‹…) e"
            using finite_imp_foldSetD [of "A' - {x''}"] A' Diff_insert โ€นA โŠ† Bโ€บ โ€นe โˆˆ Dโ€บ by fastforce
          have "y' = f x'' u"
            using Diff1_foldSetD [OF u] โ€นx'' โˆˆ A'โ€บ โ€นcard A = nโ€บ A' Suc.IH โ€นA โŠ† Bโ€บ by auto
          then have "(A'' - {x'}, u) โˆˆ foldSetD D f e"
            using "*"(1) u by auto
          then have "y'' = f x' u"
            using A'' by (metis * โ€นcard A = nโ€บ A'(1) Diff1_foldSetD Suc.IH โ€นA โŠ† Bโ€บ
                card card_Suc_Diff1 card_insert_disjoint foldSetD_imp_finite insert_subset le_imp_less_Suc)
          then show ?thesis
            using A' A''
            by (metis โ€นA โŠ† Bโ€บ โ€นy' = x'' โ‹… uโ€บ insert_subset left_commute local.foldSetD_closed u)
        qed
      qed
    qed
  next
    case 2 with Suc show ?thesis by blast
  qed
qed

lemma (in LCD) foldSetD_determ:
  "โŸฆ(A, x) โˆˆ foldSetD D f e; (A, y) โˆˆ foldSetD D f e; e โˆˆ D; A โŠ† BโŸง
  โŸน y = x"
  by (blast intro: foldSetD_determ_aux [rule_format])

lemma (in LCD) foldD_equality:
  "โŸฆ(A, y) โˆˆ foldSetD D f e; e โˆˆ D; A โŠ† BโŸง โŸน foldD D f e A = y"
  by (unfold foldD_def) (blast intro: foldSetD_determ)

lemma foldD_empty [simp]:
  "e โˆˆ D โŸน foldD D f e {} = e"
  by (unfold foldD_def) blast

lemma (in LCD) foldD_insert_aux:
  "โŸฆx โˆ‰ A; x โˆˆ B; e โˆˆ D; A โŠ† BโŸง
    โŸน ((insert x A, v) โˆˆ foldSetD D f e) โŸท (โˆƒy. (A, y) โˆˆ foldSetD D f e โˆง v = f x y)"
  apply auto
  by (metis Diff_insert_absorb f_closed finite_Diff foldSetD.insertI foldSetD_determ foldSetD_imp_finite insert_subset local.finite_imp_foldSetD local.foldSetD_closed)

lemma (in LCD) foldD_insert:
  assumes "finite A" "x โˆ‰ A" "x โˆˆ B" "e โˆˆ D" "A โŠ† B"
  shows "foldD D f e (insert x A) = f x (foldD D f e A)"
proof -
  have "(THE v. โˆƒy. (A, y) โˆˆ foldSetD D (โ‹…) e โˆง v = x โ‹… y) = x โ‹… (THE y. (A, y) โˆˆ foldSetD D (โ‹…) e)"
    by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in โ€นmetis+โ€บ)
  then show ?thesis
    unfolding foldD_def using assms by (simp add: foldD_insert_aux)
qed

lemma (in LCD) foldD_closed [simp]:
  "โŸฆfinite A; e โˆˆ D; A โŠ† BโŸง โŸน foldD D f e A โˆˆ D"
proof (induct set: finite)
  case empty then show ?case by simp
next
  case insert then show ?case by (simp add: foldD_insert)
qed

lemma (in LCD) foldD_commute:
  "โŸฆfinite A; x โˆˆ B; e โˆˆ D; A โŠ† BโŸง โŸน
   f x (foldD D f e A) = foldD D f (f x e) A"
  by (induct set: finite) (auto simp add: left_commute foldD_insert)

lemma Int_mono2:
  "โŸฆA โŠ† C; B โŠ† CโŸง โŸน A Int B โŠ† C"
  by blast

lemma (in LCD) foldD_nest_Un_Int:
  "โŸฆfinite A; finite C; e โˆˆ D; A โŠ† B; C โŠ† BโŸง โŸน
   foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
proof (induction set: finite)
  case (insert x F)
  then show ?case
    by (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb Int_mono2)
qed simp

lemma (in LCD) foldD_nest_Un_disjoint:
  "โŸฆfinite A; finite B; A Int B = {}; e โˆˆ D; A โŠ† B; C โŠ† BโŸง
    โŸน foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
  by (simp add: foldD_nest_Un_Int)

โ€• โ€นDelete rules to do with โ€นfoldSetDโ€บ relation.โ€บ

declare foldSetD_imp_finite [simp del]
  empty_foldSetDE [rule del]
  foldSetD.intros [rule del]
declare (in LCD)
  foldSetD_closed [rule del]

section โ€นMonoidsโ€บ

lemma comp_monoid_morphisms:
  assumes "monoid_homomorphism ฮท A multA oneA B multB oneB" and
          "monoid_homomorphism ฮธ B multB oneB C multC oneC"
shows "monoid_homomorphism (ฮธ โˆ˜ ฮท โ†“ A) A multA oneA C multC oneC"
proof-
  have "map (ฮธ โˆ˜ ฮท โ†“ A) A C" using assms comp_maps by (metis monoid_homomorphism.axioms(1))
  moreover have "(ฮธ โˆ˜ ฮท โ†“ A) oneA = oneC"
    using assms
    by (metis compose_eq monoid.unit_closed monoid_homomorphism.axioms(2) monoid_homomorphism.commutes_with_unit)
  moreover have "(ฮธ โˆ˜ ฮท โ†“ A) (multA x y) = multC ((ฮธ โˆ˜ ฮท โ†“ A) x) ((ฮธ โˆ˜ ฮท โ†“ A) y)"
      if "x โˆˆ A" "y โˆˆ A" for x y
    using that assms monoid_homomorphism.commutes_with_composition
    by (smt compose_eq map.map_closed monoid.composition_closed monoid_homomorphism.axioms)
  ultimately show ?thesis
    using monoid_homomorphism_def assms comp_maps by (smt monoid_homomorphism_axioms.intro)
qed

text โ€นCommutative Monoidsโ€บ

text โ€น
  We enter a more restrictive context, with โ€นf :: 'a โ‡’ 'a โ‡’ 'aโ€บ
  instead of โ€น'b โ‡’ 'a โ‡’ 'aโ€บ.
โ€บ

locale ACeD =
  fixes D :: "'a set"
    and f :: "'a โ‡’ 'a โ‡’ 'a"    (infixl "โ‹…" 70)
    and e :: 'a
  assumes ident [simp]: "x โˆˆ D โŸน x โ‹… e = x"
    and commute: "โŸฆx โˆˆ D; y โˆˆ DโŸง โŸน x โ‹… y = y โ‹… x"
    and assoc: "โŸฆx โˆˆ D; y โˆˆ D; z โˆˆ DโŸง โŸน (x โ‹… y) โ‹… z = x โ‹… (y โ‹… z)"
    and e_closed [simp]: "e โˆˆ D"
    and f_closed [simp]: "โŸฆx โˆˆ D; y โˆˆ DโŸง โŸน x โ‹… y โˆˆ D"

lemma (in ACeD) left_commute:
  "โŸฆx โˆˆ D; y โˆˆ D; z โˆˆ DโŸง โŸน x โ‹… (y โ‹… z) = y โ‹… (x โ‹… z)"
proof -
  assume D: "x โˆˆ D" "y โˆˆ D" "z โˆˆ D"
  then have "x โ‹… (y โ‹… z) = (y โ‹… z) โ‹… x" by (simp add: commute)
  also from D have "... = y โ‹… (z โ‹… x)" by (simp add: assoc)
  also from D have "z โ‹… x = x โ‹… z" by (simp add: commute)
  finally show ?thesis .
qed

lemmas (in ACeD) AC = assoc commute left_commute

lemma (in ACeD) left_ident [simp]: "x โˆˆ D โŸน e โ‹… x = x"
proof -
  assume "x โˆˆ D"
  then have "x โ‹… e = x" by (rule ident)
  with โ€นx โˆˆ Dโ€บ show ?thesis by (simp add: commute)
qed

lemma (in ACeD) foldD_Un_Int:
  "โŸฆfinite A; finite B; A โŠ† D; B โŠ† DโŸง โŸน
    foldD D f e A โ‹… foldD D f e B =
    foldD D f e (A Un B) โ‹… foldD D f e (A Int B)"
proof (induction set: finite)
  case empty
  then show ?case
    by(simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
next
  case (insert x F)
  then show ?case
    by(simp add: AC insert_absorb Int_insert_left Int_mono2
                 LCD.foldD_insert [OF LCD.intro [of D]]
                 LCD.foldD_closed [OF LCD.intro [of D]])
qed

lemma (in ACeD) foldD_Un_disjoint:
  "โŸฆfinite A; finite B; A Int B = {}; A โŠ† D; B โŠ† DโŸง โŸน
    foldD D f e (A Un B) = foldD D f e A โ‹… foldD D f e B"
  by (simp add: foldD_Un_Int
    left_commute LCD.foldD_closed [OF LCD.intro [of D]])


subsection โ€นFinite Productsโ€บ

context monoid
begin

definition finprod:: "'b set => ('b => 'a) โ‡’ 'a"
  where "finprod I f โ‰ก if finite I then foldD M (composition โˆ˜ f) ๐Ÿญ I else ๐Ÿญ"

end (* monoid *)


section โ€นGroupsโ€บ

lemma comp_group_morphisms:
  assumes "group_homomorphism ฮท A multA oneA B multB oneB" and
"group_homomorphism ฮธ B multB oneB C multC oneC"
shows "group_homomorphism (ฮธ โˆ˜ ฮท โ†“ A) A multA oneA C multC oneC"
  using assms group_homomorphism_def comp_monoid_morphisms by metis

subsection โ€นSubgroup Generated by a Subsetโ€บ

context group
begin

inductive_set generate :: "'a set โ‡’ 'a set"
  for H where
    unit:  "๐Ÿญ โˆˆ generate H"
  | incl: "a โˆˆ H โŸน a โˆˆ generate H"
  | inv:  "a โˆˆ H โŸน inverse a โˆˆ generate H"
  | mult:  "a โˆˆ generate H โŸน b โˆˆ generate H โŸน a โ‹… b โˆˆ generate H"

lemma generate_into_G: "a โˆˆ generate (G โˆฉ H) โŸน a โˆˆ G"
  by (induction rule: generate.induct) auto


definition subgroup_generated :: "'a set โ‡’ 'a set"
  where "subgroup_generated S = generate (G โˆฉ S)"

lemma inverse_in_subgroup_generated: "a โˆˆ subgroup_generated H โŸน inverse a โˆˆ subgroup_generated H"
  unfolding subgroup_generated_def
proof (induction rule: generate.induct)
  case (mult a b)
  then show ?case
    by (simp add: generate.mult generate_into_G inverse_composition_commute)
qed (auto simp add: generate.unit generate.incl generate.inv)

lemma subgroup_generated_is_monoid:
  fixes H
  shows "Group_Theory.monoid (subgroup_generated H) (โ‹…) ๐Ÿญ"
  unfolding subgroup_generated_def
proof qed (auto simp: generate.unit generate.mult associative generate_into_G)

lemma subgroup_generated_is_subset:
  fixes H
  shows "subgroup_generated H โŠ† G"
    using generate_into_G subgroup_generated_def by blast

lemma subgroup_generated_is_subgroup:
  fixes H
  shows "subgroup (subgroup_generated H) G (โ‹…) ๐Ÿญ"
proof
  show "subgroup_generated H โŠ† G"
    by (simp add: subgroup_generated_is_subset)
  show "a โ‹… b โˆˆ subgroup_generated H"
    if "a โˆˆ subgroup_generated H" "b โˆˆ subgroup_generated H" for a b
    using that by (meson monoid.composition_closed subgroup_generated_is_monoid)
  show "a โ‹… b โ‹… c = a โ‹… (b โ‹… c)"
    if "a โˆˆ subgroup_generated H" "b โˆˆ subgroup_generated H" "c โˆˆ subgroup_generated H"
    for a b c
    using that by (meson monoid.associative subgroup_generated_is_monoid)
  show "monoid.invertible (subgroup_generated H) (โ‹…) ๐Ÿญ u"
    if "u โˆˆ subgroup_generated H" for u
  proof (rule monoid.invertibleI )
    show "Group_Theory.monoid (subgroup_generated H) (โ‹…) ๐Ÿญ"
      by (simp add: subgroup_generated_is_monoid)
    show "u โ‹… local.inverse u = ๐Ÿญ" "local.inverse u โ‹… u = ๐Ÿญ" "u โˆˆ subgroup_generated H"
      using โ€นsubgroup_generated H โŠ† Gโ€บ that by auto
    show "local.inverse u โˆˆ subgroup_generated H"
      using inverse_in_subgroup_generated that by blast
  qed
qed (auto simp: generate_into_G generate.unit subgroup_generated_def)


end (* group *)


section โ€นAbelian Groupsโ€บ

context abelian_group
begin

definition minus:: "'a โ‡’ 'a โ‡’ 'a" (infixl "โ€" 70)
  where "x โ€ y โ‰ก x โ‹… inverse y "

definition finsum:: "'b set โ‡’ ('b โ‡’ 'a) โ‡’ 'a"
  where "finsum I f โ‰ก finprod I f"

(* A notation "โˆ‘iโˆˆI. f i" should be introduced for a sum of a family of elements of an abelian group *)

end (* abelian_group*)

end

Theory Topological_Space

text โ€นAuthors: Anthony Bordg and Lawrence Paulson,
with some contributions from Wenda Liโ€บ

theory Topological_Space
  imports Complex_Main
          "Jacobson_Basic_Algebra.Set_Theory"
          Set_Extras

begin

section โ€นTopological Spacesโ€บ

locale topological_space = fixes S :: "'a set" and is_open :: "'a set โ‡’ bool"
  assumes open_space [simp, intro]: "is_open S" and open_empty [simp, intro]: "is_open {}"
    and open_imp_subset: "is_open U โŸน U โŠ† S"
    and open_inter [intro]: "โŸฆis_open U; is_open VโŸง โŸน is_open (U โˆฉ V)"
    and open_union [intro]: "โ‹€F::('a set) set. (โ‹€x. x โˆˆ F โŸน is_open x) โŸน is_open (โ‹ƒxโˆˆF. x)"

begin

definition is_closed :: "'a set โ‡’ bool"
  where "is_closed U โ‰ก U โŠ† S โˆง is_open (S - U)"

definition neighborhoods:: "'a โ‡’ ('a set) set"
  where "neighborhoods x โ‰ก {U. is_open U โˆง x โˆˆ U}"

text โ€นNote that by a neighborhood we mean what some authors call an open neighborhood.โ€บ

lemma open_union' [intro]: "โ‹€F::('a set) set. (โ‹€x. x โˆˆ F โŸน is_open x) โŸน is_open (โ‹ƒF)"
  using open_union by auto

lemma open_preimage_identity [simp]: "is_open B โŸน identity S ยฏ S B = B"
  by (metis inf.orderE open_imp_subset preimage_identity_self)


definition is_connected:: "bool" where
"is_connected โ‰ก ยฌ (โˆƒU V. is_open U โˆง is_open V โˆง (U โ‰  {}) โˆง (V โ‰  {}) โˆง (U โˆฉ V = {}) โˆง (U โˆช V = S))"

definition is_hausdorff:: "bool" where
"is_hausdorff โ‰ก
โˆ€x y. (x โˆˆ S โˆง y โˆˆ S โˆง x โ‰  y) โŸถ (โˆƒU V. U โˆˆ neighborhoods x โˆง V โˆˆ neighborhoods y โˆง U โˆฉ V = {})"

end (* topological_space *)

text โ€นT2 spaces are also known as Hausdorff spaces.โ€บ

locale t2_space = topological_space +
  assumes hausdorff: "is_hausdorff"


subsection โ€นTopological Basisโ€บ

inductive generated_topology :: "'a set โ‡’ 'a set set โ‡’ 'a set โ‡’ bool"
    for S :: "'a set" and B :: "'a set set"
  where
    UNIV: "generated_topology S B S"
  | Int: "generated_topology S B (U โˆฉ V)"
            if "generated_topology S B U" and "generated_topology S B V"
  | UN: "generated_topology S B (โ‹ƒK)" if "(โ‹€U. U โˆˆ K โŸน generated_topology S B U)"
  | Basis: "generated_topology S B b" if "b โˆˆ B โˆง b โŠ† S"

lemma generated_topology_empty [simp]: "generated_topology S B {}"
  by (metis UN Union_empty empty_iff)

lemma generated_topology_subset: "generated_topology S B U โŸน U โŠ† S"
  by (induct rule:generated_topology.induct) auto

lemma generated_topology_is_topology:
  fixes S:: "'a set" and B:: "'a set set"
  shows "topological_space S (generated_topology S B)"
  by (simp add: Int UN UNIV generated_topology_subset topological_space_def)


subsection โ€นCoversโ€บ

locale cover_of_subset =
  fixes X:: "'a set" and U:: "'a set" and index:: "real set" and cover:: "real โ‡’ 'a set"
(* We use real instead of index::"'b set" otherwise we get some troubles with locale sheaf_of_rings
in Comm_Ring_Theory.thy *)
  assumes is_subset: "U โŠ† X" and are_subsets: "โ‹€i. i โˆˆ index โŸน cover i โŠ† X"
and covering: "U โŠ† (โ‹ƒiโˆˆindex. cover i)"
begin

lemma
  assumes "x โˆˆ U"
  shows "โˆƒiโˆˆindex. x โˆˆ cover i"
  using assms covering by auto

definition select_index:: "'a โ‡’ real"
  where "select_index x โ‰ก SOME i. i โˆˆ index โˆง x โˆˆ cover i"

lemma cover_of_select_index:
  assumes "x โˆˆ U"
  shows "x โˆˆ cover (select_index x)"
  using assms by (metis (mono_tags, lifting) UN_iff covering select_index_def someI_ex subset_iff)

lemma select_index_belongs:
  assumes "x โˆˆ U"
  shows "select_index x โˆˆ index"
  using assms by (metis (full_types, lifting) UN_iff covering in_mono select_index_def tfl_some)

end (* cover_of_subset *)

locale open_cover_of_subset = topological_space X is_open + cover_of_subset X U I C
  for X and is_open and U and I and C +
  assumes are_open_subspaces: "โ‹€i. iโˆˆI โŸน is_open (C i)"
begin

lemma cover_of_select_index_is_open:
  assumes "x โˆˆ U"
  shows "is_open (C (select_index x))"
  using assms by (simp add: are_open_subspaces select_index_belongs)

end (* open_cover_of_subset *)

locale open_cover_of_open_subset = open_cover_of_subset X is_open U I C
  for X and is_open and U and I and C +
  assumes is_open_subset: "is_open U"


subsection โ€นInduced Topologyโ€บ

locale ind_topology = topological_space X is_open for X and is_open +
  fixes S:: "'a set"
  assumes is_subset: "S โŠ† X"
begin

definition ind_is_open:: "'a set โ‡’ bool"
  where "ind_is_open U โ‰ก U โŠ† S โˆง (โˆƒV. V โŠ† X โˆง is_open V โˆง U = S โˆฉ V)"

lemma ind_is_open_S [iff]: "ind_is_open S"
    by (metis ind_is_open_def inf.orderE is_subset open_space order_refl)

lemma ind_is_open_empty [iff]: "ind_is_open {}"
    using ind_is_open_def by auto

lemma ind_space_is_top_space:
  shows "topological_space S (ind_is_open)"
proof
  fix U V
  assume "ind_is_open U" then obtain UX where "UX โŠ† X" "is_open UX" "U = S โˆฉ UX"
    using ind_is_open_def by auto
  moreover
  assume "ind_is_open V" then obtain VX where "VX โŠ† X" "is_open VX" "V = S โˆฉ VX"
    using ind_is_open_def by auto
  ultimately have "is_open (UX โˆฉ VX) โˆง (U โˆฉ V = S โˆฉ (UX โˆฉ VX))" using open_inter by auto
  then show "ind_is_open (U โˆฉ V)"
    by (metis โ€นUX โŠ† Xโ€บ ind_is_open_def le_infI1 subset_refl)
next
  fix F
  assume F: "โ‹€x. x โˆˆ F โŸน ind_is_open x"
  obtain F' where F': "โ‹€x. x โˆˆ F โˆง ind_is_open x โŸน is_open (F' x) โˆง x = S โˆฉ (F' x)"
    using ind_is_open_def by metis
  have "is_open (โ‹ƒ (F' ` F))"
    by (metis (mono_tags, lifting) F F' imageE image_ident open_union)
  moreover
  have "(โ‹ƒxโˆˆF. x) = S โˆฉ โ‹ƒ (F' ` F)"
    using F' โ€นโ‹€x. x โˆˆ F โŸน ind_is_open xโ€บ by fastforce
  ultimately show "ind_is_open (โ‹ƒxโˆˆF. x)"
    by (metis ind_is_open_def inf_sup_ord(1) open_imp_subset)
next
  show "โ‹€U. ind_is_open U โŸน U โŠ† S"
    by (simp add: ind_is_open_def)
qed auto

lemma is_open_from_ind_is_open:
  assumes "is_open S" and "ind_is_open U"
  shows "is_open U"
  using assms open_inter ind_is_open_def is_subset by auto

lemma open_cover_from_ind_open_cover:
  assumes "is_open S" and "open_cover_of_open_subset S ind_is_open U I C"
  shows "open_cover_of_open_subset X is_open U I C"
proof
  show "is_open U"
    using assms is_open_from_ind_is_open open_cover_of_open_subset.is_open_subset by blast
  show "โ‹€i. i โˆˆ I โŸน is_open (C i)"
    using assms is_open_from_ind_is_open open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces by blast
  show "โ‹€i. i โˆˆ I โŸน C i โŠ† X"
    using assms(2) is_subset
    by (meson cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def subset_trans)
  show "U โŠ† X"
    by (simp add: โ€นis_open Uโ€บ open_imp_subset)
  show "U โŠ† โ‹ƒ (C ` I)"
    by (meson assms(2) cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
qed

end (* induced topology *)

lemma (in topological_space) ind_topology_is_open_self [iff]: "ind_topology S is_open S"
  by (simp add: ind_topology_axioms_def ind_topology_def topological_space_axioms)

lemma (in topological_space) ind_topology_is_open_empty [iff]: "ind_topology S is_open {}"
  by (simp add: ind_topology_axioms_def ind_topology_def topological_space_axioms)

lemma (in topological_space) ind_is_open_iff_open:
  shows "ind_topology.ind_is_open S is_open S U โŸท is_open U โˆง U โŠ† S"
  by (metis ind_topology.ind_is_open_def ind_topology_is_open_self inf.absorb_iff2)

subsection โ€นContinuous Mapsโ€บ

locale continuous_map = source: topological_space S is_open + target: topological_space S' is_open'
+ map f S S'
  for S and is_open and S' and is_open' and f +
  assumes is_continuous: "โ‹€U. is_open' U โŸน is_open (fยฏ S U)"
begin

lemma open_cover_of_open_subset_from_target_to_source:
  assumes "open_cover_of_open_subset S' is_open' U I C"
  shows "open_cover_of_open_subset S is_open (fยฏ S U) I (ฮปi. fยฏ S (C i))"
proof
  show "f ยฏ S U โŠ† S" by simp
  show "f ยฏ S (C i) โŠ† S" if "i โˆˆ I" for i
    using that by simp
  show "is_open (f ยฏ S U)"
    by (meson assms is_continuous open_cover_of_open_subset.is_open_subset)
  show "โ‹€i. i โˆˆ I โŸน is_open (f ยฏ S (C i))"
    by (meson assms is_continuous open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces)
  show "f ยฏ S U โŠ† (โ‹ƒiโˆˆI. f ยฏ S (C i))"
    using assms unfolding open_cover_of_open_subset_def cover_of_subset_def open_cover_of_subset_def
    by blast
qed

end (* continuous map *)


subsection โ€นHomeomorphismsโ€บ

text โ€นThe topological isomorphisms between topological spaces are called homeomorphisms.โ€บ

locale homeomorphism =
  continuous_map + bijective_map f S S' +
  continuous_map S' is_open' S is_open "inverse_map f S S'"

lemma (in topological_space) id_is_homeomorphism:
  shows "homeomorphism S is_open S is_open (identity S)"
proof
  show "inverse_map (identity S) S S โˆˆ S โ†’E S"
    by (simp add: inv_into_into inverse_map_def)
qed (auto simp: open_inter bij_betwI')


subsection โ€นTopological Filtersโ€บ (* Imported from HOL.Topological_Spaces *)

definition (in topological_space) nhds :: "'a โ‡’ 'a filter"
  where "nhds a = (INF Sโˆˆ{S. is_open S โˆง a โˆˆ S}. principal S)"

abbreviation (in topological_space)
  tendsto :: "('b โ‡’ 'a) โ‡’ 'a โ‡’ 'b filter โ‡’ bool"  (infixr "โค" 55)
  where "(f โค l) F โ‰ก filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter โ‡’ ('f โ‡’ 'a) โ‡’ 'a"
  where "Lim A f = (THE l. (f โค l) A)"

end

Theory Comm_Ring

text โ€นAuthors: Anthony Bordg and Lawrence Paulson,
with some contributions from Wenda Liโ€บ

theory Comm_Ring
  imports
    "Group_Extras"
    "Topological_Space"
    "Jacobson_Basic_Algebra.Ring_Theory"
    "Set_Extras"
begin

(*Suppresses the built-in plus sign, but why does
 no_notation minus (infixl "-" 65)
cause errors with monoid subtraction below? --LCP
*)
no_notation plus (infixl "+" 65)

lemma (in monoid_homomorphism) monoid_preimage: "Group_Theory.monoid (ฮท ยฏ M M') (โ‹…) ๐Ÿญ"
  by (simp add: Int_absorb1 source.monoid_axioms subsetI)

lemma (in group_homomorphism) group_preimage: "Group_Theory.group (ฮท ยฏ G G') (โ‹…) ๐Ÿญ"
  by (simp add: Int_absorb1 source.group_axioms subsetI)

lemma (in ring_homomorphism) ring_preimage: "ring (ฮท ยฏ R R') (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  by (simp add: Int_absorb2 Int_commute source.ring_axioms subset_iff)

section โ€นCommutative Ringsโ€บ

subsection โ€นCommutative Ringsโ€บ

locale comm_ring = ring +
  assumes comm_mult: "โŸฆ a โˆˆ R; b โˆˆ R โŸง โŸน a โ‹… b = b โ‹… a"

text โ€นThe zero ring is a commutative ring.โ€บ

lemma invertible_0: "monoid.invertible {0} (ฮปn m. 0) 0 0"
    using Group_Theory.monoid.intro monoid.unit_invertible by force

interpretation ring0: ring "{0::nat}" "ฮปn m. 0" "ฮปn m. 0" 0 0
  using invertible_0 by unfold_locales auto

declare ring0.additive.left_unit [simp del] ring0.additive.invertible [simp del]
declare ring0.additive.invertible_left_inverse [simp del] ring0.right_zero [simp del]

interpretation cring0: comm_ring "{0::nat}" "ฮปn m. 0" "ฮปn m. 0" 0 0
  by (metis comm_ring_axioms_def comm_ring_def ring0.ring_axioms)

(* def 0.13 *)
definition (in ring) zero_divisor :: "'a โ‡’ 'a โ‡’ bool"
  where "zero_divisor x y โ‰ก (x โ‰  ๐Ÿฌ) โˆง (y โ‰  ๐Ÿฌ) โˆง (x โ‹… y = ๐Ÿฌ)"

subsection โ€นEntire Ringsโ€บ

(* def 0.14 *)
locale entire_ring = comm_ring + assumes units_neq: "๐Ÿญ โ‰  ๐Ÿฌ" and
no_zero_div: "โŸฆ x โˆˆ R; y โˆˆ RโŸง โŸน ยฌ(zero_divisor x y)"

subsection โ€นIdealsโ€บ

context comm_ring begin

lemma mult_left_assoc: "โŸฆ a โˆˆ R; b โˆˆ R; c โˆˆ R โŸง โŸน b โ‹… (a โ‹… c) = a โ‹… (b โ‹… c)"
  using comm_mult multiplicative.associative by auto

lemmas ring_mult_ac = comm_mult multiplicative.associative mult_left_assoc

(* ex. 0.16 *)
lemma ideal_R_R: "ideal R R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
proof qed auto

lemma ideal_0_R: "ideal {๐Ÿฌ} R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
proof
  show "monoid.invertible {๐Ÿฌ} (+) ๐Ÿฌ u"
    if "u โˆˆ {๐Ÿฌ}"
    for u :: 'a
  proof (rule monoid.invertibleI)
    show "Group_Theory.monoid {๐Ÿฌ} (+) ๐Ÿฌ"
    proof qed (use that in auto)
  qed (use that in auto)
qed auto

definition ideal_gen_by_prod :: "'a set โ‡’ 'a set โ‡’ 'a set"
  where "ideal_gen_by_prod ๐”ž ๐”Ÿ โ‰ก additive.subgroup_generated {x. โˆƒa b. x = a โ‹… b โˆง a โˆˆ ๐”ž โˆง b โˆˆ ๐”Ÿ}"

lemma ideal_zero: "ideal A R add mult zero unit โŸน zero โˆˆ A"
  by (simp add: ideal_def subgroup_of_additive_group_of_ring_def subgroup_def submonoid_def submonoid_axioms_def)

lemma ideal_implies_subset:
  assumes "ideal A R add mult zero unit"
  shows "A โŠ† R"
  by (meson assms ideal_def subgroup_def subgroup_of_additive_group_of_ring_def submonoid_axioms_def submonoid_def)

lemma ideal_inverse:
  assumes "a โˆˆ A" "ideal A R (+) mult zero unit"
  shows "additive.inverse a โˆˆ A"
  by (meson additive.invertible assms comm_ring.ideal_implies_subset comm_ring_axioms ideal_def subgroup.subgroup_inverse_iff subgroup_of_additive_group_of_ring_def subsetD)

lemma ideal_add:
  assumes "a โˆˆ A"  "b โˆˆ A" "ideal A R add mult zero unit"
  shows "add a b โˆˆ A"
  by (meson Group_Theory.group_def assms ideal_def monoid.composition_closed subgroup_def subgroup_of_additive_group_of_ring_def)

lemma ideal_mult_in_subgroup_generated:
  assumes ๐”ž: "ideal ๐”ž R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and ๐”Ÿ: "ideal ๐”Ÿ R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and "a โˆˆ ๐”ž" "b โˆˆ ๐”Ÿ"
  shows "a โ‹… b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
  proof -
  have "โˆƒx y. a โ‹… b = x โ‹… y โˆง x โˆˆ ๐”ž โˆง y โˆˆ ๐”Ÿ"
    using assms ideal_implies_subset by blast
  with ideal_implies_subset show ?thesis
    unfolding additive.subgroup_generated_def ideal_gen_by_prod_def
    using assms ideal_implies_subset by (blast intro: additive.generate.incl)
qed

subsection โ€นIdeals generated by an Elementโ€บ

definition gen_ideal:: "'a โ‡’ 'a set" ("โŸจ_โŸฉ")
  where "โŸจxโŸฉ โ‰ก {y. โˆƒrโˆˆR. y = r โ‹… x}"

lemma zero_in_gen_ideal:
  assumes "x โˆˆ R"
  shows "๐Ÿฌ โˆˆ โŸจxโŸฉ"
proof -
  have "โˆƒa. a โˆˆ R โˆง ๐Ÿฌ = a โ‹… x"
    by (metis (lifting) additive.unit_closed assms left_zero)
  then show ?thesis
    using gen_ideal_def by blast
qed

lemma add_in_gen_ideal:
  "โŸฆx โˆˆ R; a โˆˆ โŸจxโŸฉ; b โˆˆ โŸจxโŸฉโŸง โŸน a + b โˆˆ โŸจxโŸฉ"
    apply (clarsimp simp : gen_ideal_def)
  by (metis (no_types) additive.composition_closed distributive(2))

lemma gen_ideal_subset:
  assumes "x โˆˆ R"
  shows "โŸจxโŸฉ โŠ† R"
  using assms comm_ring.gen_ideal_def local.comm_ring_axioms by fastforce

lemma gen_ideal_monoid:
  assumes "x โˆˆ R"
  shows "Group_Theory.monoid โŸจxโŸฉ (+) ๐Ÿฌ"
proof
  show "a + b โˆˆ โŸจxโŸฉ" if "a โˆˆ โŸจxโŸฉ" "b โˆˆ โŸจxโŸฉ" for a b
    by (simp add: add_in_gen_ideal assms that)
qed (use assms zero_in_gen_ideal gen_ideal_def in auto)

lemma gen_ideal_group:
  assumes "x โˆˆ R"
  shows "Group_Theory.group โŸจxโŸฉ (+) ๐Ÿฌ"
proof
  fix a b c
  assume "a โˆˆ โŸจxโŸฉ" "b โˆˆ โŸจxโŸฉ" "c โˆˆ โŸจxโŸฉ"
  then show "a + b + c = a + (b + c)"
    by (meson assms gen_ideal_monoid monoid.associative)
next
  fix a
  assume a: "a โˆˆ โŸจxโŸฉ"
  show "๐Ÿฌ + a = a"
    by (meson a assms gen_ideal_monoid monoid.left_unit)
  show "a + ๐Ÿฌ = a"
    by (meson a assms gen_ideal_monoid monoid.right_unit)
  interpret M: monoid "โŸจxโŸฉ" "(+)" ๐Ÿฌ
    by (simp add: assms gen_ideal_monoid)
  obtain r where r: "rโˆˆR" "a = r โ‹… x"
    using a gen_ideal_def by auto
  show "monoid.invertible โŸจxโŸฉ (+) ๐Ÿฌ a"
  proof (rule M.invertibleI)
    have "โˆƒrโˆˆR. - a = r โ‹… x"
      by (metis assms ideal_R_R ideal_inverse local.left_minus r)
    then show "-a โˆˆ โŸจxโŸฉ" by (simp add: gen_ideal_def)
  qed (use a r assms in auto)
qed (auto simp: zero_in_gen_ideal add_in_gen_ideal assms)

lemma gen_ideal_ideal:
  assumes "x โˆˆ R"
  shows "ideal โŸจxโŸฉ R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
proof intro_locales
  show "submonoid_axioms โŸจxโŸฉ R (+) ๐Ÿฌ"
    by (simp add: add_in_gen_ideal assms gen_ideal_subset submonoid_axioms.intro zero_in_gen_ideal)
  show "Group_Theory.group_axioms โŸจxโŸฉ (+) ๐Ÿฌ"
    by (meson Group_Theory.group_def assms gen_ideal_group)
  show "ideal_axioms โŸจxโŸฉ R (โ‹…)"
  proof
    fix a b
    assume "a โˆˆ R" "b โˆˆ โŸจxโŸฉ"
    then obtain r where r: "rโˆˆR" "b = r โ‹… x"
      by (auto simp add: gen_ideal_def)
    have "a โ‹… (r โ‹… x) = (a โ‹… r) โ‹… x"
      using โ€นa โˆˆ Rโ€บ โ€นr โˆˆ Rโ€บ assms multiplicative.associative by presburger
    then show "a โ‹… b โˆˆ โŸจxโŸฉ"
      using โ€นa โˆˆ Rโ€บ r gen_ideal_def by blast
    then show "b โ‹… a โˆˆ โŸจxโŸฉ"
      by (simp add: โ€นa โˆˆ Rโ€บ assms comm_mult r)
  qed
qed (auto simp add: assms gen_ideal_monoid)


subsection โ€นExercisesโ€บ

lemma in_ideal_gen_by_prod:
  assumes ๐”ž: "ideal ๐”ž R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and ๐”Ÿ: "ideal ๐”Ÿ R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
    and "a โˆˆ R" and b: "b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
  shows "a โ‹… b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
  using b โ€นa โˆˆ Rโ€บ
  unfolding additive.subgroup_generated_def ideal_gen_by_prod_def
proof (induction arbitrary: a)
  case unit
  then show ?case
    by (simp add: additive.generate.unit)
next
  case (incl x u)
  with ๐”ž ๐”Ÿ have "โ‹€a b. โŸฆa โ‹… b โˆˆ R; a โˆˆ ๐”ž; b โˆˆ ๐”ŸโŸง โŸน โˆƒx y. u โ‹… (a โ‹… b) = x โ‹… y โˆง x โˆˆ ๐”ž โˆง y โˆˆ ๐”Ÿ"
    by simp (metis ideal.ideal(1) ideal_implies_subset multiplicative.associative subset_iff)
  then show ?case
    using additive.generate.incl incl.hyps incl.prems by force
next
  case (inv u v)
  then show ?case
  proof clarsimp
    fix a b
    assume "v โˆˆ R" "a โ‹… b โˆˆ R" "a โˆˆ ๐”ž" "b โˆˆ ๐”Ÿ"
    then have "v โ‹… (- a โ‹… b) = v โ‹… a โ‹… (- b) โˆง v โ‹… a โˆˆ ๐”ž โˆง - b โˆˆ ๐”Ÿ"
      by (metis ๐”ž ๐”Ÿ ideal.ideal(1) ideal_implies_subset ideal_inverse in_mono local.right_minus multiplicative.associative)
    then show "v โ‹… (- a โ‹… b) โˆˆ additive.generate (R โˆฉ {a โ‹… b |a b. a โˆˆ ๐”ž โˆง b โˆˆ ๐”Ÿ})"
      using ๐”ž ๐”Ÿ additive.subgroup_generated_def ideal_mult_in_subgroup_generated
      unfolding ideal_gen_by_prod_def
      by presburger
  qed
next
  case (mult u v)
  then show ?case
    using additive.generate.mult additive.generate_into_G distributive(1) by force
qed

(* ex. 0.12 *)
lemma ideal_subgroup_generated:
  assumes "ideal ๐”ž R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and "ideal ๐”Ÿ R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  shows "ideal (ideal_gen_by_prod ๐”ž ๐”Ÿ) R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  proof
  show "ideal_gen_by_prod ๐”ž ๐”Ÿ โŠ† R"
    by (simp add: additive.subgroup_generated_is_subset ideal_gen_by_prod_def)
  show "a + b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
    if "a โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ" "b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
    for a b
    using that additive.subgroup_generated_is_monoid monoid.composition_closed
    by (fastforce simp: ideal_gen_by_prod_def)
  show "๐Ÿฌ โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
    using additive.generate.unit additive.subgroup_generated_def ideal_gen_by_prod_def by presburger
  show "a + b + c = a + (b + c)"
    if "a โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ" "b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ" "c โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
    for a b c
    using that additive.subgroup_generated_is_subset
    unfolding ideal_gen_by_prod_def
    by blast
  show "๐Ÿฌ + a = a" "a + ๐Ÿฌ = a"
    if "a โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ" for a
    using that additive.subgroup_generated_is_subset unfolding ideal_gen_by_prod_def
    by blast+
  show "monoid.invertible (ideal_gen_by_prod ๐”ž ๐”Ÿ) (+) ๐Ÿฌ u"
    if "u โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ" for u
    using that additive.subgroup_generated_is_subgroup group.invertible
    unfolding ideal_gen_by_prod_def subgroup_def
    by fastforce
  show "a โ‹… b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
    if "a โˆˆ R" "b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ" for a b
    using that by (simp add: assms in_ideal_gen_by_prod)
  then show "b โ‹… a โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ"
    if "a โˆˆ R" "b โˆˆ ideal_gen_by_prod ๐”ž ๐”Ÿ" for a b
    using that
    by (metis โ€นideal_gen_by_prod ๐”ž ๐”Ÿ โŠ† Rโ€บ comm_mult in_mono)
qed

lemma ideal_gen_by_prod_is_inter:
  assumes "ideal ๐”ž R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and "ideal ๐”Ÿ R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  shows "ideal_gen_by_prod ๐”ž ๐”Ÿ = โ‹‚ {I. ideal I R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ โˆง {a โ‹… b |a b. a โˆˆ ๐”ž โˆง b โˆˆ ๐”Ÿ} โŠ† I}"
    (is "?lhs = ?rhs")
proof
  have "x โˆˆ ?rhs" if "x โˆˆ ?lhs" for x
    using that
    unfolding ideal_gen_by_prod_def additive.subgroup_generated_def
    by induction (force simp: ideal_zero ideal_inverse ideal_add)+
  then show "?lhs โŠ† ?rhs" by blast
  show "?rhs โŠ† ?lhs"
    using assms ideal_subgroup_generated by (force simp: ideal_mult_in_subgroup_generated)
qed

end (* comm_ring *)

text โ€นdef. 0.18, see remark 0.20โ€บ
locale pr_ideal = comm:comm_ring R "(+)" "(โ‹…)" "๐Ÿฌ" "๐Ÿญ" + ideal I R "(+)" "(โ‹…)" "๐Ÿฌ" "๐Ÿญ"
  for R and I and addition (infixl "+" 65) and multiplication (infixl "โ‹…" 70) and zero ("๐Ÿฌ") and
unit ("๐Ÿญ")
+ assumes carrier_neq: "I โ‰  R" and absorbent: "โŸฆx โˆˆ R; y โˆˆ RโŸง โŸน (x โ‹… y โˆˆ I) โŸน (x โˆˆ I โˆจ y โˆˆ I)"
begin

text โ€น
Note that in the locale prime ideal the order of I and R is reversed with respect to the locale
ideal, so that we can introduce some syntactic sugar later.
โ€บ

text โ€นremark 0.21โ€บ
lemma not_1 [simp]:
  shows "๐Ÿญ โˆ‰ I"
proof
  assume "๐Ÿญ โˆˆ I"
  then have "โ‹€x. โŸฆ๐Ÿญ โˆˆ I; x โˆˆ RโŸง โŸน x โˆˆ I"
    by (metis ideal(1) comm.multiplicative.right_unit)
  with โ€น๐Ÿญ โˆˆ Iโ€บ have "I = R"
    by auto
  then show False
    using carrier_neq by blast
qed

lemma not_invertible:
  assumes "x โˆˆ I"
  shows "ยฌ comm.multiplicative.invertible x"
  using assms ideal(2) not_1 by blast

text โ€นex. 0.22โ€บ
lemma submonoid_notin:
  assumes "S = {x โˆˆ R. x โˆ‰ I}"
  shows "submonoid S R (โ‹…) ๐Ÿญ"
proof
  show "S โŠ† R"
    using assms by force
  show "a โ‹… b โˆˆ S"
    if "a โˆˆ S"
      and "b โˆˆ S"
    for a :: 'a
      and b :: 'a
    using that
    using absorbent assms by blast
  show "๐Ÿญ โˆˆ S"
    using assms carrier_neq ideal(1) by fastforce
qed

end (* pr_ideal *)


section โ€นSpectrum of a ringโ€บ

subsection โ€นThe Zariski Topologyโ€บ

context comm_ring begin

text โ€นNotation 1โ€บ
definition closed_subsets :: "'a set โ‡’ ('a set) set" ("๐’ฑ _" [900] 900)
  where "๐’ฑ ๐”ž โ‰ก {I. pr_ideal R I (+) (โ‹…) ๐Ÿฌ ๐Ÿญ โˆง ๐”ž โŠ† I}"

text โ€นNotation 2โ€บ
definition spectrum :: "('a set) set" ("Spec")
  where "Spec โ‰ก {I. pr_ideal R I (+) (โ‹…) ๐Ÿฌ ๐Ÿญ}"

lemma cring0_spectrum_eq [simp]: "cring0.spectrum = {}"
  unfolding cring0.spectrum_def pr_ideal_def
  by (metis (no_types, lifting) Collect_empty_eq cring0.ideal_zero pr_ideal.intro pr_ideal.not_1)

text โ€นremark 0.11โ€บ
lemma closed_subsets_R [simp]:
  shows "๐’ฑ R = {}"
  using ideal_implies_subset
  by (auto simp: closed_subsets_def pr_ideal_axioms_def pr_ideal_def)

lemma closed_subsets_zero [simp]:
  shows "๐’ฑ {๐Ÿฌ} = Spec"
  unfolding closed_subsets_def spectrum_def pr_ideal_def pr_ideal_axioms_def
  by (auto dest: ideal_zero)

lemma closed_subsets_ideal_aux:
  assumes ๐”ž: "ideal ๐”ž R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and ๐”Ÿ: "ideal ๐”Ÿ R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
      and prime: "pr_ideal R x (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and disj: "๐”ž โŠ† x โˆจ ๐”Ÿ โŠ† x"
  shows "ideal_gen_by_prod ๐”ž ๐”Ÿ โŠ† x"
  unfolding ideal_gen_by_prod_def additive.subgroup_generated_def
proof
  fix u
  assume u: "u โˆˆ additive.generate (R โˆฉ {a โ‹… b |a b. a โˆˆ ๐”ž โˆง b โˆˆ ๐”Ÿ})"
  have "๐”ž โŠ† R" "๐”Ÿ โŠ† R"
    using ๐”ž ๐”Ÿ ideal_implies_subset by auto
  show "u โˆˆ x" using u
  proof induction
    case unit
    then show ?case
      by (meson comm_ring.ideal_zero prime pr_ideal_def)
  next
    case (incl a)
    then have "a โˆˆ R"
      by blast
    with incl pr_ideal.axioms [OF prime] show ?case
      by clarsimp (metis โ€น๐”ž โŠ† Rโ€บ โ€น๐”Ÿ โŠ† Rโ€บ disj ideal.ideal subset_iff)
  next
    case (inv a)
    then have "a โˆˆ R"
      by blast
    with inv pr_ideal.axioms [OF prime] show ?case
      by clarsimp (metis โ€น๐”ž โŠ† Rโ€บ โ€น๐”Ÿ โŠ† Rโ€บ disj ideal.ideal ideal_inverse subset_iff)
  next
    case (mult a b)
    then show ?case
      by (meson prime comm_ring.ideal_add pr_ideal_def)
  qed
qed


text โ€นex. 0.13โ€บ
lemma closed_subsets_ideal_iff:
  assumes "ideal ๐”ž R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" and "ideal ๐”Ÿ R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  shows "๐’ฑ (ideal_gen_by_prod ๐”ž ๐”Ÿ) = (๐’ฑ ๐”ž) โˆช (๐’ฑ ๐”Ÿ)" (is "?lhs = ?rhs")
proof
  show "?lhs โŠ† ?rhs"
    unfolding closed_subsets_def
    by clarsimp (meson assms ideal_implies_subset ideal_mult_in_subgroup_generated in_mono pr_ideal.absorbent)
  show "?rhs โŠ† ?lhs"
    unfolding closed_subsets_def
    using closed_subsets_ideal_aux [OF assms] by auto
qed

abbreviation finsum:: "'b set โ‡’ ('b โ‡’ 'a) โ‡’ 'a"
  where "finsum I f โ‰ก additive.finprod I f"

lemma finsum_empty [simp]: "finsum {} f = ๐Ÿฌ"
  by (simp add: additive.finprod_def)

lemma finsum_insert:
  assumes "finite I" "i โˆ‰ I"
    and R: "f i โˆˆ R" "โ‹€j. j โˆˆ I โŸน f j โˆˆ R"
  shows "finsum (insert i I) f = f i + finsum I f"
  unfolding additive.finprod_def
proof (subst LCD.foldD_insert [where B = "insert i I"])
  show "LCD (insert i I) R ((+) โˆ˜ f)"
  proof
    show "((+) โˆ˜ f) x (((+) โˆ˜ f) y z) = ((+) โˆ˜ f) y (((+) โˆ˜ f) x z)"
      if "x โˆˆ insert i I" "y โˆˆ insert i I" "z โˆˆ R" for x y z
      using that additive.associative additive.commutative R by auto
    show "((+) โˆ˜ f) x y โˆˆ R"
      if "x โˆˆ insert i I" "y โˆˆ R" for x y
      using that R by force
  qed
qed (use assms in auto)

lemma finsum_singleton [simp]:
  assumes "f i โˆˆ R"
  shows "finsum {i} f = f i"
  by (metis additive.right_unit assms finite.emptyI finsum_empty finsum_insert insert_absorb insert_not_empty)


(* ex. 0.15 *)
lemma ex_15:
  fixes J :: "'b set" and ๐”ž :: "'b โ‡’ 'a set"
  assumes "J โ‰  {}" and J: "โ‹€j. jโˆˆJ โŸน ideal (๐”ž j) R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  shows "๐’ฑ ({x. โˆƒI f. x = finsum I f โˆง I โŠ† J โˆง finite I โˆง (โˆ€i. iโˆˆI โŸถ f i โˆˆ ๐”ž i)}) = (โ‹‚jโˆˆJ. ๐’ฑ (๐”ž j))"
  proof -
  have "y โˆˆ U"
    if j: "j โˆˆ J" "y โˆˆ ๐”ž j"
      and "pr_ideal R U (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
      and U: "{finsum I f |I f. I โŠ† J โˆง finite I โˆง (โˆ€i. i โˆˆ I โŸถ f i โˆˆ ๐”ž i)} โŠ† U"
    for U j y
  proof -
    have "y โˆˆ R"
      using J j ideal_implies_subset by blast
    then have y: "y = finsum {j} (ฮป_. y)"
      by simp
    then have "y โˆˆ {finsum I f |I f. I โŠ† J โˆง finite I โˆง (โˆ€i. i โˆˆ I โŸถ f i โˆˆ ๐”ž i)}"
      using that by blast
    then show ?thesis
      by (rule subsetD [OF U])
  qed
  moreover have PI: "pr_ideal R x (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" if "โˆ€jโˆˆJ. pr_ideal R x (+) (โ‹…) ๐Ÿฌ ๐Ÿญ โˆง ๐”ž j โŠ† x" for x
    using that assms(1) by fastforce
  moreover have "finsum I f โˆˆ U"
    if "finite I"
      and "โˆ€jโˆˆJ. pr_ideal R U (+) (โ‹…) ๐Ÿฌ ๐Ÿญ โˆง ๐”ž j โŠ† U"
      and "I โŠ† J" "โˆ€i. i โˆˆ I โŸถ f i โˆˆ ๐”ž i" for U I f
    using that
  proof (induction I rule: finite_induct)
    case empty
    then show ?case
      using PI assms ideal_zero by fastforce
  next
    case (insert i I)
    then have "finsum (insert i I) f = f i + finsum I f"
      by (metis assms(2) finsum_insert ideal_implies_subset insertCI subset_iff)
    also have "... โˆˆ U"
      using insert by (metis ideal_add insertCI pr_ideal.axioms(2) subset_eq)
    finally show ?case .
  qed
  ultimately show ?thesis
    by (auto simp: closed_subsets_def)
qed

(* ex 0.16 *)
definition is_zariski_open:: "'a set set โ‡’ bool" where
"is_zariski_open U โ‰ก generated_topology Spec {U. (โˆƒ๐”ž. ideal ๐”ž R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ โˆง U = Spec - ๐’ฑ ๐”ž)} U"

lemma is_zariski_open_empty [simp]: "is_zariski_open {}"
  using UNIV is_zariski_open_def generated_topology_is_topology topological_space.open_empty
  by simp

lemma is_zariski_open_Spec [simp]: "is_zariski_open Spec"
  by (simp add: UNIV is_zariski_open_def)

lemma is_zariski_open_Union [intro]:
  "(โ‹€x. x โˆˆ F โŸน is_zariski_open x) โŸน is_zariski_open (โ‹ƒ F)"
  by (simp add: UN is_zariski_open_def)

lemma is_zariski_open_Int [simp]:
  "โŸฆis_zariski_open U; is_zariski_open VโŸง โŸน is_zariski_open (U โˆฉ V)"
  using Int is_zariski_open_def by blast

lemma zariski_is_topological_space [iff]:
  shows "topological_space Spec is_zariski_open"
  unfolding is_zariski_open_def using generated_topology_is_topology
  by blast

lemma zariski_open_is_subset:
  assumes "is_zariski_open U"
  shows "U โŠ† Spec"
  using assms zariski_is_topological_space topological_space.open_imp_subset by auto

lemma cring0_is_zariski_open [simp]: "cring0.is_zariski_open = (ฮปU. U={})"
  using cring0.cring0_spectrum_eq cring0.is_zariski_open_empty cring0.zariski_open_is_subset by blast

subsection โ€นStandard Open Setsโ€บ

definition standard_open:: "'a โ‡’ 'a set set" ("๐’Ÿ'(_')")
  where "๐’Ÿ(x) โ‰ก (Spec โˆ– ๐’ฑ(โŸจxโŸฉ))"

lemma standard_open_is_zariski_open:
  assumes "x โˆˆ R"
  shows "is_zariski_open ๐’Ÿ(x)"
  unfolding is_zariski_open_def standard_open_def
  using assms gen_ideal_ideal generated_topology.simps by fastforce

lemma standard_open_is_subset:
  assumes "x โˆˆ R"
  shows "๐’Ÿ(x) โŠ† Spec"
  by (simp add: assms standard_open_is_zariski_open zariski_open_is_subset)

lemma belongs_standard_open_iff:
  assumes "x โˆˆ R" and "๐”ญ โˆˆ Spec"
  shows "x โˆ‰ ๐”ญ โŸท ๐”ญ โˆˆ ๐’Ÿ(x)"
  using assms
  apply (auto simp: standard_open_def closed_subsets_def spectrum_def gen_ideal_def subset_iff)
  apply (metis pr_ideal.absorbent)
  by (meson ideal.ideal(1) pr_ideal_def)

end (* comm_ring *)


subsection โ€นPresheaves of Ringsโ€บ

(* def 0.17 *)
locale presheaf_of_rings = Topological_Space.topological_space
  + fixes ๐”‰:: "'a set โ‡’ 'b set"
  and ฯ:: "'a set โ‡’ 'a set โ‡’ ('b โ‡’ 'b)" and b:: "'b"
  and add_str:: "'a set โ‡’ ('b โ‡’ 'b โ‡’ 'b)" ("+โ‡˜_โ‡™")
  and mult_str:: "'a set โ‡’ ('b โ‡’ 'b โ‡’ 'b)" ("โ‹…โ‡˜_โ‡™")
  and zero_str:: "'a set โ‡’ 'b" ("๐Ÿฌโ‡˜_โ‡™") and one_str:: "'a set โ‡’ 'b" ("๐Ÿญโ‡˜_โ‡™")
assumes is_ring_morphism:
  "โ‹€U V. is_open U โŸน is_open V โŸน V โŠ† U โŸน ring_homomorphism (ฯ U V)
                                                  (๐”‰ U) (+U) (โ‹…U) ๐ŸฌU ๐ŸญU
                                                  (๐”‰ V) (+V) (โ‹…V) ๐ŸฌV ๐ŸญV"
  and ring_of_empty: "๐”‰ {} = {b}"
  and identity_map [simp]: "โ‹€U. is_open U โŸน (โ‹€x. x โˆˆ ๐”‰ U โŸน ฯ U U x = x)"
  and assoc_comp:
  "โ‹€U V W. is_open U โŸน is_open V โŸน is_open W โŸน V โŠ† U โŸน W โŠ† V โŸน
(โ‹€x. x โˆˆ (๐”‰ U) โŸน ฯ U W x = (ฯ V W โˆ˜ ฯ U V) x)"
begin

lemma is_ring_from_is_homomorphism:
  shows "โ‹€U. is_open U โŸน ring (๐”‰ U) (+U) (โ‹…U) ๐ŸฌU ๐ŸญU"
  using is_ring_morphism ring_homomorphism.axioms(2) by fastforce

lemma is_map_from_is_homomorphism:
  assumes "is_open U" and "is_open V" and "V โŠ† U"
  shows "Set_Theory.map (ฯ U V) (๐”‰ U) (๐”‰ V)"
  using assms by (meson is_ring_morphism ring_homomorphism.axioms(1))

lemma eq_ฯ:
  assumes "is_open U" and "is_open V" and "is_open W" and "W โŠ† U โˆฉ V" and "s โˆˆ ๐”‰ U" and "t โˆˆ ๐”‰ V"
    and "ฯ U W s = ฯ V W t" and "is_open W'" and "W' โŠ† W"
  shows "ฯ U W' s = ฯ V W' t"
  by (metis Int_subset_iff assms assoc_comp comp_apply)

end (* presheaf_of_rings *)

locale morphism_presheaves_of_rings =
source: presheaf_of_rings X is_open ๐”‰ ฯ b add_str mult_str zero_str one_str
  + target: presheaf_of_rings X is_open ๐”‰' ฯ' b' add_str' mult_str' zero_str' one_str'
  for X and is_open
    and ๐”‰ and ฯ and b and add_str ("+โ‡˜_โ‡™") and mult_str ("โ‹…โ‡˜_โ‡™")
    and zero_str ("๐Ÿฌโ‡˜_โ‡™") and one_str ("๐Ÿญโ‡˜_โ‡™")
    and ๐”‰' and ฯ' and b' and add_str' ("+''โ‡˜_โ‡™") and mult_str' ("โ‹…''โ‡˜_โ‡™")
    and zero_str' ("๐Ÿฌ''โ‡˜_โ‡™") and one_str' ("๐Ÿญ''โ‡˜_โ‡™") +
  fixes fam_morphisms:: "'a set โ‡’ ('b โ‡’ 'c)"
  assumes is_ring_morphism: "โ‹€U. is_open U โŸน ring_homomorphism (fam_morphisms U)
                                                                (๐”‰ U) (+U) (โ‹…U) ๐ŸฌU ๐ŸญU
                                                                (๐”‰' U) (+'U) (โ‹…'U) ๐Ÿฌ'U ๐Ÿญ'U"
    and comm_diagrams: "โ‹€U V. is_open U โŸน is_open V โŸน V โŠ† U โŸน
               (โ‹€x. x โˆˆ ๐”‰ U โŸน (ฯ' U V โˆ˜ fam_morphisms U) x = (fam_morphisms V โˆ˜ ฯ U V) x)"
begin

lemma fam_morphisms_are_maps:
  assumes "is_open U"
  shows "Set_Theory.map (fam_morphisms U) (๐”‰ U) (๐”‰' U)"
  using assms is_ring_morphism by (simp add: ring_homomorphism_def)

end (* morphism_presheaves_of_rings *)

(* Identity presheaf *)
lemma (in presheaf_of_rings) id_is_mor_pr_rngs:
  shows "morphism_presheaves_of_rings S is_open ๐”‰ ฯ b add_str mult_str zero_str one_str ๐”‰ ฯ b add_str mult_str zero_str one_str (ฮปU. identity (๐”‰ U))"
proof (intro morphism_presheaves_of_rings.intro morphism_presheaves_of_rings_axioms.intro)
  show "โ‹€U. is_open U โŸน ring_homomorphism (identity (๐”‰ U))
                                            (๐”‰ U) (add_str U) (mult_str U) (zero_str U) (one_str U)
                                            (๐”‰ U) (add_str U) (mult_str U) (zero_str U) (one_str U)"
    by (metis identity_map is_map_from_is_homomorphism is_ring_morphism restrict_ext restrict_on_source subset_eq)
  show "โ‹€U V. โŸฆis_open U; is_open V; V โŠ† UโŸง
           โŸน (โ‹€x. x โˆˆ (๐”‰ U) โŸน (ฯ U V โˆ˜ identity (๐”‰ U)) x = (identity (๐”‰ V) โˆ˜ ฯ U V) x)"
    using map.map_closed by (metis comp_apply is_map_from_is_homomorphism restrict_apply')
qed (use presheaf_of_rings_axioms in auto)

lemma comp_ring_morphisms:
  assumes "ring_homomorphism ฮท A addA multA zeroA oneA B addB multB zeroB oneB"
and "ring_homomorphism ฮธ B addB multB zeroB oneB C addC multC zeroC oneC"
shows "ring_homomorphism (compose A ฮธ ฮท) A addA multA zeroA oneA C addC multC zeroC oneC"
  using comp_monoid_morphisms comp_group_morphisms assms
  by (metis monoid_homomorphism_def ring_homomorphism_def)

(* Composition of presheaves *)
 lemma comp_of_presheaves:
  assumes 1: "morphism_presheaves_of_rings X is_open ๐”‰ ฯ b add_str mult_str zero_str one_str ๐”‰' ฯ' b' add_str' mult_str' zero_str' one_str' ฯ†"
    and 2: "morphism_presheaves_of_rings X is_open ๐”‰' ฯ' b' add_str' mult_str' zero_str' one_str' ๐”‰'' ฯ'' b'' add_str'' mult_str'' zero_str'' one_str'' ฯ†'"
  shows "morphism_presheaves_of_rings X is_open ๐”‰ ฯ b add_str mult_str zero_str one_str ๐”‰'' ฯ'' b'' add_str'' mult_str'' zero_str'' one_str'' (ฮปU. (ฯ†' U โˆ˜ ฯ† U โ†“ ๐”‰ U))"
proof (intro morphism_presheaves_of_rings.intro morphism_presheaves_of_rings_axioms.intro)
  show "ring_homomorphism (ฯ†' U โˆ˜ ฯ† U โ†“ ๐”‰ U) (๐”‰ U) (add_str U) (mult_str U) (zero_str U) (one_str U) (๐”‰'' U) (add_str'' U) (mult_str'' U) (zero_str'' U) (one_str'' U)"
    if "is_open U"
    for U :: "'a set"
    using that
    by (metis assms comp_ring_morphisms morphism_presheaves_of_rings.is_ring_morphism)
next
  show "โ‹€x. x โˆˆ (๐”‰ U) โŸน (ฯ'' U V โˆ˜ (ฯ†' U โˆ˜ ฯ† U โ†“ ๐”‰ U)) x = (ฯ†' V โˆ˜ ฯ† V โ†“ ๐”‰ V โˆ˜ ฯ U V) x"
    if "is_open U" "is_open V" "V โŠ† U" for U V
    using that
    using morphism_presheaves_of_rings.comm_diagrams [OF 1]
    using morphism_presheaves_of_rings.comm_diagrams [OF 2]
    using presheaf_of_rings.is_map_from_is_homomorphism [OF morphism_presheaves_of_rings.axioms(1) [OF 1]]
    by (metis "1" comp_apply compose_eq map.map_closed morphism_presheaves_of_rings.fam_morphisms_are_maps)
qed (use assms in โ€นauto simp: morphism_presheaves_of_rings_defโ€บ)

locale iso_presheaves_of_rings = mor:morphism_presheaves_of_rings
+ assumes is_inv:
"โˆƒฯˆ. morphism_presheaves_of_rings X is_open ๐”‰' ฯ' b' add_str' mult_str' zero_str' one_str' ๐”‰ ฯ b add_str mult_str zero_str one_str ฯˆ
โˆง (โˆ€U. is_open U โŸถ (โˆ€x โˆˆ (๐”‰' U). (fam_morphisms U โˆ˜ ฯˆ U) x = x) โˆง (โˆ€x โˆˆ (๐”‰ U). (ฯˆ U โˆ˜ fam_morphisms U) x = x))"


subsection โ€นSheaves of Ringsโ€บ

(* def 0.19 *)
locale sheaf_of_rings = presheaf_of_rings +
  assumes locality: "โ‹€U I V s. open_cover_of_open_subset S is_open U I V โŸน (โ‹€i. iโˆˆI โŸน V i โŠ† U) โŸน
s โˆˆ ๐”‰ U โŸน (โ‹€i. iโˆˆI โŸน ฯ U (V i) s = ๐Ÿฌ(V i)) โŸน s = ๐ŸฌU"
and
glueing: "โ‹€U I V s. open_cover_of_open_subset S is_open U I V โŸน (โˆ€i. iโˆˆI โŸถ V i โŠ† U โˆง s i โˆˆ ๐”‰ (V i)) โŸน
(โ‹€i j. iโˆˆI โŸน jโˆˆI โŸน ฯ (V i) (V i โˆฉ V j) (s i) = ฯ (V j) (V i โˆฉ V j) (s j)) โŸน
(โˆƒt. t โˆˆ ๐”‰ U โˆง (โˆ€i. iโˆˆI โŸถ ฯ U (V i) t = s i))"

(* def. 0.20 *)
locale morphism_sheaves_of_rings = morphism_presheaves_of_rings

locale iso_sheaves_of_rings = iso_presheaves_of_rings

(* ex. 0.21 *)
locale ind_sheaf = sheaf_of_rings +
  fixes U:: "'a set"
  assumes is_open_subset: "is_open U"
begin

interpretation it: ind_topology S is_open U
  by (simp add: ind_topology.intro ind_topology_axioms.intro is_open_subset open_imp_subset topological_space_axioms)

definition ind_sheaf:: "'a set โ‡’ 'b set"
  where "ind_sheaf V โ‰ก ๐”‰ (U โˆฉ V)"

definition ind_ring_morphisms:: "'a set โ‡’ 'a set โ‡’ ('b โ‡’ 'b)"
  where "ind_ring_morphisms V W โ‰ก ฯ (U โˆฉ V) (U โˆฉ W)"

definition ind_add_str:: "'a set โ‡’ ('b โ‡’ 'b โ‡’ 'b)"
  where "ind_add_str V โ‰ก ฮปx y. +(U โˆฉ V) x y"

definition ind_mult_str:: "'a set โ‡’ ('b โ‡’ 'b โ‡’ 'b)"
  where "ind_mult_str V โ‰ก ฮปx y. โ‹…(U โˆฉ V) x y"

definition ind_zero_str:: "'a set โ‡’ 'b"
  where "ind_zero_str V โ‰ก ๐Ÿฌ(UโˆฉV)"

definition ind_one_str:: "'a set โ‡’ 'b"
  where "ind_one_str V โ‰ก ๐Ÿญ(UโˆฉV)"

lemma ind_is_open_imp_ring:
  "โ‹€U. it.ind_is_open U
   โŸน ring (ind_sheaf U) (ind_add_str U) (ind_mult_str U) (ind_zero_str U) (ind_one_str U)"
    using ind_add_str_def it.ind_is_open_def ind_mult_str_def ind_one_str_def ind_sheaf_def ind_zero_str_def is_open_subset is_ring_from_is_homomorphism it.is_subset open_inter by force

lemma ind_sheaf_is_presheaf:
  shows "presheaf_of_rings U (it.ind_is_open) ind_sheaf ind_ring_morphisms b
ind_add_str ind_mult_str ind_zero_str ind_one_str"
proof -
  have "topological_space U it.ind_is_open" by (simp add: it.ind_space_is_top_space)
  moreover have "ring_homomorphism (ind_ring_morphisms W V)
                     (ind_sheaf W) (ind_add_str W) (ind_mult_str W) (ind_zero_str W) (ind_one_str W)
                     (ind_sheaf V) (ind_add_str V) (ind_mult_str V) (ind_zero_str V) (ind_one_str V)"
    if "it.ind_is_open W" "it.ind_is_open V" "V โŠ† W" for W V
  proof (intro ring_homomorphism.intro ind_is_open_imp_ring)
    show "Set_Theory.map (ind_ring_morphisms W V) (ind_sheaf W) (ind_sheaf V)"
      by (metis that it.ind_is_open_def ind_ring_morphisms_def ind_sheaf_def inf.left_idem is_open_subset is_ring_morphism open_inter ring_homomorphism_def)
    from that
    obtain o: "is_open (U โˆฉ V)" "is_open (U โˆฉ W)" "U โˆฉ V โŠ† U โˆฉ W"
      by (metis (no_types) it.ind_is_open_def inf.absorb_iff2 is_open_subset open_inter)
    then show "group_homomorphism (ind_ring_morphisms W V) (ind_sheaf W) (ind_add_str W) (ind_zero_str W) (ind_sheaf V) (ind_add_str V) (ind_zero_str V)"
      by (metis ind_sheaf.ind_add_str_def ind_sheaf_axioms ind_ring_morphisms_def ind_sheaf_def ind_zero_str_def is_ring_morphism ring_homomorphism.axioms(4))
    show "monoid_homomorphism (ind_ring_morphisms W V) (ind_sheaf W) (ind_mult_str W) (ind_one_str W) (ind_sheaf V) (ind_mult_str V) (ind_one_str V)"
      using o by (metis ind_mult_str_def ind_one_str_def ind_ring_morphisms_def ind_sheaf_def is_ring_morphism ring_homomorphism_def)
  qed (use that in auto)
  moreover have "ind_sheaf {} = {b}"
    by (simp add: ring_of_empty ind_sheaf_def)
  moreover have "โ‹€U. it.ind_is_open U โŸน (โ‹€x. x โˆˆ (ind_sheaf U) โŸน ind_ring_morphisms U U x = x)"
    by (simp add: Int_absorb1 it.ind_is_open_def ind_ring_morphisms_def ind_sheaf_def it.is_open_from_ind_is_open is_open_subset)
  moreover have "โ‹€U V W. it.ind_is_open U โŸน it.ind_is_open V โŸน it.ind_is_open W โŸน V โŠ† U โŸน W โŠ† V
             โŸน (โ‹€x. x โˆˆ (ind_sheaf U) โŸน ind_ring_morphisms U W x = (ind_ring_morphisms V W โˆ˜ ind_ring_morphisms U V) x)"
    by (metis Int_absorb1 assoc_comp it.ind_is_open_def ind_ring_morphisms_def ind_sheaf_def it.is_open_from_ind_is_open is_open_subset)
  ultimately show ?thesis
    unfolding presheaf_of_rings_def presheaf_of_rings_axioms_def by blast
qed

lemma ind_sheaf_is_sheaf:
  shows "sheaf_of_rings U it.ind_is_open ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str"
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
  show "presheaf_of_rings U it.ind_is_open ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str"
    using ind_sheaf_is_presheaf by blast
next
  fix V I W s
  assume oc: "open_cover_of_open_subset U it.ind_is_open V I W"
    and WV: "โ‹€i. i โˆˆ I โŸน W i โŠ† V"
    and s: "s โˆˆ ind_sheaf V"
    and eq: "โ‹€i. i โˆˆ I โŸน ind_ring_morphisms V (W i) s = ind_zero_str (W i)"
  have "it.ind_is_open V"
    using oc open_cover_of_open_subset.is_open_subset by blast
  then have "s โˆˆ ๐”‰ V"
    by (metis ind_sheaf.ind_sheaf_def ind_sheaf_axioms it.ind_is_open_def inf.absorb2 s)
  then have "s = ๐ŸฌV"
    by (metis Int_absorb1 Int_subset_iff WV ind_sheaf.ind_zero_str_def ind_sheaf_axioms eq it.ind_is_open_def ind_ring_morphisms_def is_open_subset locality oc it.open_cover_from_ind_open_cover open_cover_of_open_subset.is_open_subset)
  then show "s = ind_zero_str V"
    by (metis Int_absorb1 it.ind_is_open_def ind_zero_str_def oc open_cover_of_open_subset.is_open_subset)
next
  fix V I W s
  assume oc: "open_cover_of_open_subset U it.ind_is_open V I W"
    and WV: "โˆ€i. i โˆˆ I โŸถ W i โŠ† V โˆง s i โˆˆ ind_sheaf (W i)"
    and eq: "โ‹€i j. โŸฆi โˆˆ I; j โˆˆ IโŸง โŸน ind_ring_morphisms (W i) (W i โˆฉ W j) (s i) = ind_ring_morphisms (W j) (W i โˆฉ W j) (s j)"
  have "is_open V"
    using it.is_open_from_ind_is_open is_open_subset oc open_cover_of_open_subset.is_open_subset by blast
  moreover have "open_cover_of_open_subset S is_open V I W"
    using it.open_cover_from_ind_open_cover oc ind_topology.intro ind_topology_axioms_def is_open_subset it.is_subset topological_space_axioms by blast
  moreover have "ฯ (W i) (W i โˆฉ W j) (s i) = ฯ (W j) (W i โˆฉ W j) (s j)"
    if "iโˆˆI" "jโˆˆI" for i j
  proof -
    have "U โˆฉ W i = W i" and "U โˆฉ W j = W j"
      by (metis Int_absorb1 WV it.ind_is_open_def oc open_cover_of_open_subset.is_open_subset
            subset_trans that)+
    then show ?thesis
      using eq[unfolded ind_ring_morphisms_def,OF that] by (metis inf_sup_aci(2))
  qed
  moreover have "โˆ€i. iโˆˆI โŸถ W i โŠ† V โˆง s i โˆˆ ๐”‰ (W i)"
    by (metis WV it.ind_is_open_def ind_sheaf_def inf.orderE inf_idem inf_aci(3) oc open_cover_of_open_subset.is_open_subset)
  ultimately
  obtain t where "t โˆˆ (๐”‰ V) โˆง (โˆ€i. iโˆˆI โŸถ ฯ V (W i) t = s i)"
    using glueing by blast
  then have "t โˆˆ ind_sheaf V"
    unfolding ind_sheaf_def using oc
    by (metis Int_absorb1 cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
  moreover have "โˆ€i. iโˆˆI โŸถ ind_ring_morphisms V (W i) t = s i"
    unfolding ind_ring_morphisms_def
    by (metis oc Int_absorb1 โ€นt โˆˆ ๐”‰ V โˆง (โˆ€i. i โˆˆ I โŸถ ฯ V (W i) t = s i)โ€บ cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
  ultimately show "โˆƒt. t โˆˆ (ind_sheaf V) โˆง (โˆ€i. iโˆˆI โŸถ ind_ring_morphisms V (W i) t = s i)" by blast
qed

end (* ind_sheaf *)

(* construction 0.22 *)
locale im_sheaf = sheaf_of_rings + continuous_map
begin

(* def 0.24 *)
definition im_sheaf:: "'c set => 'b set"
  where "im_sheaf V โ‰ก ๐”‰ (fยฏ S V)"

definition im_sheaf_morphisms:: "'c set โ‡’ 'c set โ‡’ ('b โ‡’ 'b)"
  where "im_sheaf_morphisms U V โ‰ก ฯ (fยฏ S U) (fยฏ S V)"

definition add_im_sheaf:: "'c set โ‡’ 'b โ‡’ 'b โ‡’ 'b"
  where "add_im_sheaf โ‰ก ฮปV x y. +(fยฏ S V) x y"

definition mult_im_sheaf:: "'c set โ‡’ 'b โ‡’ 'b โ‡’ 'b"
  where "mult_im_sheaf โ‰ก ฮปV x y. โ‹…(fยฏ S V) x y"

definition zero_im_sheaf:: "'c set โ‡’ 'b"
  where "zero_im_sheaf โ‰ก ฮปV. ๐Ÿฌ(fยฏ S V)"

definition one_im_sheaf:: "'c set โ‡’ 'b"
  where "one_im_sheaf โ‰ก ฮปV. ๐Ÿญ(fยฏ S V)"

lemma im_sheaf_is_presheaf:
  "presheaf_of_rings S' (is_open') im_sheaf im_sheaf_morphisms b
add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf"
proof (intro presheaf_of_rings.intro presheaf_of_rings_axioms.intro)
  show "topological_space S' is_open'"
    by (simp add: target.topological_space_axioms)
  show "โ‹€U V. โŸฆis_open' U; is_open' V; V โŠ† UโŸง
           โŸน ring_homomorphism (im_sheaf_morphisms U V)
(im_sheaf U) (add_im_sheaf U) (mult_im_sheaf U) (zero_im_sheaf U) (one_im_sheaf U)
(im_sheaf V) (add_im_sheaf V) (mult_im_sheaf V) (zero_im_sheaf V) (one_im_sheaf V)"
    unfolding add_im_sheaf_def mult_im_sheaf_def zero_im_sheaf_def one_im_sheaf_def
    by (metis Int_commute Int_mono im_sheaf_def im_sheaf_morphisms_def is_continuous is_ring_morphism subset_refl vimage_mono)
  show "im_sheaf {} = {b}" using im_sheaf_def ring_of_empty by simp
  show "โ‹€U. is_open' U โŸน (โ‹€x. x โˆˆ (im_sheaf U) โŸน im_sheaf_morphisms U U x = x)"
    using im_sheaf_morphisms_def by (simp add: im_sheaf_def is_continuous)
  show "โ‹€U V W.
       โŸฆis_open' U; is_open' V; is_open' W; V โŠ† U; W โŠ† VโŸง
       โŸน (โ‹€x. x โˆˆ (im_sheaf U) โŸน im_sheaf_morphisms U W x = (im_sheaf_morphisms V W โˆ˜ im_sheaf_morphisms U V) x)"
    by (metis Int_mono assoc_comp im_sheaf_def im_sheaf_morphisms_def ind_topology.is_subset is_continuous ind_topology_is_open_self vimage_mono)
qed

(* ex 0.23 *)
lemma im_sheaf_is_sheaf:
  shows "sheaf_of_rings S' (is_open') im_sheaf im_sheaf_morphisms b
add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf"
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
  show "presheaf_of_rings S' is_open' im_sheaf im_sheaf_morphisms b
add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf"
    using im_sheaf_is_presheaf by force
next
  fix U I V s
  assume oc: "open_cover_of_open_subset S' is_open' U I V"
    and VU: "โ‹€i. i โˆˆ I โŸน V i โŠ† U"
    and s: "s โˆˆ im_sheaf U"
    and eq0: "โ‹€i. i โˆˆ I โŸน im_sheaf_morphisms U (V i) s =zero_im_sheaf (V i)"
  have "open_cover_of_open_subset S is_open (fยฏ S U) I (ฮปi. fยฏ S (V i))"
    by (simp add: oc open_cover_of_open_subset_from_target_to_source)
  then show "s = zero_im_sheaf U" using zero_im_sheaf_def
    by (smt VU im_sheaf_def im_sheaf_morphisms_def eq0 inf.absorb_iff2 inf_le2 inf_sup_aci(1) inf_sup_aci(3) locality s vimage_Int)
next
  fix U I V s
  assume oc: "open_cover_of_open_subset S' is_open' U I V"
    and VU: "โˆ€i. i โˆˆ I โŸถ V i โŠ† U โˆง s i โˆˆ im_sheaf (V i)"
    and eq: "โ‹€i j. โŸฆi โˆˆ I; j โˆˆ IโŸง โŸน im_sheaf_morphisms (V i) (V i โˆฉ V j) (s i) = im_sheaf_morphisms (V j) (V i โˆฉ V j) (s j)"
  have "โˆƒt. t โˆˆ ๐”‰ (f  ยฏ S U) โˆง (โˆ€i. i โˆˆ I โŸถ ฯ (f  ยฏ S U) (f  ยฏ S (V i)) t = s i)"
  proof (rule glueing)
    show "open_cover_of_open_subset S is_open (f ยฏ S U) I (ฮปi. f ยฏ S (V i))"
      using oc open_cover_of_open_subset_from_target_to_source by presburger
    show "โˆ€i. i โˆˆ I โŸถ f ยฏ S (V i) โŠ† f ยฏ S U โˆง s i โˆˆ ๐”‰ (f ยฏ S (V i))"
      using VU im_sheaf_def by blast
    show "ฯ (f ยฏ S (V i)) (f ยฏ S (V i) โˆฉ f ยฏ S (V j)) (s i) = ฯ (f ยฏ S (V j)) (f ยฏ S (V i) โˆฉ f ยฏ S (V j)) (s j)"
      if "i โˆˆ I" "j โˆˆ I" for i j
      using im_sheaf_morphisms_def eq that
      by (smt Int_commute Int_left_commute inf.left_idem vimage_Int)
  qed
  then obtain t where "t โˆˆ ๐”‰ (fยฏ S U) โˆง (โˆ€i. iโˆˆI โŸถ ฯ (fยฏ S U) (fยฏ S (V i)) t = s i)" ..
  then show "โˆƒt. t โˆˆ im_sheaf U โˆง (โˆ€i. i โˆˆ I โŸถ im_sheaf_morphisms U (V i) t = s i)"
    using im_sheaf_def im_sheaf_morphisms_def by auto
qed

sublocale sheaf_of_rings S' is_open' im_sheaf im_sheaf_morphisms b
    add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
  using im_sheaf_is_sheaf .

end (* im_sheaf *)

lemma (in sheaf_of_rings) id_to_iso_of_sheaves:
  shows "iso_sheaves_of_rings S is_open ๐”‰ ฯ b add_str mult_str zero_str one_str
            (im_sheaf.im_sheaf S ๐”‰ (identity S))
            (im_sheaf.im_sheaf_morphisms S ฯ (identity S))
            b
            (ฮปV. +identity S ยฏ S V) (ฮปV. โ‹…identity S ยฏ S V) (ฮปV. ๐Ÿฌidentity S ยฏ S V) (ฮปV. ๐Ÿญidentity S ยฏ S V) (ฮปU. identity (๐”‰ U))"
    (is "iso_sheaves_of_rings S is_open ๐”‰ ฯ b _ _ _ _ _ _ b  ?add ?mult ?zero ?one ?F")
proof-
  have preq[simp]: "โ‹€V. V โŠ† S โŸน (identity S ยฏ S V) = V"
    by auto
  interpret id: im_sheaf S is_open ๐”‰ ฯ b add_str mult_str zero_str one_str S is_open "identity S"
    by intro_locales (auto simp add: Set_Theory.map_def continuous_map_axioms_def open_imp_subset)
  have 1[simp]: "โ‹€V. V โŠ† S โŸน im_sheaf.im_sheaf S ๐”‰ (identity S) V = ๐”‰ V"
    by (simp add: id.im_sheaf_def)
  have 2[simp]: "โ‹€U V. โŸฆU โŠ† S; V โŠ† SโŸง โŸน im_sheaf.im_sheaf_morphisms S ฯ (identity S) U V โ‰ก ฯ U V"
    using id.im_sheaf_morphisms_def by auto
  show ?thesis
  proof intro_locales
    have rh: "โ‹€U. is_open U โŸน
         ring_homomorphism (identity (๐”‰ U)) (๐”‰ U) +U โ‹…U ๐ŸฌU ๐ŸญU (๐”‰ U) +U โ‹…U ๐ŸฌU ๐ŸญU"
      using id_is_mor_pr_rngs morphism_presheaves_of_rings.is_ring_morphism by fastforce
    show "morphism_presheaves_of_rings_axioms is_open ๐”‰ ฯ add_str mult_str zero_str one_str
           id.im_sheaf id.im_sheaf_morphisms ?add ?mult ?zero ?one ?F"
      unfolding morphism_presheaves_of_rings_axioms_def
      by (auto simp: rh open_imp_subset intro: is_map_from_is_homomorphism map.map_closed)
    have ฯ: "โ‹€U V W x. โŸฆis_open U; is_open V; is_open W; V โŠ† U; W โŠ† V; x โˆˆ ๐”‰ UโŸง โŸน ฯ V W (ฯ U V x) = ฯ U W x"
      by (metis assoc_comp comp_def)
    show "presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one"
      by (auto simp: ฯ presheaf_of_rings_axioms_def is_ring_morphism open_imp_subset ring_of_empty)
    then have "presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one"
      by (metis id.im_sheaf_is_presheaf presheaf_of_rings_def)
    moreover
    have "morphism_presheaves_of_rings_axioms is_open
          id.im_sheaf id.im_sheaf_morphisms ?add ?mult ?zero ?one ๐”‰ ฯ add_str
          mult_str zero_str one_str (ฮปU. ฮปxโˆˆ๐”‰ U. x)"
      unfolding morphism_presheaves_of_rings_axioms_def
      by (auto simp: rh open_imp_subset intro: is_map_from_is_homomorphism map.map_closed)
    ultimately
    show "iso_presheaves_of_rings_axioms S is_open ๐”‰ ฯ b add_str mult_str zero_str one_str
            id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one ?F"
      by (auto simp: presheaf_of_rings_axioms iso_presheaves_of_rings_axioms_def morphism_presheaves_of_rings_def open_imp_subset)
  qed
qed


subsection โ€นQuotient Ringโ€บ

(*Probably for Group_Theory*)
context group begin

lemma cancel_imp_equal:
  "โŸฆ u โ‹… inverse v = ๐Ÿญ;  u โˆˆ G; v โˆˆ G โŸง โŸน u = v"
  by (metis invertible invertible_inverse_closed invertible_right_cancel invertible_right_inverse)

end

(*Probably for Ring_Theory*)
context ring begin

lemma inverse_distributive: "โŸฆ a โˆˆ R; b โˆˆ R; c โˆˆ R โŸง โŸน a โ‹… (b - c) = a โ‹… b - a โ‹… c"
    "โŸฆ a โˆˆ R; b โˆˆ R; c โˆˆ R โŸง โŸน (b - c) โ‹… a = b โ‹… a - c โ‹… a"
  using additive.invertible additive.invertible_inverse_closed distributive
        local.left_minus local.right_minus by presburger+

end

locale quotient_ring = comm:comm_ring R "(+)" "(โ‹…)" "๐Ÿฌ" "๐Ÿญ" + submonoid S R "(โ‹…)" "๐Ÿญ"
  for S and R and addition (infixl "+" 65) and multiplication (infixl "โ‹…" 70) and zero ("๐Ÿฌ") and
unit ("๐Ÿญ")
begin

lemmas comm_ring_simps =
  comm.multiplicative.associative
  comm.additive.associative
  comm.comm_mult
  comm.additive.commutative
  right_minus

definition rel:: "('a ร— 'a) โ‡’ ('a ร— 'a) โ‡’ bool" (infix "โˆผ" 80)
  where "x โˆผ y โ‰ก โˆƒs1. s1 โˆˆ S โˆง s1 โ‹… (snd y โ‹… fst x - snd x โ‹… fst y) = ๐Ÿฌ"

lemma rel_refl: "โ‹€x. x โˆˆ R ร— S โŸน x โˆผ x"
    by (auto simp: rel_def)

lemma rel_sym:
  assumes "x โˆผ y" "x โˆˆ R ร— S" "y โˆˆ R ร— S" shows "y โˆผ x"
proof -
  obtain rx sx ry sy s
    where ยง: "rx โˆˆ R" "sx โˆˆ S" "ry โˆˆ R" "s โˆˆ S" "sy โˆˆ S" "s โ‹… (sy โ‹… rx - sx โ‹… ry) = ๐Ÿฌ" "x = (rx,sx)" "y = (ry,sy)"
    using assms by (auto simp: rel_def)
  then have "s โ‹… (sx โ‹… ry - sy โ‹… rx) = ๐Ÿฌ"
    by (metis sub comm.additive.cancel_imp_equal comm.inverse_distributive(1) comm.multiplicative.composition_closed)
  with ยง show ?thesis
    by (auto simp: rel_def)
qed

lemma rel_trans:
  assumes "x โˆผ y" "y โˆผ z" "x โˆˆ R ร— S" "y โˆˆ R ร— S" "z โˆˆ R ร— S" shows "x โˆผ z"
  using assms
proof (clarsimp simp: rel_def)
  fix r s r2 s2 r1 s1 sx sy
  assume ยง: "r โˆˆ R" "s โˆˆ S" "r1 โˆˆ R" "s1 โˆˆ S" "sx โˆˆ S" "r2 โˆˆ R" "s2 โˆˆ S" "sy โˆˆ S"
    and sx0: "sx โ‹… (s1 โ‹… r2 - s2 โ‹… r1) = ๐Ÿฌ" and sy0: "sy โ‹… (s2 โ‹… r - s โ‹… r2) = ๐Ÿฌ"
  show "โˆƒu. u โˆˆ S โˆง u โ‹… (s1 โ‹… r - s โ‹… r1) = ๐Ÿฌ"
  proof (intro exI conjI)
    show "sx โ‹… sy โ‹… s1 โ‹… s2 โˆˆ S"
      using ยง by blast
    have sx: "sx โ‹… s1 โ‹… r2 = sx โ‹… s2 โ‹… r1" and sy: "sy โ‹… s2 โ‹… r = sy โ‹… s โ‹… r2"
      using sx0 sy0 ยง comm.additive.cancel_imp_equal comm.inverse_distributive(1)
        comm.multiplicative.associative comm.multiplicative.composition_closed sub
      by metis+
    then
    have "sx โ‹… sy โ‹… s1 โ‹… s2 โ‹… (s1 โ‹… r - s โ‹… r1) = sx โ‹… sy โ‹… s1 โ‹… s2 โ‹… s1 โ‹… r - sx โ‹… sy โ‹… s1 โ‹… s2 โ‹… s โ‹… r1"
      using "ยง" โ€นsx โ‹… sy โ‹… s1 โ‹… s2 โˆˆ Sโ€บ
        comm.inverse_distributive(1) comm.multiplicative.associative comm.multiplicative.composition_closed
        sub
      by presburger
    also have "... = sx โ‹… sy โ‹… s1 โ‹… s โ‹… s1 โ‹… r2 - sx โ‹… sy โ‹… s1 โ‹… s2 โ‹… s โ‹… r1"
      using ยง
      by (smt sy comm.comm_mult comm.multiplicative.associative comm.multiplicative.composition_closed sub)
    also have "... = sx โ‹… sy โ‹… s1 โ‹… s โ‹… s1 โ‹… r2 - sx โ‹… sy โ‹… s1 โ‹… s1 โ‹… s โ‹… r2"
      using ยง by (smt sx comm.comm_mult comm.multiplicative.associative
          comm.multiplicative.composition_closed sub)
    also have "... = ๐Ÿฌ"
      using ยง by (simp add: comm.ring_mult_ac)
    finally show "sx โ‹… sy โ‹… s1 โ‹… s2 โ‹… (s1 โ‹… r - s โ‹… r1) = ๐Ÿฌ" .
  qed
qed

interpretation rel: equivalence "R ร— S" "{(x,y) โˆˆ (Rร—S)ร—(Rร—S). x โˆผ y}"
  by (blast intro: equivalence.intro rel_refl rel_sym rel_trans)


notation equivalence.Partition (infixl "'/" 75)

definition frac:: "'a โ‡’ 'a โ‡’ ('a ร— 'a) set" (infixl "'/" 75)
  where "r / s โ‰ก rel.Class (r, s)"

lemma frac_Pow:"(r, s) โˆˆ R ร— S โŸน frac r s โˆˆ Pow (R ร— S) "
  using local.frac_def rel.Class_closed2 by auto

lemma frac_eqI:
  assumes "s1โˆˆS" and "(r, s) โˆˆ R ร— S" "(r', s') โˆˆ R ร— S"
     and eq:"s1 โ‹… s' โ‹… r = s1 โ‹… s โ‹… r'"
  shows "frac r s = frac r' s'"
  unfolding frac_def
proof (rule rel.Class_eq)
  have "s1 โ‹… (s' โ‹… r - s โ‹… r') = ๐Ÿฌ"
    using assms comm.inverse_distributive(1) comm.multiplicative.associative by auto
  with โ€นs1โˆˆSโ€บ have "(r, s) โˆผ (r', s')"
    unfolding rel_def by auto
  then show "((r, s), r', s') โˆˆ {(x, y). (x, y) โˆˆ (R ร— S) ร— R ร— S โˆง x โˆผ y}"
    using assms(2,3) by auto
qed

lemma frac_eq_Ex:
  assumes "(r, s) โˆˆ R ร— S" "(r', s') โˆˆ R ร— S" "frac r s = frac r' s'"
  obtains s1 where "s1โˆˆS" "s1 โ‹… (s' โ‹… r - s โ‹… r') = ๐Ÿฌ"
proof -
  have "(r, s) โˆผ (r', s')"
    using โ€นfrac r s = frac r' s'โ€บ rel.Class_equivalence[OF assms(1,2)]
    unfolding frac_def by auto
  then show ?thesis unfolding rel_def
    by (metis fst_conv snd_conv that)
qed

lemma frac_cancel:
  assumes "s1โˆˆS" and "(r, s) โˆˆ R ร— S"
  shows "frac (s1โ‹…r) (s1โ‹…s) = frac r s"
  apply (rule frac_eqI[of ๐Ÿญ])
  using assms comm_ring_simps by auto

lemma frac_eq_obtains:
  assumes "(r,s) โˆˆ R ร— S" and x_def:"x=(SOME x. xโˆˆ(frac r s))"
  obtains s1 where "s1โˆˆS" "s1 โ‹… s โ‹… fst x = s1 โ‹… snd x โ‹… r" and "x โˆˆ R ร— S"
proof -
  have "xโˆˆ(r/s)"
    unfolding x_def
    apply (rule someI[of _ "(r,s)"])
    using assms(1) local.frac_def by blast
  from rel.ClassD[OF this[unfolded frac_def] โ€น(r,s) โˆˆ R ร— Sโ€บ]
  have x_RS:"xโˆˆR ร— S" and "x โˆผ (r,s)" by auto
  from this(2) obtain s1 where "s1โˆˆS" and "s1 โ‹… (s โ‹… fst x - snd x โ‹… r) = ๐Ÿฌ"
    unfolding rel_def by auto
  then have x_eq:"s1 โ‹… s โ‹… fst x = s1 โ‹… snd x โ‹… r"
    using comm.distributive x_RS assms(1)
    by (smt comm.additive.group_axioms group.cancel_imp_equal comm.inverse_distributive(1)
        mem_Sigma_iff comm.multiplicative.associative comm.multiplicative.composition_closed prod.collapse sub)
  then show ?thesis using that x_RS โ€นs1โˆˆSโ€บ by auto
qed

definition valid_frac::"('a ร— 'a) set โ‡’ bool" where
  "valid_frac X โ‰ก โˆƒrโˆˆR. โˆƒsโˆˆS. r / s = X"

lemma frac_non_empty[simp]:"(a,b) โˆˆ R ร— S โŸน valid_frac (frac a b)"
  unfolding frac_def valid_frac_def by blast

definition add_rel_aux:: "'a โ‡’ 'a โ‡’ 'a โ‡’ 'a โ‡’ ('a ร— 'a) set"
  where "add_rel_aux r s r' s' โ‰ก (rโ‹…s' + r'โ‹…s) / (sโ‹…s')"

definition add_rel:: "('a ร— 'a) set โ‡’ ('a ร— 'a) set โ‡’ ('a ร— 'a) set"
  where "add_rel X Y โ‰ก
  let x = (SOME x. x โˆˆ X) in
  let y = (SOME y. y โˆˆ Y) in
  add_rel_aux (fst x) (snd x) (fst y) (snd y)"

lemma add_rel_frac:
  assumes "(r,s) โˆˆ R ร— S" "(r',s')โˆˆ R ร— S"
  shows "add_rel (r/s) (r'/s') = (rโ‹…s' + r'โ‹…s) / (sโ‹…s')"
proof -
  define x where "x=(SOME x. xโˆˆ(r/s))"
  define y where "y=(SOME y. yโˆˆ(r'/s'))"

  obtain s1 where [simp]:"s1 โˆˆ S" and x_eq:"s1 โ‹… s โ‹… fst x = s1 โ‹… snd x โ‹… r" and x_RS:"x โˆˆ R ร— S"
    using frac_eq_obtains[OF โ€น(r,s) โˆˆ R ร— Sโ€บ x_def] by auto
  obtain s2 where [simp]:"s2 โˆˆ S" and y_eq:"s2 โ‹… s' โ‹… fst y = s2 โ‹… snd y โ‹… r'" and y_RS:"y โˆˆ R ร— S"
    using frac_eq_obtains[OF โ€น(r',s') โˆˆ R ร— Sโ€บ y_def] by auto

  have "add_rel (r/s) (r'/s') = (fst x โ‹… snd y + fst y โ‹… snd x) / (snd x โ‹… snd y)"
    unfolding add_rel_def add_rel_aux_def x_def y_def Let_def by auto
  also have "... = (rโ‹…s' + r'โ‹…s) / (sโ‹…s')"
  proof (rule frac_eqI[of "s1 โ‹… s2"])
    have "snd y โ‹…  s' โ‹… s2 โ‹… (s1 โ‹…  s โ‹… fst x)  = snd y โ‹… s' โ‹… s2 โ‹… (s1 โ‹…  snd x โ‹…  r)"
      using x_eq by simp
    then have "s1 โ‹… s2 โ‹… s โ‹… s' โ‹… fst x โ‹… snd y =  s1 โ‹… s2 โ‹… snd x โ‹… snd y โ‹… r โ‹… s'"
      using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult by auto
    moreover have "snd x โ‹… s โ‹…s1 โ‹… (s2 โ‹… s' โ‹… fst y) = snd x โ‹… s โ‹…s1 โ‹… (s2 โ‹… snd y โ‹… r')"
      using y_eq by simp
    then have "s1 โ‹… s2 โ‹… s โ‹… s' โ‹… fst y โ‹… snd x = s1 โ‹… s2 โ‹… snd x โ‹… snd y โ‹… r' โ‹… s"
      using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult
      by auto
    ultimately show "s1 โ‹… s2 โ‹… (s โ‹… s') โ‹… (fst x โ‹… snd y + fst y โ‹… snd x)
        = s1 โ‹… s2 โ‹… (snd x โ‹… snd y) โ‹… (r โ‹… s' + r' โ‹… s)"
      using comm.multiplicative.associative assms x_RS y_RS comm.distributive
      by auto
    show "s1 โ‹… s2 โˆˆ S" "(fst x โ‹… snd y + fst y โ‹… snd x, snd x โ‹… snd y) โˆˆ R ร— S"
        "(r โ‹… s' + r' โ‹… s, s โ‹… s') โˆˆ R ร— S"
      using assms x_RS y_RS by auto
  qed
  finally show ?thesis by auto
qed

lemma valid_frac_add[intro,simp]:
  assumes "valid_frac X" "valid_frac Y"
  shows "valid_frac (add_rel X Y)"
proof -
  obtain r s r' s' where "rโˆˆR" "sโˆˆS" "r'โˆˆR" "s'โˆˆS"
      and *:"add_rel X Y = (rโ‹…s' + r'โ‹…s) / (sโ‹…s')"
  proof -
    define x where "x=(SOME x. xโˆˆX)"
    define y where "y=(SOME y. yโˆˆY)"
    have "xโˆˆX" "yโˆˆY"
      using assms unfolding x_def y_def valid_frac_def some_in_eq local.frac_def
      by blast+
    then obtain "x โˆˆ R ร— S" "y โˆˆ R ร— S"
      using assms
      by (simp add: valid_frac_def x_def y_def) (metis frac_eq_obtains mem_Sigma_iff)
    moreover have "add_rel X Y = (fst x โ‹… snd y + fst y โ‹… snd x) / (snd x โ‹… snd y)"
      unfolding add_rel_def add_rel_aux_def x_def y_def Let_def by auto
    ultimately show ?thesis using that by auto
  qed
  from this(1-4)
  have "(rโ‹…s' + r'โ‹…s,sโ‹…s') โˆˆ R ร— S"
    by auto
  with * show ?thesis by auto
qed

definition uminus_rel:: "('a ร— 'a) set โ‡’ ('a ร— 'a) set"
  where "uminus_rel X โ‰ก let x = (SOME x. x โˆˆ X) in (comm.additive.inverse (fst x) / snd x)"

lemma uminus_rel_frac:
  assumes "(r,s) โˆˆ R ร— S"
  shows "uminus_rel (r/s) = (comm.additive.inverse r) / s"
proof -
  define x where "x=(SOME x. xโˆˆ(r/s))"

  obtain s1 where [simp]:"s1 โˆˆ S" and x_eq:"s1 โ‹… s โ‹… fst x = s1 โ‹… snd x โ‹… r" and x_RS:"x โˆˆ R ร— S"
    using frac_eq_obtains[OF โ€น(r,s) โˆˆ R ร— Sโ€บ x_def] by auto

  have "uminus_rel (r/s)= (comm.additive.inverse (fst x)) / (snd x )"
    unfolding uminus_rel_def x_def Let_def by auto
  also have "... = (comm.additive.inverse r) / s"
    apply (rule frac_eqI[of s1])
    using x_RS assms x_eq by (auto simp add: comm.right_minus)
  finally show ?thesis .
qed

lemma valid_frac_uminus[intro,simp]:
  assumes "valid_frac X"
  shows "valid_frac (uminus_rel X)"
proof -
  obtain r s where "rโˆˆR" "sโˆˆS"
      and *:"uminus_rel X = (comm.additive.inverse r) / s"
  proof -
    define x where "x=(SOME x. xโˆˆX)"
    have "xโˆˆX"
      using assms unfolding x_def valid_frac_def some_in_eq local.frac_def
      by blast
    then have "xโˆˆ R ร— S"
      using assms valid_frac_def
      by (metis frac_eq_obtains mem_Sigma_iff x_def)
    moreover have "uminus_rel X = (comm.additive.inverse (fst x) ) / (snd x)"
      unfolding uminus_rel_def x_def Let_def by auto
    ultimately show ?thesis using that by auto
  qed
  from this(1-3)
  have "(comm.additive.inverse r,s) โˆˆ R ร— S" by auto
  with * show ?thesis by auto
qed

definition mult_rel_aux:: "'a โ‡’ 'a โ‡’ 'a โ‡’ 'a โ‡’ ('a ร— 'a) set"
  where "mult_rel_aux r s r' s' โ‰ก (rโ‹…r') / (sโ‹…s')"

definition mult_rel:: "('a ร— 'a) set โ‡’ ('a ร— 'a) set โ‡’ ('a ร— 'a) set"
  where "mult_rel X Y โ‰ก
  let x = (SOME x. x โˆˆ X) in
  let y = (SOME y. y โˆˆ Y) in
  mult_rel_aux (fst x) (snd x) (fst y) (snd y)"

lemma mult_rel_frac:
  assumes "(r,s) โˆˆ R ร— S" "(r',s')โˆˆ R ร— S"
  shows "mult_rel (r/s) (r'/s') = (rโ‹… r') / (sโ‹…s')"
proof -
   define x where "x=(SOME x. xโˆˆ(r/s))"
  define y where "y=(SOME y. yโˆˆ(r'/s'))"

  obtain s1 where [simp]:"s1 โˆˆ S" and x_eq:"s1 โ‹… s โ‹… fst x = s1 โ‹… snd x โ‹… r" and x_RS:"x โˆˆ R ร— S"
    using frac_eq_obtains[OF โ€น(r,s) โˆˆ R ร— Sโ€บ x_def] by auto
  obtain s2 where [simp]:"s2 โˆˆ S" and y_eq:"s2 โ‹… s' โ‹… fst y = s2 โ‹… snd y โ‹… r'" and y_RS:"y โˆˆ R ร— S"
    using frac_eq_obtains[OF โ€น(r',s') โˆˆ R ร— Sโ€บ y_def] by auto

  have "mult_rel (r/s) (r'/s') = (fst x โ‹… fst y ) / (snd x โ‹… snd y)"
    unfolding mult_rel_def mult_rel_aux_def x_def y_def Let_def by auto
  also have "... = (rโ‹… r') / (sโ‹…s')"
  proof (rule frac_eqI[of "s1 โ‹… s2"])
    have "(s1 โ‹… s โ‹… fst x) โ‹… (s2 โ‹… s' โ‹… fst y)  = (s1 โ‹… snd x โ‹… r) โ‹… (s2 โ‹… snd y โ‹… r')"
      using x_eq y_eq by auto
    then show "s1 โ‹… s2 โ‹… (s โ‹… s') โ‹… (fst x โ‹… fst y) = s1 โ‹… s2 โ‹… (snd x โ‹… snd y) โ‹… (r โ‹… r')"
      using comm.multiplicative.associative assms x_RS y_RS comm.distributive comm.comm_mult by auto
    show "s1 โ‹… s2 โˆˆ S" "(fst x โ‹… fst y, snd x โ‹… snd y) โˆˆ R ร— S"
        "(r โ‹… r', s โ‹… s') โˆˆ R ร— S"
      using assms x_RS y_RS by auto
  qed
  finally show ?thesis by auto
qed

lemma valid_frac_mult[intro,simp]:
  assumes "valid_frac X" "valid_frac Y"
  shows "valid_frac (mult_rel X Y)"
proof -
  obtain r s r' s' where "rโˆˆR" "sโˆˆS" "r'โˆˆR" "s'โˆˆS"
      and *:"mult_rel X Y = (rโ‹… r') / (sโ‹…s')"
  proof -
    define x where "x=(SOME x. xโˆˆX)"
    define y where "y=(SOME y. yโˆˆY)"
    have "xโˆˆX" "yโˆˆY"
      using assms unfolding x_def y_def valid_frac_def some_in_eq local.frac_def
      by blast+
    then obtain "x โˆˆ R ร— S" "y โˆˆ R ร— S"
      using assms
      by (simp add: valid_frac_def x_def y_def) (metis frac_eq_obtains mem_Sigma_iff)
    moreover have "mult_rel X Y = (fst x โ‹… fst y) / (snd x โ‹… snd y)"
      unfolding mult_rel_def mult_rel_aux_def x_def y_def Let_def by auto
    ultimately show ?thesis using that by auto
  qed
  from this(1-4)
  have "(rโ‹…r',sโ‹…s') โˆˆ R ร— S"
    by auto
  with * show ?thesis by auto
qed

definition zero_rel::"('a ร— 'a) set" where
  "zero_rel = frac ๐Ÿฌ ๐Ÿญ"

definition one_rel::"('a ร— 'a) set" where
  "one_rel = frac ๐Ÿญ ๐Ÿญ"

lemma valid_frac_zero[simp]:
  "valid_frac zero_rel"
  unfolding zero_rel_def valid_frac_def by blast

lemma valid_frac_one[simp]:
  "valid_frac one_rel"
  unfolding one_rel_def valid_frac_def by blast

definition carrier_quotient_ring:: "('a ร— 'a) set set"
  where "carrier_quotient_ring โ‰ก rel.Partition"

lemma carrier_quotient_ring_iff[iff]: "X โˆˆ carrier_quotient_ring โŸท valid_frac X "
  unfolding valid_frac_def carrier_quotient_ring_def
  using local.frac_def rel.natural.map_closed rel.representant_exists by fastforce

lemma frac_from_carrier:
  assumes "X โˆˆ carrier_quotient_ring"
  obtains r s where "r โˆˆ R" "s โˆˆ S" "X = rel.Class (r,s)"
  using assms carrier_quotient_ring_def
  by (metis (no_types, lifting) SigmaE rel.representant_exists)

lemma add_minus_zero_rel:
  assumes "valid_frac a"
  shows "add_rel a (uminus_rel a) = zero_rel"
proof -
  obtain a1 a2 where a_RS:"(a1, a2)โˆˆR ร— S" and a12:"a = a1 / a2 "
    using โ€นvalid_frac aโ€บ unfolding valid_frac_def by auto
  have "add_rel a (uminus_rel a) =  ๐Ÿฌ / (a2 โ‹… a2)"
    unfolding a12 using comm_ring_simps a_RS
    by (simp add:add_rel_frac uminus_rel_frac comm.right_minus)
  also have "... = ๐Ÿฌ / ๐Ÿญ"
    apply (rule frac_eqI[of ๐Ÿญ])
    using a_RS by auto
  also have "... = zero_rel" unfolding zero_rel_def ..
  finally show "add_rel a (uminus_rel a) = zero_rel" .
qed


(* ex. 0.26 *)
sublocale comm_ring carrier_quotient_ring add_rel mult_rel zero_rel one_rel
proof (unfold_locales; unfold carrier_quotient_ring_iff)
  show add_assoc:"add_rel (add_rel a b) c = add_rel a (add_rel b c)" and
       mult_assoc:"mult_rel (mult_rel a b) c = mult_rel a (mult_rel b c)" and
       distr:"mult_rel a (add_rel b c) = add_rel (mult_rel a b) (mult_rel a c)"
    if "valid_frac a" and "valid_frac b" and "valid_frac c" for a b c
  proof -
    obtain a1 a2 where a_RS:"(a1, a2)โˆˆR ร— S" and a12:"a = a1 / a2 "
      using โ€นvalid_frac aโ€บ unfolding valid_frac_def by auto
    obtain b1 b2 where b_RS:"(b1, b2)โˆˆR ร— S" and b12:"b = b1 / b2 "
      using โ€นvalid_frac bโ€บ unfolding valid_frac_def by auto
    obtain c1 c2 where c_RS:"(c1, c2)โˆˆR ร— S" and c12:"c = c1 / c2"
      using โ€นvalid_frac cโ€บ unfolding valid_frac_def by auto

    have "add_rel (add_rel a b) c = add_rel (add_rel (a1/a2) (b1/b2)) (c1/c2)"
      using a12 b12 c12 by auto
    also have "... = ((a1 โ‹… b2 + b1 โ‹… a2) โ‹… c2 + c1 โ‹… (a2 โ‹… b2)) / (a2 โ‹… b2 โ‹… c2)"
      using a_RS b_RS c_RS by (simp add:add_rel_frac)
    also have "... = add_rel (a1/a2) (add_rel (b1/b2) (c1/c2))"
      using a_RS b_RS c_RS comm.distributive comm_ring_simps
      by (auto simp add:add_rel_frac)
    also have "... = add_rel a (add_rel b c)"
      using a12 b12 c12 by auto
    finally show "add_rel (add_rel a b) c = add_rel a (add_rel b c)" .

    show "mult_rel (mult_rel a b) c = mult_rel a (mult_rel b c)"
      unfolding a12 b12 c12 using comm_ring_simps a_RS b_RS c_RS
      by (auto simp add:mult_rel_frac)

    have "mult_rel a (add_rel b c) = (a1 โ‹… (b1 โ‹… c2 + c1 โ‹… b2)) / (a2 โ‹… (b2 โ‹… c2))"
      unfolding a12 b12 c12 using a_RS b_RS c_RS
      by (simp add:mult_rel_frac add_rel_frac)
    also have "... = (a2 โ‹… (a1 โ‹… (b1 โ‹… c2 + c1 โ‹… b2))) / (a2 โ‹… (a2 โ‹… (b2 โ‹… c2)))"
      using a_RS b_RS c_RS by (simp add:frac_cancel)
    also have "... = add_rel (mult_rel a b) (mult_rel a c)"
      unfolding a12 b12 c12 using comm_ring_simps a_RS b_RS c_RS comm.distributive
      by (auto simp add:mult_rel_frac add_rel_frac)
    finally show "mult_rel a (add_rel b c) = add_rel (mult_rel a b) (mult_rel a c)"
      .
  qed
  show add_0:"add_rel zero_rel a = a"
      and mult_1:"mult_rel one_rel a = a"
     if "valid_frac a" for a
  proof -
    obtain a1 a2 where a_RS:"(a1, a2)โˆˆR ร— S" and a12:"a = a1 / a2 "
      using โ€นvalid_frac aโ€บ unfolding valid_frac_def by auto
    have "add_rel zero_rel a = add_rel zero_rel (a1/a2)"
      using a12 by simp
    also have "... = (a1/a2)"
      using a_RS comm_ring_simps comm.distributive zero_rel_def
      by (auto simp add:add_rel_frac)
    also have "... = a"
      using a12 by auto
    finally show "add_rel zero_rel a = a" .
    show "mult_rel one_rel a = a"
      unfolding a12 one_rel_def using a_RS by (auto simp add:mult_rel_frac)
  qed
  show add_commute:"add_rel a b = add_rel b a"
    and mult_commute:"mult_rel a b = mult_rel b a"
    if "valid_frac a" and "valid_frac b" for a b
  proof -
    obtain a1 a2 where a_RS:"(a1, a2)โˆˆR ร— S" and a12:"a = a1 / a2 "
      using โ€นvalid_frac aโ€บ unfolding valid_frac_def by auto
    obtain b1 b2 where b_RS:"(b1, b2)โˆˆR ร— S" and b12:"b = b1 / b2 "
      using โ€นvalid_frac bโ€บ unfolding valid_frac_def by auto

    show "add_rel a b = add_rel b a" "mult_rel a b = mult_rel b a"
      unfolding a12 b12  using comm_ring_simps a_RS b_RS
      by (auto simp add:mult_rel_frac add_rel_frac)
  qed
  show "add_rel a zero_rel = a" if "valid_frac a" for a
    using that add_0 add_commute by auto
  show "mult_rel a one_rel = a" if "valid_frac a" for a
    using that mult_commute mult_1 by auto
  show "monoid.invertible carrier_quotient_ring add_rel zero_rel a"
    if "valid_frac a" for a
  proof -
    have "Group_Theory.monoid carrier_quotient_ring add_rel zero_rel"
      apply (unfold_locales)
      using add_0 add_assoc add_commute by simp_all
    moreover have "add_rel a (uminus_rel a) = zero_rel" "add_rel (uminus_rel a) a = zero_rel"
      using add_minus_zero_rel add_commute that by auto
    ultimately show "monoid.invertible carrier_quotient_ring add_rel zero_rel a"
      unfolding monoid.invertible_def
      apply (rule monoid.invertibleI)
      using add_commute โ€นvalid_frac aโ€บ by auto
  qed
  show "mult_rel (add_rel b c) a = add_rel (mult_rel b a) (mult_rel c a)"
    if "valid_frac a" and "valid_frac b" and "valid_frac c" for a b c
    using that mult_commute add_commute distr by (simp add: valid_frac_add)
qed auto

end (* quotient_ring *)

notation quotient_ring.carrier_quotient_ring
           ("(_ ยฏ _/ โ‡˜(2_ _ _))โ‡™" [60,1000,1000,1000,1000]1000)


subsection โ€นLocal Rings at Prime Idealsโ€บ

context pr_ideal
begin

lemma submonoid_pr_ideal:
  shows "submonoid (R โˆ– I) R (โ‹…) ๐Ÿญ"
proof
  show "a โ‹… b โˆˆ Rโˆ–I" if "a โˆˆ Rโˆ–I" "b โˆˆ Rโˆ–I" for a b
    using that by (metis Diff_iff absorbent comm.multiplicative.composition_closed)
  show "๐Ÿญ โˆˆ Rโˆ–I"
    using ideal.ideal(2) ideal_axioms pr_ideal.carrier_neq pr_ideal_axioms by fastforce
qed auto

interpretation local:quotient_ring "(R โˆ– I)" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
  by intro_locales (meson submonoid_def submonoid_pr_ideal)

(* definition 0.28 *)
definition carrier_local_ring_at:: "('a ร— 'a) set set"
  where "carrier_local_ring_at โ‰ก (R โˆ– I)ยฏ R(+) (โ‹…) ๐Ÿฌ"

definition add_local_ring_at:: "('a ร— 'a) set โ‡’ ('a ร— 'a) set โ‡’ ('a ร— 'a) set"
  where "add_local_ring_at โ‰ก local.add_rel "

definition mult_local_ring_at:: "('a ร— 'a) set โ‡’ ('a ร— 'a) set โ‡’ ('a ร— 'a) set"
  where "mult_local_ring_at โ‰ก local.mult_rel "

definition uminus_local_ring_at:: "('a ร— 'a) set โ‡’ ('a ร— 'a) set"
  where "uminus_local_ring_at โ‰ก local.uminus_rel "

definition zero_local_ring_at:: "('a ร— 'a) set"
  where "zero_local_ring_at โ‰ก local.zero_rel"

definition one_local_ring_at:: "('a ร— 'a) set"
  where "one_local_ring_at โ‰ก local.one_rel"

sublocale comm_ring carrier_local_ring_at add_local_ring_at mult_local_ring_at
            zero_local_ring_at one_local_ring_at
  by (simp add: add_local_ring_at_def carrier_local_ring_at_def local.local.comm_ring_axioms
      mult_local_ring_at_def one_local_ring_at_def zero_local_ring_at_def)


lemma frac_from_carrier_local:
  assumes "X โˆˆ carrier_local_ring_at"
  obtains r s where "r โˆˆ R" "s โˆˆ R" "s โˆ‰ I" "X = local.frac r s"
proof-
  have "X โˆˆ (R โˆ– I)ยฏ R(+) (โ‹…) ๐Ÿฌ" using assms by (simp add: carrier_local_ring_at_def)
  then have "X โˆˆ quotient_ring.carrier_quotient_ring (R โˆ– I) R (+) (โ‹…) ๐Ÿฌ" by blast
  then obtain r s where "r โˆˆ R" "s โˆˆ (R โˆ– I)" "X = local.frac r s"
    using local.frac_from_carrier by (metis local.frac_def)
  thus thesis using that by blast
qed

lemma eq_from_eq_frac:
  assumes "local.frac r s = local.frac r' s'"
    and "s โˆˆ (R โˆ– I)" and "s' โˆˆ (R โˆ– I)" and "r โˆˆ R" "r' โˆˆ R"
  obtains h where "h โˆˆ (R โˆ– I)" "h โ‹… (s' โ‹… r - s โ‹… r') = ๐Ÿฌ"
    using local.frac_eq_Ex[of r s r' s'] assms by blast

end (* pr_ideal *)

abbreviation carrier_of_local_ring_at::
"'a set โ‡’ 'a set โ‡’ ('a โ‡’ 'a โ‡’ 'a) โ‡’ ('a โ‡’ 'a โ‡’ 'a) โ‡’ 'a โ‡’ ('a ร— 'a) set set" ("_ โ‡˜_ _ _ _โ‡™" [1000]1000)
where "R I add mult zero โ‰ก pr_ideal.carrier_local_ring_at R I add mult zero"


subsection โ€นSpectrum of a Ringโ€บ

(* construction 0.29 *)
context comm_ring
begin

interpretation zariski_top_space: topological_space Spec is_zariski_open
  unfolding is_zariski_open_def using generated_topology_is_topology
  by blast

lemma spectrum_imp_cxt_quotient_ring:
  "๐”ญ โˆˆ Spec โŸน quotient_ring (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  apply (intro_locales)
  using pr_ideal.submonoid_pr_ideal spectrum_def submonoid_def by fastforce

lemma spectrum_imp_pr:
  "๐”ญ โˆˆ Spec โŸน pr_ideal R ๐”ญ (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
  unfolding spectrum_def by auto

lemma frac_in_carrier_local:
  assumes "๐”ญ โˆˆ Spec" and "r โˆˆ R" and "s โˆˆ R" and "s โˆ‰ ๐”ญ"
  shows "(quotient_ring.frac (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ r s) โˆˆ R๐”ญ (+) (โ‹…) ๐Ÿฌ"
proof -
  interpret qr:quotient_ring "R โˆ– ๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
    using spectrum_imp_cxt_quotient_ring[OF โ€น๐”ญ โˆˆ Specโ€บ] .
  interpret pi:pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
    using spectrum_imp_pr[OF โ€น๐”ญ โˆˆ Specโ€บ] .
  show ?thesis unfolding pi.carrier_local_ring_at_def
    using assms(2-) by (auto intro:qr.frac_non_empty)
qed

definition is_locally_frac:: "('a set โ‡’ ('a ร— 'a) set) โ‡’ 'a set set โ‡’ bool"
  where "is_locally_frac s V โ‰ก (โˆƒr f. r โˆˆ R โˆง f โˆˆ R โˆง (โˆ€๐”ฎ โˆˆ V. f โˆ‰ ๐”ฎ โˆง
            s ๐”ฎ = quotient_ring.frac (R โˆ– ๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r f))"

lemma is_locally_frac_subset:
  assumes "is_locally_frac s U" "V โŠ† U"
  shows "is_locally_frac s V"
  using assms unfolding is_locally_frac_def
  by (meson subsetD)

lemma is_locally_frac_cong:
  assumes "โ‹€x. xโˆˆU โŸน f x=g x"
  shows "is_locally_frac f U = is_locally_frac g U"
  unfolding is_locally_frac_def using assms by simp

definition is_regular:: "('a set โ‡’ ('a ร— 'a) set) โ‡’ 'a set set โ‡’ bool"
  where "is_regular s U โ‰ก
โˆ€๐”ญ. ๐”ญ โˆˆ U โŸถ (โˆƒV. is_zariski_open V โˆง V โŠ† U โˆง ๐”ญ โˆˆ V โˆง (is_locally_frac s V))"

lemma map_on_empty_is_regular:
  fixes s:: "'a set โ‡’ ('a ร— 'a) set"
  shows "is_regular s {}"
  by (simp add: is_regular_def)

lemma cring0_is_regular [simp]: "cring0.is_regular x = (ฮปU. U={})"
  unfolding cring0.is_regular_def cring0_is_zariski_open
  by blast

definition sheaf_spec:: "'a set set โ‡’ ('a set โ‡’ ('a ร— 'a) set) set" ("๐’ช _" [90]90)
  where "๐’ช U โ‰ก {sโˆˆ(ฮ E ๐”ญโˆˆU. (R๐”ญ (+) (โ‹…) ๐Ÿฌ)). is_regular s U}"

lemma cring0_sheaf_spec_empty [simp]: "cring0.sheaf_spec {} = {ฮปx. undefined}"
  by (simp add: cring0.sheaf_spec_def)

lemma sec_has_right_codom:
  assumes "s โˆˆ ๐’ช U" and "๐”ญ โˆˆ U"
  shows "s ๐”ญ โˆˆ (R๐”ญ (+) (โ‹…) ๐Ÿฌ)"
using assms sheaf_spec_def by auto


lemma is_regular_has_right_codom:
  assumes "U โŠ† Spec" "๐”ญ โˆˆ U" "is_regular s U"
  shows "s ๐”ญ โˆˆ Rโˆ–๐”ญ ยฏ R(+) (โ‹…) ๐Ÿฌ"
proof -
  interpret qr:quotient_ring "(R โˆ– ๐”ญ)" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
    using spectrum_imp_cxt_quotient_ring assms by auto
  show ?thesis using assms
    by (smt frac_in_carrier_local is_locally_frac_def is_regular_def
          pr_ideal.carrier_local_ring_at_def spectrum_imp_pr subset_eq)
qed

lemma sec_is_extensional:
  assumes "s โˆˆ ๐’ช U"
  shows "s โˆˆ extensional U"
  using assms sheaf_spec_def by (simp add: PiE_iff)

definition ๐’ชb::"'a set โ‡’ ('a ร— 'a) set"
  where "๐’ชb = (ฮป๐”ญ. undefined)"

lemma ๐’ช_on_emptyset: "๐’ช {} = {๐’ชb}"
  unfolding sheaf_spec_def ๐’ชb_def
  by (auto simp:Set_Theory.map_def map_on_empty_is_regular)

lemma sheaf_spec_of_empty_is_singleton:
  fixes U:: "'a set set"
  assumes "U = {}" and "s โˆˆ extensional U" and "t โˆˆ extensional U"
  shows "s = t"
  using assms by (simp add: Set_Theory.map_def)

definition add_sheaf_spec:: "('a set) set โ‡’ ('a set โ‡’ ('a ร— 'a) set) โ‡’ ('a set โ‡’ ('a ร— 'a) set) โ‡’ ('a set โ‡’ ('a ร— 'a) set)"
  where "add_sheaf_spec U s s' โ‰ก ฮป๐”ญโˆˆU. quotient_ring.add_rel (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ (s ๐”ญ) (s' ๐”ญ)"

lemma is_regular_add_sheaf_spec:
  assumes "is_regular s U" and "is_regular s' U" and "U โŠ† Spec"
  shows "is_regular (add_sheaf_spec U s s') U"
proof -
  have "add_sheaf_spec U s s' ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ" if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret pi: pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      using โ€นU โŠ† Specโ€บ[unfolded spectrum_def] โ€น๐”ญ โˆˆ Uโ€บ by blast
    have "s ๐”ญ โˆˆ pi.carrier_local_ring_at"
      "s' ๐”ญ โˆˆ pi.carrier_local_ring_at"
      using โ€นis_regular s Uโ€บ โ€นis_regular s' Uโ€บ
      unfolding is_regular_def is_locally_frac_def using that
      using assms(3) frac_in_carrier_local by fastforce+
    then show ?thesis
      unfolding add_sheaf_spec_def using that
      by (simp flip:pi.add_local_ring_at_def)
  qed
  moreover have "(โˆƒVโŠ†U. is_zariski_open V โˆง ๐”ญ โˆˆ V โˆง is_locally_frac (add_sheaf_spec U s s') V)"
    if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    obtain V1 r1 f1 where "V1 โŠ†U" "is_zariski_open V1" "๐”ญ โˆˆ V1" "r1 โˆˆ R" "f1 โˆˆ R" and
        q_V1:"(โˆ€๐”ฎ. ๐”ฎ โˆˆ V1 โŸถ f1 โˆ‰ ๐”ฎ โˆง s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r1 f1)"
      using โ€นis_regular s Uโ€บ[unfolded is_regular_def] โ€น๐”ญ โˆˆ Uโ€บ
      unfolding is_locally_frac_def by auto
    obtain V2 r2 f2 where "V2 โŠ†U" "is_zariski_open V2" "๐”ญ โˆˆ V2" "r2 โˆˆ R" "f2 โˆˆ R" and
        q_V2:"(โˆ€๐”ฎ. ๐”ฎ โˆˆ V2 โŸถ f2 โˆ‰ ๐”ฎ โˆง s' ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r2 f2)"
      using โ€นis_regular s' Uโ€บ[unfolded is_regular_def]  โ€น๐”ญ โˆˆ Uโ€บ
      unfolding is_locally_frac_def by auto

    define V3 where "V3 = V1 โˆฉ V2"
    define r3 where "r3 = r1 โ‹… f2 + r2 โ‹… f1 "
    define f3 where "f3 = f1 โ‹… f2"
    have "V3 โŠ†U" "๐”ญ โˆˆ V3" "r3 โˆˆ R" "f3 โˆˆ R"
      unfolding V3_def r3_def f3_def
      using โ€นV1 โŠ† Uโ€บ โ€น๐”ญ โˆˆ V1โ€บ โ€นV2 โŠ† Uโ€บ โ€น๐”ญ โˆˆ V2โ€บ โ€นf1 โˆˆ Rโ€บ โ€นf2 โˆˆ Rโ€บ โ€นr1 โˆˆ Rโ€บ โ€นr2 โˆˆ Rโ€บ by blast+
    moreover have "is_zariski_open V3" using โ€นis_zariski_open V1โ€บ โ€นis_zariski_open V2โ€บ topological_space.open_inter by (simp add: V3_def)
    moreover have "f3 โˆ‰ ๐”ฎ"
        "add_sheaf_spec U s s' ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r3 f3"
        if "๐”ฎ โˆˆ V3" for ๐”ฎ
    proof -
      interpret q:quotient_ring "Rโˆ–๐”ฎ" R "(+)" "(โ‹…)" ๐Ÿฌ
        using โ€นU โŠ† Specโ€บ โ€นV3 โŠ† Uโ€บ โ€น๐”ฎ โˆˆ V3โ€บ quotient_ring_def local.comm_ring_axioms
          pr_ideal.submonoid_pr_ideal spectrum_def
        by fastforce
      have "f1 โˆ‰ ๐”ฎ" "s ๐”ฎ = q.frac r1 f1"
        using q_V1 โ€น๐”ฎ โˆˆ V3โ€บ  unfolding V3_def by auto
      have "f2 โˆ‰ ๐”ฎ" "s' ๐”ฎ = q.frac r2 f2"
        using q_V2 โ€น๐”ฎ โˆˆ V3โ€บ  unfolding V3_def by auto

      have "q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 โ‹… f2 + r2 โ‹… f1) (f1 โ‹… f2)"
        apply (rule q.add_rel_frac)
        subgoal by (simp add: โ€นf1 โˆˆ Rโ€บ โ€นf1 โˆ‰ ๐”ฎโ€บ โ€นr1 โˆˆ Rโ€บ โ€นr2 โˆˆ Rโ€บ)
        subgoal using โ€นf2 โˆˆ Rโ€บ โ€นf2 โˆ‰ ๐”ฎโ€บ โ€นr2 โˆˆ Rโ€บ by blast
        done
      then have "q.add_rel (s ๐”ฎ) (s' ๐”ฎ) = q.frac r3 f3"
        unfolding r3_def f3_def using โ€นs ๐”ฎ = q.frac r1 f1โ€บ โ€นs' ๐”ฎ = q.frac r2 f2โ€บ
        by auto
      then show "add_sheaf_spec U s s' ๐”ฎ = q.frac r3 f3"
        unfolding add_sheaf_spec_def using โ€นV3 โŠ† Uโ€บ โ€น๐”ฎ โˆˆ V3โ€บ by auto
      show "f3 โˆ‰ ๐”ฎ" using that unfolding V3_def f3_def
        using โ€นf1 โˆˆ Rโ€บ โ€นf1 โˆ‰ ๐”ฎโ€บ โ€นf2 โˆˆ Rโ€บ โ€นf2 โˆ‰ ๐”ฎโ€บ q.sub_composition_closed by auto
    qed
    ultimately show ?thesis using is_locally_frac_def by metis
  qed
  ultimately show ?thesis unfolding is_regular_def is_locally_frac_def by meson
qed

lemma add_sheaf_spec_in_sheaf_spec:
  assumes "s โˆˆ ๐’ช U" and "t โˆˆ ๐’ช U" and "U โŠ† Spec"
  shows "add_sheaf_spec U s t โˆˆ ๐’ช U"
proof -
  have "add_sheaf_spec U s t ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ"
      if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret qr:quotient_ring "(Rโˆ–๐”ญ)" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      apply (rule spectrum_imp_cxt_quotient_ring)
      using that โ€นU โŠ† Specโ€บ by auto
    interpret pi:pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      using that โ€นU โŠ† Specโ€บ by (auto intro:spectrum_imp_pr)
    have "qr.valid_frac (s ๐”ญ)" "qr.valid_frac (t ๐”ญ)"
      using sec_has_right_codom[OF _ that] โ€นs โˆˆ ๐’ช Uโ€บ โ€นt โˆˆ ๐’ช Uโ€บ
      by (auto simp:pi.carrier_local_ring_at_def)
    then show ?thesis
      using that unfolding add_sheaf_spec_def pi.carrier_local_ring_at_def
      by auto
  qed
  moreover have "is_regular (add_sheaf_spec U s t) U"
    using โ€นs โˆˆ ๐’ช Uโ€บ โ€นt โˆˆ ๐’ช Uโ€บ โ€นU โŠ† Specโ€บ is_regular_add_sheaf_spec
    unfolding sheaf_spec_def by auto
  moreover have "add_sheaf_spec U s t โˆˆ extensional U"
    unfolding add_sheaf_spec_def by auto
  ultimately show ?thesis
    unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition mult_sheaf_spec:: "('a set) set โ‡’ ('a set โ‡’ ('a ร— 'a) set) โ‡’ ('a set โ‡’ ('a ร— 'a) set) โ‡’ ('a set โ‡’ ('a ร— 'a) set)"
  where "mult_sheaf_spec U s s' โ‰ก ฮป๐”ญโˆˆU. quotient_ring.mult_rel (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ (s ๐”ญ) (s' ๐”ญ)"

lemma is_regular_mult_sheaf_spec:
  assumes "is_regular s U" and "is_regular s' U" and "U โŠ† Spec"
  shows "is_regular (mult_sheaf_spec U s s') U"
proof -
  have "mult_sheaf_spec U s s' ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ" if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret pi: pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      using โ€นU โŠ† Specโ€บ[unfolded spectrum_def] โ€น๐”ญ โˆˆ Uโ€บ by blast
    have "s ๐”ญ โˆˆ pi.carrier_local_ring_at"
      "s' ๐”ญ โˆˆ pi.carrier_local_ring_at"
      using โ€นis_regular s Uโ€บ โ€นis_regular s' Uโ€บ
      unfolding is_regular_def using that
      using assms(3) frac_in_carrier_local in_mono is_locally_frac_def by fastforce+
    then show ?thesis
      unfolding mult_sheaf_spec_def using that
      by (simp flip:pi.mult_local_ring_at_def)
  qed
  moreover have "(โˆƒVโŠ†U. is_zariski_open V โˆง ๐”ญ โˆˆ V โˆง is_locally_frac (mult_sheaf_spec U s s') V)"
    if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    obtain V1 r1 f1 where "V1 โŠ†U" "is_zariski_open V1" "๐”ญ โˆˆ V1" "r1 โˆˆ R" "f1 โˆˆ R" and
        q_V1:"(โˆ€๐”ฎ. ๐”ฎ โˆˆ V1 โŸถ f1 โˆ‰ ๐”ฎ โˆง s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r1 f1)"
      using โ€นis_regular s Uโ€บ[unfolded is_regular_def] โ€น๐”ญ โˆˆ Uโ€บ unfolding is_locally_frac_def
      by auto
    obtain V2 r2 f2 where "V2 โŠ†U" "is_zariski_open V2" "๐”ญ โˆˆ V2" "r2 โˆˆ R" "f2 โˆˆ R" and
        q_V2:"(โˆ€๐”ฎ. ๐”ฎ โˆˆ V2 โŸถ f2 โˆ‰ ๐”ฎ โˆง s' ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r2 f2)"
      using โ€นis_regular s' Uโ€บ[unfolded is_regular_def] โ€น๐”ญ โˆˆ Uโ€บ unfolding is_locally_frac_def
      by auto

    define V3 where "V3 = V1 โˆฉ V2"
    define r3 where "r3 = r1 โ‹… r2  "
    define f3 where "f3 = f1 โ‹… f2"
    have "V3 โŠ†U" "๐”ญ โˆˆ V3" "r3 โˆˆ R" "f3 โˆˆ R"
      unfolding V3_def r3_def f3_def
      using โ€นV1 โŠ† Uโ€บ โ€น๐”ญ โˆˆ V1โ€บ โ€น๐”ญ โˆˆ V2โ€บ โ€นf1 โˆˆ Rโ€บ โ€นf2 โˆˆ Rโ€บ โ€นr1 โˆˆ Rโ€บ โ€นr2 โˆˆ Rโ€บ by blast+
    moreover have "is_zariski_open V3"
      using topological_space.open_inter by (simp add: V3_def โ€นis_zariski_open V1โ€บ โ€นis_zariski_open V2โ€บ)
    moreover have "f3 โˆ‰ ๐”ฎ"
        "mult_sheaf_spec U s s' ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r3 f3"
        if "๐”ฎ โˆˆ V3" for ๐”ฎ
    proof -
      interpret q:quotient_ring "Rโˆ–๐”ฎ" R "(+)" "(โ‹…)" ๐Ÿฌ
        using โ€นU โŠ† Specโ€บ โ€นV3 โŠ† Uโ€บ โ€น๐”ฎ โˆˆ V3โ€บ quotient_ring_def local.comm_ring_axioms
          pr_ideal.submonoid_pr_ideal spectrum_def
        by fastforce
      have "f1 โˆ‰ ๐”ฎ" "s ๐”ฎ = q.frac r1 f1"
        using q_V1 โ€น๐”ฎ โˆˆ V3โ€บ  unfolding V3_def by auto
      have "f2 โˆ‰ ๐”ฎ" "s' ๐”ฎ = q.frac r2 f2"
        using q_V2 โ€น๐”ฎ โˆˆ V3โ€บ  unfolding V3_def by auto

      have "q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 โ‹… r2 ) (f1 โ‹… f2)"
        apply (rule q.mult_rel_frac)
        subgoal by (simp add: โ€นf1 โˆˆ Rโ€บ โ€นf1 โˆ‰ ๐”ฎโ€บ โ€นr1 โˆˆ Rโ€บ โ€นr2 โˆˆ Rโ€บ)
        subgoal using โ€นf2 โˆˆ Rโ€บ โ€นf2 โˆ‰ ๐”ฎโ€บ โ€นr2 โˆˆ Rโ€บ by blast
        done
      then have "q.mult_rel (s ๐”ฎ) (s' ๐”ฎ) = q.frac r3 f3"
        unfolding r3_def f3_def using โ€นs ๐”ฎ = q.frac r1 f1โ€บ โ€นs' ๐”ฎ = q.frac r2 f2โ€บ
        by auto
      then show "mult_sheaf_spec U s s' ๐”ฎ = q.frac r3 f3"
        unfolding mult_sheaf_spec_def using โ€นV3 โŠ† Uโ€บ โ€น๐”ฎ โˆˆ V3โ€บ by auto
      show "f3 โˆ‰ ๐”ฎ" using that unfolding V3_def f3_def
        using โ€นf1 โˆˆ Rโ€บ โ€นf1 โˆ‰ ๐”ฎโ€บ โ€นf2 โˆˆ Rโ€บ โ€นf2 โˆ‰ ๐”ฎโ€บ q.sub_composition_closed by auto
    qed
    ultimately show ?thesis using is_locally_frac_def by metis
  qed
  ultimately show ?thesis unfolding is_regular_def is_locally_frac_def by meson
qed

lemma mult_sheaf_spec_in_sheaf_spec:
  assumes "s โˆˆ ๐’ช U" and "t โˆˆ ๐’ช U" and "U โŠ† Spec"
  shows "mult_sheaf_spec U s t โˆˆ ๐’ช U"
proof -
  have "mult_sheaf_spec U s t ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ"
      if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret qr:quotient_ring "(Rโˆ–๐”ญ)" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      apply (rule spectrum_imp_cxt_quotient_ring)
      using that โ€นU โŠ† Specโ€บ by auto
    interpret pi:pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      using that โ€นU โŠ† Specโ€บ by (auto intro:spectrum_imp_pr)
    have "qr.valid_frac (s ๐”ญ)" "qr.valid_frac (t ๐”ญ)"
      using sec_has_right_codom[OF _ that] โ€นs โˆˆ ๐’ช Uโ€บ โ€นt โˆˆ ๐’ช Uโ€บ
      by (auto simp:pi.carrier_local_ring_at_def)
    then show ?thesis
      using that unfolding mult_sheaf_spec_def pi.carrier_local_ring_at_def
      by auto
  qed
  moreover have "is_regular (mult_sheaf_spec U s t) U"
    using โ€นs โˆˆ ๐’ช Uโ€บ โ€นt โˆˆ ๐’ช Uโ€บ โ€นU โŠ† Specโ€บ is_regular_mult_sheaf_spec
    unfolding sheaf_spec_def by auto
  moreover have "mult_sheaf_spec U s t โˆˆ extensional U"
    unfolding mult_sheaf_spec_def by auto
  ultimately show ?thesis
    unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition uminus_sheaf_spec::"('a set) set โ‡’ ('a set โ‡’ ('a ร— 'a) set) โ‡’ ('a set โ‡’ ('a ร— 'a) set)"
  where "uminus_sheaf_spec U s โ‰ก ฮป๐”ญโˆˆU. quotient_ring.uminus_rel (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ (s ๐”ญ) "

lemma is_regular_uminus_sheaf_spec:
  assumes "is_regular s U" and "U โŠ† Spec"
  shows "is_regular (uminus_sheaf_spec U s) U"
proof -
  have "uminus_sheaf_spec U s ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ" if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret pi: pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      using โ€นU โŠ† Specโ€บ[unfolded spectrum_def] โ€น๐”ญ โˆˆ Uโ€บ by blast
    interpret qr:quotient_ring "(Rโˆ–๐”ญ)"
      by (simp add: quotient_ring_def local.comm_ring_axioms pi.submonoid_pr_ideal)

    have "s ๐”ญ โˆˆ pi.carrier_local_ring_at"
      using โ€นis_regular s Uโ€บ
      unfolding is_regular_def using that
      using assms(2) frac_in_carrier_local in_mono is_locally_frac_def by fastforce
    then show ?thesis
      unfolding uminus_sheaf_spec_def pi.carrier_local_ring_at_def using that
      by simp
  qed
  moreover have "(โˆƒVโŠ†U. is_zariski_open V โˆง ๐”ญ โˆˆ V โˆง is_locally_frac (uminus_sheaf_spec U s) V)"
    if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    obtain V1 r1 f1 where "V1 โŠ†U" "is_zariski_open V1" "๐”ญ โˆˆ V1" "r1 โˆˆ R" "f1 โˆˆ R" and
        q_V1:"(โˆ€๐”ฎ. ๐”ฎ โˆˆ V1 โŸถ f1 โˆ‰ ๐”ฎ โˆง s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r1 f1)"
      using โ€นis_regular s Uโ€บ[unfolded is_regular_def] โ€น๐”ญ โˆˆ Uโ€บ unfolding is_locally_frac_def
      by auto

    define V3 where "V3 = V1 "
    define r3 where "r3 = additive.inverse r1"
    define f3 where "f3 = f1"
    have "V3 โŠ†U" "๐”ญ โˆˆ V3" "r3 โˆˆ R" "f3 โˆˆ R"
      unfolding V3_def r3_def f3_def
      using โ€นV1 โŠ† Uโ€บ โ€น๐”ญ โˆˆ V1โ€บ โ€นf1 โˆˆ Rโ€บ  โ€นr1 โˆˆ Rโ€บ by blast+
    moreover have "is_zariski_open V3"
      using topological_space.open_inter by (simp add: V3_def โ€นis_zariski_open V1โ€บ)
    moreover have "f3 โˆ‰ ๐”ฎ"
        "uminus_sheaf_spec U s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r3 f3"
        if "๐”ฎ โˆˆ V3" for ๐”ฎ
    proof -
      interpret q:quotient_ring "Rโˆ–๐”ฎ" R "(+)" "(โ‹…)" ๐Ÿฌ
        using โ€นU โŠ† Specโ€บ โ€นV3 โŠ† Uโ€บ โ€น๐”ฎ โˆˆ V3โ€บ quotient_ring_def local.comm_ring_axioms
          pr_ideal.submonoid_pr_ideal spectrum_def
        by fastforce
      have "f1 โˆ‰ ๐”ฎ" "s ๐”ฎ = q.frac r1 f1"
        using q_V1 โ€น๐”ฎ โˆˆ V3โ€บ  unfolding V3_def by auto

      have "q.uminus_rel (q.frac r1 f1) = q.frac (additive.inverse r1) f1"
        apply (rule q.uminus_rel_frac)
        by (simp add: โ€นf1 โˆˆ Rโ€บ โ€นf1 โˆ‰ ๐”ฎโ€บ โ€นr1 โˆˆ Rโ€บ)
      then have "q.uminus_rel (s ๐”ฎ) = q.frac r3 f3"
        unfolding r3_def f3_def using โ€นs ๐”ฎ = q.frac r1 f1โ€บ by auto
      then show "uminus_sheaf_spec U s ๐”ฎ = q.frac r3 f3"
        unfolding uminus_sheaf_spec_def using โ€นV3 โŠ† Uโ€บ โ€น๐”ฎ โˆˆ V3โ€บ by auto
      show "f3 โˆ‰ ๐”ฎ" using that unfolding V3_def f3_def
        using โ€นf1 โˆˆ Rโ€บ โ€นf1 โˆ‰ ๐”ฎโ€บ q.sub_composition_closed by auto
    qed
    ultimately show ?thesis using is_locally_frac_def by metis
  qed
  ultimately show ?thesis unfolding is_regular_def is_locally_frac_def by meson
qed

lemma uminus_sheaf_spec_in_sheaf_spec:
  assumes "s โˆˆ ๐’ช U" and "U โŠ† Spec"
  shows "uminus_sheaf_spec U s โˆˆ ๐’ช U"
proof -
  have "uminus_sheaf_spec U s ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ"
      if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret qr:quotient_ring "(Rโˆ–๐”ญ)" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      apply (rule spectrum_imp_cxt_quotient_ring)
      using that โ€นU โŠ† Specโ€บ by auto
    interpret pi:pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      using that โ€นU โŠ† Specโ€บ by (auto intro:spectrum_imp_pr)
    have "qr.valid_frac (s ๐”ญ)"
      using sec_has_right_codom[OF _ that] โ€นs โˆˆ ๐’ช Uโ€บ
      by (auto simp:pi.carrier_local_ring_at_def)
    then show ?thesis
      using that unfolding uminus_sheaf_spec_def pi.carrier_local_ring_at_def
      by auto
  qed
  moreover have "is_regular (uminus_sheaf_spec U s) U"
    using โ€นs โˆˆ ๐’ช Uโ€บ  โ€นU โŠ† Specโ€บ is_regular_uminus_sheaf_spec
    unfolding sheaf_spec_def by auto
  moreover have "uminus_sheaf_spec U s โˆˆ extensional U"
    unfolding uminus_sheaf_spec_def by auto
  ultimately show ?thesis
    unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition zero_sheaf_spec:: "'a set set โ‡’ ('a set โ‡’ ('a ร— 'a) set)"
  where "zero_sheaf_spec U โ‰ก ฮป๐”ญโˆˆU. quotient_ring.zero_rel (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"

lemma is_regular_zero_sheaf_spec:
  assumes "is_zariski_open U"
  shows "is_regular (zero_sheaf_spec U) U"
proof -
  have "zero_sheaf_spec U ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ" if "๐”ญ โˆˆ U" for ๐”ญ
    unfolding zero_sheaf_spec_def
    using assms comm_ring.frac_in_carrier_local local.comm_ring_axioms pr_ideal.not_1 
          quotient_ring.zero_rel_def spectrum_imp_cxt_quotient_ring spectrum_imp_pr subsetD that 
          zariski_top_space.open_imp_subset by fastforce
  moreover have "(โˆƒVโŠ†U. is_zariski_open V โˆง ๐”ญ โˆˆ V โˆง is_locally_frac (zero_sheaf_spec U) V)"
    if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    define V3 where "V3 = U"
    define r3 where "r3 = ๐Ÿฌ "
    define f3 where "f3 = ๐Ÿญ"
    have "V3 โŠ†U" "๐”ญ โˆˆ V3" "r3 โˆˆ R" "f3 โˆˆ R"
      unfolding V3_def r3_def f3_def using that by auto
    moreover have "is_zariski_open V3" using assms by (simp add: V3_def)
    moreover have "f3 โˆ‰ ๐”ฎ"
        "zero_sheaf_spec U ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r3 f3"
        if "๐”ฎ โˆˆ V3" for ๐”ฎ
      subgoal using V3_def assms f3_def pr_ideal.submonoid_pr_ideal spectrum_def
          submonoid.sub_unit_closed that zariski_open_is_subset by fastforce
      subgoal
      proof -
        interpret q:quotient_ring "Rโˆ–๐”ฎ" R
          using V3_def assms quotient_ring_def local.comm_ring_axioms
            pr_ideal.submonoid_pr_ideal spectrum_def that zariski_open_is_subset by fastforce
        show ?thesis unfolding zero_sheaf_spec_def
          using V3_def f3_def q.zero_rel_def r3_def that by auto
      qed
      done
    ultimately show ?thesis using is_locally_frac_def  by metis
  qed
  ultimately show ?thesis unfolding is_regular_def is_locally_frac_def  by meson
qed

lemma zero_sheaf_spec_in_sheaf_spec:
  assumes "is_zariski_open U"
  shows "zero_sheaf_spec U โˆˆ ๐’ช U"
proof -
  have "zero_sheaf_spec U ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ"if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret qr:quotient_ring "(Rโˆ–๐”ญ)" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      by (meson assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
          spectrum_imp_cxt_quotient_ring subsetD that)
    interpret pi:pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      by (meson assms spectrum_imp_pr subsetD that zariski_open_is_subset)
    show ?thesis unfolding zero_sheaf_spec_def pi.carrier_local_ring_at_def
      using that by auto
  qed
  moreover have "is_regular (zero_sheaf_spec U) U"
    using is_regular_zero_sheaf_spec assms by auto
  moreover have "zero_sheaf_spec U โˆˆ extensional U"
    by (simp add: zero_sheaf_spec_def)
  ultimately show ?thesis unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition one_sheaf_spec:: "'a set set โ‡’ ('a set โ‡’ ('a ร— 'a) set)"
  where "one_sheaf_spec U โ‰ก ฮป๐”ญโˆˆU. quotient_ring.one_rel (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"

lemma is_regular_one_sheaf_spec:
  assumes "is_zariski_open U"
  shows "is_regular (one_sheaf_spec U) U"
proof -
  have "one_sheaf_spec U ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ" if "๐”ญ โˆˆ U" for ๐”ญ
    unfolding one_sheaf_spec_def
    by (smt assms closed_subsets_zero comm_ring.closed_subsets_def
        quotient_ring.carrier_quotient_ring_iff quotient_ring.valid_frac_one
        quotient_ring_def local.comm_ring_axioms mem_Collect_eq
        pr_ideal.carrier_local_ring_at_def pr_ideal.submonoid_pr_ideal
        restrict_apply subsetD that zariski_open_is_subset)
  moreover have "(โˆƒVโŠ†U. is_zariski_open V โˆง ๐”ญ โˆˆ V โˆง is_locally_frac (one_sheaf_spec U) V)"
    if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    define V3 where "V3 = U"
    define r3 where "r3 = ๐Ÿญ"
    define f3 where "f3 = ๐Ÿญ"
    have "V3 โŠ†U" "๐”ญ โˆˆ V3" "r3 โˆˆ R" "f3 โˆˆ R"
      unfolding V3_def r3_def f3_def using that by auto
    moreover have "is_zariski_open V3" using assms by (simp add: V3_def)
    moreover have "f3 โˆ‰ ๐”ฎ"
        "one_sheaf_spec U ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ r3 f3"
        if "๐”ฎ โˆˆ V3" for ๐”ฎ
      subgoal using V3_def assms f3_def pr_ideal.submonoid_pr_ideal spectrum_def
          submonoid.sub_unit_closed that zariski_open_is_subset by fastforce
      subgoal
      proof -
        interpret q:quotient_ring "Rโˆ–๐”ฎ" R
          using V3_def assms quotient_ring_def local.comm_ring_axioms
            pr_ideal.submonoid_pr_ideal spectrum_def that zariski_open_is_subset by fastforce
        show ?thesis unfolding one_sheaf_spec_def
          using V3_def f3_def q.one_rel_def r3_def that by auto
      qed
      done
    ultimately show ?thesis using is_locally_frac_def by metis
  qed
  ultimately show ?thesis unfolding is_regular_def is_locally_frac_def by meson
qed

lemma one_sheaf_spec_in_sheaf_spec:
  assumes "is_zariski_open U"
  shows "one_sheaf_spec U โˆˆ ๐’ช U"
proof -
  have "one_sheaf_spec U ๐”ญ โˆˆ R ๐”ญ (+) (โ‹…) ๐Ÿฌ"if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    interpret qr:quotient_ring "(Rโˆ–๐”ญ)" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      by (meson assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
          spectrum_imp_cxt_quotient_ring subsetD that)
    interpret pi:pr_ideal R ๐”ญ "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
      by (meson assms spectrum_imp_pr subsetD that zariski_open_is_subset)
    show ?thesis unfolding one_sheaf_spec_def pi.carrier_local_ring_at_def
      using that by auto
  qed
  moreover have "is_regular (one_sheaf_spec U) U"
    using is_regular_one_sheaf_spec assms by auto
  moreover have "one_sheaf_spec U โˆˆ extensional U"
    by (simp add: one_sheaf_spec_def)
  ultimately show ?thesis unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

lemma zero_sheaf_spec_extensional[simp]:
  "zero_sheaf_spec U โˆˆ extensional U"
  unfolding zero_sheaf_spec_def by simp

lemma one_sheaf_spec_extensional[simp]:
  "one_sheaf_spec U โˆˆ extensional U"
  unfolding one_sheaf_spec_def by simp

lemma add_sheaf_spec_extensional[simp]:
  "add_sheaf_spec U a b โˆˆ extensional U"
  unfolding add_sheaf_spec_def by simp

lemma mult_sheaf_spec_extensional[simp]:
  "mult_sheaf_spec U a b โˆˆ extensional U"
  unfolding mult_sheaf_spec_def by simp

lemma sheaf_spec_extensional[simp]:
  "a โˆˆ ๐’ช U โŸน a โˆˆ extensional U"
  unfolding sheaf_spec_def by (simp add: PiE_iff Set_Theory.map_def)

lemma sheaf_spec_on_open_is_comm_ring:
  assumes "is_zariski_open U"
  shows "comm_ring (๐’ช U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)"
proof unfold_locales
  show add_๐’ช:"add_sheaf_spec U a b โˆˆ ๐’ช U"
    and "mult_sheaf_spec U a b โˆˆ ๐’ช U"
    if "a โˆˆ ๐’ช U" "b โˆˆ ๐’ช U" for a b
    subgoal by (simp add: add_sheaf_spec_in_sheaf_spec assms that(1,2) zariski_open_is_subset)
    subgoal by (simp add: assms mult_sheaf_spec_in_sheaf_spec that(1,2) zariski_open_is_subset)
    done
  show "zero_sheaf_spec U โˆˆ ๐’ช U" "one_sheaf_spec U โˆˆ ๐’ช U"
    subgoal by (simp add: assms zero_sheaf_spec_in_sheaf_spec)
    subgoal by (simp add: assms one_sheaf_spec_in_sheaf_spec)
    done

  have imp_qr:"quotient_ring (Rโˆ–๐”ญ) R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ" if "๐”ญ โˆˆ U" for ๐”ญ
    using that
    by (meson assms comm_ring.spectrum_imp_cxt_quotient_ring in_mono local.comm_ring_axioms
          zariski_open_is_subset)
  have qr_valid_frac:"quotient_ring.valid_frac (Rโˆ–๐”ญ) R (+) (โ‹…) ๐Ÿฌ (s ๐”ญ)"
      if "s โˆˆ ๐’ช U" "๐”ญ โˆˆ U" for s ๐”ญ
    using assms comm_ring.zariski_open_is_subset quotient_ring.carrier_quotient_ring_iff
      imp_qr local.comm_ring_axioms pr_ideal.carrier_local_ring_at_def sec_has_right_codom
      spectrum_imp_pr that(1) that(2) by fastforce

  show add_zero:"add_sheaf_spec U (zero_sheaf_spec U) a = a" if "a โˆˆ ๐’ช U" for a
  proof -
    have "add_sheaf_spec U (zero_sheaf_spec U) a ๐”ญ = a ๐”ญ" if "๐”ญ โˆˆ U" for ๐”ญ
    proof -
      interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ
        using imp_qr that by auto
      show ?thesis unfolding add_sheaf_spec_def zero_sheaf_spec_def
        using that by (simp add: โ€นa โˆˆ ๐’ช Uโ€บ qr_valid_frac)
    qed
    then show "add_sheaf_spec U (zero_sheaf_spec U) a = a"
      using that by(auto intro: extensionalityI[where A=U])
  qed
  show add_assoc:"add_sheaf_spec U (add_sheaf_spec U a b) c
      = add_sheaf_spec U a (add_sheaf_spec U b c)"
    if "a โˆˆ ๐’ช U" and "b โˆˆ ๐’ช U" and "c โˆˆ ๐’ช U"
    for a b c
  proof (rule extensionalityI)
    fix ๐”ญ assume "๐”ญ โˆˆ U"
    interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ using โ€น๐”ญ โˆˆ Uโ€บ imp_qr by auto
    show "add_sheaf_spec U (add_sheaf_spec U a b) c ๐”ญ = add_sheaf_spec U a (add_sheaf_spec U b c) ๐”ญ"
      unfolding add_sheaf_spec_def using โ€น๐”ญ โˆˆ Uโ€บ
      by (simp add: cq.additive.associative qr_valid_frac that(1) that(2) that(3))
  qed (auto simp add:add_sheaf_spec_def)
  show add_comm:"add_sheaf_spec U x y = add_sheaf_spec U y x"
    if "x โˆˆ ๐’ช U" and "y โˆˆ ๐’ช U" for x y
  proof (rule extensionalityI)
    fix ๐”ญ assume "๐”ญ โˆˆ U"
    interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ using โ€น๐”ญ โˆˆ Uโ€บ imp_qr by auto
    show " add_sheaf_spec U x y ๐”ญ = add_sheaf_spec U y x ๐”ญ"
      unfolding add_sheaf_spec_def using โ€น๐”ญ โˆˆ Uโ€บ
      by (simp add: cq.additive.commutative qr_valid_frac that(1) that(2))
  qed auto
  show mult_comm:"mult_sheaf_spec U x y = mult_sheaf_spec U y x"
    if "x โˆˆ ๐’ช U" and "y โˆˆ ๐’ช U" for x y
  proof (rule extensionalityI)
    fix ๐”ญ assume "๐”ญ โˆˆ U"
    interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ using โ€น๐”ญ โˆˆ Uโ€บ imp_qr by auto
    show "mult_sheaf_spec U x y ๐”ญ = mult_sheaf_spec U y x ๐”ญ"
      unfolding mult_sheaf_spec_def using โ€น๐”ญ โˆˆ Uโ€บ
      by (simp add: cq.comm_mult qr_valid_frac that(1) that(2))
  qed auto
  show add_zero:"add_sheaf_spec U a (zero_sheaf_spec U) = a"
      if "a โˆˆ ๐’ช U" for a
    using add_zero add_comm that by (simp add: โ€นzero_sheaf_spec U โˆˆ ๐’ช Uโ€บ)

  show "mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)"
    if "a โˆˆ ๐’ช U" and "b โˆˆ ๐’ช U"
      and "c โˆˆ ๐’ช U"
    for a b c
  proof (rule extensionalityI)
    fix ๐”ญ assume "๐”ญ โˆˆ U"
    interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ using โ€น๐”ญ โˆˆ Uโ€บ imp_qr by auto
    show "mult_sheaf_spec U (mult_sheaf_spec U a b) c ๐”ญ
                = mult_sheaf_spec U a (mult_sheaf_spec U b c) ๐”ญ"
      unfolding mult_sheaf_spec_def using โ€น๐”ญ โˆˆ Uโ€บ
      by (simp add: cq.multiplicative.associative qr_valid_frac that(1) that(2) that(3))
  qed (auto simp add:add_sheaf_spec_def)

  show "mult_sheaf_spec U (one_sheaf_spec U) a = a"
    if "a โˆˆ ๐’ช U" for a
  proof (rule extensionalityI)
    fix ๐”ญ assume "๐”ญ โˆˆ U"
    interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ using โ€น๐”ญ โˆˆ Uโ€บ imp_qr by auto
    show "mult_sheaf_spec U (one_sheaf_spec U) a ๐”ญ = a ๐”ญ"
      unfolding mult_sheaf_spec_def using โ€น๐”ญ โˆˆ Uโ€บ
      by (simp add: one_sheaf_spec_def qr_valid_frac that)
  qed (auto simp add: โ€นa โˆˆ ๐’ช Uโ€บ)
  then show "mult_sheaf_spec U a (one_sheaf_spec U) = a"
    if "a โˆˆ ๐’ช U" for a
    by (simp add: โ€นone_sheaf_spec U โˆˆ ๐’ช Uโ€บ mult_comm that)

  show "mult_sheaf_spec U a (add_sheaf_spec U b c)
          = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)"
    if "a โˆˆ ๐’ช U" and "b โˆˆ ๐’ช U" and "c โˆˆ ๐’ช U" for a b c
  proof (rule extensionalityI)
    fix ๐”ญ assume "๐”ญ โˆˆ U"
    interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ using โ€น๐”ญ โˆˆ Uโ€บ imp_qr by auto
    show "mult_sheaf_spec U a (add_sheaf_spec U b c) ๐”ญ =
         add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) ๐”ญ"
      unfolding mult_sheaf_spec_def add_sheaf_spec_def
      by (simp add: cq.distributive(1) qr_valid_frac that(1) that(2) that(3))
  qed auto
  then show "mult_sheaf_spec U (add_sheaf_spec U b c) a
                = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)"
    if "a โˆˆ ๐’ช U" and "b โˆˆ ๐’ช U" and "c โˆˆ ๐’ช U" for a b c
    by (simp add: add_๐’ช mult_comm that(1) that(2) that(3))
  show "monoid.invertible (๐’ช U) (add_sheaf_spec U) (zero_sheaf_spec U) u"
    if "u โˆˆ ๐’ช U" for u
  proof (rule monoid.invertibleI)
    show "Group_Theory.monoid (๐’ช U) (add_sheaf_spec U) (zero_sheaf_spec U)"
      apply unfold_locales
      using add_๐’ช โ€นzero_sheaf_spec U โˆˆ ๐’ช Uโ€บ add_assoc โ€นzero_sheaf_spec U โˆˆ ๐’ช Uโ€บ
        add_comm add_zero  add_zero
      by simp_all
    show "add_sheaf_spec U u (uminus_sheaf_spec U u) = zero_sheaf_spec U"
    proof (rule extensionalityI)
      fix ๐”ญ assume "๐”ญ โˆˆ U"
      interpret cq:quotient_ring "Rโˆ–๐”ญ" R "(+)" "(โ‹…)" ๐Ÿฌ ๐Ÿญ using โ€น๐”ญ โˆˆ Uโ€บ imp_qr by auto

      have "cq.add_rel (u ๐”ญ) (cq.uminus_rel (u ๐”ญ)) = cq.zero_rel"
        by (simp add: โ€น๐”ญ โˆˆ Uโ€บ cq.add_minus_zero_rel qr_valid_frac that)
      then show "add_sheaf_spec U u (uminus_sheaf_spec U u) ๐”ญ = zero_sheaf_spec U ๐”ญ"
        unfolding add_sheaf_spec_def uminus_sheaf_spec_def zero_sheaf_spec_def
        using โ€น๐”ญ โˆˆ Uโ€บ by simp
    qed auto
    then show "add_sheaf_spec U (uminus_sheaf_spec U u) u = zero_sheaf_spec U"
      by (simp add: add_comm assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
          that uminus_sheaf_spec_in_sheaf_spec)
    show "u โˆˆ ๐’ช U" using that .
    show "uminus_sheaf_spec U u โˆˆ ๐’ช U"
      by (simp add: assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
            that uminus_sheaf_spec_in_sheaf_spec)
  qed
qed

definition sheaf_spec_morphisms::
"'a set set โ‡’ 'a set set โ‡’ (('a set โ‡’ ('a ร— 'a) set) โ‡’ ('a set โ‡’ ('a ร— 'a) set))"
where "sheaf_spec_morphisms U V โ‰ก ฮปsโˆˆ(๐’ช U). restrict s V"

lemma sheaf_morphisms_sheaf_spec:
  assumes "s โˆˆ ๐’ช U"
  shows "sheaf_spec_morphisms U U s = s"
  using assms sheaf_spec_def restrict_on_source sheaf_spec_morphisms_def
  by auto

lemma sheaf_spec_morphisms_are_maps:
  assumes (*this assumption seems redundant: "is_zariski_open U" and*)
    "is_zariski_open V" and "V โŠ† U"
  shows "Set_Theory.map (sheaf_spec_morphisms U V) (๐’ช U) (๐’ช V)"
proof -
  have "sheaf_spec_morphisms U V โˆˆ extensional (๐’ช U)"
    unfolding sheaf_spec_morphisms_def by auto
  moreover have "sheaf_spec_morphisms U V โˆˆ (๐’ช U) โ†’ (๐’ช V)"
    unfolding sheaf_spec_morphisms_def
  proof
    fix s assume "s โˆˆ ๐’ช U"
    then have "s โˆˆ (ฮ E ๐”ญโˆˆU. R ๐”ญ (+) (โ‹…) ๐Ÿฌ)"
        and p:"โˆ€๐”ญ. ๐”ญ โˆˆ U โŸถ (โˆƒV. is_zariski_open V โˆง V โŠ† U โˆง ๐”ญ โˆˆ V โˆง is_locally_frac s V)"
      unfolding sheaf_spec_def is_regular_def by auto
    have "restrict s V โˆˆ (ฮ E ๐”ญโˆˆV. R ๐”ญ (+) (โ‹…) ๐Ÿฌ)"
      using โ€นs โˆˆ (ฮ E ๐”ญโˆˆU. R ๐”ญ (+) (โ‹…) ๐Ÿฌ)โ€บ using โ€นV โŠ† Uโ€บ by auto
    moreover have "(โˆƒVa. is_zariski_open Va โˆง Va โŠ† V โˆง ๐”ญ โˆˆ Va โˆง is_locally_frac (restrict s V) Va)"
      if "๐”ญ โˆˆ V" for ๐”ญ
    proof -
      obtain U1 where "is_zariski_open U1" "U1 โŠ† U" "๐”ญ โˆˆ U1" "is_locally_frac s U1"
        using p[rule_format, of ๐”ญ] that โ€นV โŠ† Uโ€บ โ€น๐”ญ โˆˆ Vโ€บ by auto
      define V1 where "V1 = U1 โˆฉ V"
      have "is_zariski_open V1"
        using โ€นis_zariski_open Vโ€บ โ€นis_zariski_open U1โ€บ by (simp add: V1_def)
      moreover have "is_locally_frac s V1"
        using is_locally_frac_subset[OF โ€นis_locally_frac s U1โ€บ] unfolding V1_def by simp
      then have "is_locally_frac (restrict s V) V1"
        unfolding restrict_def V1_def using is_locally_frac_cong by (smt in_mono inf_le2)
      moreover have "V1 โŠ† V" "๐”ญ โˆˆ V1"
        unfolding V1_def using โ€นV โŠ† Uโ€บ โ€น๐”ญ โˆˆ U1โ€บ that by auto
      ultimately show ?thesis by auto
    qed
    ultimately show "restrict s V โˆˆ ๐’ช V"
      unfolding sheaf_spec_def is_regular_def by auto
  qed
  ultimately show ?thesis
    by (simp add: extensional_funcset_def map.intro)
qed

lemma sheaf_spec_morphisms_are_ring_morphisms:
  assumes U: "is_zariski_open U" and V: "is_zariski_open V" and "V โŠ† U"
  shows "ring_homomorphism (sheaf_spec_morphisms U V)
                           (๐’ช U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
                           (๐’ช V) (add_sheaf_spec V) (mult_sheaf_spec V) (zero_sheaf_spec V) (one_sheaf_spec V)"
proof intro_locales
  show "Set_Theory.map (sheaf_spec_morphisms U V) (๐’ช U) (๐’ช V)"
    by (simp add: assms sheaf_spec_morphisms_are_maps)
  show "Group_Theory.monoid (๐’ช U) (add_sheaf_spec U) (zero_sheaf_spec U)"
    using sheaf_spec_on_open_is_comm_ring [OF U]
    by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def)
  show "Group_Theory.group_axioms (๐’ช U) (add_sheaf_spec U) (zero_sheaf_spec U)"
    using sheaf_spec_on_open_is_comm_ring [OF U]
    by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
  show "commutative_monoid_axioms (๐’ช U) (add_sheaf_spec U)"
    using sheaf_spec_on_open_is_comm_ring [OF U]
    by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
  show "Group_Theory.monoid (๐’ช U) (mult_sheaf_spec U) (one_sheaf_spec U)"
    by (meson U comm_ring_def ring_def sheaf_spec_on_open_is_comm_ring)
  show "ring_axioms (๐’ช U) (add_sheaf_spec U) (mult_sheaf_spec U)"
    by (meson U comm_ring.axioms(1) ring_def sheaf_spec_on_open_is_comm_ring)
  show "Group_Theory.monoid (๐’ช V) (add_sheaf_spec V) (zero_sheaf_spec V)"
    using sheaf_spec_on_open_is_comm_ring [OF V]
    by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def)
  show "Group_Theory.group_axioms (๐’ช V) (add_sheaf_spec V) (zero_sheaf_spec V)"
    using sheaf_spec_on_open_is_comm_ring [OF V]
    by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
  show "commutative_monoid_axioms (๐’ช V) (add_sheaf_spec V)"
    using sheaf_spec_on_open_is_comm_ring [OF V]
    by (auto simp: comm_ring_def ring_def abelian_group_def commutative_monoid_def group_def)
  show "Group_Theory.monoid (๐’ช V) (mult_sheaf_spec V) (one_sheaf_spec V)"
    by (meson V comm_ring.axioms(1) ring_def sheaf_spec_on_open_is_comm_ring)
  show "ring_axioms (๐’ช V) (add_sheaf_spec V) (mult_sheaf_spec V)"
    by (meson V comm_ring_def ring_def sheaf_spec_on_open_is_comm_ring)
  show "monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (๐’ช U)
              (add_sheaf_spec U) (zero_sheaf_spec U) (add_sheaf_spec V) (zero_sheaf_spec V)"
  proof
    fix x y
    assume xy: "x โˆˆ ๐’ช U" "y โˆˆ ๐’ช U"
    have "sheaf_spec_morphisms U V (add_sheaf_spec U x y) = restrict (add_sheaf_spec U x y) V"
      by (simp add: U add_sheaf_spec_in_sheaf_spec comm_ring.zariski_open_is_subset local.comm_ring_axioms sheaf_spec_morphisms_def xy)
    also have "... = add_sheaf_spec V (restrict x V) (restrict y V)"
      using add_sheaf_spec_def โ€นV โŠ† Uโ€บ by force
    also have "... = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)"
      by (simp add: sheaf_spec_morphisms_def xy)
    finally show "sheaf_spec_morphisms U V (add_sheaf_spec U x y) = add_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)" .
  next
    have "sheaf_spec_morphisms U V (zero_sheaf_spec U) = restrict (zero_sheaf_spec U) V"
      by (simp add: U comm_ring.sheaf_spec_morphisms_def local.comm_ring_axioms zero_sheaf_spec_in_sheaf_spec)
    also have "... = zero_sheaf_spec V"
      by (metis FuncSet.restrict_restrict assms(3) inf.absorb_iff2 zero_sheaf_spec_def)
    finally show "sheaf_spec_morphisms U V (zero_sheaf_spec U) = zero_sheaf_spec V" .
  qed
  show "monoid_homomorphism_axioms (sheaf_spec_morphisms U V) (๐’ช U)
              (mult_sheaf_spec U) (one_sheaf_spec U) (mult_sheaf_spec V) (one_sheaf_spec V)"
  proof
    fix x y
    assume xy: "x โˆˆ ๐’ช U" "y โˆˆ ๐’ช U"
        have "sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = restrict (mult_sheaf_spec U x y) V"
      by (simp add: U mult_sheaf_spec_in_sheaf_spec comm_ring.zariski_open_is_subset local.comm_ring_axioms sheaf_spec_morphisms_def xy)
    also have "... = mult_sheaf_spec V (restrict x V) (restrict y V)"
      using mult_sheaf_spec_def โ€นV โŠ† Uโ€บ by force
    also have "... = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)"
      by (simp add: sheaf_spec_morphisms_def xy)
    finally show "sheaf_spec_morphisms U V (mult_sheaf_spec U x y) = mult_sheaf_spec V (sheaf_spec_morphisms U V x) (sheaf_spec_morphisms U V y)" .
  next
    have "sheaf_spec_morphisms U V (one_sheaf_spec U) = restrict (one_sheaf_spec U) V"
      by (simp add: U comm_ring.sheaf_spec_morphisms_def local.comm_ring_axioms one_sheaf_spec_in_sheaf_spec)
    also have "... = one_sheaf_spec V"
      by (metis FuncSet.restrict_restrict assms(3) inf.absorb_iff2 one_sheaf_spec_def)
    finally show "sheaf_spec_morphisms U V (one_sheaf_spec U) = one_sheaf_spec V" .
  qed
qed

lemma sheaf_spec_is_presheaf:
  shows "presheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms ๐’ชb
add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
proof intro_locales
  have "sheaf_spec {} = {๐’ชb}"
  proof
    show "{๐’ชb} โŠ† ๐’ช {}"
      using undefined_is_map_on_empty map_on_empty_is_regular sheaf_spec_def ๐’ช_on_emptyset by auto
    thus "๐’ช {} โŠ† {๐’ชb}"
      using sheaf_spec_def sheaf_spec_of_empty_is_singleton by auto
  qed
  moreover have "โ‹€U. is_zariski_open U โŸน (โ‹€s. s โˆˆ (๐’ช U) โŸน sheaf_spec_morphisms U U s = s)"
    using sheaf_spec_morphisms_def sheaf_morphisms_sheaf_spec by simp
  moreover have "sheaf_spec_morphisms U W s = (sheaf_spec_morphisms V W โˆ˜ sheaf_spec_morphisms U V) s"
    if "is_zariski_open U" "is_zariski_open V" "is_zariski_open W" "V โŠ† U" "W โŠ† V" and "s โˆˆ ๐’ช U"
    for U V W s
  proof -
    have "restrict s V โˆˆ ๐’ช V"
      using that by (smt map.map_closed restrict_apply sheaf_spec_morphisms_are_maps sheaf_spec_morphisms_def)
    with that show ?thesis
      by (simp add: sheaf_spec_morphisms_def inf_absorb2)
  qed
  ultimately show "presheaf_of_rings_axioms is_zariski_open sheaf_spec
                    sheaf_spec_morphisms ๐’ชb add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
    unfolding presheaf_of_rings_def presheaf_of_rings_axioms_def using sheaf_spec_morphisms_are_ring_morphisms
    by blast
qed

(* ex. 0.30 *)
lemma sheaf_spec_is_sheaf:
  shows "sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms ๐’ชb
add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
  show "presheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms ๐’ชb
     add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
    using sheaf_spec_is_presheaf by simp
next
  fix U I V s assume H: "open_cover_of_open_subset Spec is_zariski_open U I V"
                        "โ‹€i. i โˆˆ I โŸน V i โŠ† U"
                        "s โˆˆ ๐’ช U"
                        "โ‹€i. i โˆˆ I โŸน sheaf_spec_morphisms U (V i) s = zero_sheaf_spec (V i)"
  then have "s ๐”ญ = zero_sheaf_spec U ๐”ญ" if "๐”ญ โˆˆ U" for ๐”ญ
  proof -
    from that obtain i where F: "i โˆˆ I" "๐”ญ โˆˆ (V i)" "is_zariski_open (V i)"
      using H(1) unfolding open_cover_of_subset_def open_cover_of_open_subset_def
      by (metis cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs open_cover_of_subset_axioms_def)
    then have "sheaf_spec_morphisms U (V i) s ๐”ญ = quotient_ring.zero_rel (R โˆ– ๐”ญ) R (+) (โ‹…) ๐Ÿฌ ๐Ÿญ"
      using H(2,4) F by (simp add: zero_sheaf_spec_def)
    thus "s ๐”ญ = zero_sheaf_spec U ๐”ญ"
      using sheaf_spec_morphisms_def zero_sheaf_spec_def F(2) by (simp add: H(3) โ€น๐”ญ โˆˆ Uโ€บ)
  qed
  moreover have "s โˆˆ extensional U" " zero_sheaf_spec U โˆˆ extensional U"
    by (simp_all add: H(3))
  ultimately show "s = zero_sheaf_spec U" using extensionalityI by blast
next
  fix U I V s assume H: "open_cover_of_open_subset Spec is_zariski_open U I V"
                        "โˆ€i. i โˆˆ I โŸถ V i โŠ† U โˆง s i โˆˆ ๐’ช (V i)"
                        "โ‹€i j. i โˆˆ I โŸน
                                  j โˆˆ I โŸน
                                    sheaf_spec_morphisms (V i) (V i โˆฉ V j) (s i) =
                                    sheaf_spec_morphisms (V j) (V i โˆฉ V j) (s j)"
  define t where D: "t โ‰ก ฮป๐”ญโˆˆU. s (cover_of_subset.select_index I V ๐”ญ) ๐”ญ"
  then have F1: "s i ๐”ญ = s j ๐”ญ" if "i โˆˆ I" "j โˆˆ I" "๐”ญ โˆˆ V i" "๐”ญ โˆˆ V j" for ๐”ญ i j
  proof -
    have "s i ๐”ญ = sheaf_spec_morphisms (V i) (V i โˆฉ V j) (s i) ๐”ญ"
      using that sheaf_spec_morphisms_def by (simp add: H(2))
    moreover have "โ€ฆ = sheaf_spec_morphisms (V j) (V i โˆฉ V j) (s j) ๐”ญ"
      using H(3) that by fastforce
    moreover have "โ€ฆ = s j ๐”ญ"
      using sheaf_spec_morphisms_def that by (simp add: H(2))
    ultimately show "s i ๐”ญ = s j ๐”ญ" by blast
  qed
  have "t โˆˆ ๐’ช U"
  proof-
    have "t ๐”ญ โˆˆ (R๐”ญ (+) (โ‹…) ๐Ÿฌ)" if "๐”ญโˆˆU" for ๐”ญ
      using D H(1) H(2) cover_of_subset.cover_of_select_index
        cover_of_subset.select_index_belongs open_cover_of_open_subset.axioms(1)
        open_cover_of_subset_def sec_has_right_codom that by fastforce
    moreover have "t โˆˆ extensional U"
      using D by blast
    moreover have "is_regular t U"
      unfolding is_regular_def
    proof (intro strip conjI)
      fix ๐”ญ
      assume "๐”ญ โˆˆ U"
      show "โˆƒV. is_zariski_open V โˆง V โŠ† U โˆง ๐”ญ โˆˆ V โˆง is_locally_frac t V"
      proof -
        have cov_in_I: "cover_of_subset.select_index I V ๐”ญ โˆˆ I"
          by (meson H(1) โ€น๐”ญ โˆˆ Uโ€บ cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def)
        have V: "V (cover_of_subset.select_index I V ๐”ญ) โŠ† U"
          using H(2) by (meson H(1) โ€น๐”ญ โˆˆ Uโ€บ cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def)
        have V2: "โˆƒV'. is_zariski_open V' โˆง V'โŠ† V (cover_of_subset.select_index I V ๐”ญ) โˆง ๐”ญ โˆˆ V' โˆง
                 is_locally_frac (s (cover_of_subset.select_index I V ๐”ญ)) V'"
          using H(1,2)
          unfolding sheaf_spec_def open_cover_of_open_subset_def open_cover_of_subset_def is_regular_def
          using โ€น๐”ญ โˆˆ Uโ€บ cov_in_I cover_of_subset.cover_of_select_index by fastforce
        have "โ‹€V' ๐”ฎ. is_zariski_open V' โˆง V' โŠ† V (cover_of_subset.select_index I V ๐”ญ) โŸน ๐”ฎ โˆˆ V' โŸน t ๐”ฎ = s (cover_of_subset.select_index I V ๐”ญ) ๐”ฎ"
          by (smt D F1 H(1) V โ€น๐”ญ โˆˆ Uโ€บ cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def restrict_apply subsetD)
        with V V2 show ?thesis unfolding is_locally_frac_def
          by (smt subset_trans)
      qed
    qed
    ultimately show ?thesis unfolding sheaf_spec_def by (simp add:PiE_iff)
  qed
  have "sheaf_spec_morphisms U (V i) t = s i" if "i โˆˆ I" for i
  proof
    fix ๐”ญ
    have "sheaf_spec_morphisms U (V i) t ๐”ญ = s i ๐”ญ" if "๐”ญ โˆˆ U"
    proof-
      from that H(1)
      obtain j where "j โˆˆ I โˆง ๐”ญ โˆˆ V j โˆง t ๐”ญ = s j ๐”ญ"
        unfolding D open_cover_of_subset_def open_cover_of_open_subset_def
        by (meson cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs restrict_apply')
      thus "sheaf_spec_morphisms U (V i) t ๐”ญ = s i ๐”ญ"
        using โ€นt โˆˆ ๐’ช Uโ€บ โ€นi โˆˆ Iโ€บ H(2) that
        unfolding sheaf_spec_morphisms_def
        apply (simp add: D split: if_split_asm)
        by (metis (mono_tags, hide_lams) F1  extensional_arb [OF sec_is_extensional])
    qed
    thus "sheaf_spec_morphisms U (V i) t ๐”ญ = s i ๐”ญ"
      using sheaf_spec_morphisms_def D F1
      by (smt H(2) โ€นi โˆˆ Iโ€บ โ€นt โˆˆ ๐’ช Uโ€บ comm_ring.sheaf_morphisms_sheaf_spec local.comm_ring_axioms restrict_apply subsetD)
  qed
  thus "โˆƒt. t โˆˆ (๐’ช U) โˆง (โˆ€i. i โˆˆ I โŸถ sheaf_spec_morphisms U (V i) t = s i)"
    using โ€นt โˆˆ ๐’ช Uโ€บ by blast
qed

lemma shrinking:
  assumes "is_zariski_open U" and "๐”ญ โˆˆ U" and "s โˆˆ ๐’ช U" and "t โˆˆ ๐’ช U"
  obtains V a f b g where "is_zariski_open V" "V โŠ† U" "๐”ญ โˆˆ V" "a โˆˆ R" "f โˆˆ R" "b โˆˆ R" "g โˆˆ R"
"f โˆ‰ ๐”ญ" "g โˆ‰ ๐”ญ"
"โ‹€๐”ฎ. ๐”ฎ โˆˆ V โŸน f โˆ‰ ๐”ฎ โˆง s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ a f"
"โ‹€๐”ฎ. ๐”ฎ โˆˆ V โŸน g โˆ‰ ๐”ฎ โˆง t ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ b g"
proof-
  obtain Vs a f where "is_zariski_open Vs" "Vs โŠ† U" "๐”ญ โˆˆ Vs" "a โˆˆ R" "f โˆˆ R"
"โ‹€๐”ฎ. ๐”ฎ โˆˆ Vs โŸน f โˆ‰ ๐”ฎ โˆง s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ a f"
    using assms(2,3) sheaf_spec_def is_regular_def is_locally_frac_def by auto
  obtain Vt b g where "is_zariski_open Vt" "Vt โŠ† U" "๐”ญ โˆˆ Vt" "b โˆˆ R" "g โˆˆ R"
"โ‹€๐”ฎ. ๐”ฎ โˆˆ Vt โŸน g โˆ‰ ๐”ฎ โˆง t ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ b g"
    using assms(2,4) sheaf_spec_def is_regular_def is_locally_frac_def by auto
  then have "is_zariski_open (Vs โˆฉ Vt)" "Vs โˆฉ Vt โŠ† U" "๐”ญ โˆˆ Vs โˆฉ Vt"
"โ‹€๐”ฎ. ๐”ฎ โˆˆ (Vs โˆฉ Vt) โŸน f โˆ‰ ๐”ฎ โˆง s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ a f"
"โ‹€๐”ฎ. ๐”ฎ โˆˆ (Vs โˆฉ Vt) โŸน g โˆ‰ ๐”ฎ โˆง t ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ b g"
    using topological_space.open_inter apply (simp add: โ€นis_zariski_open Vsโ€บ)
    using โ€นVs โŠ† Uโ€บ apply auto[1] apply (simp add: โ€น๐”ญ โˆˆ Vsโ€บ โ€น๐”ญ โˆˆ Vtโ€บ)
    apply (simp add: โ€นโ‹€๐”ฎ. ๐”ฎ โˆˆ Vs โŸน f โˆ‰ ๐”ฎ โˆง s ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ a fโ€บ)
    by (simp add: โ€นโ‹€๐”ฎ. ๐”ฎ โˆˆ Vt โŸน g โˆ‰ ๐”ฎ โˆง t ๐”ฎ = quotient_ring.frac (Rโˆ–๐”ฎ) R (+) (โ‹…) ๐Ÿฌ b gโ€บ)
  thus ?thesis using โ€นa โˆˆ Rโ€บ โ€นb โˆˆ Rโ€บ โ€นf โˆˆ Rโ€บ โ€นg โˆˆ Rโ€บ that by presburger
qed

end (* comm_ring *)


section โ€นSchemesโ€บ

subsection โ€นRinged Spacesโ€บ

(* definition 0.32 *)
locale ringed_space = sheaf_of_rings

context comm_ring
begin

lemma spec_is_ringed_space:
  shows "ringed_space Spec is_zariski_open sheaf_spec sheaf_spec_morphisms ๐’ชb
add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
proof (intro ringed_space.intro)
  show "sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms ๐’ชb
     add_sheaf_spec mult_sheaf_spec zero_sheaf_spec one_sheaf_spec"
    using sheaf_spec_is_sheaf by simp
qed

end (* comm_ring *)

(* definition 0.33 *)
locale morphism_ringed_spaces =
im_sheaf X is_openX ๐’ชX ฯX b add_strX mult_strX zero_strX one_strX Y is_openY f +
 codom: ringed_space Y is_openY ๐’ชY ฯY d add_strY mult_strY zero_strY one_strY
for X and is_openX and ๐’ชX and ฯX and b and add_strX and mult_strX and zero_strX and one_strX
and Y and is_openY and ๐’ชY and ฯY and d and add_strY and mult_strY and zero_strY and one_strY
and f +
fixes ฯ†f:: "'c set โ‡’ ('d โ‡’ 'b)"
assumes is_morphism_of_sheaves: "morphism_sheaves_of_rings
Y is_openY ๐’ชY ฯY d add_strY mult_strY zero_strY one_strY
im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
ฯ†f"


subsection โ€นDirect Limits of Ringsโ€บ

(* construction 0.34 *)
locale direct_lim = sheaf_of_rings +
  fixes I:: "'a set set"
  assumes subset_of_opens: "โ‹€U. U โˆˆ I โŸน is_open U"
    and has_lower_bound: "โ‹€U V. โŸฆ UโˆˆI; VโˆˆI โŸง โŸน โˆƒWโˆˆI. W โŠ† U โˆฉ V"
begin

definition get_lower_bound:: "'a set โ‡’ 'a set โ‡’ 'a set" where
  "get_lower_bound U V= (SOME W. W โˆˆ I โˆง W โŠ† U โˆง W โŠ† V)"

lemma get_lower_bound[intro]:
  assumes "U โˆˆ I" "V โˆˆ I"
  shows "get_lower_bound U V โˆˆ I" "get_lower_bound U V โŠ† U" "get_lower_bound U V โŠ† V"
proof -
  have "โˆƒW. W โˆˆ I โˆง W โŠ† U โˆง W โŠ† V"
    using has_lower_bound[OF assms] by auto
  from someI_ex[OF this]
  show "get_lower_bound U V โˆˆ I" "get_lower_bound U V โŠ† U" "get_lower_bound U V โŠ† V"
    unfolding get_lower_bound_def by auto
qed

lemma obtain_lower_bound_finite:
  assumes "finite Us"  "Us โ‰  {}" "Us โŠ† I"
  obtains W where "W โˆˆ I" "โˆ€UโˆˆUs. W โŠ† U"
  using assms
proof (induct Us arbitrary:thesis)
  case (insert U F)
  have ?case when "F={}"
    using insert.prems(1) insert.prems(3) that by blast
  moreover have ?case when "Fโ‰ {}"
  proof -
    obtain W where "W โˆˆ I" "โˆ€UโˆˆF. W โŠ† U"
      using insert.hyps(3) insert.prems(3) by auto
    obtain W1 where "W1 โˆˆI" "W1 โŠ† U" "W1 โŠ† W"
      by (meson โ€นW โˆˆ Iโ€บ get_lower_bound(1) get_lower_bound(2) get_lower_bound(3)
          insert.prems(3) insert_subset)
    then have "โˆ€aโˆˆinsert U F. W1 โŠ† a"
      using โ€นโˆ€UโˆˆF. W โŠ† Uโ€บ by auto
    with โ€นW1 โˆˆIโ€บ show ?thesis
      using insert(4) by auto
  qed
  ultimately show ?case by auto
qed simp

definition principal_subs :: "'a set set โ‡’ 'a set โ‡’ 'a set filter" where
  "principal_subs As A = Abs_filter (ฮปP. โˆ€x. (xโˆˆAs โˆง x โŠ† A) โŸถ P x)"

lemma eventually_principal_subs: "eventually P (principal_subs As A) โŸท (โˆ€x. xโˆˆAs โˆง xโŠ†A โŸถ P x)"
  unfolding principal_subs_def
  by (rule eventually_Abs_filter, rule is_filter.intro) auto

lemma principal_subs_UNIV[simp]: "principal_subs UNIV UNIV = top"
  by (auto simp: filter_eq_iff eventually_principal_subs)

lemma principal_subs_empty[simp]: "principal_subs {} s = bot"
  (*"principal_subs ss {} = bot"*)
  by (auto simp: filter_eq_iff eventually_principal_subs)

lemma principal_subs_le_iff[iff]:
  "principal_subs As A โ‰ค principal_subs As' A'
            โŸท {x. xโˆˆAs โˆง x โŠ† A} โŠ† {x. xโˆˆAs' โˆง x โŠ† A'}"
  unfolding le_filter_def eventually_principal_subs by blast

lemma principal_subs_eq_iff[iff]:
    "principal_subs As A = principal_subs As' A' โŸท{x. xโˆˆAs โˆง x โŠ† A} = {x. xโˆˆAs' โˆง x โŠ† A'}"
  unfolding eq_iff by simp

lemma principal_subs_inj_on[simp]:"inj_on (principal_subs As) As"
  unfolding inj_on_def by auto

definition lbound :: "'a set set โ‡’ ('a set) filter" where
  "lbound Us = (INF Sโˆˆ{S. SโˆˆI โˆง (โˆ€uโˆˆUs. S โŠ† u)}. principal_subs I S)"

lemma eventually_lbound_finite:
  assumes "finite A" "Aโ‰ {}" "AโŠ†I"
  shows "(โˆ€F w in lbound A. P w) โŸท (โˆƒw0. w0 โˆˆ I โˆง (โˆ€aโˆˆA. w0 โŠ† a) โˆง (โˆ€w. (wโŠ†w0 โˆง wโˆˆI) โŸถ P w))"
proof -
  have "โˆƒx. x โˆˆ I โˆง (โˆ€xaโˆˆA. x โŠ† xa)"
    by (metis Int_iff assms inf.order_iff obtain_lower_bound_finite)
  moreover have " โˆƒx. x โˆˆ I โˆง Ball A ((โŠ†) x)
              โˆง {xa โˆˆ I. xa โŠ† x} โŠ† {x โˆˆ I. x โŠ† a}
                โˆง {xa โˆˆ I. xa โŠ† x} โŠ† {x โˆˆ I. x โŠ† b}"
    if "a โˆˆ I โˆง (โˆ€xโˆˆA. a โŠ† x)" "b โˆˆ I โˆง (โˆ€xโˆˆA. b โŠ† x)" for a b
    apply (rule exI[where x="get_lower_bound a b"])
    using that apply auto
    subgoal using get_lower_bound(2) by blast
    subgoal by (meson get_lower_bound(2) subsetD)
    subgoal by (meson get_lower_bound(3) subsetD)
    done
  moreover have "(โˆƒbโˆˆ{S โˆˆ I. Ball A ((โŠ†) S)}. eventually P (principal_subs I b)) =
    (โˆƒw0. w0 โˆˆ I โˆง Ball A ((โŠ†) w0) โˆง (โˆ€w. w โŠ† w0 โˆง w โˆˆ I โŸถ P w))"
    unfolding eventually_principal_subs by force
  ultimately show ?thesis unfolding lbound_def
    by (subst eventually_INF_base) auto
qed

lemma lbound_eq:
  assumes A:"finite A" "Aโ‰ {}" "AโŠ†I"
  assumes B:"finite B" "Bโ‰ {}" "BโŠ†I"
  shows "lbound A = lbound B"
proof -
  have "eventually P (lbound A')" if "eventually P (lbound B')"
    and A':"finite A'" "A'โ‰ {}" "A' โŠ† I"
    and B':"finite B'" "B'โ‰ {}" "B' โŠ† I"
  for P A' B'
  proof -
    obtain w0 where w0:"w0 โˆˆ I" "(โˆ€aโˆˆB'. w0 โŠ† a)" "(โˆ€w. w โŠ† w0 โˆง w โˆˆ I โŸถ P w)"
      using โ€นeventually P (lbound B')โ€บ unfolding eventually_lbound_finite[OF B',of P]
      by auto
    obtain w1 where w1:"w1 โˆˆ I" "โˆ€UโˆˆA'. w1 โŠ† U"
      using obtain_lower_bound_finite[OF A'] by auto
    define w2 where "w2=get_lower_bound w0 w1"
    have "w2 โˆˆ I" using โ€นw0 โˆˆ Iโ€บ โ€นw1 โˆˆ Iโ€บ unfolding w2_def by auto
    moreover have "โˆ€aโˆˆA'. w2 โŠ† a"
      unfolding w2_def by (meson dual_order.trans get_lower_bound(3) w0(1) w1(1) w1(2))
    moreover have "โˆ€w. w โŠ† w2 โˆง w โˆˆ I โŸถ P w"
      unfolding w2_def by (meson dual_order.trans get_lower_bound(2) w0(1) w0(3) w1(1))
    ultimately show ?thesis unfolding eventually_lbound_finite[OF A',of P] by auto
  qed
  then have "eventually P (lbound A) = eventually P (lbound B)" for P
    using A B by auto
  then show ?thesis unfolding filter_eq_iff by auto
qed

lemma lbound_leq:
  assumes "A โŠ† B"
  shows "lbound A โ‰คlbound B"
  unfolding lbound_def
  apply (rule Inf_superset_mono)
  apply (rule image_mono)
  using assms by auto

definition llbound::"('a set) filter" where
  "llbound = lbound {SOME a. aโˆˆI}"

lemma llbound_not_bot:
  assumes "Iโ‰  {}"
  shows "llbound โ‰  bot"
  unfolding trivial_limit_def llbound_def
  apply (subst eventually_lbound_finite)
  using assms by (auto simp add: some_in_eq)

lemma llbound_lbound:
  assumes "finite A" "Aโ‰ {}" "AโŠ†I"
  shows "lbound A = llbound"
  unfolding llbound_def
  apply (rule lbound_eq)
  using assms by (auto simp add: some_in_eq)

definition rel:: "('a set ร— 'b) โ‡’ ('a set ร— 'b) โ‡’ bool" (infix "โˆผ" 80)
  where "x โˆผ y โ‰ก (fst x โˆˆ I โˆง fst y โˆˆ I) โˆง (snd x โˆˆ ๐”‰ (fst x) โˆง snd y โˆˆ ๐”‰ (fst y)) โˆง
(โˆƒW. (W โˆˆ I) โˆง (W โŠ† fst x โˆฉ fst y) โˆง ฯ (fst x) W (snd x) = ฯ (fst y) W (snd y))"

lemma rel_is_equivalence:
  shows "equivalence (Sigma I ๐”‰) {(x, y). x โˆผ y}"
  unfolding equivalence_def
proof (intro conjI strip)
  show "(a, c) โˆˆ {(x, y). x โˆผ y}"
    if "(a, b) โˆˆ {(x, y). x โˆผ y}" "(b, c) โˆˆ {(x, y). x โˆผ y}" for a b c
  proof -
    obtain W1 where W1:"fst a โˆˆ I" "fst b โˆˆ I" "snd a โˆˆ ๐”‰ (fst a)" "snd b โˆˆ ๐”‰ (fst b)"
                    "W1 โˆˆ I" "W1 โŠ† fst a" "W1 โŠ† fst b"
                    "ฯ (fst a) W1 (snd a) = ฯ (fst b) W1 (snd b)"
      using โ€น(a, b) โˆˆ {(x, y). x โˆผ y}โ€บ unfolding rel_def by auto
    obtain W2 where W2:"fst b โˆˆ I" "fst c โˆˆ I" "snd b โˆˆ ๐”‰ (fst b)" "snd c โˆˆ ๐”‰ (fst c)"
                    "W2 โˆˆ I" "W2 โŠ† fst b" "W2 โŠ† fst c"
                    "ฯ (fst b) W2 (snd b) = ฯ (fst c) W2 (snd c)"
      using โ€น(b, c) โˆˆ {(x, y). x โˆผ y}โ€บ unfolding rel_def by auto
    obtain W3 where W3:"W3 โˆˆI" "W3 โŠ† W1 โˆฉ W2"
      using has_lower_bound[OF โ€นW1โˆˆIโ€บ โ€นW2โˆˆIโ€บ] by auto
    from โ€นW3 โŠ† W1 โˆฉ W2โ€บ
    have "W3 โŠ† fst a โˆฉ fst c" using W1(6) W2(7) by blast
    moreover have "ฯ (fst a) W3 (snd a) = ฯ (fst c) W3 (snd c)"
      using W1 W2 by (metis W3(1) W3(2) eq_ฯ le_inf_iff subset_of_opens)
    moreover note โ€นW3 โˆˆIโ€บ W1 W2
    ultimately show ?thesis
      unfolding rel_def by auto
  qed
qed (auto simp: rel_def Int_commute)

interpretation rel:equivalence "(Sigma I ๐”‰)" "{(x, y). x โˆผ y}"
  using rel_is_equivalence .

definition class_of:: "'a set โ‡’ 'b โ‡’ ('a set ร— 'b) set" ("โŒŠ(_,/ _)โŒ‹")
  where "โŒŠU,sโŒ‹ โ‰ก rel.Class (U, s)"

lemma class_of_eqD:
  assumes "โŒŠU1,s1โŒ‹ = โŒŠU2,s2โŒ‹" "(U1,s1) โˆˆ Sigma I ๐”‰" "(U2,s2) โˆˆ Sigma I ๐”‰"
  obtains W where "W โˆˆ I" "W โŠ† U1 โˆฉ U2" "ฯ U1 W s1 = ฯ U2 W s2"
  using rel.Class_equivalence[OF assms(2,3)] assms(1)
  unfolding class_of_def rel_def by auto

lemma class_of_eqI:
  assumes "(U1,s1) โˆˆ Sigma I ๐”‰" "(U2,s2) โˆˆ Sigma I ๐”‰"
  assumes "W โˆˆ I" "W โŠ† U1 โˆฉ U2" "ฯ U1 W s1 = ฯ U2 W s2"
  shows "โŒŠU1,s1โŒ‹ = โŒŠU2,s2โŒ‹"
  unfolding class_of_def
  apply (rule rel.Class_eq)
  using assms  by (auto simp: rel_def)

lemma class_of_0_in:
  assumes "U โˆˆ I"
  shows "๐ŸฌU โˆˆ ๐”‰ U"
proof -
  have "ring (๐”‰ U) +U โ‹…U ๐ŸฌU ๐ŸญU"
    using assms subset_of_opens is_ring_from_is_homomorphism by blast
  then show ?thesis
    unfolding ring_def abelian_group_def Group_Theory.group_def by (meson monoid.unit_closed)
qed

lemma rel_Class_iff: "x โˆผ y โŸท y โˆˆ Sigma I ๐”‰ โˆง x โˆˆ rel.Class y"
  by blast

lemma class_of_0_eq:
  assumes "U โˆˆ I" "U' โˆˆ I"
  shows "โŒŠU, ๐ŸฌUโŒ‹ = โŒŠU', ๐ŸฌU'โŒ‹"
proof -
  obtain W where W: "W โˆˆ I" "W โŠ† U" "W โŠ† U'"
    by (metis Int_subset_iff assms has_lower_bound)
  then have "is_open W" "is_open U" "is_open U'"
    by (auto simp add: assms subset_of_opens)
  then have "ฯ U W ๐ŸฌU = ฯ U' W ๐ŸฌU'"
    using W is_ring_morphism [of U W] is_ring_morphism [of U' W]
    by (simp add: ring_homomorphism_def group_homomorphism_def monoid_homomorphism_def
               monoid_homomorphism_axioms_def)
  with W have "โˆƒW. W โˆˆ I โˆง W โŠ† U โˆง W โŠ† U' โˆง ฯ U W ๐ŸฌU = ฯ U' W ๐ŸฌU'" by blast
  moreover have "๐ŸฌU โˆˆ ๐”‰ U" "๐ŸฌU' โˆˆ ๐”‰ U'"
    by (auto simp add: assms class_of_0_in)
  ultimately have "(U, ๐ŸฌU) โˆผ (U', ๐ŸฌU')"
    using assms by (auto simp: rel_def)
  then show ?thesis
    unfolding class_of_def by (simp add: rel.Class_eq)
qed

lemma class_of_1_in:
  assumes "U โˆˆ I"
  shows "๐ŸญU โˆˆ ๐”‰ U"
proof -
  have "ring (๐”‰ U) +U โ‹…U ๐ŸฌU ๐ŸญU"
    using assms subset_of_opens is_ring_from_is_homomorphism by blast
  then show ?thesis
    unfolding ring_def by (meson monoid.unit_closed)
qed

lemma class_of_1_eq:
  assumes "U โˆˆ I" and "U' โˆˆ I"
  shows "โŒŠU, ๐ŸญUโŒ‹ = โŒŠU', ๐ŸญU'โŒ‹"
proof -
  obtain W where W: "W โˆˆ I" "W โŠ† U" "W โŠ† U'"
    by (metis Int_subset_iff assms has_lower_bound)
  then have "is_open W" "is_open U" "is_open U'"
    by (auto simp add: assms subset_of_opens)
  then have "ฯ U W ๐ŸญU = ฯ U' W ๐ŸญU'