# Theory Set_Extras

text ‹Authors: Anthony Bordg and Lawrence Paulson›

theory Set_Extras
imports "Jacobson_Basic_Algebra.Set_Theory"

begin

text ‹Some new notation for built-in primitives›

section ‹Sets›

abbreviation complement_in_of:: "'a set ⇒ 'a set ⇒ 'a set" ("_∖_" [65,65]65)
where "A ∖ B ≡ A-B"

section ‹Functions›

abbreviation preimage:: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ 'a set" ("_ ⇧¯ _ _" [90,90,1000]90)
where "f⇧¯ X V ≡ (vimage f V) ∩ X"

lemma preimage_of_inter:
fixes f::"'a ⇒ 'b" and X::"'a set" and V::"'b set" and V'::"'b set"
shows "f⇧¯ X (V ∩ V') = (f⇧¯ X V) ∩ (f⇧¯ X V')"
by blast

lemma preimage_identity_self: "identity A ⇧¯ A B = B ∩ A"

text ‹Simplification actually replaces the RHS by the LHS›
lemma preimage_vimage_eq: "(f ⇧¯ (f - U') U) ∩ X = f⇧¯ X (U ∩ U')"
by simp

definition inverse_map:: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ ('b ⇒ 'a)"
where "inverse_map f S T ≡ restrict (inv_into S f) T"

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

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

abbreviation composing ("_ ∘ _ ↓ _" [60,0,60]59)
where "g ∘ f ↓ D ≡ compose D g f"

lemma comp_maps:
assumes "Set_Theory.map η A B" and "Set_Theory.map θ B C"
shows "Set_Theory.map (θ ∘ η ↓ A) A C"
proof-
have "(θ ∘ η ↓ A) ∈ A →⇩E C"
using assms by (metis Int_iff PiE_def compose_def funcset_compose map.graph restrict_extensional)
thus ?thesis by (simp add: Set_Theory.map_def)
qed

lemma undefined_is_map_on_empty:
fixes f:: "'a set ⇒ 'b set"
assumes "f = (λx. undefined)"
shows "map f {} {}"
using assms by (simp add: map.intro)

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

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

lemma map_eq:
assumes "map f S T" and "map g S T" and "⋀x. x ∈ S ⟹ f x = g x"
shows "f = g"
using assms by (metis restrict_ext restrict_on_source)

lemma image_subset_of_target:
assumes "map f S T"
shows "f  S ⊆ T"
using assms by (meson image_subsetI map.map_closed)

end


# Theory Group_Extras

text ‹Authors: Anthony Bordg and Lawrence Paulson›

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

begin

section ‹Fold operator with a subdomain›

inductive_set
foldSetD :: "['a set, 'b ⇒ 'a ⇒ 'a, 'a] ⇒ ('b set * 'a) set"
for D :: "'a set" and f :: "'b ⇒ 'a ⇒ 'a" and e :: 'a
where
emptyI [intro]: "e ∈ D ⟹ ({}, e) ∈ foldSetD D f e"
| insertI [intro]: "⟦x ∉ A; f x y ∈ D; (A, y) ∈ foldSetD D f e⟧ ⟹
(insert x A, f x y) ∈ foldSetD D f e"

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

definition
foldD :: "['a set, 'b ⇒ 'a ⇒ 'a, 'a, 'b set] ⇒ 'a"
where "foldD D f e A = (THE x. (A, x) ∈ foldSetD D f e)"

lemma foldSetD_closed: "(A, z) ∈ foldSetD D f e ⟹ z ∈ D"
by (erule foldSetD.cases) auto

lemma Diff1_foldSetD:
"⟦(A - {x}, y) ∈ foldSetD D f e; x ∈ A; f x y ∈ D⟧ ⟹
(A, f x y) ∈ foldSetD D f e"
by (metis Diff_insert_absorb foldSetD.insertI mk_disjoint_insert)

lemma foldSetD_imp_finite [simp]: "(A, x) ∈ foldSetD D f e ⟹ finite A"
by (induct set: foldSetD) auto

lemma finite_imp_foldSetD:
"⟦finite A; e ∈ D; ⋀x y. ⟦x ∈ A; y ∈ D⟧ ⟹ f x y ∈ D⟧
⟹ ∃x. (A, x) ∈ foldSetD D f e"
proof (induct set: finite)
case empty then show ?case by auto
next
case (insert x F)
then obtain y where y: "(F, y) ∈ foldSetD D f e" by auto
with insert have "y ∈ D" by (auto dest: foldSetD_closed)
with y and insert have "(insert x F, f x y) ∈ foldSetD D f e"
by (intro foldSetD.intros) auto
then show ?case ..
qed

lemma foldSetD_backwards:
assumes "A ≠ {}" "(A, z) ∈ foldSetD D f e"
shows "∃x y. x ∈ A ∧ (A - { x }, y) ∈ foldSetD D f e ∧ z = f x y"
using assms(2) by (cases) (simp add: assms(1), metis Diff_insert_absorb insertI1)

subsection ‹Left-Commutative Operations›

locale LCD =
fixes B :: "'b set"
and D :: "'a set"
and f :: "'b ⇒ 'a ⇒ 'a"    (infixl "⋅" 70)
assumes left_commute:
"⟦x ∈ B; y ∈ B; z ∈ D⟧ ⟹ x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
and f_closed [simp, intro!]: "!!x y. ⟦x ∈ B; y ∈ D⟧ ⟹ f x y ∈ D"

lemma (in LCD) foldSetD_closed [dest]: "(A, z) ∈ foldSetD D f e ⟹ z ∈ D"
by (erule foldSetD.cases) auto

lemma (in LCD) Diff1_foldSetD:
"⟦(A - {x}, y) ∈ foldSetD D f e; x ∈ A; A ⊆ B⟧ ⟹
(A, f x y) ∈ foldSetD D f e"
by (meson Diff1_foldSetD f_closed local.foldSetD_closed subsetCE)

lemma (in LCD) finite_imp_foldSetD:
"⟦finite A; A ⊆ B; e ∈ D⟧ ⟹ ∃x. (A, x) ∈ foldSetD D f e"
proof (induct set: finite)
case empty then show ?case by auto
next
case (insert x F)
then obtain y where y: "(F, y) ∈ foldSetD D f e" by auto
with insert have "y ∈ D" by auto
with y and insert have "(insert x F, f x y) ∈ foldSetD D f e"
by (intro foldSetD.intros) auto
then show ?case ..
qed

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

lemma (in LCD) foldSetD_determ:
"⟦(A, x) ∈ foldSetD D f e; (A, y) ∈ foldSetD D f e; e ∈ D; A ⊆ B⟧
⟹ y = x"
by (blast intro: foldSetD_determ_aux [rule_format])

lemma (in LCD) foldD_equality:
"⟦(A, y) ∈ foldSetD D f e; e ∈ D; A ⊆ B⟧ ⟹ foldD D f e A = y"
by (unfold foldD_def) (blast intro: foldSetD_determ)

lemma foldD_empty [simp]:
"e ∈ D ⟹ foldD D f e {} = e"
by (unfold foldD_def) blast

lemma (in LCD) foldD_insert_aux:
"⟦x ∉ A; x ∈ B; e ∈ D; A ⊆ B⟧
⟹ ((insert x A, v) ∈ foldSetD D f e) ⟷ (∃y. (A, y) ∈ foldSetD D f e ∧ v = f x y)"
apply auto
by (metis Diff_insert_absorb f_closed finite_Diff foldSetD.insertI foldSetD_determ foldSetD_imp_finite insert_subset local.finite_imp_foldSetD local.foldSetD_closed)

lemma (in LCD) foldD_insert:
assumes "finite A" "x ∉ A" "x ∈ B" "e ∈ D" "A ⊆ B"
shows "foldD D f e (insert x A) = f x (foldD D f e A)"
proof -
have "(THE v. ∃y. (A, y) ∈ foldSetD D (⋅) e ∧ v = x ⋅ y) = x ⋅ (THE y. (A, y) ∈ foldSetD D (⋅) e)"
by (rule the_equality) (use assms foldD_def foldD_equality foldD_def finite_imp_foldSetD in ‹metis+›)
then show ?thesis
unfolding foldD_def using assms by (simp add: foldD_insert_aux)
qed

lemma (in LCD) foldD_closed [simp]:
"⟦finite A; e ∈ D; A ⊆ B⟧ ⟹ foldD D f e A ∈ D"
proof (induct set: finite)
case empty then show ?case by simp
next
case insert then show ?case by (simp add: foldD_insert)
qed

lemma (in LCD) foldD_commute:
"⟦finite A; x ∈ B; e ∈ D; A ⊆ B⟧ ⟹
f x (foldD D f e A) = foldD D f (f x e) A"
by (induct set: finite) (auto simp add: left_commute foldD_insert)

lemma Int_mono2:
"⟦A ⊆ C; B ⊆ C⟧ ⟹ A Int B ⊆ C"
by blast

lemma (in LCD) foldD_nest_Un_Int:
"⟦finite A; finite C; e ∈ D; A ⊆ B; C ⊆ B⟧ ⟹
foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
proof (induction set: finite)
case (insert x F)
then show ?case
by (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb Int_mono2)
qed simp

lemma (in LCD) foldD_nest_Un_disjoint:
"⟦finite A; finite B; A Int B = {}; e ∈ D; A ⊆ B; C ⊆ B⟧
⟹ foldD D f e (A Un B) = foldD D f (foldD D f e B) A"

― ‹Delete rules to do with ‹foldSetD› relation.›

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

section ‹Monoids›

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

text ‹Commutative Monoids›

text ‹
We enter a more restrictive context, with ‹f :: 'a ⇒ 'a ⇒ 'a›
instead of ‹'b ⇒ 'a ⇒ 'a›.
›

locale ACeD =
fixes D :: "'a set"
and f :: "'a ⇒ 'a ⇒ 'a"    (infixl "⋅" 70)
and e :: 'a
assumes ident [simp]: "x ∈ D ⟹ x ⋅ e = x"
and commute: "⟦x ∈ D; y ∈ D⟧ ⟹ x ⋅ y = y ⋅ x"
and assoc: "⟦x ∈ D; y ∈ D; z ∈ D⟧ ⟹ (x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
and e_closed [simp]: "e ∈ D"
and f_closed [simp]: "⟦x ∈ D; y ∈ D⟧ ⟹ x ⋅ y ∈ D"

lemma (in ACeD) left_commute:
"⟦x ∈ D; y ∈ D; z ∈ D⟧ ⟹ x ⋅ (y ⋅ z) = y ⋅ (x ⋅ z)"
proof -
assume D: "x ∈ D" "y ∈ D" "z ∈ D"
then have "x ⋅ (y ⋅ z) = (y ⋅ z) ⋅ x" by (simp add: commute)
also from D have "... = y ⋅ (z ⋅ x)" by (simp add: assoc)
also from D have "z ⋅ x = x ⋅ z" by (simp add: commute)
finally show ?thesis .
qed

lemmas (in ACeD) AC = assoc commute left_commute

lemma (in ACeD) left_ident [simp]: "x ∈ D ⟹ e ⋅ x = x"
proof -
assume "x ∈ D"
then have "x ⋅ e = x" by (rule ident)
with ‹x ∈ D› show ?thesis by (simp add: commute)
qed

lemma (in ACeD) foldD_Un_Int:
"⟦finite A; finite B; A ⊆ D; B ⊆ D⟧ ⟹
foldD D f e A ⋅ foldD D f e B =
foldD D f e (A Un B) ⋅ foldD D f e (A Int B)"
proof (induction set: finite)
case empty
then show ?case
by(simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]])
next
case (insert x F)
then show ?case
by(simp add: AC insert_absorb Int_insert_left Int_mono2
LCD.foldD_insert [OF LCD.intro [of D]]
LCD.foldD_closed [OF LCD.intro [of D]])
qed

lemma (in ACeD) foldD_Un_disjoint:
"⟦finite A; finite B; A Int B = {}; A ⊆ D; B ⊆ D⟧ ⟹
foldD D f e (A Un B) = foldD D f e A ⋅ foldD D f e B"
left_commute LCD.foldD_closed [OF LCD.intro [of D]])

subsection ‹Finite Products›

context monoid
begin

definition finprod:: "'b set => ('b => 'a) ⇒ 'a"
where "finprod I f ≡ if finite I then foldD M (composition ∘ f) 𝟭 I else 𝟭"

end (* monoid *)

section ‹Groups›

lemma comp_group_morphisms:
assumes "group_homomorphism η A multA oneA B multB oneB" and
"group_homomorphism θ B multB oneB C multC oneC"
shows "group_homomorphism (θ ∘ η ↓ A) A multA oneA C multC oneC"
using assms group_homomorphism_def comp_monoid_morphisms by metis

subsection ‹Subgroup Generated by a Subset›

context group
begin

inductive_set generate :: "'a set ⇒ 'a set"
for H where
unit:  "𝟭 ∈ generate H"
| incl: "a ∈ H ⟹ a ∈ generate H"
| inv:  "a ∈ H ⟹ inverse a ∈ generate H"
| mult:  "a ∈ generate H ⟹ b ∈ generate H ⟹ a ⋅ b ∈ generate H"

lemma generate_into_G: "a ∈ generate (G ∩ H) ⟹ a ∈ G"
by (induction rule: generate.induct) auto

definition subgroup_generated :: "'a set ⇒ 'a set"
where "subgroup_generated S = generate (G ∩ S)"

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

lemma subgroup_generated_is_monoid:
fixes H
shows "Group_Theory.monoid (subgroup_generated H) (⋅) 𝟭"
unfolding subgroup_generated_def
proof qed (auto simp: generate.unit generate.mult associative generate_into_G)

lemma subgroup_generated_is_subset:
fixes H
shows "subgroup_generated H ⊆ G"
using generate_into_G subgroup_generated_def by blast

lemma subgroup_generated_is_subgroup:
fixes H
shows "subgroup (subgroup_generated H) G (⋅) 𝟭"
proof
show "subgroup_generated H ⊆ G"
show "a ⋅ b ∈ subgroup_generated H"
if "a ∈ subgroup_generated H" "b ∈ subgroup_generated H" for a b
using that by (meson monoid.composition_closed subgroup_generated_is_monoid)
show "a ⋅ b ⋅ c = a ⋅ (b ⋅ c)"
if "a ∈ subgroup_generated H" "b ∈ subgroup_generated H" "c ∈ subgroup_generated H"
for a b c
using that by (meson monoid.associative subgroup_generated_is_monoid)
show "monoid.invertible (subgroup_generated H) (⋅) 𝟭 u"
if "u ∈ subgroup_generated H" for u
proof (rule monoid.invertibleI )
show "Group_Theory.monoid (subgroup_generated H) (⋅) 𝟭"
show "u ⋅ local.inverse u = 𝟭" "local.inverse u ⋅ u = 𝟭" "u ∈ subgroup_generated H"
using ‹subgroup_generated H ⊆ G› that by auto
show "local.inverse u ∈ subgroup_generated H"
using inverse_in_subgroup_generated that by blast
qed
qed (auto simp: generate_into_G generate.unit subgroup_generated_def)

