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. rR. 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: "rR" "a = r  x"
    using a gen_ideal_def by auto
  show "monoid.invertible x (+) 𝟬 a"
  proof (rule M.invertibleI)
    have "rR. - 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: "rR" "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. jJ  ideal (𝔞 j) R (+) (⋅) 𝟬 𝟭"
  shows "𝒱 ({x. I f. x = finsum I f  I  J  finite I  (i. iI  f i  𝔞 i)}) = (jJ. 𝒱 (𝔞 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 "jJ. pr_ideal R x (+) (⋅) 𝟬 𝟭  𝔞 j  x" for x
    using that assms(1) by fastforce
  moreover have "finsum I f  U"
    if "finite I"
      and "jJ. 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. iI  V i  U) 
s  𝔉 U  (i. iI  ρ 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. iI  V i  U  s i  𝔉 (V i)) 
(i j. iI  jI  ρ (V i) (V i  V j) (s i) = ρ (V j) (V i  V j) (s j)) 
(t. t  𝔉 U  (i. iI  ρ 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  𝟬(UV)"

definition ind_one_str:: "'a set  'b"
  where "ind_one_str V  𝟭(UV)"

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)"
  unfolding ind_add_str_def it.ind_is_open_def ind_mult_str_def ind_one_str_def ind_sheaf_def ind_zero_str_def 
  using 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)"
      unfolding ind_ring_morphisms_def ind_sheaf_def
      by (metis that it.ind_is_open_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)"
      unfolding ind_ring_morphisms_def ind_sheaf_def ind_zero_str_def
      by (metis ind_sheaf.ind_add_str_def ind_sheaf_axioms 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 "iI" "jI" 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. iI  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. iI  ρ 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. iI  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. iI  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. iI  ρ (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) +UU 𝟬U 𝟭U (𝔉 U) +UU 𝟬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 "s1S" 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 s1S 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 "s1S" "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 "s1S" and "(r, s)  R × S"
  shows "frac (s1r) (s1s) = 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 "s1S" "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:"xR × S" and "x  (r,s)" by auto
  from this(2) obtain s1 where "s1S" 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 s1S by auto
qed

definition valid_frac::"('a × 'a) set  bool" where
  "valid_frac X  rR. sS. 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'  (rs' + r's) / (ss')"

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') = (rs' + r's) / (ss')"
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 "... = (rs' + r's) / (ss')"
  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 "rR" "sS" "r'R" "s'S"
      and *:"add_rel X Y = (rs' + r's) / (ss')"
  proof -
    define x where "x=(SOME x. xX)"
    define y where "y=(SOME y. yY)"
    have "xX" "yY"
      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 "(rs' + r's,ss')  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 "rR" "sS"
      and *:"uminus_rel X = (comm.additive.inverse r) / s"
  proof -
    define x where "x=(SOME x. xX)"
    have "xX"
      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'  (rr') / (ss')"

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') / (ss')"
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') / (ss')"
  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 "rR" "sS" "r'R" "s'S"
      and *:"mult_rel X Y = (r r') / (ss')"
  proof -
    define x where "x=(SOME x. xX)"
    define y where "y=(SOME y. yY)"
    have "xX" "yY"
      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 "(rr',ss')  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  RI" if "a  RI" "b  RI" for a b
    using that by (metis Diff_iff absorbent comm.multiplicative.composition_closed)
  show "𝟭  RI"
    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. xU  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 "(VU. 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 "(VU. 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 "(VU. 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 "(VU. 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 "(VU. 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, opaque_lifting) 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.  UI; VI   WI. 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" "UUs. 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" "UF. 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 "ainsert U F. W1  a"
      using UF. 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. (xAs  x  A)  P x)"

lemma eventually_principal_subs: "eventually P (principal_subs As A)  (x. xAs  xA  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. xAs  x  A}  {x. xAs'  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. xAs  x  A} = {x. xAs'  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. SI  (uUs. S  u)}. principal_subs I S)"

lemma eventually_lbound_finite:
  assumes "finite A" "A{}" "AI"
  shows "(F w in lbound A. P w)  (w0. w0  I  (aA. w0  a)  (w. (ww0  wI)  P w))"
proof -
  have "x. x  I  (xaA. 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  (xA. a  x)" "b  I  (xA. 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{}" "AI"
  assumes B:"finite B" "B{}" "BI"
  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" "(aB'. 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" "UA'. 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 "aA'. 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. aI}"

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{}" "AI"
  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 W1I W2I] 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) +UU 𝟬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) +UU 𝟬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'"
    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_1_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

