:: {Z}ariski {T}opology
:: by Yasushige Watase
::
:: Received October 16, 2018
:: Copyright (c) 2018-2019 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, RING_2, PRE_TOPC, TDLAT_3, TEX_1, SCMRINGI;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
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;