end (* group *)

section ‹Abelian Groups›

context abelian_group
begin

definition minus:: "'a ⇒ 'a ⇒ 'a" (infixl "‐" 70)
where "x ‐ y ≡ x ⋅ inverse y "

definition finsum:: "'b set ⇒ ('b ⇒ 'a) ⇒ 'a"
where "finsum I f ≡ finprod I f"

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

end (* abelian_group*)

end


# Theory Topological_Space

text ‹Authors: Anthony Bordg and Lawrence Paulson,
with some contributions from Wenda Li›

theory Topological_Space
imports Complex_Main
"Jacobson_Basic_Algebra.Set_Theory"
Set_Extras

begin

section ‹Topological Spaces›

locale topological_space = fixes S :: "'a set" and is_open :: "'a set ⇒ bool"
assumes open_space [simp, intro]: "is_open S" and open_empty [simp, intro]: "is_open {}"
and open_imp_subset: "is_open U ⟹ U ⊆ S"
and open_inter [intro]: "⟦is_open U; is_open V⟧ ⟹ is_open (U ∩ V)"
and open_union [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃x∈F. x)"

begin

definition is_closed :: "'a set ⇒ bool"
where "is_closed U ≡ U ⊆ S ∧ is_open (S - U)"

definition neighborhoods:: "'a ⇒ ('a set) set"
where "neighborhoods x ≡ {U. is_open U ∧ x ∈ U}"

text ‹Note that by a neighborhood we mean what some authors call an open neighborhood.›

lemma open_union' [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃F)"
using open_union by auto

lemma open_preimage_identity [simp]: "is_open B ⟹ identity S ⇧¯ S B = B"
by (metis inf.orderE open_imp_subset preimage_identity_self)

definition is_connected:: "bool" where
"is_connected ≡ ¬ (∃U V. is_open U ∧ is_open V ∧ (U ≠ {}) ∧ (V ≠ {}) ∧ (U ∩ V = {}) ∧ (U ∪ V = S))"

definition is_hausdorff:: "bool" where
"is_hausdorff ≡
∀x y. (x ∈ S ∧ y ∈ S ∧ x ≠ y) ⟶ (∃U V. U ∈ neighborhoods x ∧ V ∈ neighborhoods y ∧ U ∩ V = {})"

end (* topological_space *)

text ‹T2 spaces are also known as Hausdorff spaces.›

locale t2_space = topological_space +
assumes hausdorff: "is_hausdorff"

subsection ‹Topological Basis›

inductive generated_topology :: "'a set ⇒ 'a set set ⇒ 'a set ⇒ bool"
for S :: "'a set" and B :: "'a set set"
where
UNIV: "generated_topology S B S"
| Int: "generated_topology S B (U ∩ V)"
if "generated_topology S B U" and "generated_topology S B V"
| UN: "generated_topology S B (⋃K)" if "(⋀U. U ∈ K ⟹ generated_topology S B U)"
| Basis: "generated_topology S B b" if "b ∈ B ∧ b ⊆ S"

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

lemma generated_topology_subset: "generated_topology S B U ⟹ U ⊆ S"
by (induct rule:generated_topology.induct) auto

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

subsection ‹Covers›

locale cover_of_subset =
fixes X:: "'a set" and U:: "'a set" and index:: "real set" and cover:: "real ⇒ 'a set"
(* We use real instead of index::"'b set" otherwise we get some troubles with locale sheaf_of_rings
in Comm_Ring_Theory.thy *)
assumes is_subset: "U ⊆ X" and are_subsets: "⋀i. i ∈ index ⟹ cover i ⊆ X"
and covering: "U ⊆ (⋃i∈index. cover i)"
begin

lemma
assumes "x ∈ U"
shows "∃i∈index. x ∈ cover i"
using assms covering by auto

definition select_index:: "'a ⇒ real"
where "select_index x ≡ SOME i. i ∈ index ∧ x ∈ cover i"

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

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

end (* cover_of_subset *)

locale open_cover_of_subset = topological_space X is_open + cover_of_subset X U I C
for X and is_open and U and I and C +
assumes are_open_subspaces: "⋀i. i∈I ⟹ is_open (C i)"
begin

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

end (* open_cover_of_subset *)

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

subsection ‹Induced Topology›

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

definition ind_is_open:: "'a set ⇒ bool"
where "ind_is_open U ≡ U ⊆ S ∧ (∃V. V ⊆ X ∧ is_open V ∧ U = S ∩ V)"

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

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

lemma ind_space_is_top_space:
shows "topological_space S (ind_is_open)"
proof
fix U V
assume "ind_is_open U" then obtain UX where "UX ⊆ X" "is_open UX" "U = S ∩ UX"
using ind_is_open_def by auto
moreover
assume "ind_is_open V" then obtain VX where "VX ⊆ X" "is_open VX" "V = S ∩ VX"
using ind_is_open_def by auto
ultimately have "is_open (UX ∩ VX) ∧ (U ∩ V = S ∩ (UX ∩ VX))" using open_inter by auto
then show "ind_is_open (U ∩ V)"
by (metis ‹UX ⊆ X› ind_is_open_def le_infI1 subset_refl)
next
fix F
assume F: "⋀x. x ∈ F ⟹ ind_is_open x"
obtain F' where F': "⋀x. x ∈ F ∧ ind_is_open x ⟹ is_open (F' x) ∧ x = S ∩ (F' x)"
using ind_is_open_def by metis
have "is_open (⋃ (F'  F))"
by (metis (mono_tags, lifting) F F' imageE image_ident open_union)
moreover
have "(⋃x∈F. x) = S ∩ ⋃ (F'  F)"
using F' ‹⋀x. x ∈ F ⟹ ind_is_open x› by fastforce
ultimately show "ind_is_open (⋃x∈F. x)"
by (metis ind_is_open_def inf_sup_ord(1) open_imp_subset)
next
show "⋀U. ind_is_open U ⟹ U ⊆ S"
qed auto

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

lemma open_cover_from_ind_open_cover:
assumes "is_open S" and "open_cover_of_open_subset S ind_is_open U I C"
shows "open_cover_of_open_subset X is_open U I C"
proof
show "is_open U"
using assms is_open_from_ind_is_open open_cover_of_open_subset.is_open_subset by blast
show "⋀i. i ∈ I ⟹ is_open (C i)"
using assms is_open_from_ind_is_open open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces by blast
show "⋀i. i ∈ I ⟹ C i ⊆ X"
using assms(2) is_subset
by (meson cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def subset_trans)
show "U ⊆ X"
by (simp add: ‹is_open U› open_imp_subset)
show "U ⊆ ⋃ (C  I)"
by (meson assms(2) cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
qed

end (* induced topology *)

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

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

lemma (in topological_space) ind_is_open_iff_open:
shows "ind_topology.ind_is_open S is_open S U ⟷ is_open U ∧ U ⊆ S"
by (metis ind_topology.ind_is_open_def ind_topology_is_open_self inf.absorb_iff2)

subsection ‹Continuous Maps›

locale continuous_map = source: topological_space S is_open + target: topological_space S' is_open'
+ map f S S'
for S and is_open and S' and is_open' and f +
assumes is_continuous: "⋀U. is_open' U ⟹ is_open (f⇧¯ S U)"
begin

lemma open_cover_of_open_subset_from_target_to_source:
assumes "open_cover_of_open_subset S' is_open' U I C"
shows "open_cover_of_open_subset S is_open (f⇧¯ S U) I (λi. f⇧¯ S (C i))"
proof
show "f ⇧¯ S U ⊆ S" by simp
show "f ⇧¯ S (C i) ⊆ S" if "i ∈ I" for i
using that by simp
show "is_open (f ⇧¯ S U)"
by (meson assms is_continuous open_cover_of_open_subset.is_open_subset)
show "⋀i. i ∈ I ⟹ is_open (f ⇧¯ S (C i))"
by (meson assms is_continuous open_cover_of_open_subset_def open_cover_of_subset.are_open_subspaces)
show "f ⇧¯ S U ⊆ (⋃i∈I. f ⇧¯ S (C i))"
using assms unfolding open_cover_of_open_subset_def cover_of_subset_def open_cover_of_subset_def
by blast
qed

end (* continuous map *)

subsection ‹Homeomorphisms›

text ‹The topological isomorphisms between topological spaces are called homeomorphisms.›

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

lemma (in topological_space) id_is_homeomorphism:
shows "homeomorphism S is_open S is_open (identity S)"
proof
show "inverse_map (identity S) S S ∈ S →⇩E S"
qed (auto simp: open_inter bij_betwI')

subsection ‹Topological Filters› (* Imported from HOL.Topological_Spaces *)

definition (in topological_space) nhds :: "'a ⇒ 'a filter"
where "nhds a = (INF S∈{S. is_open S ∧ a ∈ S}. principal S)"

abbreviation (in topological_space)
tendsto :: "('b ⇒ 'a) ⇒ 'a ⇒ 'b filter ⇒ bool"  (infixr "⤏" 55)
where "(f ⤏ l) F ≡ filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter ⇒ ('f ⇒ 'a) ⇒ 'a"
where "Lim A f = (THE l. (f ⤏ l) A)"

end


# Theory Comm_Ring

text ‹Authors: Anthony Bordg and Lawrence Paulson,
with some contributions from Wenda Li›

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

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

lemma (in monoid_homomorphism) monoid_preimage: "Group_Theory.monoid (η ⇧¯ M M') (⋅) 𝟭"
by (simp add: Int_absorb1 source.monoid_axioms subsetI)

lemma (in group_homomorphism) group_preimage: "Group_Theory.group (η ⇧¯ G G') (⋅) 𝟭"
by (simp add: Int_absorb1 source.group_axioms subsetI)

lemma (in ring_homomorphism) ring_preimage: "ring (η ⇧¯ R R') (+) (⋅) 𝟬 𝟭"
by (simp add: Int_absorb2 Int_commute source.ring_axioms subset_iff)

section ‹Commutative Rings›

subsection ‹Commutative Rings›

locale comm_ring = ring +
assumes comm_mult: "⟦ a ∈ R; b ∈ R ⟧ ⟹ a ⋅ b = b ⋅ a"

text ‹The zero ring is a commutative ring.›

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

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

declare ring0.additive.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"

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"

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
using assms ideal_implies_subset by (blast intro: additive.generate.incl)
qed

subsection ‹Ideals generated by an Element›

definition gen_ideal:: "'a ⇒ 'a set" ("⟨_⟩")
where "⟨x⟩ ≡ {y. ∃r∈R. y = r ⋅ x}"

lemma zero_in_gen_ideal:
assumes "x ∈ R"
shows "𝟬 ∈ ⟨x⟩"
proof -
have "∃a. a ∈ R ∧ 𝟬 = a ⋅ x"
by (metis (lifting) additive.unit_closed assms left_zero)
then show ?thesis
using gen_ideal_def by blast
qed

"⟦x ∈ R; a ∈ ⟨x⟩; b ∈ ⟨x⟩⟧ ⟹ a + b ∈ ⟨x⟩"
apply (clarsimp simp : gen_ideal_def)

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
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⟩" "(+)" 𝟬
obtain r where r: "r∈R" "a = r ⋅ x"
using a gen_ideal_def by auto
show "monoid.invertible ⟨x⟩ (+) 𝟬 a"
proof (rule M.invertibleI)
have "∃r∈R. - a = r ⋅ x"
by (metis assms ideal_R_R ideal_inverse local.left_minus r)
then show "-a ∈ ⟨x⟩" by (simp add: gen_ideal_def)
qed (use a r assms in auto)
qed (auto simp: zero_in_gen_ideal add_in_gen_ideal assms)

lemma gen_ideal_ideal:
assumes "x ∈ R"
shows "ideal ⟨x⟩ R (+) (⋅) 𝟬 𝟭"
proof intro_locales
show "submonoid_axioms ⟨x⟩ R (+) 𝟬"
show "Group_Theory.group_axioms ⟨x⟩ (+) 𝟬"
by (meson Group_Theory.group_def assms gen_ideal_group)
show "ideal_axioms ⟨x⟩ R (⋅)"
proof
fix a b
assume "a ∈ R" "b ∈ ⟨x⟩"
then obtain r where r: "r∈R" "b = r ⋅ x"
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›
proof (induction arbitrary: a)
case unit
then show ?case
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 ∈ 𝔟})"
unfolding ideal_gen_by_prod_def
by presburger
qed
next
case (mult u v)
then show ?case
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"
show "a + b ∈ ideal_gen_by_prod 𝔞 𝔟"
if "a ∈ ideal_gen_by_prod 𝔞 𝔟" "b ∈ ideal_gen_by_prod 𝔞 𝔟"
for a b
by (fastforce simp: ideal_gen_by_prod_def)
show "𝟬 ∈ ideal_gen_by_prod 𝔞 𝔟"
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
unfolding ideal_gen_by_prod_def
by blast
show "𝟬 + a = a" "a + 𝟬 = a"
if "a ∈ ideal_gen_by_prod 𝔞 𝔟" for a
by blast+
show "monoid.invertible (ideal_gen_by_prod 𝔞 𝔟) (+) 𝟬 u"
if "u ∈ ideal_gen_by_prod 𝔞 𝔟" for u
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
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)
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"
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
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 = 𝟬"

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"
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
show "((+) ∘ f) x y ∈ R"
if "x ∈ insert i I" "y ∈ R" for x y
using that R by force
qed
qed (use assms in auto)

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