definition add_rel :: "('a set × 'b) set  ('a set × 'b) set  ('a set × 'b) set"
  where "add_rel X Y  let
              x = (SOME x. x  X);
              y = (SOME y. y  Y);
              w = get_lower_bound (fst x) (fst y)
            in
              w, add_str w (ρ (fst x) w (snd x)) (ρ (fst y) w (snd y))"

definition mult_rel :: "('a set × 'b) set  ('a set × 'b) set  ('a set × 'b) set"
  where "mult_rel X Y  let
              x = (SOME x. x  X);
              y = (SOME y. y  Y);
              w = get_lower_bound (fst x) (fst y)
            in
              w, mult_str w (ρ (fst x) w (snd x)) (ρ (fst y) w (snd y))"

definition carrier_direct_lim:: "('a set × 'b) set set"
  where "carrier_direct_lim  rel.Partition"

lemma zero_rel_carrier[intro]:
  assumes "U  I"
  shows "U, 𝟬U  carrier_direct_lim"
  unfolding carrier_direct_lim_def class_of_def
proof (rule rel.Block_closed)
  interpret ring "(𝔉 U)" "+U" "⋅U" "𝟬U" "𝟭U"
    by (simp add: assms is_ring_from_is_homomorphism subset_of_opens)
  show "(U, 𝟬U)  Sigma I 𝔉"
    by (simp add: assms)
qed

lemma one_rel_carrier[intro]:
  assumes "U  I"
  shows "U, 𝟭U  carrier_direct_lim"
  unfolding carrier_direct_lim_def class_of_def
  apply (rule rel.Block_closed)
  by (simp add: assms class_of_1_in)

lemma rel_carrier_Eps_in:
  fixes X :: "('a set × 'b) set"
  defines "a(SOME x. x  X)"
  assumes "X  carrier_direct_lim"
  shows "a  X" "a Sigma I 𝔉"  "X = fst a, snd a"
proof -
  have "aSigma I 𝔉. a  X  X = rel.Class a"
    using rel.representant_exists[OF X  carrier_direct_lim›[unfolded carrier_direct_lim_def]]
    by simp
  then have "a  X  a Sigma I 𝔉  X = fst a, snd a"
    unfolding class_of_def
    by (metis a_def assms(2) carrier_direct_lim_def ex_in_conv prod.collapse rel.Block_self
        rel.Class_closed some_in_eq)
  then show "a  X" "a Sigma I 𝔉"  "X = fst a, snd a" by auto
qed

lemma add_rel_carrier[intro]:
  assumes "X  carrier_direct_lim" "Y  carrier_direct_lim"
  shows "add_rel X Y  carrier_direct_lim"
proof -
  define x where "x=(SOME x. x  X)"
  define y where "y=(SOME y. y  Y)"
  define z where "z=get_lower_bound (fst x) (fst y)"

  have "xX" "xSigma I 𝔉"
    using rel_carrier_Eps_in[OF X  carrier_direct_lim›] unfolding x_def by auto
  have "yY" "y  Sigma I 𝔉"
    using rel_carrier_Eps_in[OF Y  carrier_direct_lim›] unfolding y_def by auto

  have "add_rel X Y = z, add_str z (ρ (fst x) z (snd x)) (ρ (fst y) z (snd y))"
    unfolding add_rel_def Let_def
    by (fold x_def y_def z_def,rule)
  also have "...  carrier_direct_lim"
    unfolding carrier_direct_lim_def class_of_def
  proof (rule rel.Block_closed)
    have "zI" using xSigma I 𝔉 ySigma I 𝔉 unfolding z_def by auto
    then interpret ring "(𝔉 z)" "+z" "⋅z" "𝟬z" "𝟭z"
      using is_ring_from_is_homomorphism subset_of_opens by auto
    show "(z, +z (ρ (fst x) z (snd x)) (ρ (fst y) z (snd y)))  Sigma I 𝔉"
      using zI
      apply simp
      by (metis x  Sigma I 𝔉 y  Sigma I 𝔉 additive.composition_closed
          direct_lim.subset_of_opens direct_lim_axioms get_lower_bound(2) get_lower_bound(3)
          is_map_from_is_homomorphism map.map_closed mem_Sigma_iff prod.exhaust_sel z_def)
  qed
  finally show ?thesis .
