:: {Z}ariski {T}opology :: by Yasushige Watase :: :: Received October 16, 2018 :: Copyright (c) 2018-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ARYTM_3, FUNCT_1, RELAT_1, WELLORD1, CARD_3, XBOOLE_0, TARSKI, XCMPLX_0, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, CARD_1, MESFUNC1, GROUP_1, ARYTM_1, FINSEQ_1, SETFAM_1, INT_2, QUOFIELD, MSSUBFAM, BINOP_1, GROUP_4, NUMBERS, IDEAL_1, C0SP1, ZFMISC_1, FUNCSDOM, CARD_FIL, RING_1, SQUARE_1, BCIALG_2, NEWTON, RING_2, ORDERS_1, XXREAL_0, FINSET_1, WELLORD2, PRE_TOPC, RCOMP_1, TEX_1, ORDINAL2, TOPZARI1, ALGSTR_0, LATTICEA; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, RELAT_1, ORDINAL1, WELLORD1, FUNCT_1, FUNCT_2, FINSET_1, STRUCT_0, PRE_TOPC, ALGSTR_0, RLVECT_1, ORDERS_1, GROUP_1, VECTSP_1, IDEAL_1, RING_1, RING_2, TEX_1, RELSET_1, XCMPLX_0, XXREAL_0, NUMBERS, BINOM, GROUP_6, QUOFIELD, C0SP1, FINSEQ_1; constructors ARYTM_3, TDLAT_3, ORDERS_1, RINGCAT1, RING_2, BINOM, RELSET_1, GCD_1, ALGSTR_0, TEX_1; registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, STRUCT_0, CARD_1, VECTSP_1, ALGSTR_1, SUBSET_1, FUNCT_2, ALGSTR_0, RLVECT_1, IDEAL_1, RINGCAT1, RING_1, PRE_TOPC, SCMRINGI; requirements NUMERALS, SUBSET, BOOLE; begin :: Preliminaries: Some Properties of Ideals reserve R for commutative Ring; reserve A,B for non degenerated commutative Ring; reserve h for Function of A,B; reserve I0,I,I1,I2 for Ideal of A; reserve J,J1,J2 for proper Ideal of A; reserve p for prime Ideal of A; reserve S,S1 for non empty Subset of A; reserve E,E1,E2 for Subset of A; reserve a,b,f for Element of A; reserve n for Nat; reserve x,o,o1 for object; definition let A,S; func Ideals(A,S) -> Subset of Ideals A equals :: TOPZARI1:def 1 { I where I is Ideal of A: S c= I }; end; registration let A,S; cluster Ideals(A,S) -> non empty; end; theorem :: TOPZARI1:1 Ideals(A,S) = Ideals(A,S-Ideal); :: Some Properties of power of an element of a ring :: Definition of Nilpotency definition let A be unital non empty multLoopStr_0, a be Element of A; attr a is nilpotent means :: TOPZARI1:def 2 ex k being non zero Nat st a|^k = 0.A; end; registration let A be unital non empty multLoopStr_0; cluster 0.A -> nilpotent; end; registration let A be unital non empty multLoopStr_0; cluster nilpotent for Element of A; end; registration let A; cluster 1.A -> non nilpotent; end; :: Definition of a multiplicatively closed set generated by an element :: which does not meet a proper Ideal J definition let A,J,f; func multClSet(J,f) -> Subset of A equals :: TOPZARI1:def 3 the set of all f|^i where i is Nat; end; registration let A,J,f; cluster multClSet(J,f) -> multiplicatively-closed; end; theorem :: TOPZARI1:2 for n be Nat holds (1.A)|^n = 1.A; theorem :: TOPZARI1:3 not 1.A in sqrt J; theorem :: TOPZARI1:4 multClSet(J,1.A) = {1.A}; definition let A,J,f; func Ideals(A,J,f) -> Subset of Ideals A equals :: TOPZARI1:def 4 {I where I is Subset of A: I is proper Ideal of A & J c= I & I /\ multClSet(J,f) = {} }; end; theorem :: TOPZARI1:5 for A, J, f st not f in sqrt J holds J in Ideals(A,J,f); ::[AM] Theorem 1.3 theorem :: TOPZARI1:6 for A, J, f st not f in sqrt J holds Ideals(A,J,f) has_upper_Zorn_property_wrt RelIncl(Ideals(A,J,f) ); theorem :: TOPZARI1:7 for f,J st not f in sqrt J holds ex m be prime Ideal of A st not f in m & J c= m; ::[AM] Cor 1.4 theorem :: TOPZARI1:8 ex m be maximal Ideal of A st J c= m; theorem :: TOPZARI1:9 ex m be prime Ideal of A st J c= m; ::[AM] Cor 1.5 theorem :: TOPZARI1:10 a is NonUnit of A implies ex m be maximal Ideal of A st a in m; begin :: Spectrum of Prime Ideals and Maximal Ideal definition let R be commutative Ring; func Spectrum R -> Subset-Family of R equals :: TOPZARI1:def 5 {I where I is Ideal of R: I is quasi-prime & I <> [#]R} if R is non degenerated otherwise {}; end; definition let A; redefine func Spectrum A -> Subset-Family of A equals :: TOPZARI1:def 6 the set of all I where I is prime Ideal of A; end; registration let A; cluster Spectrum A -> non empty; end; definition let R; func m-Spectrum R -> Subset-Family of R equals :: TOPZARI1:def 7 {I where I is Ideal of R: I is quasi-maximal & I <> [#]R} if R is non degenerated otherwise {}; end; definition let A; redefine func m-Spectrum A -> Subset-Family of the carrier of A equals :: TOPZARI1:def 8 the set of all I where I is maximal Ideal of A; end; registration let A; cluster m-Spectrum A -> non empty; end; begin :: Local & Semi-Local Ring definition let A; attr A is local means :: TOPZARI1:def 9 ex m be Ideal of A st m-Spectrum A = {m}; end; definition let A; attr A is semi-local means :: TOPZARI1:def 10 m-Spectrum A is finite; end; theorem :: TOPZARI1:11 x in I & I is proper Ideal of A implies x is NonUnit of A; theorem :: TOPZARI1:12 (for m1,m2 be object st m1 in m-Spectrum A & m2 in m-Spectrum A holds m1 = m2) implies A is local; ::[AM] prop 1.6 i) theorem :: TOPZARI1:13 (for x holds x in [#]A \ J implies x is Unit of A) implies A is local; reserve m for maximal Ideal of A; theorem :: TOPZARI1:14 a in [#]A \ m implies {a}-Ideal + m = [#]A; ::[AM] prop 1.6 ii) theorem :: TOPZARI1:15 (for a holds a in m implies 1.A + a is Unit of A) implies A is local; definition let R; let E be Subset of R; func PrimeIdeals(R,E) -> Subset of Spectrum R equals :: TOPZARI1:def 11 {p where p is Ideal of R: p is quasi-prime & p <> [#]R & E c= p} if R is non degenerated otherwise {}; end; definition let A; let E be Subset of A; redefine func PrimeIdeals(A,E) -> Subset of Spectrum A equals :: TOPZARI1:def 12 {p where p is prime Ideal of A: E c=p }; end; registration let A,J; cluster PrimeIdeals(A,J) -> non empty; end; reserve p for prime Ideal of A; reserve k for non zero Nat; theorem :: TOPZARI1:16 not a in p implies not a|^k in p; begin :: Nilradical & Jacobson Radical definition let A; func nilrad A -> Subset of A equals :: TOPZARI1:def 13 the set of all a where a is nilpotent Element of A; end; theorem :: TOPZARI1:17 nilrad A = sqrt({0.A}); registration let A; cluster nilrad A -> non empty; end; registration let A; cluster nilrad A -> add-closed for Subset of A; end; registration let A; cluster nilrad A -> left-ideal right-ideal for Subset of A; end; ::::: [AM] Prop 1.14 theorem :: TOPZARI1:18 sqrt J = meet PrimeIdeals(A,J); ::::: [AM] Prop 1.8 theorem :: TOPZARI1:19 nilrad A = meet Spectrum A; :::[AM] Ex 1.13 i) theorem :: TOPZARI1:20 I c= sqrt I; theorem :: TOPZARI1:21 I c= J implies sqrt I c= sqrt J; definition let A; func J-Rad A -> Subset of A equals :: TOPZARI1:def 14 meet m-Spectrum A; end; begin :: Construction of Zariski Topology of the Prime Spectrum of A (Spec A) theorem :: TOPZARI1:22 PrimeIdeals(A,S) c= Ideals(A,S); theorem :: TOPZARI1:23 PrimeIdeals(A,S) = Ideals(A,S) /\ Spectrum A; :: [AM] p.12 Ex15 i) theorem :: TOPZARI1:24 PrimeIdeals(A,S) = PrimeIdeals(A,S-Ideal); theorem :: TOPZARI1:25 I c= p implies sqrt I c= p; theorem :: TOPZARI1:26 sqrt I c= p implies I c= p; :: [AM] p.12 Ex15 i) theorem :: TOPZARI1:27 PrimeIdeals(A,sqrt(S-Ideal)) = PrimeIdeals(A,S-Ideal); theorem :: TOPZARI1:28 E2 c= E1 implies PrimeIdeals(A,E1) c= PrimeIdeals(A,E2); ::[AM] p.12 Ex.17 iv) not yet introduce X_f = PrimeIdeals(A,{f}) theorem :: TOPZARI1:29 PrimeIdeals(A,J1) = PrimeIdeals(A,J2) iff sqrt J1 = sqrt J2; ::[AM] Prop 1.11 ii) case of n=2 theorem :: TOPZARI1:30 I1 *' I2 c= p implies I1 c= p or I2 c= p; ::[AM] p.12 Ex.15 ii) theorem :: TOPZARI1:31 PrimeIdeals(A,{1.A}) = {}; ::[AM] p.12 Ex.15 ii) theorem :: TOPZARI1:32 Spectrum A = PrimeIdeals(A,{0.A}); ::[AM] p.12 Ex.15 iv) theorem :: TOPZARI1:33 for E1,E2 be non empty Subset of A holds ex E3 be non empty Subset of A st PrimeIdeals(A,E1) \/ PrimeIdeals(A,E2) = PrimeIdeals(A,E3); ::[AM] p.12 Ex.15 iii) theorem :: TOPZARI1:34 for G being Subset-Family of Spectrum A st for S being set st S in G holds (ex E be non empty Subset of A st S = PrimeIdeals(A,E)) holds ex F be non empty Subset of A st Intersect G = PrimeIdeals(A,F); ::[AM] p.12 Ex.15 definition let A; func ZariskiTS(A) -> strict TopSpace means :: TOPZARI1:def 15 the carrier of it = Spectrum A & for F being Subset of it holds F is closed iff (ex E be non empty Subset of A st F = PrimeIdeals(A,E)); end; registration let A; cluster ZariskiTS(A) -> non empty; end; theorem :: TOPZARI1:35 for P,Q being Point of ZariskiTS A st P <> Q holds ex V being Subset of ZariskiTS A st V is open & ( P in V & not Q in V or Q in V & not P in V ); registration cluster degenerated for commutative Ring; end; registration let R be degenerated commutative Ring; cluster ADTS Spectrum R -> T_0; end; ::[AM] p.13 Ex18 iv) registration let A; cluster ZariskiTS A -> T_0; end; begin :: Continuous Map ZariskiTS B -> ZariskiTS A :: associated with a ring homomorphism. reserve M0 for Ideal of B; theorem :: TOPZARI1:36 h is RingHomomorphism implies h"M0 is Ideal of A; reserve M0 for prime Ideal of B; theorem :: TOPZARI1:37 h is RingHomomorphism implies h"M0 is prime Ideal of A; :: Spec h is continuous map of ZariskiTS B -> ZariskiTS A :: associated with a ring homomorphism h:A->B. ::[AM] p.13 Ex22 definition ::: similar to "f from FUNCT_3 let A, B, h; assume h is RingHomomorphism; func Spec h -> Function of ZariskiTS B, ZariskiTS A means :: TOPZARI1:def 16 for x be Point of ZariskiTS B holds it.x = h"x; end; ::[AM] p.13 Ex22 ii) theorem :: TOPZARI1:38 h is RingHomomorphism implies (Spec h)"PrimeIdeals(A,E) = PrimeIdeals(B,h.:E); ::[AM] p.13 Ex22 i) theorem :: TOPZARI1:39 h is RingHomomorphism implies Spec h is continuous;