(* ex. 0.15 *)
lemma ex_15:
fixes J :: "'b set" and 𝔞 :: "'b ⇒ 'a set"
assumes "J ≠ {}" and J: "⋀j. j∈J ⟹ ideal (𝔞 j) R (+) (⋅) 𝟬 𝟭"
shows "𝒱 ({x. ∃I f. x = finsum I f ∧ I ⊆ J ∧ finite I ∧ (∀i. i∈I ⟶ f i ∈ 𝔞 i)}) = (⋂j∈J. 𝒱 (𝔞 j))"
proof -
have "y ∈ U"
if j: "j ∈ J" "y ∈ 𝔞 j"
and "pr_ideal R U (+) (⋅) 𝟬 𝟭"
and U: "{finsum I f |I f. I ⊆ J ∧ finite I ∧ (∀i. i ∈ I ⟶ f i ∈ 𝔞 i)} ⊆ U"
for U j y
proof -
have "y ∈ R"
using J j ideal_implies_subset by blast
then have y: "y = finsum {j} (λ_. y)"
by simp
then have "y ∈ {finsum I f |I f. I ⊆ J ∧ finite I ∧ (∀i. i ∈ I ⟶ f i ∈ 𝔞 i)}"
using that by blast
then show ?thesis
by (rule subsetD [OF U])
qed
moreover have PI: "pr_ideal R x (+) (⋅) 𝟬 𝟭" if "∀j∈J. pr_ideal R x (+) (⋅) 𝟬 𝟭 ∧ 𝔞 j ⊆ x" for x
using that assms(1) by fastforce
moreover have "finsum I f ∈ U"
if "finite I"
and "∀j∈J. pr_ideal R U (+) (⋅) 𝟬 𝟭 ∧ 𝔞 j ⊆ U"
and "I ⊆ J" "∀i. i ∈ I ⟶ f i ∈ 𝔞 i" for U I f
using that
proof (induction I rule: finite_induct)
case empty
then show ?case
using PI assms ideal_zero by fastforce
next
case (insert i I)
then have "finsum (insert i I) f = f i + finsum I f"
by (metis assms(2) finsum_insert ideal_implies_subset insertCI subset_iff)
also have "... ∈ U"
using insert by (metis ideal_add insertCI pr_ideal.axioms(2) subset_eq)
finally show ?case .
qed
ultimately show ?thesis
by (auto simp: closed_subsets_def)
qed

(* ex 0.16 *)
definition is_zariski_open:: "'a set set ⇒ bool" where
"is_zariski_open U ≡ generated_topology Spec {U. (∃𝔞. ideal 𝔞 R (+) (⋅) 𝟬 𝟭 ∧ U = Spec - 𝒱 𝔞)} U"

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

lemma is_zariski_open_Spec [simp]: "is_zariski_open Spec"

lemma is_zariski_open_Union [intro]:
"(⋀x. x ∈ F ⟹ is_zariski_open x) ⟹ is_zariski_open (⋃ F)"

lemma is_zariski_open_Int [simp]:
"⟦is_zariski_open U; is_zariski_open V⟧ ⟹ is_zariski_open (U ∩ V)"
using Int is_zariski_open_def by blast

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

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

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

subsection ‹Standard Open Sets›

definition standard_open:: "'a ⇒ 'a set set" ("𝒟'(_')")
where "𝒟(x) ≡ (Spec ∖ 𝒱(⟨x⟩))"

lemma standard_open_is_zariski_open:
assumes "x ∈ R"
shows "is_zariski_open 𝒟(x)"
unfolding is_zariski_open_def standard_open_def
using assms gen_ideal_ideal generated_topology.simps by fastforce

lemma standard_open_is_subset:
assumes "x ∈ R"
shows "𝒟(x) ⊆ Spec"
by (simp add: assms standard_open_is_zariski_open zariski_open_is_subset)

lemma belongs_standard_open_iff:
assumes "x ∈ R" and "𝔭 ∈ Spec"
shows "x ∉ 𝔭 ⟷ 𝔭 ∈ 𝒟(x)"
using assms
apply (auto simp: standard_open_def closed_subsets_def spectrum_def gen_ideal_def subset_iff)
apply (metis pr_ideal.absorbent)
by (meson ideal.ideal(1) pr_ideal_def)

end (* comm_ring *)

subsection ‹Presheaves of Rings›

(* def 0.17 *)
locale presheaf_of_rings = Topological_Space.topological_space
+ fixes 𝔉:: "'a set ⇒ 'b set"
and ρ:: "'a set ⇒ 'a set ⇒ ('b ⇒ 'b)" and b:: "'b"
and add_str:: "'a set ⇒ ('b ⇒ 'b ⇒ 'b)" ("+⇘_⇙")
and mult_str:: "'a set ⇒ ('b ⇒ 'b ⇒ 'b)" ("⋅⇘_⇙")
and zero_str:: "'a set ⇒ 'b" ("𝟬⇘_⇙") and one_str:: "'a set ⇒ 'b" ("𝟭⇘_⇙")
assumes is_ring_morphism:
"⋀U V. is_open U ⟹ is_open V ⟹ V ⊆ U ⟹ ring_homomorphism (ρ U V)
(𝔉 U) (+⇘U⇙) (⋅⇘U⇙) 𝟬⇘U⇙ 𝟭⇘U⇙
(𝔉 V) (+⇘V⇙) (⋅⇘V⇙) 𝟬⇘V⇙ 𝟭⇘V⇙"
and ring_of_empty: "𝔉 {} = {b}"
and identity_map [simp]: "⋀U. is_open U ⟹ (⋀x. x ∈ 𝔉 U ⟹ ρ U U x = x)"
and assoc_comp:
"⋀U V W. is_open U ⟹ is_open V ⟹ is_open W ⟹ V ⊆ U ⟹ W ⊆ V ⟹
(⋀x. x ∈ (𝔉 U) ⟹ ρ U W x = (ρ V W ∘ ρ U V) x)"
begin

lemma is_ring_from_is_homomorphism:
shows "⋀U. is_open U ⟹ ring (𝔉 U) (+⇘U⇙) (⋅⇘U⇙) 𝟬⇘U⇙ 𝟭⇘U⇙"
using is_ring_morphism ring_homomorphism.axioms(2) by fastforce

lemma is_map_from_is_homomorphism:
assumes "is_open U" and "is_open V" and "V ⊆ U"
shows "Set_Theory.map (ρ U V) (𝔉 U) (𝔉 V)"
using assms by (meson is_ring_morphism ring_homomorphism.axioms(1))

lemma eq_ρ:
assumes "is_open U" and "is_open V" and "is_open W" and "W ⊆ U ∩ V" and "s ∈ 𝔉 U" and "t ∈ 𝔉 V"
and "ρ U W s = ρ V W t" and "is_open W'" and "W' ⊆ W"
shows "ρ U W' s = ρ V W' t"
by (metis Int_subset_iff assms assoc_comp comp_apply)

end (* presheaf_of_rings *)