qed


lemma rel_eventually_llbound:
  assumes "x  y"
  shows "F w in llbound. ρ (fst x) w (snd x) = ρ (fst y) w (snd y)"
proof -
  have xy:"fst x  I" "fst y  I" "snd x  𝔉 (fst x)" "snd y  𝔉 (fst y)"
    using x  y unfolding rel_def by auto
  obtain w0 where w0:"w0  I" "w0  fst x  fst y" "ρ (fst x) w0 (snd x) = ρ (fst y) w0 (snd y)"
    using x  y unfolding rel_def by auto

  interpret xw0:ring_homomorphism "ρ (fst x) w0" "𝔉 (fst x)" "+fst x" "⋅fst x" "𝟬fst x"
        "𝟭fst x" "𝔉 w0" "+w0" "⋅w0" "𝟬w0" "𝟭w0"
    by (meson is_ring_morphism le_inf_iff subset_of_opens w0 xy(1))
  interpret yw0:ring_homomorphism "ρ (fst y) w0" "𝔉 (fst y)" "+fst y" "⋅fst y" "𝟬fst y"
        "𝟭fst y" "𝔉 w0" "+w0" "⋅w0" "𝟬w0" "𝟭w0"
    using w0 by (metis is_ring_morphism le_inf_iff subset_of_opens  xy(2))
  have "ρ (fst x) w (snd x) = ρ (fst y) w (snd y)" if "w  w0" "w  I" for w
  proof -
    interpret w0w:ring_homomorphism "ρ w0 w" "𝔉 w0" "+w0" "⋅w0" "𝟬w0" "𝟭w0" "𝔉 w"
                  "+w" "⋅w" "𝟬w" "𝟭w"
      using is_ring_morphism subset_of_opens that w0(1) by presburger

    have "ρ (fst x) w (snd x) = (ρ w0 w  ρ (fst x) w0) (snd x)"
      by (meson assoc_comp le_inf_iff subset_of_opens that w0 xy)
    also have "... = (ρ w0 w  ρ (fst y) w0) (snd y)"
      unfolding comp_def
      using w0(3) by auto
    also have "... = ρ (fst y) w (snd y)"
      using w0 xy by (metis Int_subset_iff assoc_comp subset_of_opens that)
    finally show ?thesis .
  qed
  with w0 have "w0. w0  I  w0  fst x  fst y
             (w. (ww0  wI)  ρ (fst x) w (snd x) = ρ (fst y) w (snd y))"
    by auto
  then have "F w in lbound {fst x,fst y}. ρ (fst x) w (snd x) = ρ (fst y) w (snd y)"
    apply (subst eventually_lbound_finite)
    using xy(1,2) by auto
  then show ?thesis
    using llbound_lbound[of "{fst x,fst y}"] xy(1,2) by auto
qed

lemma
  fixes x y:: "'a set × 'b" and z z':: "'a set"
  assumes xy:"x  Sigma I 𝔉" "y  Sigma I 𝔉"
  assumes z:"zI" "z  fst x" "z  fst y"
  assumes z':"z'I" "z'  fst x" "z'  fst y"
  shows add_rel_well_defined:"z, add_str z (ρ (fst x) z (snd x)) (ρ (fst y) z (snd y)) =
          z', add_str z' (ρ (fst x) z' (snd x)) (ρ (fst y) z' (snd y))" (is "?add")
    and mult_rel_well_defined:
        "z, mult_str z (ρ (fst x) z (snd x)) (ρ (fst y) z (snd y)) =
         z', mult_str z' (ρ (fst x) z' (snd x)) (ρ (fst y) z' (snd y))" (is "?mult")
