(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2022 Daniel de la Concepcion This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Rings - Zariski Topology› text‹This file deals with the definition of the topology on the set of prime ideals› text‹It defines the topology, computes the closed sets and the closure and interior operators› theory Ring_Zariski_ZF imports Ring_ZF_2 Topology_ZF begin text‹The set where the topology is defined is in the spectrum of a ring; i.e. the set of all prime ideals.› definition (in ring0) Spec where "Spec ≡ {I∈ℐ. I◃⇩_{p}R}" text‹The basic set that defines the topoogy is given by the D operator› definition (in ring0) openBasic ("D") where "S⊆R ⟹ D(S) ≡ {I∈Spec. ¬(S⊆I)}" text‹The D operator preserves subsets› lemma (in ring0) D_operator_preserve_subset: assumes "S ⊆ T" "T⊆R" shows "D(S) ⊆ D(T)" proof from assms have S:"S⊆R" by auto fix x assume "x∈D(S)" then have x:"x∈Spec" "¬(S⊆x)" using openBasic_def S by auto with assms(1) have "x∈Spec" "¬(T⊆x)" by auto then show "x:D(T)" using openBasic_def assms(2) by auto qed text‹The D operator values can be obtained by considering only ideals. This is useful as we have operations on ideals that we do not have on subsets.› lemma (in ring0) D_operator_only_ideals: assumes "T⊆R" shows "D(T) = D(⟨T⟩⇩_{I})" proof have T:"T⊆⟨T⟩⇩_{I}" "⟨T⟩⇩_{I}⊆R" using generated_ideal_contains_set assms generated_ideal_is_ideal[OF assms] ideal_dest_subset by auto with D_operator_preserve_subset show "D(T) ⊆ D(⟨T⟩⇩_{I})" by auto { fix t assume "t∈D(⟨T⟩⇩_{I})" with T(2) have t:"t∈Spec" "¬(⟨T⟩⇩_{I}⊆t)" using openBasic_def by auto { assume as:"T ⊆ t" from t(1) have "t◃R" unfolding Spec_def primeIdeal_def by auto with as have "⟨T⟩⇩_{I}⊆t" using generated_ideal_small by auto with t(2) have False by auto } then have "¬(T ⊆ t)" by auto with t(1) have "t∈D(T)" using openBasic_def assms by auto } then show "D(⟨T⟩⇩_{I}) ⊆ D(T)" by auto qed text‹The intersection of to D-sets is the D-set on the product of ideals› lemma (in ring0) intersection_open_basic: assumes "I◃R" "J◃R" shows "D(I)∩D(J) = D(I⋅⇩_{I}J)" proof have S:"I⋅⇩_{I}J ⊆ R" using product_in_intersection(2) ideal_dest_subset assms by auto { fix K assume K:"K∈D(I)∩D(J)" then have "K◃⇩_{p}R" "¬(I⊆K)" "¬(J⊆K)" using assms ideal_dest_subset openBasic_def unfolding Spec_def by auto then have "¬(I⊆K)" "¬(J⊆K)" "∀I∈ℐ. ∀J∈ℐ. I⋅⇩_{I}J⊆K ⟶ I ⊆ K ∨ J ⊆ K" unfolding primeIdeal_def by auto then have "¬(I⋅⇩_{I}J⊆K)" using assms using ideal_dest_subset[of I] ideal_dest_subset[of J] by auto moreover note K ultimately have "K∈D(I⋅⇩_{I}J)" using openBasic_def[of "I"] ideal_dest_subset[OF assms(1)] unfolding Spec_def openBasic_def[OF S] by auto } then show "D(I)∩D(J) ⊆ D(I⋅⇩_{I}J)" by auto { fix K assume Kass:"K∈D(I⋅⇩_{I}J)" then have K:"K◃⇩_{p}R" "¬(I⋅⇩_{I}J⊆K)" using openBasic_def[OF S] unfolding Spec_def by auto { assume "I ⊆ K ∨ J ⊆K" then have "I∩J ⊆ K" by auto then have "I⋅⇩_{I}J⊆K" using product_in_intersection assms by auto with K(2) have False by auto } then have "¬(I⊆K)" "¬(J⊆K)" by auto with Kass have "K∈D(I)∩D(J)" using assms ideal_dest_subset openBasic_def[of I] openBasic_def[of J] unfolding openBasic_def[OF S] Spec_def by auto } then show "D(I ⋅⇩_{I}J) ⊆ D(I) ∩ D(J)" by auto qed text‹The union of D-sets is the D-set of the sum of the ideals› lemma (in ring0) union_open_basic: assumes "𝒥 ⊆ ℐ" shows "⋃{D(I). I∈𝒥} = D(⊕⇩_{I}𝒥)" proof have S:"(⊕⇩_{I}𝒥) ⊆ R" using generated_ideal_is_ideal[of "⋃𝒥"] assms unfolding sumArbitraryIdeals_def[OF assms] using ideal_dest_subset by auto { fix t assume "t∈⋃{D(I). I∈𝒥}" then obtain K where K:"K∈𝒥" "t∈D(K)" by auto then have t:"t◃⇩_{p}R" "¬(K⊆t)" using assms openBasic_def unfolding Spec_def by auto { assume "(⊕⇩_{I}𝒥) ⊆ t" then have "⋃𝒥 ⊆ t" using generated_ideal_contains_set[of "⋃𝒥"] assms unfolding sumArbitraryIdeals_def[OF assms] by auto with K(1) have "K ⊆ t" by auto with t(2) have False by auto } then have "¬((⊕⇩_{I}𝒥) ⊆ t)" by auto moreover note K S ultimately have "t∈D(⊕⇩_{I}𝒥)" using openBasic_def[of K] openBasic_def[of "⊕⇩_{I}𝒥"] assms by auto } then show "⋃{D(I). I∈𝒥} ⊆ D(⊕⇩_{I}𝒥)" by auto { fix t assume as:"t∈D(⊕⇩_{I}𝒥)" then have t:"t∈Spec" "¬((⊕⇩_{I}𝒥)⊆t)" unfolding openBasic_def[OF S] by auto { assume "⋃𝒥 ⊆ t" with t(1) have "⟨⋃𝒥⟩⇩_{I}⊆ t" using generated_ideal_small unfolding Spec_def primeIdeal_def by auto with t(2) have False unfolding sumArbitraryIdeals_def[OF assms] by auto } then obtain J where J:"¬(J ⊆ t)" "J∈𝒥" by auto note J(1) moreover have "J⊆R" using `J∈𝒥` assms by auto moreover note t(1) ultimately have "t∈D(J)" using openBasic_def[of J] by auto then have "t:⋃{D(I). I∈𝒥}" using J(2) by auto } then show "D(⊕⇩_{I}𝒥) ⊆ ⋃{D(I). I∈𝒥}" by auto qed text‹From the previous results on intesertion and union, we conclude that the D-sets we computed form a topology› corollary (in ring0) zariski_top: shows "{D(J). J∈ℐ}{is a topology}" unfolding IsATopology_def proof(safe) fix M assume "M ⊆ {D(J). J∈ℐ}" then have "M = {D(J). J∈{K∈ℐ. D(K)∈M}}" by auto then have "⋃M = ⋃{D(J). J∈{K∈ℐ. D(K)∈M}}" by auto then have "⋃M = D(⊕⇩_{I}{K∈ℐ. D(K)∈M})" using union_open_basic[of "{K ∈ ℐ . D(K) ∈ M}"] by auto moreover have "(⊕⇩_{I}{K∈ℐ. D(K)∈M})◃R" using generated_ideal_is_ideal[of "⋃{K∈ℐ. D(K)∈M}"] sumArbitraryIdeals_def [of "{K∈ℐ. D(K)∈M}"] by force then have "(⊕⇩_{I}{K∈ℐ. D(K)∈M})∈ℐ" using ideal_dest_subset by auto ultimately show "⋃M:{D(J). J∈ℐ}" by auto next fix x xa assume as:"x◃R" "xa◃R" then have "D(x) ∩ D(xa) = D(x⋅⇩_{I}xa)" using intersection_open_basic by auto moreover have "(x⋅⇩_{I}xa) ◃R" using product_in_intersection(2) as by auto then have "(x⋅⇩_{I}xa):ℐ" using ideal_dest_subset by auto ultimately show "D(x) ∩ D(xa)∈{D(J). J∈ℐ}" by auto qed text‹We include all the results of topology0 into ring0 under the namespace "zariski"› definition(in ring0) ZarInt ("int") where "int(U) ≡ Interior(U,{D(J). J∈ℐ})" definition (in ring0) ZarCl ("cl") where "cl(U) ≡ Closure(U,{D(J). J∈ℐ})" definition (in ring0) ZarBound ("∂_") where "∂U ≡ Boundary(U,{D(J). J∈ℐ})" sublocale ring0 < zariski:topology0 "{D(J). J∈ℐ}" ZarInt ZarCl ZarBound unfolding topology0_def ZarBound_def ZarInt_def ZarCl_def using zariski_top by auto text‹The interior of a proper subset is given by the D-set of the intersection of all the prime ideals not in that subset› lemma (in ring0) interior_zariski: assumes "U ⊆ Spec" "U≠Spec" shows "int(U) = D(⋂(Spec-U))" proof { fix t assume t:"t∈⋂(Spec-U)" then have "∀V∈Spec-U. t:V" by auto moreover from t have "(Spec-U) ≠0" by auto ultimately obtain V where "V∈Spec-U" "t∈V" by auto then have "t∈⋃Spec" by auto then have "t∈R" unfolding Spec_def by auto } then have S:"⋂(Spec-U) ⊆ R" by auto { fix t assume "t∈D(⋂(Spec-U))" then have t:"t:Spec" "¬(⋂(Spec-U) ⊆ t)" using openBasic_def[OF S] by auto { assume "t∉U" with t(1) have "t∈Spec-U" by auto then have "⋂(Spec-U) ⊆ t" by auto then have False using t(2) by auto } then have "t∈U" by auto } then have "D(⋂(Spec-U)) ⊆ U" by auto moreover { assume "Spec-U = 0" with assms(1) have "U=Spec" by auto with assms(2) have False by auto } then have P:"Spec-U ⊆ ℐ" "Spec-U ≠0" unfolding Spec_def by auto then have "(⋂(Spec-U))◃R" using intersection_ideals by auto then have "(⋂(Spec-U))∈ℐ" using ideal_dest_subset by auto then have "D(⋂(Spec-U)) ∈{D(J). J∈ℐ}" by auto ultimately show "D(⋂(Spec-U)) ⊆int(U)" using zariski.Top_2_L5 by auto { fix V assume V:"V∈{D(J). J∈ℐ}" "V ⊆ U" from V(1) obtain J where J:"J:ℐ" "V=D(J)" by auto from V(2) have SS:"Spec-U ⊆ Spec-V" by auto { fix K assume K:"K∈Spec-U" { assume "¬(J⊆K)" with K have "K∈D(J)" using J(1) using openBasic_def by auto with SS K J(2) have False by auto } then have "J⊆K" by auto } then have "J⊆ ⋂(Spec-U)" using P(2) by auto then have "D(J) ⊆ D(⋂(Spec-U))" using D_operator_preserve_subset S by auto with J(2) have "V ⊆D(⋂(Spec-U))" by auto } then show "int(U) ⊆ D(⋂(Spec-U))" using zariski.Top_2_L1 zariski.Top_2_L2 by auto qed text‹The whole space is the D-set of the ring as an ideal of itself› lemma (in ring0) openBasic_total: shows "D(R) = Spec" proof show "D(R) ⊆ Spec" using openBasic_def by auto { fix t assume t:"t∈Spec" { assume "R ⊆ t" then have False using t unfolding Spec_def primeIdeal_def using ideal_dest_subset[of t] by auto } with t have "t∈D(R)" using openBasic_def by auto } then show "Spec ⊆ D(R)" by auto qed corollary (in ring0) total_spec: shows "⋃{D(J). J∈ℐ} = Spec" proof show "⋃{D(J). J∈ℐ} ⊆ Spec" using openBasic_def by auto have "D(R)∈{D(J). J∈ℐ}" using R_ideal by auto then have "D(R) ⊆ ⋃{D(J). J∈ℐ}" by auto then show "Spec ⊆ ⋃{D(J). J∈ℐ}" using openBasic_total by auto qed text‹The empty set is the D-set of the zero ideal› lemma (in ring0) openBasic_empty: shows "D({𝟬}) = 0" proof- { fix t assume t:"t∈D({𝟬})" then have "t◃⇩_{p}R" "¬({𝟬} ⊆ t)" using openBasic_def Ring_ZF_1_L2(1) unfolding Spec_def by auto then have False using ideal_dest_zero unfolding primeIdeal_def by auto } then show "D({𝟬}) =0" by auto qed text‹A closed set is a set of primes containing a given ideal› lemma (in ring0) closeBasic: assumes "U{is closed in}{D(J). J∈ℐ}" obtains J where "J∈ℐ" and "U={K∈Spec. J⊆K}" proof- assume rule:"⋀J. J ∈ ℐ ⟹ U = {K ∈ Spec . J ⊆ K} ⟹ thesis" from assms have U:"U⊆Spec" "Spec-U ∈ {D(J). J∈ℐ}" unfolding IsClosed_def using total_spec by auto then obtain J where J:"J∈ℐ" "Spec-U = D(J)" by auto moreover from U(1) have "Spec-(Spec-U) = U" by auto ultimately have "U = Spec-{K∈Spec. ¬(J⊆K)}" using openBasic_def by auto then have "U = {K∈Spec. J⊆K}" by auto with J show ?thesis using rule by auto qed text‹We define the closed sets as V-sets› definition (in ring0) closeBasic ("V") where "S ⊆ R ⟹ V(S) = {K∈Spec. S⊆K}" text‹V-sets and D-sets are complementary› lemma (in ring0) V_is_closed: assumes "J∈ℐ" shows "Spec-V(J) = D(J)" and "V(J){is closed in}{D(J). J∈ℐ}" unfolding IsClosed_def proof(safe) from assms have "V(J) ⊆ Spec" using closeBasic_def by auto then show "⋀x. x ∈ V(J) ⟹ x ∈ ⋃RepFun(ℐ, D)" using total_spec by auto show "Spec-V(J) = D(J)" using assms closeBasic_def openBasic_def by auto with assms show "⋃RepFun(ℐ, D) - V(J) ∈ RepFun(ℐ, D)" using total_spec by auto qed text‹As with D-sets, by De Morgan's Laws we get the same result for unions and intersections on V-sets› lemma (in ring0) V_union: assumes "J∈ℐ" "K∈ℐ" shows "V(J)∪V(K) = V(J⋅⇩_{I}K)" proof- { fix t assume "t∈V(J)" then have "t∈Spec" "J⊆t" using closeBasic_def assms(1) by auto moreover have "J⋅⇩_{I}K ⊆ J" using product_in_intersection(1)[of J K] assms by auto ultimately have "t∈Spec" "J⋅⇩_{I}K ⊆t" by auto then have "t: V(J⋅⇩_{I}K)" using closeBasic_def product_in_intersection(2)[of J K] assms ideal_dest_subset by auto } moreover { fix t assume "t∈V(K)" then have "t∈Spec" "K⊆t" using closeBasic_def assms(2) by auto moreover have "J⋅⇩_{I}K ⊆ K" using product_in_intersection(1)[of J K] assms by auto ultimately have "t∈Spec" "J⋅⇩_{I}K ⊆t" by auto then have "t: V(J⋅⇩_{I}K)" using closeBasic_def product_in_intersection(2)[of J K] assms ideal_dest_subset by auto } moreover { fix t assume "t∈ V(J⋅⇩_{I}K)" then have t:"t∈Spec" "J⋅⇩_{I}K⊆t" using closeBasic_def assms product_in_intersection(2)[of J K] ideal_dest_subset by auto from this(1) have "∀Ia∈ℐ. ∀J∈ℐ. Ia ⋅⇩_{I}J ⊆ t ⟶ Ia ⊆ t ∨ J ⊆ t" unfolding Spec_def primeIdeal_def by blast with assms have "J⋅⇩_{I}K⊆t ⟶ J⊆t ∨ K⊆t" by auto with t have "t∈Spec" "J ⊆ t ∨ K ⊆ t" by auto then have "t∈V(J)∪V(K)" using closeBasic_def assms by auto } ultimately show ?thesis by auto qed lemma (in ring0) V_intersect: assumes "𝒥 ⊆ ℐ" "𝒥 ≠0" shows "⋂{V(I). I∈𝒥} = V(⊕⇩_{I}𝒥)" proof- have "Spec - (⋂{V(I). I∈𝒥}) = ⋃{D(I). I∈𝒥}" proof { fix t assume "t:Spec - (⋂{V(I). I∈𝒥})" then have t:"t:Spec" "t∉⋂{V(I). I∈𝒥}" by auto from t(2) obtain K where "(t∉V(K) ∧ K∈𝒥) ∨ 𝒥=0" by auto with assms(2) have "t∉V(K)" "K∈𝒥" by auto with t(1) have "t∈Spec-V(K)" "K:𝒥" by auto moreover from `K:𝒥` have "Spec-V(K) = D(K)" using assms(1) V_is_closed(1) by auto ultimately have "t:D(K)" "K:𝒥" by auto then have "t∈⋃{D(I). I∈𝒥}" by auto } then show "Spec - (⋂{V(I). I∈𝒥}) ⊆ ⋃{D(I). I∈𝒥}" by auto { fix t assume "t∈⋃{D(I). I∈𝒥}" then obtain K where K:"K:𝒥" "t:D(K)" using assms(2) by auto from `K:𝒥` have "Spec-V(K) = D(K)" using assms(1) V_is_closed(1) by auto with K(2) have "t:Spec-V(K)" by auto with K(1) have "t∈Spec-⋂{V(I). I:𝒥}" by auto } then show "⋃{D(I). I∈𝒥} ⊆ Spec - (⋂{V(I). I∈𝒥})" by auto qed then have "Spec - (⋂{V(I). I∈𝒥}) = D(⊕⇩_{I}𝒥)" using union_open_basic assms by auto then have "Spec-(Spec - (⋂{V(I). I∈𝒥})) = Spec- D(⊕⇩_{I}𝒥)" by auto moreover have JI:"(⊕⇩_{I}𝒥) ∈ ℐ" using generated_ideal_is_ideal[of "⋃𝒥"] assms unfolding sumArbitraryIdeals_def[OF assms(1)] using ideal_dest_subset by auto then have "Spec- V(⊕⇩_{I}𝒥) = D(⊕⇩_{I}𝒥)" using V_is_closed(1)[of "⊕⇩_{I}𝒥"] by auto then have "Spec-(Spec-V(⊕⇩_{I}𝒥) ) = Spec-D(⊕⇩_{I}𝒥)" by auto ultimately have R:"Spec-(Spec - (⋂{V(I). I∈𝒥})) = Spec-(Spec-V(⊕⇩_{I}𝒥) )" by auto { fix t assume t:"t∈⋂{V(I). I∈𝒥}" with assms(2) obtain I where "I:𝒥" "t:V(I)" by auto then have "t∈Spec" using closeBasic_def assms(1) by auto with t have "t∈Spec-(Spec - (⋂{V(I). I∈𝒥}))" by auto with R have "t∈Spec-(Spec-V(⊕⇩_{I}𝒥) )" by auto then have "t∈V(⊕⇩_{I}𝒥)" by auto } moreover { fix t assume t:"t∈V(⊕⇩_{I}𝒥)" with JI have "t:Spec" using closeBasic_def by auto with t have "t∈Spec-(Spec-V(⊕⇩_{I}𝒥) )" by auto then have "t∈Spec-(Spec - (⋂{V(I). I∈𝒥}))" using R by auto then have "t∈⋂{V(I). I∈𝒥}" by auto } ultimately show ?thesis by force qed text‹The closure of a set is the V-set of the intersection of all its points.› lemma (in ring0) closure_zariski: assumes "U ⊆ Spec" "U≠0" shows "cl(U) = V(⋂U)" proof have "U ⊆ ℐ" using assms(1) unfolding Spec_def by auto then have ideal:"(⋂U)◃R" using intersection_ideals[of U] assms(2) by auto { fix t assume t:"t∈V(⋂U)" { fix q assume q:"q∈⋂U" with q obtain M where "M:U" "q:M" using assms(2) by blast with assms have "q∈⋃Spec" by auto then have "q:R" unfolding Spec_def by auto } then have sub:"⋂U ⊆ R" by auto with t have tt:"t∈Spec" "⋂U ⊆ t" using closeBasic_def by auto { fix VV assume VV:"VV∈{D(J). J∈ℐ}" "t∈VV" then obtain J where J:"VV= D(J)" "J∈ℐ" by auto from VV(2) J have jt:"¬(J ⊆ t)" using openBasic_def by auto { assume "U∩D(J) = 0" then have "∀x∈U. x∉D(J)" by auto with J(2) have "∀x∈U. J⊆x" using openBasic_def[of J] assms(1) by auto then have "J⊆ ⋂U ∨ U=0" by auto with tt(2) jt have False using assms(2) by auto } then have "U∩VV ≠ 0" using J(1) by auto } then have R:"∀VV∈{D(J). J∈ℐ}. t∈VV ⟶ VV∩U ≠ 0" by auto from tt(1) assms(1) have RR:"t∈⋃{D(J). J∈ℐ}" "U ⊆ ⋃{D(J). J∈ℐ}" using total_spec by auto have "t∈cl(U)" using zariski.inter_neigh_cl[OF RR(2,1) R]. } then show "V(⋂U) ⊆ cl(U)" apply (rule subsetI) by auto { fix p assume p:"p∈U" then have "⋂U ⊆p" by auto moreover from p assms(1) have "p∈Spec" "⋂U⊆⋃Spec" by auto then have "p∈Spec" "⋂U⊆R" unfolding Spec_def by auto ultimately have "p∈V(⋂U)" using closeBasic_def[of "⋂U"] by auto } then have A:"U⊆V(⋂U)" by auto have B:"V(⋂U){is closed in}{D(J). J∈ℐ}" using V_is_closed(2) ideal ideal_dest_subset by auto show "cl(U) ⊆ V(⋂U)" apply (rule zariski.Top_3_L13[of "V(⋂U)" U]) using A B by auto qed end