locale morphism_presheaves_of_rings =
source: presheaf_of_rings X is_open 𝔉 ρ b add_str mult_str zero_str one_str
+ target: presheaf_of_rings X is_open 𝔉' ρ' b' add_str' mult_str' zero_str' one_str'
for X and is_open
and 𝔉 and ρ and b and add_str ("+⇘_⇙") and mult_str ("⋅⇘_⇙")
and zero_str ("𝟬⇘_⇙") and one_str ("𝟭⇘_⇙")
and 𝔉' and ρ' and b' and add_str' ("+''⇘_⇙") and mult_str' ("⋅''⇘_⇙")
and zero_str' ("𝟬''⇘_⇙") and one_str' ("𝟭''⇘_⇙") +
fixes fam_morphisms:: "'a set ⇒ ('b ⇒ 'c)"
assumes is_ring_morphism: "⋀U. is_open U ⟹ ring_homomorphism (fam_morphisms U)
(𝔉 U) (+⇘U⇙) (⋅⇘U⇙) 𝟬⇘U⇙ 𝟭⇘U⇙
(𝔉' U) (+'⇘U⇙) (⋅'⇘U⇙) 𝟬'⇘U⇙ 𝟭'⇘U⇙"
and comm_diagrams: "⋀U V. is_open U ⟹ is_open V ⟹ V ⊆ U ⟹
(⋀x. x ∈ 𝔉 U ⟹ (ρ' U V ∘ fam_morphisms U) x = (fam_morphisms V ∘ ρ U V) x)"
begin

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

end (* morphism_presheaves_of_rings *)

(* Identity presheaf *)
lemma (in presheaf_of_rings) id_is_mor_pr_rngs:
shows "morphism_presheaves_of_rings S is_open 𝔉 ρ b add_str mult_str zero_str one_str 𝔉 ρ b add_str mult_str zero_str one_str (λU. identity (𝔉 U))"
proof (intro morphism_presheaves_of_rings.intro morphism_presheaves_of_rings_axioms.intro)
show "⋀U. is_open U ⟹ ring_homomorphism (identity (𝔉 U))
(𝔉 U) (add_str U) (mult_str U) (zero_str U) (one_str U)
(𝔉 U) (add_str U) (mult_str U) (zero_str U) (one_str U)"
by (metis identity_map is_map_from_is_homomorphism is_ring_morphism restrict_ext restrict_on_source subset_eq)
show "⋀U V. ⟦is_open U; is_open V; V ⊆ U⟧
⟹ (⋀x. x ∈ (𝔉 U) ⟹ (ρ U V ∘ identity (𝔉 U)) x = (identity (𝔉 V) ∘ ρ U V) x)"
using map.map_closed by (metis comp_apply is_map_from_is_homomorphism restrict_apply')
qed (use presheaf_of_rings_axioms in auto)

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

(* Composition of presheaves *)
lemma comp_of_presheaves:
assumes 1: "morphism_presheaves_of_rings X is_open 𝔉 ρ b add_str mult_str zero_str one_str 𝔉' ρ' b' add_str' mult_str' zero_str' one_str' φ"
and 2: "morphism_presheaves_of_rings X is_open 𝔉' ρ' b' add_str' mult_str' zero_str' one_str' 𝔉'' ρ'' b'' add_str'' mult_str'' zero_str'' one_str'' φ'"
shows "morphism_presheaves_of_rings X is_open 𝔉 ρ b add_str mult_str zero_str one_str 𝔉'' ρ'' b'' add_str'' mult_str'' zero_str'' one_str'' (λU. (φ' U ∘ φ U ↓ 𝔉 U))"
proof (intro morphism_presheaves_of_rings.intro morphism_presheaves_of_rings_axioms.intro)
show "ring_homomorphism (φ' U ∘ φ U ↓ 𝔉 U) (𝔉 U) (add_str U) (mult_str U) (zero_str U) (one_str U) (𝔉'' U) (add_str'' U) (mult_str'' U) (zero_str'' U) (one_str'' U)"
if "is_open U"
for U :: "'a set"
using that
by (metis assms comp_ring_morphisms morphism_presheaves_of_rings.is_ring_morphism)
next
show "⋀x. x ∈ (𝔉 U) ⟹ (ρ'' U V ∘ (φ' U ∘ φ U ↓ 𝔉 U)) x = (φ' V ∘ φ V ↓ 𝔉 V ∘ ρ U V) x"
if "is_open U" "is_open V" "V ⊆ U" for U V
using that
using morphism_presheaves_of_rings.comm_diagrams [OF 1]
using morphism_presheaves_of_rings.comm_diagrams [OF 2]
using presheaf_of_rings.is_map_from_is_homomorphism [OF morphism_presheaves_of_rings.axioms(1) [OF 1]]
by (metis "1" comp_apply compose_eq map.map_closed morphism_presheaves_of_rings.fam_morphisms_are_maps)
qed (use assms in ‹auto simp: morphism_presheaves_of_rings_def›)

locale iso_presheaves_of_rings = mor:morphism_presheaves_of_rings
+ assumes is_inv:
"∃ψ. morphism_presheaves_of_rings X is_open 𝔉' ρ' b' add_str' mult_str' zero_str' one_str' 𝔉 ρ b add_str mult_str zero_str one_str ψ
∧ (∀U. is_open U ⟶ (∀x ∈ (𝔉' U). (fam_morphisms U ∘ ψ U) x = x) ∧ (∀x ∈ (𝔉 U). (ψ U ∘ fam_morphisms U) x = x))"

subsection ‹Sheaves of Rings›

(* def 0.19 *)
locale sheaf_of_rings = presheaf_of_rings +
assumes locality: "⋀U I V s. open_cover_of_open_subset S is_open U I V ⟹ (⋀i. i∈I ⟹ V i ⊆ U) ⟹
s ∈ 𝔉 U ⟹ (⋀i. i∈I ⟹ ρ U (V i) s = 𝟬⇘(V i)⇙) ⟹ s = 𝟬⇘U⇙"
and
glueing: "⋀U I V s. open_cover_of_open_subset S is_open U I V ⟹ (∀i. i∈I ⟶ V i ⊆ U ∧ s i ∈ 𝔉 (V i)) ⟹
(⋀i j. i∈I ⟹ j∈I ⟹ ρ (V i) (V i ∩ V j) (s i) = ρ (V j) (V i ∩ V j) (s j)) ⟹
(∃t. t ∈ 𝔉 U ∧ (∀i. i∈I ⟶ ρ U (V i) t = s i))"

(* def. 0.20 *)
locale morphism_sheaves_of_rings = morphism_presheaves_of_rings

locale iso_sheaves_of_rings = iso_presheaves_of_rings

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

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

definition ind_sheaf:: "'a set ⇒ 'b set"
where "ind_sheaf V ≡ 𝔉 (U ∩ V)"

definition ind_ring_morphisms:: "'a set ⇒ 'a set ⇒ ('b ⇒ 'b)"
where "ind_ring_morphisms V W ≡ ρ (U ∩ V) (U ∩ W)"

definition ind_add_str:: "'a set ⇒ ('b ⇒ 'b ⇒ 'b)"
where "ind_add_str V ≡ λx y. +⇘(U ∩ V)⇙ x y"

definition ind_mult_str:: "'a set ⇒ ('b ⇒ 'b ⇒ 'b)"
where "ind_mult_str V ≡ λx y. ⋅⇘(U ∩ V)⇙ x y"

definition ind_zero_str:: "'a set ⇒ 'b"
where "ind_zero_str V ≡ 𝟬⇘(U∩V)⇙"

definition ind_one_str:: "'a set ⇒ 'b"
where "ind_one_str V ≡ 𝟭⇘(U∩V)⇙"

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

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

lemma ind_sheaf_is_sheaf:
shows "sheaf_of_rings U it.ind_is_open ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str"
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
show "presheaf_of_rings U it.ind_is_open ind_sheaf ind_ring_morphisms b ind_add_str ind_mult_str ind_zero_str ind_one_str"
using ind_sheaf_is_presheaf by blast
next
fix V I W s
assume oc: "open_cover_of_open_subset U it.ind_is_open V I W"
and WV: "⋀i. i ∈ I ⟹ W i ⊆ V"
and s: "s ∈ ind_sheaf V"
and eq: "⋀i. i ∈ I ⟹ ind_ring_morphisms V (W i) s = ind_zero_str (W i)"
have "it.ind_is_open V"
using oc open_cover_of_open_subset.is_open_subset by blast
then have "s ∈ 𝔉 V"
by (metis ind_sheaf.ind_sheaf_def ind_sheaf_axioms it.ind_is_open_def inf.absorb2 s)
then have "s = 𝟬⇘V⇙"
by (metis Int_absorb1 Int_subset_iff WV ind_sheaf.ind_zero_str_def ind_sheaf_axioms eq it.ind_is_open_def ind_ring_morphisms_def is_open_subset locality oc it.open_cover_from_ind_open_cover open_cover_of_open_subset.is_open_subset)
then show "s = ind_zero_str V"
by (metis Int_absorb1 it.ind_is_open_def ind_zero_str_def oc open_cover_of_open_subset.is_open_subset)
next
fix V I W s
assume oc: "open_cover_of_open_subset U it.ind_is_open V I W"
and WV: "∀i. i ∈ I ⟶ W i ⊆ V ∧ s i ∈ ind_sheaf (W i)"
and eq: "⋀i j. ⟦i ∈ I; j ∈ I⟧ ⟹ ind_ring_morphisms (W i) (W i ∩ W j) (s i) = ind_ring_morphisms (W j) (W i ∩ W j) (s j)"
have "is_open V"
using it.is_open_from_ind_is_open is_open_subset oc open_cover_of_open_subset.is_open_subset by blast
moreover have "open_cover_of_open_subset S is_open V I W"
using it.open_cover_from_ind_open_cover oc ind_topology.intro ind_topology_axioms_def is_open_subset it.is_subset topological_space_axioms by blast
moreover have "ρ (W i) (W i ∩ W j) (s i) = ρ (W j) (W i ∩ W j) (s j)"
if "i∈I" "j∈I" for i j
proof -
have "U ∩ W i = W i" and "U ∩ W j = W j"
by (metis Int_absorb1 WV it.ind_is_open_def oc open_cover_of_open_subset.is_open_subset
subset_trans that)+
then show ?thesis
using eq[unfolded ind_ring_morphisms_def,OF that] by (metis inf_sup_aci(2))
qed
moreover have "∀i. i∈I ⟶ W i ⊆ V ∧ s i ∈ 𝔉 (W i)"
by (metis WV it.ind_is_open_def ind_sheaf_def inf.orderE inf_idem inf_aci(3) oc open_cover_of_open_subset.is_open_subset)
ultimately
obtain t where "t ∈ (𝔉 V) ∧ (∀i. i∈I ⟶ ρ V (W i) t = s i)"
using glueing by blast
then have "t ∈ ind_sheaf V"
unfolding ind_sheaf_def using oc
by (metis Int_absorb1 cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
moreover have "∀i. i∈I ⟶ ind_ring_morphisms V (W i) t = s i"
unfolding ind_ring_morphisms_def
by (metis oc Int_absorb1 ‹t ∈ 𝔉 V ∧ (∀i. i ∈ I ⟶ ρ V (W i) t = s i)› cover_of_subset_def open_cover_of_open_subset_def open_cover_of_subset_def)
ultimately show "∃t. t ∈ (ind_sheaf V) ∧ (∀i. i∈I ⟶ ind_ring_morphisms V (W i) t = s i)" by blast
qed

end (* ind_sheaf *)

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

(* def 0.24 *)
definition im_sheaf:: "'c set => 'b set"
where "im_sheaf V ≡ 𝔉 (f⇧¯ S V)"

definition im_sheaf_morphisms:: "'c set ⇒ 'c set ⇒ ('b ⇒ 'b)"
where "im_sheaf_morphisms U V ≡ ρ (f⇧¯ S U) (f⇧¯ S V)"

definition add_im_sheaf:: "'c set ⇒ 'b ⇒ 'b ⇒ 'b"
where "add_im_sheaf ≡ λV x y. +⇘(f⇧¯ S V)⇙ x y"

definition mult_im_sheaf:: "'c set ⇒ 'b ⇒ 'b ⇒ 'b"
where "mult_im_sheaf ≡ λV x y. ⋅⇘(f⇧¯ S V)⇙ x y"

definition zero_im_sheaf:: "'c set ⇒ 'b"
where "zero_im_sheaf ≡ λV. 𝟬⇘(f⇧¯ S V)⇙"

definition one_im_sheaf:: "'c set ⇒ 'b"
where "one_im_sheaf ≡ λV. 𝟭⇘(f⇧¯ S V)⇙"

lemma im_sheaf_is_presheaf:
"presheaf_of_rings S' (is_open') im_sheaf im_sheaf_morphisms b
proof (intro presheaf_of_rings.intro presheaf_of_rings_axioms.intro)
show "topological_space S' is_open'"
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)"
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
proof (intro sheaf_of_rings.intro sheaf_of_rings_axioms.intro)
show "presheaf_of_rings S' is_open' im_sheaf im_sheaf_morphisms b
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))"
then show "s = zero_im_sheaf U" using zero_im_sheaf_def
by (smt VU im_sheaf_def im_sheaf_morphisms_def eq0 inf.absorb_iff2 inf_le2 inf_sup_aci(1) inf_sup_aci(3) locality s vimage_Int)
next
fix U I V s
assume oc: "open_cover_of_open_subset S' is_open' U I V"
and VU: "∀i. i ∈ I ⟶ V i ⊆ U ∧ s i ∈ im_sheaf (V i)"
and eq: "⋀i j. ⟦i ∈ I; j ∈ I⟧ ⟹ im_sheaf_morphisms (V i) (V i ∩ V j) (s i) = im_sheaf_morphisms (V j) (V i ∩ V j) (s j)"
have "∃t. t ∈ 𝔉 (f  ⇧¯ S U) ∧ (∀i. i ∈ I ⟶ ρ (f  ⇧¯ S U) (f  ⇧¯ S (V i)) t = s i)"
proof (rule glueing)
show "open_cover_of_open_subset S is_open (f ⇧¯ S U) I (λi. f ⇧¯ S (V i))"
using oc open_cover_of_open_subset_from_target_to_source by presburger
show "∀i. i ∈ I ⟶ f ⇧¯ S (V i) ⊆ f ⇧¯ S U ∧ s i ∈ 𝔉 (f ⇧¯ S (V i))"
using VU im_sheaf_def by blast
show "ρ (f ⇧¯ S (V i)) (f ⇧¯ S (V i) ∩ f ⇧¯ S (V j)) (s i) = ρ (f ⇧¯ S (V j)) (f ⇧¯ S (V i) ∩ f ⇧¯ S (V j)) (s j)"
if "i ∈ I" "j ∈ I" for i j
using im_sheaf_morphisms_def eq that
by (smt Int_commute Int_left_commute inf.left_idem vimage_Int)
qed
then obtain t where "t ∈ 𝔉 (f⇧¯ S U) ∧ (∀i. i∈I ⟶ ρ (f⇧¯ S U) (f⇧¯ S (V i)) t = s i)" ..
then show "∃t. t ∈ im_sheaf U ∧ (∀i. i ∈ I ⟶ im_sheaf_morphisms U (V i) t = s i)"
using im_sheaf_def im_sheaf_morphisms_def by auto
qed

sublocale sheaf_of_rings S' is_open' im_sheaf im_sheaf_morphisms b
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"
have 2[simp]: "⋀U V. ⟦U ⊆ S; V ⊆ S⟧ ⟹ im_sheaf.im_sheaf_morphisms S ρ (identity S) U V ≡ ρ U V"
using id.im_sheaf_morphisms_def by auto
show ?thesis
proof intro_locales
have rh: "⋀U. is_open U ⟹
ring_homomorphism (identity (𝔉 U)) (𝔉 U) +⇘U⇙ ⋅⇘U⇙ 𝟬⇘U⇙ 𝟭⇘U⇙ (𝔉 U) +⇘U⇙ ⋅⇘U⇙ 𝟬⇘U⇙ 𝟭⇘U⇙"
using id_is_mor_pr_rngs morphism_presheaves_of_rings.is_ring_morphism by fastforce
show "morphism_presheaves_of_rings_axioms is_open 𝔉 ρ add_str mult_str zero_str one_str
id.im_sheaf id.im_sheaf_morphisms ?add ?mult ?zero ?one ?F"
unfolding morphism_presheaves_of_rings_axioms_def
by (auto simp: rh open_imp_subset intro: is_map_from_is_homomorphism map.map_closed)
have ρ: "⋀U V W x. ⟦is_open U; is_open V; is_open W; V ⊆ U; W ⊆ V; x ∈ 𝔉 U⟧ ⟹ ρ V W (ρ U V x) = ρ U W x"
by (metis assoc_comp comp_def)
show "presheaf_of_rings_axioms is_open id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one"
by (auto simp: ρ presheaf_of_rings_axioms_def is_ring_morphism open_imp_subset ring_of_empty)
then have "presheaf_of_rings S is_open id.im_sheaf id.im_sheaf_morphisms b ?add ?mult ?zero ?one"
by (metis id.im_sheaf_is_presheaf presheaf_of_rings_def)
moreover
have "morphism_presheaves_of_rings_axioms is_open
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"
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.comm_mult
right_minus

definition rel:: "('a × 'a) ⇒ ('a × 'a) ⇒ bool" (infix "∼" 80)
where "x ∼ y ≡ ∃s1. s1 ∈ S ∧ s1 ⋅ (snd y ⋅ fst x - snd x ⋅ fst y) = 𝟬"

lemma rel_refl: "⋀x. x ∈ R × S ⟹ x ∼ x"
by (auto simp: rel_def)

lemma rel_sym:
assumes "x ∼ y" "x ∈ R × S" "y ∈ R × S" shows "y ∼ x"
proof -
obtain rx sx ry sy s
where §: "rx ∈ R" "sx ∈ S" "ry ∈ R" "s ∈ S" "sy ∈ S" "s ⋅ (sy ⋅ rx - sx ⋅ ry) = 𝟬" "x = (rx,sx)" "y = (ry,sy)"
using assms by (auto simp: rel_def)
then have "s ⋅ (sx ⋅ ry - sy ⋅ rx) = 𝟬"
by (metis sub comm.additive.cancel_imp_equal comm.inverse_distributive(1) comm.multiplicative.composition_closed)
with § show ?thesis
by (auto simp: rel_def)
qed

lemma rel_trans:
assumes "x ∼ y" "y ∼ z" "x ∈ R × S" "y ∈ R × S" "z ∈ R × S" shows "x ∼ z"
using assms
proof (clarsimp simp: rel_def)
fix r s r2 s2 r1 s1 sx sy
assume §: "r ∈ R" "s ∈ S" "r1 ∈ R" "s1 ∈ S" "sx ∈ S" "r2 ∈ R" "s2 ∈ S" "sy ∈ S"
and sx0: "sx ⋅ (s1 ⋅ r2 - s2 ⋅ r1) = 𝟬" and sy0: "sy ⋅ (s2 ⋅ r - s ⋅ r2) = 𝟬"
show "∃u. u ∈ S ∧ u ⋅ (s1 ⋅ r - s ⋅ r1) = 𝟬"
proof (intro exI conjI)
show "sx ⋅ sy ⋅ s1 ⋅ s2 ∈ S"
using § by blast
have sx: "sx ⋅ s1 ⋅ r2 = sx ⋅ s2 ⋅ r1" and sy: "sy ⋅ s2 ⋅ r = sy ⋅ s ⋅ r2"
using sx0 sy0 § comm.additive.cancel_imp_equal comm.inverse_distributive(1)
comm.multiplicative.associative comm.multiplicative.composition_closed sub
by metis+
then
have "sx ⋅ sy ⋅ s1 ⋅ s2 ⋅ (s1 ⋅ r - s ⋅ r1) = sx ⋅ sy ⋅ s1 ⋅ s2 ⋅ s1 ⋅ r - sx ⋅ sy ⋅ s1 ⋅ s2 ⋅ s ⋅ r1"
using "§" ‹sx ⋅ sy ⋅ s1 ⋅ s2 ∈ S›
comm.inverse_distributive(1) comm.multiplicative.associative comm.multiplicative.composition_closed
sub
by presburger
also have "... = sx ⋅ sy ⋅ s1 ⋅ s ⋅ s1 ⋅ r2 - sx ⋅ sy ⋅ s1 ⋅ s2 ⋅ s ⋅ r1"
using §
by (smt sy comm.comm_mult comm.multiplicative.associative comm.multiplicative.composition_closed sub)
also have "... = sx ⋅ sy ⋅ s1 ⋅ s ⋅ s1 ⋅ r2 - sx ⋅ sy ⋅ s1 ⋅ s1 ⋅ s ⋅ r2"
using § by (smt sx comm.comm_mult comm.multiplicative.associative
comm.multiplicative.composition_closed sub)
also have "... = 𝟬"
using § by (simp add: comm.ring_mult_ac)
finally show "sx ⋅ sy ⋅ s1 ⋅ s2 ⋅ (s1 ⋅ r - s ⋅ r1) = 𝟬" .
qed
qed

interpretation rel: equivalence "R × S" "{(x,y) ∈ (R×S)×(R×S). x ∼ y}"
by (blast intro: equivalence.intro rel_refl rel_sym rel_trans)

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

definition frac:: "'a ⇒ 'a ⇒ ('a × 'a) set" (infixl "'/" 75)
where "r / s ≡ rel.Class (r, s)"

lemma frac_Pow:"(r, s) ∈ R × S ⟹ frac r s ∈ Pow (R × S) "
using local.frac_def rel.Class_closed2 by auto

lemma frac_eqI:
assumes "s1∈S" and "(r, s) ∈ R × S" "(r', s') ∈ R × S"
and eq:"s1 ⋅ s' ⋅ r = s1 ⋅ s ⋅ r'"
shows "frac r s = frac r' s'"
unfolding frac_def
proof (rule rel.Class_eq)
have "s1 ⋅ (s' ⋅ r - s ⋅ r') = 𝟬"
using assms comm.inverse_distributive(1) comm.multiplicative.associative by auto
with ‹s1∈S› have "(r, s) ∼ (r', s')"
unfolding rel_def by auto
then show "((r, s), r', s') ∈ {(x, y). (x, y) ∈ (R × S) × R × S ∧ x ∼ y}"
using assms(2,3) by auto
qed

lemma frac_eq_Ex:
assumes "(r, s) ∈ R × S" "(r', s') ∈ R × S" "frac r s = frac r' s'"
obtains s1 where "s1∈S" "s1 ⋅ (s' ⋅ r - s ⋅ r') = 𝟬"
proof -
have "(r, s) ∼ (r', s')"
using ‹frac r s = frac r' s'› rel.Class_equivalence[OF assms(1,2)]
unfolding frac_def by auto
then show ?thesis unfolding rel_def
by (metis fst_conv snd_conv that)
qed

lemma frac_cancel:
assumes "s1∈S" and "(r, s) ∈ R × S"
shows "frac (s1⋅r) (s1⋅s) = frac r s"
apply (rule frac_eqI[of 𝟭])
using assms comm_ring_simps by auto

lemma frac_eq_obtains:
assumes "(r,s) ∈ R × S" and x_def:"x=(SOME x. x∈(frac r s))"
obtains s1 where "s1∈S" "s1 ⋅ s ⋅ fst x = s1 ⋅ snd x ⋅ r" and "x ∈ R × S"
proof -
have "x∈(r/s)"
unfolding x_def
apply (rule someI[of _ "(r,s)"])
using assms(1) local.frac_def by blast
from rel.ClassD[OF this[unfolded frac_def] ‹(r,s) ∈ R × S›]
have x_RS:"x∈R × S" and "x ∼ (r,s)" by auto
from this(2) obtain s1 where "s1∈S" and "s1 ⋅ (s ⋅ fst x - snd x ⋅ r) = 𝟬"
unfolding rel_def by auto
then have x_eq:"s1 ⋅ s ⋅ fst x = s1 ⋅ snd x ⋅ r"
using comm.distributive x_RS assms(1)
mem_Sigma_iff comm.multiplicative.associative comm.multiplicative.composition_closed prod.collapse sub)
then show ?thesis using that x_RS ‹s1∈S› by auto
qed

definition valid_frac::"('a × 'a) set ⇒ bool" where
"valid_frac X ≡ ∃r∈R. ∃s∈S. r / s = X"

lemma frac_non_empty[simp]:"(a,b) ∈ R × S ⟹ valid_frac (frac a b)"
unfolding frac_def valid_frac_def by blast

definition add_rel_aux:: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ ('a × 'a) set"
where "add_rel_aux r s r' s' ≡ (r⋅s' + r'⋅s) / (s⋅s')"

definition add_rel:: "('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
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)"

assumes "(r,s) ∈ R × S" "(r',s')∈ R × S"
shows "add_rel (r/s) (r'/s') = (r⋅s' + r'⋅s) / (s⋅s')"
proof -
define x where "x=(SOME x. x∈(r/s))"
define y where "y=(SOME y. y∈(r'/s'))"

obtain s1 where [simp]:"s1 ∈ S" and x_eq:"s1 ⋅ s ⋅ fst x = s1 ⋅ snd x ⋅ r" and x_RS:"x ∈ R × S"
using frac_eq_obtains[OF ‹(r,s) ∈ R × S› x_def] by auto
obtain s2 where [simp]:"s2 ∈ S" and y_eq:"s2 ⋅ s' ⋅ fst y = s2 ⋅ snd y ⋅ r'" and y_RS:"y ∈ R × S"
using frac_eq_obtains[OF ‹(r',s') ∈ R × S› y_def] by auto

have "add_rel (r/s) (r'/s') = (fst x ⋅ snd y + fst y ⋅ snd x) / (snd x ⋅ snd y)"
also have "... = (r⋅s' + r'⋅s) / (s⋅s')"
proof (rule frac_eqI[of "s1 ⋅ s2"])
have "snd y ⋅  s' ⋅ s2 ⋅ (s1 ⋅  s ⋅ fst x)  = snd y ⋅ s' ⋅ s2 ⋅ (s1 ⋅  snd x ⋅  r)"
using x_eq by simp
then have "s1 ⋅ s2 ⋅ s ⋅ s' ⋅ fst x ⋅ snd y =  s1 ⋅ s2 ⋅ snd x ⋅ snd y ⋅ r ⋅ s'"
using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult by auto
moreover have "snd x ⋅ s ⋅s1 ⋅ (s2 ⋅ s' ⋅ fst y) = snd x ⋅ s ⋅s1 ⋅ (s2 ⋅ snd y ⋅ r')"
using y_eq by simp
then have "s1 ⋅ s2 ⋅ s ⋅ s' ⋅ fst y ⋅ snd x = s1 ⋅ s2 ⋅ snd x ⋅ snd y ⋅ r' ⋅ s"
using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult
by auto
ultimately show "s1 ⋅ s2 ⋅ (s ⋅ s') ⋅ (fst x ⋅ snd y + fst y ⋅ snd x)
= s1 ⋅ s2 ⋅ (snd x ⋅ snd y) ⋅ (r ⋅ s' + r' ⋅ s)"
using comm.multiplicative.associative assms x_RS y_RS comm.distributive
by auto
show "s1 ⋅ s2 ∈ S" "(fst x ⋅ snd y + fst y ⋅ snd x, snd x ⋅ snd y) ∈ R × S"
"(r ⋅ s' + r' ⋅ s, s ⋅ s') ∈ R × S"
using assms x_RS y_RS by auto
qed
finally show ?thesis by auto
qed

assumes "valid_frac X" "valid_frac Y"
proof -
obtain r s r' s' where "r∈R" "s∈S" "r'∈R" "s'∈S"
and *:"add_rel X Y = (r⋅s' + r'⋅s) / (s⋅s')"
proof -
define x where "x=(SOME x. x∈X)"
define y where "y=(SOME y. y∈Y)"
have "x∈X" "y∈Y"
using assms unfolding x_def y_def valid_frac_def some_in_eq local.frac_def
by blast+
then obtain "x ∈ R × S" "y ∈ R × S"
using assms
by (simp add: valid_frac_def x_def y_def) (metis frac_eq_obtains mem_Sigma_iff)
moreover have "add_rel X Y = (fst x ⋅ snd y + fst y ⋅ snd x) / (snd x ⋅ snd y)"
ultimately show ?thesis using that by auto
qed
from this(1-4)
have "(r⋅s' + r'⋅s,s⋅s') ∈ R × S"
by auto
with * show ?thesis by auto
qed

definition uminus_rel:: "('a × 'a) set ⇒ ('a × 'a) set"
where "uminus_rel X ≡ let x = (SOME x. x ∈ X) in (comm.additive.inverse (fst x) / snd x)"

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

obtain s1 where [simp]:"s1 ∈ S" and x_eq:"s1 ⋅ s ⋅ fst x = s1 ⋅ snd x ⋅ r" and x_RS:"x ∈ R × S"
using frac_eq_obtains[OF ‹(r,s) ∈ R × S› x_def] by auto

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

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

definition mult_rel_aux:: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ ('a × 'a) set"
where "mult_rel_aux r s r' s' ≡ (r⋅r') / (s⋅s')"

definition mult_rel:: "('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"
where "mult_rel X Y ≡
let x = (SOME x. x ∈ X) in
let y = (SOME y. y ∈ Y) in
mult_rel_aux (fst x) (snd x) (fst y) (snd y)"

lemma mult_rel_frac:
assumes "(r,s) ∈ R × S" "(r',s')∈ R × S"
shows "mult_rel (r/s) (r'/s') = (r⋅ r') / (s⋅s')"
proof -
define x where "x=(SOME x. x∈(r/s))"
define y where "y=(SOME y. y∈(r'/s'))"

obtain s1 where [simp]:"s1 ∈ S" and x_eq:"s1 ⋅ s ⋅ fst x = s1 ⋅ snd x ⋅ r" and x_RS:"x ∈ R × S"
using frac_eq_obtains[OF ‹(r,s) ∈ R × S› x_def] by auto
obtain s2 where [simp]:"s2 ∈ S" and y_eq:"s2 ⋅ s' ⋅ fst y = s2 ⋅ snd y ⋅ r'" and y_RS:"y ∈ R × S"
using frac_eq_obtains[OF ‹(r',s') ∈ R × S› y_def] by auto

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

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

definition zero_rel::"('a × 'a) set" where
"zero_rel = frac 𝟬 𝟭"

definition one_rel::"('a × 'a) set" where
"one_rel = frac 𝟭 𝟭"

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

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

definition carrier_quotient_ring:: "('a × 'a) set set"
where "carrier_quotient_ring ≡ rel.Partition"

lemma carrier_quotient_ring_iff[iff]: "X ∈ carrier_quotient_ring ⟷ valid_frac X "
unfolding valid_frac_def carrier_quotient_ring_def
using local.frac_def rel.natural.map_closed rel.representant_exists by fastforce

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

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
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)
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

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 comm.distributive comm_ring_simps
using a12 b12 c12 by auto

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

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
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
finally show "mult_rel a (add_rel b c) = add_rel (mult_rel a b) (mult_rel a c)"
.
qed
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
using a12 by simp
also have "... = (a1/a2)"
using a_RS comm_ring_simps comm.distributive zero_rel_def
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
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
qed
show "add_rel a zero_rel = a" if "valid_frac a" for a
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 -
apply (unfold_locales)
moreover have "add_rel a (uminus_rel a) = zero_rel" "add_rel (uminus_rel a) a = zero_rel"
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
qed auto

end (* quotient_ring *)

notation quotient_ring.carrier_quotient_ring
("(_ ⇧¯ _/ ⇘(2_ _ _))⇙" [60,1000,1000,1000,1000]1000)

subsection ‹Local Rings at Prime Ideals›

context pr_ideal
begin

lemma submonoid_pr_ideal:
shows "submonoid (R ∖ I) R (⋅) 𝟭"
proof
show "a ⋅ b ∈ R∖I" if "a ∈ R∖I" "b ∈ R∖I" for a b
using that by (metis Diff_iff absorbent comm.multiplicative.composition_closed)
show "𝟭 ∈ R∖I"
using ideal.ideal(2) ideal_axioms pr_ideal.carrier_neq pr_ideal_axioms by fastforce
qed auto

interpretation local:quotient_ring "(R ∖ I)" R "(+)" "(⋅)" 𝟬 𝟭
by intro_locales (meson submonoid_def submonoid_pr_ideal)

(* definition 0.28 *)
definition carrier_local_ring_at:: "('a × 'a) set set"
where "carrier_local_ring_at ≡ (R ∖ I)⇧¯ R⇘(+) (⋅) 𝟬⇙"

definition add_local_ring_at:: "('a × 'a) set ⇒ ('a × 'a) set ⇒ ('a × 'a) set"

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"

zero_local_ring_at one_local_ring_at
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)
where "R ⇘I add mult zero⇙ ≡ pr_ideal.carrier_local_ring_at R I add mult zero"

subsection ‹Spectrum of a Ring›

(* construction 0.29 *)
context comm_ring
begin

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

lemma spectrum_imp_cxt_quotient_ring:
"𝔭 ∈ Spec ⟹ quotient_ring (R ∖ 𝔭) R (+) (⋅) 𝟬 𝟭"
apply (intro_locales)
using pr_ideal.submonoid_pr_ideal spectrum_def submonoid_def by fastforce

lemma spectrum_imp_pr:
"𝔭 ∈ Spec ⟹ pr_ideal R 𝔭 (+) (⋅) 𝟬 𝟭"
unfolding spectrum_def by auto

lemma frac_in_carrier_local:
assumes "𝔭 ∈ Spec" and "r ∈ R" and "s ∈ R" and "s ∉ 𝔭"
shows "(quotient_ring.frac (R ∖ 𝔭) R (+) (⋅) 𝟬 r s) ∈ R⇘𝔭 (+) (⋅) 𝟬⇙"
proof -
interpret qr:quotient_ring "R ∖ 𝔭" R "(+)" "(⋅)" 𝟬 𝟭
using spectrum_imp_cxt_quotient_ring[OF ‹𝔭 ∈ Spec›] .
interpret pi:pr_ideal R 𝔭 "(+)" "(⋅)" 𝟬 𝟭
using spectrum_imp_pr[OF ‹𝔭 ∈ Spec›] .
show ?thesis unfolding pi.carrier_local_ring_at_def
using assms(2-) by (auto intro:qr.frac_non_empty)
qed

definition is_locally_frac:: "('a set ⇒ ('a × 'a) set) ⇒ 'a set set ⇒ bool"
where "is_locally_frac s V ≡ (∃r f. r ∈ R ∧ f ∈ R ∧ (∀𝔮 ∈ V. f ∉ 𝔮 ∧
s 𝔮 = quotient_ring.frac (R ∖ 𝔮) R (+) (⋅) 𝟬 r f))"

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