proof -
  interpret xz:ring_homomorphism "(ρ (fst x) z)" "(𝔉 (fst x))"
              "+fst x" "⋅fst x" "𝟬fst x" "𝟭fst x" "(𝔉 z)" "+z" "⋅z" "𝟬z" "𝟭z"
    using is_ring_morphism x  Sigma I 𝔉 z subset_of_opens by force
  interpret yz:ring_homomorphism "(ρ (fst y) z)" "(𝔉 (fst y))"
              "+fst y" "⋅fst y" "𝟬fst y" "𝟭fst y" "(𝔉 z)" "+z" "⋅z" "𝟬z" "𝟭z"
    using is_ring_morphism y  Sigma I 𝔉 z subset_of_opens by force
  interpret xz':ring_homomorphism "(ρ (fst x) z')" "(𝔉 (fst x))"
              "+fst x" "⋅fst x" "𝟬fst x" "𝟭fst x" "(𝔉 z')" "+z'" "⋅z'" "𝟬z'" "𝟭z'"
    using is_ring_morphism x  Sigma I 𝔉 z' subset_of_opens by force
  interpret yz':ring_homomorphism "(ρ (fst y) z')" "(𝔉 (fst y))"
              "+fst y" "⋅fst y" "𝟬fst y" "𝟭fst y" "(𝔉 z')" "+z'" "⋅z'" "𝟬z'" "𝟭z'"
    using is_ring_morphism y  Sigma I 𝔉 z' subset_of_opens by force

  obtain w where w:"w  I" "w  z  z'"
    using has_lower_bound zI z'I by meson

  interpret zw:ring_homomorphism "ρ z w" "(𝔉 z)" "+z" "⋅z" "𝟬z" "𝟭z"
      "𝔉 w" "+w" "⋅w" "𝟬w" "𝟭w"
    using w by (meson is_ring_morphism le_inf_iff subset_of_opens z(1))
  interpret z'w:ring_homomorphism "ρ z' w" "(𝔉 z')" "+z'" "⋅z'" "𝟬z'" "𝟭z'"
      "𝔉 w" "+w" "⋅w" "𝟬w" "𝟭w"
    using w  I w  z  z' z' by (meson is_ring_morphism le_inf_iff subset_of_opens)

  show ?add
  proof (rule class_of_eqI[OF _ _ w  I w  z  z'])
    define xz yz where "xz = ρ (fst x) z (snd x)" and "yz = ρ (fst y) z (snd y)"
    define xz' yz' where "xz' = ρ (fst x) z' (snd x)" and "yz' = ρ (fst y) z' (snd y)"
    show "(z, +z xz yz)  Sigma I 𝔉" "(z', +z' xz' yz')  Sigma I 𝔉"
      subgoal using assms(1) assms(2) xz_def yz_def z(1) by fastforce
      subgoal using assms(1) assms(2) xz'_def yz'_def z'(1) by fastforce
      done
    have "ρ z w (+z xz yz) = +w (ρ z w xz) (ρ z w yz)"
      apply (rule zw.additive.commutes_with_composition)
      using assms(1,2) xz_def yz_def by force+
    also have "... = +w (ρ (fst x) w (snd x)) (ρ (fst y) w (snd y))"
      unfolding xz_def yz_def
      using assoc_comp w z subset_of_opens assms
      by (metis SigmaE le_inf_iff o_def prod.sel)
    also have "... = +w (ρ z' w xz') (ρ z' w yz')"
      unfolding xz'_def yz'_def
      using assoc_comp  w z' subset_of_opens assms
      by (metis SigmaE le_inf_iff o_def prod.sel)
    also have "... = ρ z' w (+z' xz' yz')"
      using assms(2) xy(1) xz'_def yz'_def z'w.additive.commutes_with_composition by force
    finally show "ρ z w (+z xz yz) = ρ z' w (+z' xz' yz')" .
  qed

  show ?mult
  proof (rule class_of_eqI[OF _ _ w  I w  z  z'])
    define xz yz where "xz = ρ (fst x) z (snd x)" and "yz = ρ (fst y) z (snd y)"
    define xz' yz' where "xz' = ρ (fst x) z' (snd x)" and "yz' = ρ (fst y) z' (snd y)"
    show "(z,z xz yz)  Sigma I 𝔉" "(z',z' xz' yz')  Sigma I 𝔉"
      unfolding xz_def yz_def xz'_def yz'_def
      using assms by auto
    have "ρ z w (z xz yz) =w (ρ z w xz) (ρ z w yz)"
      apply (rule zw.multiplicative.commutes_with_composition)
      using xy xz_def yz_def by force+
    also have "... =w (ρ (fst x) w (snd x)) (ρ (fst y) w (snd y))"
      unfolding xz_def yz_def
      using xy w z assoc_comp
      by (metis SigmaE fst_conv le_inf_iff o_def snd_conv subset_of_opens)
    also have "... =w (ρ z' w xz') (ρ z' w yz')"
      unfolding xz'_def yz'_def
      using xy w z' assoc_comp
      by (metis SigmaE fst_conv le_inf_iff o_def snd_conv subset_of_opens)
    also have "... = ρ z' w (z' xz' yz')"
      unfolding xz'_def yz'_def
      using monoid_homomorphism.commutes_with_composition xy z'w.multiplicative.monoid_homomorphism_axioms by fastforce
    finally show "ρ z w (z xz yz) = ρ z' w (z' xz' yz')" .
  qed
qed

lemma add_rel_well_defined_llbound:
  fixes x y:: "'a set × 'b" and z z':: "'a set"
  assumes "x  Sigma I 𝔉" "y  Sigma I 𝔉"
  assumes z:"zI" "z  fst x" "z  fst y"
  shows "F w in llbound. z, add_str z (ρ (fst x) z (snd x)) (ρ (fst y) z (snd y)) =
          w, add_str w (ρ (fst x) w (snd x)) (ρ (fst y) w (snd y))" (is "F w in _. ?P w")
proof -
  have  "w. w  z  w  I ?P w "
    by (meson add_rel_well_defined assms(1) assms(2) dual_order.trans z(1) z(2) z(3))
  then have "F w in lbound {fst x,fst y}. ?P w"
    apply (subst eventually_lbound_finite)
    using assms by auto
  then show ?thesis
    using llbound_lbound[of "{fst x,fst y}"] assms(1,2) by auto
qed

lemma mult_rel_well_defined_llbound:
  fixes x y:: "'a set × 'b" and z z':: "'a set"
  assumes "x  Sigma I 𝔉" "y  Sigma I 𝔉"
  assumes z:"zI" "z  fst x" "z  fst y"
  shows "F w in llbound. z, mult_str z (ρ (fst x) z (snd x)) (ρ (fst y) z (snd y)) =
          w, mult_str w (ρ (fst x) w (snd x)) (ρ (fst y) w (snd y))" (is "F w in _. ?P w")
proof -
  have  "w. w  z  w  I ?P w "
    by (meson mult_rel_well_defined assms(1) assms(2) dual_order.trans z(1) z(2) z(3))
  then have "F w in lbound {fst x,fst y}. ?P w"
    apply (subst eventually_lbound_finite)
    using assms by auto
  then show ?thesis
    using llbound_lbound[of "{fst x,fst y}"] assms(1,2) by auto
qed

lemma add_rel_class_of:
  fixes U V W :: "'a set" and x y :: 'b
  assumes uv_sigma:"(U, x)  Sigma I 𝔉" "(V, y)  Sigma I 𝔉"
  assumes w:"W  I" "W  U" "W  V"
  shows "add_rel U, x V, y = W, +W (ρ U W x) (ρ V W y)"
proof -
  define ux where "ux = (SOME ux. ux  U, x)"
  define vy where "vy = (SOME ux. ux  V, y)"
  have "ux  U, x" "vy  V, y "
    unfolding ux_def vy_def using uv_sigma class_of_def some_in_eq by blast+
  then have "ux  Sigma I 𝔉" "vy  Sigma I 𝔉"
    using class_of_def uv_sigma by blast+
  then have "fst ux  I" "fst vy  I" by auto

  define w1 where "w1 = get_lower_bound (fst ux) (fst vy)"
  have w1:"w1  I" "w1  fst ux" "w1  fst vy"
    using get_lower_bound[OF ‹fst ux  I ‹fst vy  I] unfolding w1_def by auto

  have "add_rel U, x V, y = w1, +w1 (ρ (fst ux) w1 (snd ux)) (ρ (fst vy) w1 (snd vy))"
    unfolding add_rel_def
    apply (fold ux_def vy_def)
    by (simp add:Let_def w1_def)
  moreover have "F w in llbound.
            ... = w, add_str w (ρ (fst ux) w (snd ux)) (ρ (fst vy) w (snd vy))"
    apply (rule add_rel_well_defined_llbound)
    using ux  Sigma I 𝔉 vy  Sigma I 𝔉 w1 by auto
  ultimately have "F w in llbound. add_rel U, x V, y
      = w, add_str w (ρ (fst ux) w (snd ux)) (ρ (fst vy) w (snd vy))"
    by simp
  moreover have
    "F w in llbound. ρ (fst ux) w (snd ux) = ρ (fst (U, x)) w (snd (U, x))"
    "F w in llbound. ρ (fst vy) w (snd vy) = ρ (fst (V, y)) w (snd (V, y))"
    subgoal
      apply (rule rel_eventually_llbound)
      using ux  U, x class_of_def uv_sigma(1) by auto
    subgoal
      apply (rule rel_eventually_llbound)
      using vy  V, y class_of_def uv_sigma(2) by auto
    done
  ultimately have "F w in llbound. add_rel U, x V, y
      = w, add_str w (ρ U w x) (ρ V w y)"
    apply eventually_elim
    by auto
  moreover have "F w in llbound. W, +W (ρ U W x) (ρ V W y) = w, +w (ρ U w x) (ρ V w y)"
    apply (rule add_rel_well_defined_llbound[of "(U,x)" "(V,y)" W,simplified])
    using w uv_sigma by auto
  ultimately have "F w in llbound.
      add_rel U, x V, y = W, +W (ρ U W x) (ρ V W y)"
    apply eventually_elim
    by auto
  moreover have "llboundbot" using llbound_not_bot w(1) by blast
  ultimately show ?thesis by auto
qed

lemma mult_rel_class_of:
  fixes U V W :: "'a set" and x y :: 'b
  assumes uv_sigma:"(U, x)  Sigma I 𝔉" "(V, y)  Sigma I 𝔉"
  assumes w:"W  I" "W  U" "W  V"
  shows "mult_rel U, x V, y = W,W (ρ U W x) (ρ V W y)"
proof -
  define ux where "ux = (SOME ux. ux  U, x)"
  define vy where "vy = (SOME ux. ux  V, y)"
  have "ux  U, x" "vy  V, y "
    unfolding ux_def vy_def using uv_sigma class_of_def some_in_eq by blast+
  then have "ux  Sigma I 𝔉" "vy  Sigma I 𝔉"
    using class_of_def uv_sigma by blast+
  then have "fst ux  I" "fst vy  I" by auto

  define w1 where "w1 = get_lower_bound (fst ux) (fst vy)"
  have w1:"w1  I" "w1  fst ux" "w1  fst vy"
    using get_lower_bound[OF ‹fst ux  I ‹fst vy  I] unfolding w1_def by auto

  have "mult_rel U, x V, y = w1,w1 (ρ (fst ux) w1 (snd ux)) (ρ (fst vy) w1 (snd vy))"
    unfolding mult_rel_def
    apply (fold ux_def vy_def)
    by (simp add:Let_def w1_def)
  moreover have "F w in llbound.
            ... = w, mult_str w (ρ (fst ux) w (snd ux)) (ρ (fst vy) w (snd vy))"
    apply (rule mult_rel_well_defined_llbound)
    using ux  Sigma I 𝔉 vy  Sigma I 𝔉 w1 by auto
  ultimately have "F w in llbound. mult_rel U, x V, y
      = w, mult_str w (ρ (fst ux) w (snd ux)) (ρ (fst vy) w (snd vy))"
    by simp
  moreover have
    "F w in llbound. ρ (fst ux) w (snd ux) = ρ (fst (U, x)) w (snd (U, x))"
    "F w in llbound. ρ (fst vy) w (snd vy) = ρ (fst (V, y)) w (snd (V, y))"
    subgoal
      apply (rule rel_eventually_llbound)
      using ux  U, x class_of_def uv_sigma(1) by auto
    subgoal
      apply (rule rel_eventually_llbound)
      using vy  V, y class_of_def uv_sigma(2) by auto
    done
  ultimately have "F w in llbound. mult_rel U, x V, y
      = w, mult_str w (ρ U w x) (ρ V w y)"
    apply eventually_elim
    by auto
  moreover have "F w in llbound. W,W (ρ U W x) (ρ V W y) = w,w (ρ U w x) (ρ V w y)"
    apply (rule mult_rel_well_defined_llbound[of "(U,x)" "(V,y)" W,simplified])
    using w uv_sigma by auto
  ultimately have "F w in llbound.
      mult_rel U, x V, y = W,W (ρ U W x) (ρ V W y)"
    apply eventually_elim
    by auto
  moreover have "llboundbot" using llbound_not_bot w(1) by blast
  ultimately show ?thesis by auto
qed

lemma mult_rel_carrier[intro]