lemma is_locally_frac_cong:
assumes "⋀x. x∈U ⟹ f x=g x"
shows "is_locally_frac f U = is_locally_frac g U"
unfolding is_locally_frac_def using assms by simp

definition is_regular:: "('a set ⇒ ('a × 'a) set) ⇒ 'a set set ⇒ bool"
where "is_regular s U ≡
∀𝔭. 𝔭 ∈ U ⟶ (∃V. is_zariski_open V ∧ V ⊆ U ∧ 𝔭 ∈ V ∧ (is_locally_frac s V))"

lemma map_on_empty_is_regular:
fixes s:: "'a set ⇒ ('a × 'a) set"
shows "is_regular s {}"

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)
where "𝒪 U ≡ {s∈(Π⇩E 𝔭∈U. (R⇘𝔭 (+) (⋅) 𝟬⇙)). is_regular s U}"

lemma cring0_sheaf_spec_empty [simp]: "cring0.sheaf_spec {} = {λx. undefined}"

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' 𝔭)"

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
qed
moreover have "(∃V⊆U. is_zariski_open V ∧ 𝔭 ∈ V ∧ is_locally_frac (add_sheaf_spec U s s') V)"
if "𝔭 ∈ U" for 𝔭
proof -
obtain V1 r1 f1 where "V1 ⊆U" "is_zariski_open V1" "𝔭 ∈ V1" "r1 ∈ R" "f1 ∈ R" and
q_V1:"(∀𝔮. 𝔮 ∈ V1 ⟶ f1 ∉ 𝔮 ∧ s 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r1 f1)"
using ‹is_regular s U›[unfolded is_regular_def] ‹𝔭 ∈ U›
unfolding is_locally_frac_def by auto
obtain V2 r2 f2 where "V2 ⊆U" "is_zariski_open V2" "𝔭 ∈ V2" "r2 ∈ R" "f2 ∈ R" and
q_V2:"(∀𝔮. 𝔮 ∈ V2 ⟶ f2 ∉ 𝔮 ∧ s' 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r2 f2)"
using ‹is_regular s' U›[unfolded is_regular_def]  ‹𝔭 ∈ U›
unfolding is_locally_frac_def by auto

define V3 where "V3 = V1 ∩ V2"
define r3 where "r3 = r1 ⋅ f2 + r2 ⋅ f1 "
define f3 where "f3 = f1 ⋅ f2"
have "V3 ⊆U" "𝔭 ∈ V3" "r3 ∈ R" "f3 ∈ R"
unfolding V3_def r3_def f3_def
using ‹V1 ⊆ U› ‹𝔭 ∈ V1› ‹V2 ⊆ U› ‹𝔭 ∈ V2› ‹f1 ∈ R› ‹f2 ∈ R› ‹r1 ∈ R› ‹r2 ∈ R› by blast+
moreover have "is_zariski_open V3" using ‹is_zariski_open V1› ‹is_zariski_open V2› topological_space.open_inter by (simp add: V3_def)
moreover have "f3 ∉ 𝔮"
"add_sheaf_spec U s s' 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r3 f3"
if "𝔮 ∈ V3" for 𝔮
proof -
interpret q:quotient_ring "R∖𝔮" R "(+)" "(⋅)" 𝟬
using ‹U ⊆ Spec› ‹V3 ⊆ U› ‹𝔮 ∈ V3› quotient_ring_def local.comm_ring_axioms
pr_ideal.submonoid_pr_ideal spectrum_def
by fastforce
have "f1 ∉ 𝔮" "s 𝔮 = q.frac r1 f1"
using q_V1 ‹𝔮 ∈ V3›  unfolding V3_def by auto
have "f2 ∉ 𝔮" "s' 𝔮 = q.frac r2 f2"
using q_V2 ‹𝔮 ∈ V3›  unfolding V3_def by auto

have "q.add_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 ⋅ f2 + r2 ⋅ f1) (f1 ⋅ f2)"
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

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
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"
ultimately show ?thesis
unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition mult_sheaf_spec:: "('a set) set ⇒ ('a set ⇒ ('a × 'a) set) ⇒ ('a set ⇒ ('a × 'a) set) ⇒ ('a set ⇒ ('a × 'a) set)"
where "mult_sheaf_spec U s s' ≡ λ𝔭∈U. quotient_ring.mult_rel (R ∖ 𝔭) R (+) (⋅) 𝟬 (s 𝔭) (s' 𝔭)"

lemma is_regular_mult_sheaf_spec:
assumes "is_regular s U" and "is_regular s' U" and "U ⊆ Spec"
shows "is_regular (mult_sheaf_spec U s s') U"
proof -
have "mult_sheaf_spec U s s' 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙" if "𝔭 ∈ U" for 𝔭
proof -
interpret pi: pr_ideal R 𝔭 "(+)" "(⋅)" 𝟬 𝟭
using ‹U ⊆ Spec›[unfolded spectrum_def] ‹𝔭 ∈ U› by blast
have "s 𝔭 ∈ pi.carrier_local_ring_at"
"s' 𝔭 ∈ pi.carrier_local_ring_at"
using ‹is_regular s U› ‹is_regular s' U›
unfolding is_regular_def using that
using assms(3) frac_in_carrier_local in_mono is_locally_frac_def by fastforce+
then show ?thesis
unfolding mult_sheaf_spec_def using that
by (simp flip:pi.mult_local_ring_at_def)
qed
moreover have "(∃V⊆U. is_zariski_open V ∧ 𝔭 ∈ V ∧ is_locally_frac (mult_sheaf_spec U s s') V)"
if "𝔭 ∈ U" for 𝔭
proof -
obtain V1 r1 f1 where "V1 ⊆U" "is_zariski_open V1" "𝔭 ∈ V1" "r1 ∈ R" "f1 ∈ R" and
q_V1:"(∀𝔮. 𝔮 ∈ V1 ⟶ f1 ∉ 𝔮 ∧ s 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r1 f1)"
using ‹is_regular s U›[unfolded is_regular_def] ‹𝔭 ∈ U› unfolding is_locally_frac_def
by auto
obtain V2 r2 f2 where "V2 ⊆U" "is_zariski_open V2" "𝔭 ∈ V2" "r2 ∈ R" "f2 ∈ R" and
q_V2:"(∀𝔮. 𝔮 ∈ V2 ⟶ f2 ∉ 𝔮 ∧ s' 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r2 f2)"
using ‹is_regular s' U›[unfolded is_regular_def] ‹𝔭 ∈ U› unfolding is_locally_frac_def
by auto

define V3 where "V3 = V1 ∩ V2"
define r3 where "r3 = r1 ⋅ r2  "
define f3 where "f3 = f1 ⋅ f2"
have "V3 ⊆U" "𝔭 ∈ V3" "r3 ∈ R" "f3 ∈ R"
unfolding V3_def r3_def f3_def
using ‹V1 ⊆ U› ‹𝔭 ∈ V1› ‹𝔭 ∈ V2› ‹f1 ∈ R› ‹f2 ∈ R› ‹r1 ∈ R› ‹r2 ∈ R› by blast+
moreover have "is_zariski_open V3"
using topological_space.open_inter by (simp add: V3_def ‹is_zariski_open V1› ‹is_zariski_open V2›)
moreover have "f3 ∉ 𝔮"
"mult_sheaf_spec U s s' 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r3 f3"
if "𝔮 ∈ V3" for 𝔮
proof -
interpret q:quotient_ring "R∖𝔮" R "(+)" "(⋅)" 𝟬
using ‹U ⊆ Spec› ‹V3 ⊆ U› ‹𝔮 ∈ V3› quotient_ring_def local.comm_ring_axioms
pr_ideal.submonoid_pr_ideal spectrum_def
by fastforce
have "f1 ∉ 𝔮" "s 𝔮 = q.frac r1 f1"
using q_V1 ‹𝔮 ∈ V3›  unfolding V3_def by auto
have "f2 ∉ 𝔮" "s' 𝔮 = q.frac r2 f2"
using q_V2 ‹𝔮 ∈ V3›  unfolding V3_def by auto

have "q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 ⋅ r2 ) (f1 ⋅ f2)"
apply (rule q.mult_rel_frac)
subgoal by (simp add: ‹f1 ∈ R› ‹f1 ∉ 𝔮› ‹r1 ∈ R› ‹r2 ∈ R›)
subgoal using ‹f2 ∈ R› ‹f2 ∉ 𝔮› ‹r2 ∈ R› by blast
done
then have "q.mult_rel (s 𝔮) (s' 𝔮) = q.frac r3 f3"
unfolding r3_def f3_def using ‹s 𝔮 = q.frac r1 f1› ‹s' 𝔮 = q.frac r2 f2›
by auto
then show "mult_sheaf_spec U s s' 𝔮 = q.frac r3 f3"
unfolding mult_sheaf_spec_def using ‹V3 ⊆ U› ‹𝔮 ∈ V3› by auto
show "f3 ∉ 𝔮" using that unfolding V3_def f3_def
using ‹f1 ∈ R› ‹f1 ∉ 𝔮› ‹f2 ∈ R› ‹f2 ∉ 𝔮› q.sub_composition_closed by auto
qed
ultimately show ?thesis using is_locally_frac_def by metis
qed
ultimately show ?thesis unfolding is_regular_def is_locally_frac_def by meson
qed

lemma mult_sheaf_spec_in_sheaf_spec:
assumes "s ∈ 𝒪 U" and "t ∈ 𝒪 U" and "U ⊆ Spec"
shows "mult_sheaf_spec U s t ∈ 𝒪 U"
proof -
have "mult_sheaf_spec U s t 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙"
if "𝔭 ∈ U" for 𝔭
proof -
interpret qr:quotient_ring "(R∖𝔭)" R "(+)" "(⋅)" 𝟬 𝟭
apply (rule spectrum_imp_cxt_quotient_ring)
using that ‹U ⊆ Spec› by auto
interpret pi:pr_ideal R 𝔭 "(+)" "(⋅)" 𝟬 𝟭
using that ‹U ⊆ Spec› by (auto intro:spectrum_imp_pr)
have "qr.valid_frac (s 𝔭)" "qr.valid_frac (t 𝔭)"
using sec_has_right_codom[OF _ that] ‹s ∈ 𝒪 U› ‹t ∈ 𝒪 U›
by (auto simp:pi.carrier_local_ring_at_def)
then show ?thesis
using that unfolding mult_sheaf_spec_def pi.carrier_local_ring_at_def
by auto
qed
moreover have "is_regular (mult_sheaf_spec U s t) U"
using ‹s ∈ 𝒪 U› ‹t ∈ 𝒪 U› ‹U ⊆ Spec› is_regular_mult_sheaf_spec
unfolding sheaf_spec_def by auto
moreover have "mult_sheaf_spec U s t ∈ extensional U"
unfolding mult_sheaf_spec_def by auto
ultimately show ?thesis
unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition uminus_sheaf_spec::"('a set) set ⇒ ('a set ⇒ ('a × 'a) set) ⇒ ('a set ⇒ ('a × 'a) set)"
where "uminus_sheaf_spec U s ≡ λ𝔭∈U. quotient_ring.uminus_rel (R ∖ 𝔭) R (+) (⋅) 𝟬 (s 𝔭) "

lemma is_regular_uminus_sheaf_spec:
assumes "is_regular s U" and "U ⊆ Spec"
shows "is_regular (uminus_sheaf_spec U s) U"
proof -
have "uminus_sheaf_spec U s 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙" if "𝔭 ∈ U" for 𝔭
proof -
interpret pi: pr_ideal R 𝔭 "(+)" "(⋅)" 𝟬 𝟭
using ‹U ⊆ Spec›[unfolded spectrum_def] ‹𝔭 ∈ U› by blast
interpret qr:quotient_ring "(R∖𝔭)"
by (simp add: quotient_ring_def local.comm_ring_axioms pi.submonoid_pr_ideal)

have "s 𝔭 ∈ pi.carrier_local_ring_at"
using ‹is_regular s U›
unfolding is_regular_def using that
using assms(2) frac_in_carrier_local in_mono is_locally_frac_def by fastforce
then show ?thesis
unfolding uminus_sheaf_spec_def pi.carrier_local_ring_at_def using that
by simp
qed
moreover have "(∃V⊆U. is_zariski_open V ∧ 𝔭 ∈ V ∧ is_locally_frac (uminus_sheaf_spec U s) V)"
if "𝔭 ∈ U" for 𝔭
proof -
obtain V1 r1 f1 where "V1 ⊆U" "is_zariski_open V1" "𝔭 ∈ V1" "r1 ∈ R" "f1 ∈ R" and
q_V1:"(∀𝔮. 𝔮 ∈ V1 ⟶ f1 ∉ 𝔮 ∧ s 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r1 f1)"
using ‹is_regular s U›[unfolded is_regular_def] ‹𝔭 ∈ U› unfolding is_locally_frac_def
by auto

define V3 where "V3 = V1 "
define r3 where "r3 = additive.inverse r1"
define f3 where "f3 = f1"
have "V3 ⊆U" "𝔭 ∈ V3" "r3 ∈ R" "f3 ∈ R"
unfolding V3_def r3_def f3_def
using ‹V1 ⊆ U› ‹𝔭 ∈ V1› ‹f1 ∈ R›  ‹r1 ∈ R› by blast+
moreover have "is_zariski_open V3"
using topological_space.open_inter by (simp add: V3_def ‹is_zariski_open V1›)
moreover have "f3 ∉ 𝔮"
"uminus_sheaf_spec U s 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r3 f3"
if "𝔮 ∈ V3" for 𝔮
proof -
interpret q:quotient_ring "R∖𝔮" R "(+)" "(⋅)" 𝟬
using ‹U ⊆ Spec› ‹V3 ⊆ U› ‹𝔮 ∈ V3› quotient_ring_def local.comm_ring_axioms
pr_ideal.submonoid_pr_ideal spectrum_def
by fastforce
have "f1 ∉ 𝔮" "s 𝔮 = q.frac r1 f1"
using q_V1 ‹𝔮 ∈ V3›  unfolding V3_def by auto

have "q.uminus_rel (q.frac r1 f1) = q.frac (additive.inverse r1) f1"
apply (rule q.uminus_rel_frac)
by (simp add: ‹f1 ∈ R› ‹f1 ∉ 𝔮› ‹r1 ∈ R›)
then have "q.uminus_rel (s 𝔮) = q.frac r3 f3"
unfolding r3_def f3_def using ‹s 𝔮 = q.frac r1 f1› by auto
then show "uminus_sheaf_spec U s 𝔮 = q.frac r3 f3"
unfolding uminus_sheaf_spec_def using ‹V3 ⊆ U› ‹𝔮 ∈ V3› by auto
show "f3 ∉ 𝔮" using that unfolding V3_def f3_def
using ‹f1 ∈ R› ‹f1 ∉ 𝔮› q.sub_composition_closed by auto
qed
ultimately show ?thesis using is_locally_frac_def by metis
qed
ultimately show ?thesis unfolding is_regular_def is_locally_frac_def by meson
qed

lemma uminus_sheaf_spec_in_sheaf_spec:
assumes "s ∈ 𝒪 U" and "U ⊆ Spec"
shows "uminus_sheaf_spec U s ∈ 𝒪 U"
proof -
have "uminus_sheaf_spec U s 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙"
if "𝔭 ∈ U" for 𝔭
proof -
interpret qr:quotient_ring "(R∖𝔭)" R "(+)" "(⋅)" 𝟬 𝟭
apply (rule spectrum_imp_cxt_quotient_ring)
using that ‹U ⊆ Spec› by auto
interpret pi:pr_ideal R 𝔭 "(+)" "(⋅)" 𝟬 𝟭
using that ‹U ⊆ Spec› by (auto intro:spectrum_imp_pr)
have "qr.valid_frac (s 𝔭)"
using sec_has_right_codom[OF _ that] ‹s ∈ 𝒪 U›
by (auto simp:pi.carrier_local_ring_at_def)
then show ?thesis
using that unfolding uminus_sheaf_spec_def pi.carrier_local_ring_at_def
by auto
qed
moreover have "is_regular (uminus_sheaf_spec U s) U"
using ‹s ∈ 𝒪 U›  ‹U ⊆ Spec› is_regular_uminus_sheaf_spec
unfolding sheaf_spec_def by auto
moreover have "uminus_sheaf_spec U s ∈ extensional U"
unfolding uminus_sheaf_spec_def by auto
ultimately show ?thesis
unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition zero_sheaf_spec:: "'a set set ⇒ ('a set ⇒ ('a × 'a) set)"
where "zero_sheaf_spec U ≡ λ𝔭∈U. quotient_ring.zero_rel (R ∖ 𝔭) R (+) (⋅) 𝟬 𝟭"

lemma is_regular_zero_sheaf_spec:
assumes "is_zariski_open U"
shows "is_regular (zero_sheaf_spec U) U"
proof -
have "zero_sheaf_spec U 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙" if "𝔭 ∈ U" for 𝔭
unfolding zero_sheaf_spec_def
using assms comm_ring.frac_in_carrier_local local.comm_ring_axioms pr_ideal.not_1
quotient_ring.zero_rel_def spectrum_imp_cxt_quotient_ring spectrum_imp_pr subsetD that
zariski_top_space.open_imp_subset by fastforce
moreover have "(∃V⊆U. is_zariski_open V ∧ 𝔭 ∈ V ∧ is_locally_frac (zero_sheaf_spec U) V)"
if "𝔭 ∈ U" for 𝔭
proof -
define V3 where "V3 = U"
define r3 where "r3 = 𝟬 "
define f3 where "f3 = 𝟭"
have "V3 ⊆U" "𝔭 ∈ V3" "r3 ∈ R" "f3 ∈ R"
unfolding V3_def r3_def f3_def using that by auto
moreover have "is_zariski_open V3" using assms by (simp add: V3_def)
moreover have "f3 ∉ 𝔮"
"zero_sheaf_spec U 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r3 f3"
if "𝔮 ∈ V3" for 𝔮
subgoal using V3_def assms f3_def pr_ideal.submonoid_pr_ideal spectrum_def
submonoid.sub_unit_closed that zariski_open_is_subset by fastforce
subgoal
proof -
interpret q:quotient_ring "R∖𝔮" R
using V3_def assms quotient_ring_def local.comm_ring_axioms
pr_ideal.submonoid_pr_ideal spectrum_def that zariski_open_is_subset by fastforce
show ?thesis unfolding zero_sheaf_spec_def
using V3_def f3_def q.zero_rel_def r3_def that by auto
qed
done
ultimately show ?thesis using is_locally_frac_def  by metis
qed
ultimately show ?thesis unfolding is_regular_def is_locally_frac_def  by meson
qed

lemma zero_sheaf_spec_in_sheaf_spec:
assumes "is_zariski_open U"
shows "zero_sheaf_spec U ∈ 𝒪 U"
proof -
have "zero_sheaf_spec U 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙"if "𝔭 ∈ U" for 𝔭
proof -
interpret qr:quotient_ring "(R∖𝔭)" R "(+)" "(⋅)" 𝟬 𝟭
by (meson assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
spectrum_imp_cxt_quotient_ring subsetD that)
interpret pi:pr_ideal R 𝔭 "(+)" "(⋅)" 𝟬 𝟭
by (meson assms spectrum_imp_pr subsetD that zariski_open_is_subset)
show ?thesis unfolding zero_sheaf_spec_def pi.carrier_local_ring_at_def
using that by auto
qed
moreover have "is_regular (zero_sheaf_spec U) U"
using is_regular_zero_sheaf_spec assms by auto
moreover have "zero_sheaf_spec U ∈ extensional U"
ultimately show ?thesis unfolding sheaf_spec_def by (simp add: PiE_iff)
qed

definition one_sheaf_spec:: "'a set set ⇒ ('a set ⇒ ('a × 'a) set)"
where "one_sheaf_spec U ≡ λ𝔭∈U. quotient_ring.one_rel (R ∖ 𝔭) R (+) (⋅) 𝟬 𝟭"

lemma is_regular_one_sheaf_spec:
assumes "is_zariski_open U"
shows "is_regular (one_sheaf_spec U) U"
proof -
have "one_sheaf_spec U 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙" if "𝔭 ∈ U" for 𝔭
unfolding one_sheaf_spec_def
by (smt assms closed_subsets_zero comm_ring.closed_subsets_def
quotient_ring.carrier_quotient_ring_iff quotient_ring.valid_frac_one
quotient_ring_def local.comm_ring_axioms mem_Collect_eq
pr_ideal.carrier_local_ring_at_def pr_ideal.submonoid_pr_ideal
restrict_apply subsetD that zariski_open_is_subset)
moreover have "(∃V⊆U. is_zariski_open V ∧ 𝔭 ∈ V ∧ is_locally_frac (one_sheaf_spec U) V)"
if "𝔭 ∈ U" for 𝔭
proof -
define V3 where "V3 = U"
define r3 where "r3 = 𝟭"
define f3 where "f3 = 𝟭"
have "V3 ⊆U" "𝔭 ∈ V3" "r3 ∈ R" "f3 ∈ R"
unfolding V3_def r3_def f3_def using that by auto
moreover have "is_zariski_open V3" using assms by (simp add: V3_def)
moreover have "f3 ∉ 𝔮"
"one_sheaf_spec U 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 r3 f3"
if "𝔮 ∈ V3" for 𝔮
subgoal using V3_def assms f3_def pr_ideal.submonoid_pr_ideal spectrum_def
submonoid.sub_unit_closed that zariski_open_is_subset by fastforce
subgoal
proof -
interpret q:quotient_ring "R∖𝔮" R
using V3_def assms quotient_ring_def local.comm_ring_axioms
pr_ideal.submonoid_pr_ideal spectrum_def that zariski_open_is_subset by fastforce
show ?thesis unfolding one_sheaf_spec_def
using V3_def f3_def q.one_rel_def r3_def that by auto
qed
done
ultimately show ?thesis using is_locally_frac_def by metis
qed
ultimately show ?thesis unfolding is_regular_def is_locally_frac_def by meson
qed

lemma one_sheaf_spec_in_sheaf_spec:
assumes "is_zariski_open U"
shows "one_sheaf_spec U ∈ 𝒪 U"
proof -
have "one_sheaf_spec U 𝔭 ∈ R ⇘𝔭 (+) (⋅) 𝟬⇙"if "𝔭 ∈ U" for 𝔭
proof -
interpret qr:quotient_ring "(R∖𝔭)" R "(+)" "(⋅)" 𝟬 𝟭
by (meson assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
spectrum_imp_cxt_quotient_ring subsetD that)
interpret pi:pr_ideal R 𝔭 "(+)" "(⋅)" 𝟬 𝟭
by (meson assms spectrum_imp_pr subsetD that zariski_open_is_subset)
show ?thesis unfolding one_sheaf_spec_def pi.carrier_local_ring_at_def
using that by auto
qed
moreover have "is_regular (one_sheaf_spec U) U"
using is_regular_one_sheaf_spec assms by auto
moreover have "one_sheaf_spec U ∈ extensional U"
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

"add_sheaf_spec U a b ∈ extensional U"

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
and "mult_sheaf_spec U a b ∈ 𝒪 U"
if "a ∈ 𝒪 U" "b ∈ 𝒪 U" for a b
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
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
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
unfolding add_sheaf_spec_def using ‹𝔭 ∈ U›
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›
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
if "a ∈ 𝒪 U" for a

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))

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) 𝔭"
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
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›
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"
then show "add_sheaf_spec U u (uminus_sheaf_spec U u) 𝔭 = zero_sheaf_spec U 𝔭"
using ‹𝔭 ∈ U› by simp
qed auto
then show "add_sheaf_spec U (uminus_sheaf_spec U u) u = zero_sheaf_spec U"
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
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)"
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)
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"
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)"
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)"
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
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
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
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
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"
ultimately show "s = zero_sheaf_spec U" using extensionalityI by blast
next
fix U I V s assume H: "open_cover_of_open_subset Spec is_zariski_open U I V"
"∀i. i ∈ I ⟶ V i ⊆ U ∧ s i ∈ 𝒪 (V i)"
"⋀i j. i ∈ I ⟹
j ∈ I ⟹
sheaf_spec_morphisms (V i) (V i ∩ V j) (s i) =
sheaf_spec_morphisms (V j) (V i ∩ V j) (s j)"
define t where D: "t ≡ λ𝔭∈U. s (cover_of_subset.select_index I V 𝔭) 𝔭"
then have F1: "s i 𝔭 = s j 𝔭" if "i ∈ I" "j ∈ I" "𝔭 ∈ V i" "𝔭 ∈ V j" for 𝔭 i j
proof -
have "s i 𝔭 = sheaf_spec_morphisms (V i) (V i ∩ V j) (s i) 𝔭"
using that sheaf_spec_morphisms_def by (simp add: H(2))
moreover have "… = sheaf_spec_morphisms (V j) (V i ∩ V j) (s j) 𝔭"
using H(3) that by fastforce
moreover have "… = s j 𝔭"
using sheaf_spec_morphisms_def that by (simp add: H(2))
ultimately show "s i 𝔭 = s j 𝔭" by blast
qed
have "t ∈ 𝒪 U"
proof-
have "t 𝔭 ∈ (R⇘𝔭 (+) (⋅) 𝟬⇙)" if "𝔭∈U" for 𝔭
using D H(1) H(2) cover_of_subset.cover_of_select_index
cover_of_subset.select_index_belongs open_cover_of_open_subset.axioms(1)
open_cover_of_subset_def sec_has_right_codom that by fastforce
moreover have "t ∈ extensional U"
using D by blast
moreover have "is_regular t U"
unfolding is_regular_def
proof (intro strip conjI)
fix 𝔭
assume "𝔭 ∈ U"
show "∃V. is_zariski_open V ∧ V ⊆ U ∧ 𝔭 ∈ V ∧ is_locally_frac t V"
proof -
have cov_in_I: "cover_of_subset.select_index I V 𝔭 ∈ I"
by (meson H(1) ‹𝔭 ∈ U› cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def)
have V: "V (cover_of_subset.select_index I V 𝔭) ⊆ U"
using H(2) by (meson H(1) ‹𝔭 ∈ U› cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def)
have V2: "∃V'. is_zariski_open V' ∧ V'⊆ V (cover_of_subset.select_index I V 𝔭) ∧ 𝔭 ∈ V' ∧
is_locally_frac (s (cover_of_subset.select_index I V 𝔭)) V'"
using H(1,2)
unfolding sheaf_spec_def open_cover_of_open_subset_def open_cover_of_subset_def is_regular_def
using ‹𝔭 ∈ U› cov_in_I cover_of_subset.cover_of_select_index by fastforce
have "⋀V' 𝔮. is_zariski_open V' ∧ V' ⊆ V (cover_of_subset.select_index I V 𝔭) ⟹ 𝔮 ∈ V' ⟹ t 𝔮 = s (cover_of_subset.select_index I V 𝔭) 𝔮"
by (smt D F1 H(1) V ‹𝔭 ∈ U› cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs open_cover_of_open_subset_def open_cover_of_subset_def restrict_apply subsetD)
with V V2 show ?thesis unfolding is_locally_frac_def
by (smt subset_trans)
qed
qed
ultimately show ?thesis unfolding sheaf_spec_def by (simp add:PiE_iff)
qed
have "sheaf_spec_morphisms U (V i) t = s i" if "i ∈ I" for i
proof
fix 𝔭
have "sheaf_spec_morphisms U (V i) t 𝔭 = s i 𝔭" if "𝔭 ∈ U"
proof-
from that H(1)
obtain j where "j ∈ I ∧ 𝔭 ∈ V j ∧ t 𝔭 = s j 𝔭"
unfolding D open_cover_of_subset_def open_cover_of_open_subset_def
by (meson cover_of_subset.cover_of_select_index cover_of_subset.select_index_belongs restrict_apply')
thus "sheaf_spec_morphisms U (V i) t 𝔭 = s i 𝔭"
using ‹t ∈ 𝒪 U› ‹i ∈ I› H(2) that
unfolding sheaf_spec_morphisms_def
apply (simp add: D split: if_split_asm)
by (metis (mono_tags, hide_lams) F1  extensional_arb [OF sec_is_extensional])
qed
thus "sheaf_spec_morphisms U (V i) t 𝔭 = s i 𝔭"
using sheaf_spec_morphisms_def D F1
by (smt H(2) ‹i ∈ I› ‹t ∈ 𝒪 U› comm_ring.sheaf_morphisms_sheaf_spec local.comm_ring_axioms restrict_apply subsetD)
qed
thus "∃t. t ∈ (𝒪 U) ∧ (∀i. i ∈ I ⟶ sheaf_spec_morphisms U (V i) t = s i)"
using ‹t ∈ 𝒪 U› by blast
qed

lemma shrinking:
assumes "is_zariski_open U" and "𝔭 ∈ U" and "s ∈ 𝒪 U" and "t ∈ 𝒪 U"
obtains V a f b g where "is_zariski_open V" "V ⊆ U" "𝔭 ∈ V" "a ∈ R" "f ∈ R" "b ∈ R" "g ∈ R"
"f ∉ 𝔭" "g ∉ 𝔭"
"⋀𝔮. 𝔮 ∈ V ⟹ f ∉ 𝔮 ∧ s 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 a f"
"⋀𝔮. 𝔮 ∈ V ⟹ g ∉ 𝔮 ∧ t 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 b g"
proof-
obtain Vs a f where "is_zariski_open Vs" "Vs ⊆ U" "𝔭 ∈ Vs" "a ∈ R" "f ∈ R"
"⋀𝔮. 𝔮 ∈ Vs ⟹ f ∉ 𝔮 ∧ s 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 a f"
using assms(2,3) sheaf_spec_def is_regular_def is_locally_frac_def by auto
obtain Vt b g where "is_zariski_open Vt" "Vt ⊆ U" "𝔭 ∈ Vt" "b ∈ R" "g ∈ R"
"⋀𝔮. 𝔮 ∈ Vt ⟹ g ∉ 𝔮 ∧ t 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 b g"
using assms(2,4) sheaf_spec_def is_regular_def is_locally_frac_def by auto
then have "is_zariski_open (Vs ∩ Vt)" "Vs ∩ Vt ⊆ U" "𝔭 ∈ Vs ∩ Vt"
"⋀𝔮. 𝔮 ∈ (Vs ∩ Vt) ⟹ f ∉ 𝔮 ∧ s 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 a f"
"⋀𝔮. 𝔮 ∈ (Vs ∩ Vt) ⟹ g ∉ 𝔮 ∧ t 𝔮 = quotient_ring.frac (R∖𝔮) R (+) (⋅) 𝟬 b g"
using topological_space.open_inter apply (simp add: ‹is_zariski_open Vs›)
using ‹Vs ⊆ U› apply auto 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
proof (intro ringed_space.intro)
show "sheaf_of_rings Spec is_zariski_open sheaf_spec sheaf_spec_morphisms 𝒪b
using sheaf_spec_is_sheaf by simp
qed

end (* comm_ring *)

(* definition 0.33 *)
locale morphism_ringed_spaces =
im_sheaf X is_open⇩X 𝒪⇩X ρ⇩X b add_str⇩X mult_str⇩X zero_str⇩X one_str⇩X Y is_open⇩Y f +
codom: ringed_space Y is_open⇩Y 𝒪⇩Y ρ⇩Y d add_str⇩Y mult_str⇩Y zero_str⇩Y one_str⇩Y
for X and is_open⇩X and 𝒪⇩X and ρ⇩X and b and add_str⇩X and mult_str⇩X and zero_str⇩X and one_str⇩X
and Y and is_open⇩Y and 𝒪⇩Y and ρ⇩Y and d and add_str⇩Y and mult_str⇩Y and zero_str⇩Y and one_str⇩Y
and f +
fixes φ⇩f:: "'c set ⇒ ('d ⇒ 'b)"
assumes is_morphism_of_sheaves: "morphism_sheaves_of_rings
Y is_open⇩Y 𝒪⇩Y ρ⇩Y d add_str⇩Y mult_str⇩Y zero_str⇩Y one_str⇩Y
im_sheaf im_sheaf_morphisms b add_im_sheaf mult_im_sheaf zero_im_sheaf one_im_sheaf
φ⇩f"

subsection ‹Direct Limits of Rings›

(* construction 0.34 *)
locale direct_lim = sheaf_of_rings +
fixes I:: "'a set set"
assumes subset_of_opens: "⋀U. U ∈ I ⟹ is_open U"
and has_lower_bound: "⋀U V. ⟦ U∈I; V∈I ⟧ ⟹ ∃W∈I. W ⊆ U ∩ V"
begin

definition get_lower_bound:: "'a set ⇒ 'a set ⇒ 'a set" where
"get_lower_bound U V= (SOME W. W ∈ I ∧ W ⊆ U ∧ W ⊆ V)"

lemma get_lower_bound[intro]:
assumes "U ∈ I" "V ∈ I"
shows "get_lower_bound U V ∈ I" "get_lower_bound U V ⊆ U" "get_lower_bound U V ⊆ V"
proof -
have "∃W. W ∈ I ∧ W ⊆ U ∧ W ⊆ V"
using has_lower_bound[OF assms] by auto
from someI_ex[OF this]
show "get_lower_bound U V ∈ I" "get_lower_bound U V ⊆ U" "get_lower_bound U V ⊆ V"
unfolding get_lower_bound_def by auto
qed

lemma obtain_lower_bound_finite:
assumes "finite Us"  "Us ≠ {}" "Us ⊆ I"
obtains W where "W ∈ I" "∀U∈Us. W ⊆ U"
using assms
proof (induct Us arbitrary:thesis)
case (insert U F)
have ?case when "F={}"
using insert.prems(1) insert.prems(3) that by blast
moreover have ?case when "F≠{}"
proof -
obtain W where "W ∈ I" "∀U∈F. W ⊆ U"
using insert.hyps(3) insert.prems(3) by auto
obtain W1 where "W1 ∈I" "W1 ⊆ U" "W1 ⊆ W"
by (meson ‹W ∈ I› get_lower_bound(1) get_lower_bound(2) get_lower_bound(3)
insert.prems(3) insert_subset)
then have "∀a∈insert U F. W1 ⊆ a"
using ‹∀U∈F. W ⊆ U› by auto
with ‹W1 ∈I› show ?thesis
using insert(4) by auto
qed
ultimately show ?case by auto
qed simp

definition principal_subs :: "'a set set ⇒ 'a set ⇒ 'a set filter" where
"principal_subs As A = Abs_filter (λP. ∀x. (x∈As ∧ x ⊆ A) ⟶ P x)"

lemma eventually_principal_subs: "eventually P (principal_subs As A) ⟷ (∀x. x∈As ∧ x⊆A ⟶ P x)"
unfolding principal_subs_def
by (rule eventually_Abs_filter, rule is_filter.intro) auto

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

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

lemma principal_subs_le_iff[iff]:
"principal_subs As A ≤ principal_subs As' A'
⟷ {x. x∈As ∧ x ⊆ A} ⊆ {x. x∈As' ∧ x ⊆ A'}"
unfolding le_filter_def eventually_principal_subs by blast

lemma principal_subs_eq_iff[iff]:
"principal_subs As A = principal_subs As' A' ⟷{x. x∈As ∧ x ⊆ A} = {x. x∈As' ∧ x ⊆ A'}"
unfolding eq_iff by simp

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

definition lbound :: "'a set set ⇒ ('a set) filter" where
"lbound Us = (INF S∈{S. S∈I ∧ (∀u∈Us. S ⊆ u)}. principal_subs I S)"

lemma eventually_lbound_finite:
assumes "finite A" "A≠{}" "A⊆I"
shows "(∀⇩F w in lbound A. P w) ⟷ (∃w0. w0 ∈ I ∧ (∀a∈A. w0 ⊆ a) ∧ (∀w. (w⊆w0 ∧ w∈I) ⟶ P w))"
proof -
have "∃x. x ∈ I ∧ (∀xa∈A. x ⊆ xa)"
by (metis Int_iff assms inf.order_iff obtain_lower_bound_finite)
moreover have " ∃x. x ∈ I ∧ Ball A ((⊆) x)
∧ {xa ∈ I. xa ⊆ x} ⊆ {x ∈ I. x ⊆ a}
∧ {xa ∈ I. xa ⊆ x} ⊆ {x ∈ I. x ⊆ b}"
if "a ∈ I ∧ (∀x∈A. a ⊆ x)" "b ∈ I ∧ (∀x∈A. b ⊆ x)" for a b
apply (rule exI[where x="get_lower_bound a b"])
using that apply auto
subgoal using get_lower_bound(2) by blast
subgoal by (meson get_lower_bound(2) subsetD)
subgoal by (meson get_lower_bound(3) subsetD)
done
moreover have "(∃b∈{S ∈ I. Ball A ((⊆) S)}. eventually P (principal_subs I b)) =
(∃w0. w0 ∈ I ∧ Ball A ((⊆) w0) ∧ (∀w. w ⊆ w0 ∧ w ∈ I ⟶ P w))"
unfolding eventually_principal_subs by force
ultimately show ?thesis unfolding lbound_def
by (subst eventually_INF_base) auto
qed

lemma lbound_eq:
assumes A:"finite A" "A≠{}" "A⊆I"
assumes B:"finite B" "B≠{}" "B⊆I"
shows "lbound A = lbound B"
proof -
have "eventually P (lbound A')" if "eventually P (lbound B')"
and A':"finite A'" "A'≠{}" "A' ⊆ I"
and B':"finite B'" "B'≠{}" "B' ⊆ I"
for P A' B'
proof -
obtain w0 where w0:"w0 ∈ I" "(∀a∈B'. w0 ⊆ a)" "(∀w. w ⊆ w0 ∧ w ∈ I ⟶ P w)"
using ‹eventually P (lbound B')› unfolding eventually_lbound_finite[OF B',of P]
by auto
obtain w1 where w1:"w1 ∈ I" "∀U∈A'. w1 ⊆ U"
using obtain_lower_bound_finite[OF A'] by auto
define w2 where "w2=get_lower_bound w0 w1"
have "w2 ∈ I" using ‹w0 ∈ I› ‹w1 ∈ I› unfolding w2_def by auto
moreover have "∀a∈A'. w2 ⊆ a"
unfolding w2_def by (meson dual_order.trans get_lower_bound(3) w0(1) w1(1) w1(2))
moreover have "∀w. w ⊆ w2 ∧ w ∈ I ⟶ P w"
unfolding w2_def by (meson dual_order.trans get_lower_bound(2) w0(1) w0(3) w1(1))
ultimately show ?thesis unfolding eventually_lbound_finite[OF A',of P] by auto
qed
then have "eventually P (lbound A) = eventually P (lbound B)" for P
using A B by auto
then show ?thesis unfolding filter_eq_iff by auto
qed

lemma lbound_leq:
assumes "A ⊆ B"
shows "lbound A ≤lbound B"
unfolding lbound_def
apply (rule Inf_superset_mono)
apply (rule image_mono)
using assms by auto

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

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

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

definition rel:: "('a set × 'b) ⇒ ('a set × 'b) ⇒ bool" (infix "∼" 80)
where "x ∼ y ≡ (fst x ∈ I ∧ fst y ∈ I) ∧ (snd x ∈ 𝔉 (fst x) ∧ snd y ∈ 𝔉 (fst y)) ∧
(∃W. (W ∈ I) ∧ (W ⊆ fst x ∩ fst y) ∧ ρ (fst x) W (snd x) = ρ (fst y) W (snd y))"

lemma rel_is_equivalence:
shows "equivalence (Sigma I 𝔉) {(x, y). x ∼ y}"
unfolding equivalence_def
proof (intro conjI strip)
show "(a, c) ∈ {(x, y). x ∼ y}"
if "(a, b) ∈ {(x, y). x ∼ y}" "(b, c) ∈ {(x, y). x ∼ y}" for a b c
proof -
obtain W1 where W1:"fst a ∈ I" "fst b ∈ I" "snd a ∈ 𝔉 (fst a)" "snd b ∈ 𝔉 (fst b)"
"W1 ∈ I" "W1 ⊆ fst a" "W1 ⊆ fst b"
"ρ (fst a) W1 (snd a) = ρ (fst b) W1 (snd b)"
using ‹(a, b) ∈ {(x, y). x ∼ y}› unfolding rel_def by auto
obtain W2 where W2:"fst b ∈ I" "fst c ∈ I" "snd b ∈ 𝔉 (fst b)" "snd c ∈ 𝔉 (fst c)"
"W2 ∈ I" "W2 ⊆ fst b" "W2 ⊆ fst c"
"ρ (fst b) W2 (snd b) = ρ (fst c) W2 (snd c)"
using ‹(b, c) ∈ {(x, y). x ∼ y}› unfolding rel_def by auto
obtain W3 where W3:"W3 ∈I" "W3 ⊆ W1 ∩ W2"
using has_lower_bound[OF ‹W1∈I› ‹W2∈I›] by auto
from ‹W3 ⊆ W1 ∩ W2›
have "W3 ⊆ fst a ∩ fst c" using W1(6) W2(7) by blast
moreover have "ρ (fst a) W3 (snd a) = ρ (fst c) W3 (snd c)"
using W1 W2 by (metis W3(1) W3(2) eq_ρ le_inf_iff subset_of_opens)
moreover note ‹W3 ∈I› W1 W2
ultimately show ?thesis
unfolding rel_def by auto
qed
qed (auto simp: rel_def Int_commute)

interpretation rel:equivalence "(Sigma I 𝔉)" "{(x, y). x ∼ y}"
using rel_is_equivalence .

definition class_of:: "'a set ⇒ 'b ⇒ ('a set × 'b) set" ("⌊(_,/ _)⌋")
where "⌊U,s⌋ ≡ rel.Class (U, s)"

lemma class_of_eqD:
assumes "⌊U1,s1⌋ = ⌊U2,s2⌋" "(U1,s1) ∈ Sigma I 𝔉" "(U2,s2) ∈ Sigma I 𝔉"
obtains W where "W ∈ I" "W ⊆ U1 ∩ U2" "ρ U1 W s1 = ρ U2 W s2"
using rel.Class_equivalence[OF assms(2,3)] assms(1)
unfolding class_of_def rel_def by auto

lemma class_of_eqI:
assumes "(U1,s1) ∈ Sigma I 𝔉" "(U2,s2) ∈ Sigma I 𝔉"
assumes "W ∈ I" "W ⊆ U1 ∩ U2" "ρ U1 W s1 = ρ U2 W s2"
shows "⌊U1,s1⌋ = ⌊U2,s2⌋"
unfolding class_of_def
apply (rule rel.Class_eq)
using assms  by (auto simp: rel_def)

lemma class_of_0_in:
assumes "U ∈ I"
shows "𝟬⇘U⇙ ∈ 𝔉 U"
proof -
have "ring (𝔉 U) +⇘U⇙ ⋅⇘U⇙ 𝟬⇘U⇙ 𝟭⇘U⇙"
using assms subset_of_opens is_ring_from_is_homomorphism by blast
then show ?thesis
unfolding ring_def abelian_group_def Group_Theory.group_def by (meson monoid.unit_closed)
qed

lemma rel_Class_iff: "x ∼ y ⟷ y ∈ Sigma I 𝔉 ∧ x ∈ rel.Class y"
by blast

lemma class_of_0_eq:
assumes "U ∈ I" "U' ∈ I"
shows "⌊U, 𝟬⇘U⇙⌋ = ⌊U', 𝟬⇘U'⇙⌋"
proof -
obtain W where W: "W ∈ I" "W ⊆ U" "W ⊆ U'"
by (metis Int_subset_iff assms has_lower_bound)
then have "is_open W" "is_open U" "is_open U'"
by (auto simp add: assms subset_of_opens)
then have "ρ U W 𝟬⇘U⇙ = ρ U' W 𝟬⇘U'⇙"
using W is_ring_morphism [of U W] is_ring_morphism [of U' W]
by (simp add: ring_homomorphism_def group_homomorphism_def monoid_homomorphism_def
monoid_homomorphism_axioms_def)
with W have "∃W. W ∈ I ∧ W ⊆ U ∧ W ⊆ U' ∧ ρ U W 𝟬⇘U⇙ = ρ U' W 𝟬⇘U'⇙" by blast
moreover have "𝟬⇘U⇙ ∈ 𝔉 U" "𝟬⇘U'⇙ ∈ 𝔉 U'"
by (auto simp add: assms class_of_0_in)
ultimately have "(U, 𝟬⇘U⇙) ∼ (U', 𝟬⇘U'⇙)"
using assms by (auto simp: rel_def)
then show ?thesis
unfolding class_of_def by (simp add: rel.Class_eq)
qed

lemma class_of_1_in:
assumes "U ∈ I"
shows "𝟭⇘U⇙ ∈ 𝔉 U"
proof -
have "ring (𝔉 U) +⇘U⇙ ⋅⇘U⇙ 𝟬⇘U⇙ 𝟭⇘U⇙"
using assms subset_of_opens is_ring_from_is_homomorphism by blast
then show ?thesis
unfolding ring_def by (meson monoid.unit_closed)
qed

lemma class_of_1_eq:
assumes "U ∈ I" and "U' ∈ I"
shows "⌊U, 𝟭⇘U⇙⌋ = ⌊U', 𝟭⇘U'⇙⌋"
proof -
obtain W where W: "W ∈ I" "W ⊆ U" "W ⊆ U'"
by (metis Int_subset_iff assms has_lower_bound)
then have "is_open W" "is_open U" "is_open U'"
by (auto simp add: assms subset_of_opens)
then have "ρ U W 𝟭⇘U⇙ = ρ U' W 𝟭⇘U'`