:: {Z}ariski {T}opology
:: by Yasushige Watase
::
:: Copyright (c) 2018-2021 Association of Mizar Users

Lm1: for A being non degenerated commutative Ring
for x being object holds
( x in Ideals A iff x is Ideal of A )

proof end;

definition
let A be non degenerated commutative Ring;
let S be non empty Subset of A;
func Ideals (A,S) -> Subset of () equals :: TOPZARI1:def 1
{ I where I is Ideal of A : S c= I } ;
coherence
{ I where I is Ideal of A : S c= I } is Subset of ()
proof end;
end;

:: deftheorem defines Ideals TOPZARI1:def 1 :
for A being non degenerated commutative Ring
for S being non empty Subset of A holds Ideals (A,S) = { I where I is Ideal of A : S c= I } ;

registration
let A be non degenerated commutative Ring;
let S be non empty Subset of A;
cluster Ideals (A,S) -> non empty ;
coherence
not Ideals (A,S) is empty
proof end;
end;

theorem Th2: :: TOPZARI1:1
for A being non degenerated commutative Ring
for S being non empty Subset of A holds Ideals (A,S) = Ideals (A,())
proof end;

:: Some Properties of power of an element of a ring
:: Definition of Nilpotency
definition
let A be non empty unital multLoopStr_0 ;
let 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;

:: deftheorem defines nilpotent TOPZARI1:def 2 :
for A being non empty unital multLoopStr_0
for a being Element of A holds
( a is nilpotent iff ex k being non zero Nat st a |^ k = 0. A );

registration
let A be non empty unital multLoopStr_0 ;
coherence
0. A is nilpotent
proof end;
end;

registration
let A be non empty unital multLoopStr_0 ;
cluster nilpotent for Element of the carrier of A;
existence
ex b1 being Element of A st b1 is nilpotent
proof end;
end;

registration
let A be non degenerated commutative Ring;
cluster 1. A -> non nilpotent ;
coherence
not 1. A is nilpotent
proof end;
end;

:: Definition of a multiplicatively closed set generated by an element
:: which does not meet a proper Ideal J
definition
let A be non degenerated commutative Ring;
let J be proper Ideal of A;
let f be Element of A;
func multClSet (J,f) -> Subset of A equals :: TOPZARI1:def 3
{ (f |^ i) where i is Nat : verum } ;
coherence
{ (f |^ i) where i is Nat : verum } is Subset of A
proof end;
end;

:: deftheorem defines multClSet TOPZARI1:def 3 :
for A being non degenerated commutative Ring
for J being proper Ideal of A
for f being Element of A holds multClSet (J,f) = { (f |^ i) where i is Nat : verum } ;

registration
let A be non degenerated commutative Ring;
let J be proper Ideal of A;
let f be Element of A;
coherence
multClSet (J,f) is multiplicatively-closed
proof end;
end;

theorem Lm4: :: TOPZARI1:2
for A being non degenerated commutative Ring
for n being Nat holds (1. A) |^ n = 1. A
proof end;

theorem Lm5: :: TOPZARI1:3
for A being non degenerated commutative Ring
for J being proper Ideal of A holds not 1. A in sqrt J
proof end;

theorem Lm6: :: TOPZARI1:4
for A being non degenerated commutative Ring
for J being proper Ideal of A holds multClSet (J,(1. A)) = {(1. A)}
proof end;

definition
let A be non degenerated commutative Ring;
let J be proper Ideal of A;
let f be Element of A;
func Ideals (A,J,f) -> Subset of () equals :: TOPZARI1:def 4
{ I where I is Subset of A : ( I is proper Ideal of A & J c= I & I /\ (multClSet (J,f)) = {} ) } ;
coherence
{ I where I is Subset of A : ( I is proper Ideal of A & J c= I & I /\ (multClSet (J,f)) = {} ) } is Subset of ()
proof end;
end;

:: deftheorem defines Ideals TOPZARI1:def 4 :
for A being non degenerated commutative Ring
for J being proper Ideal of A
for f being Element of A holds Ideals (A,J,f) = { I where I is Subset of A : ( I is proper Ideal of A & J c= I & I /\ (multClSet (J,f)) = {} ) } ;

theorem Th7: :: TOPZARI1:5
for A being non degenerated commutative Ring
for J being proper Ideal of A
for f being Element of A st not f in sqrt J holds
J in Ideals (A,J,f)
proof end;

::[AM] Theorem 1.3
theorem Th8: :: TOPZARI1:6
for A being non degenerated commutative Ring
for J being proper Ideal of A
for f being Element of A st not f in sqrt J holds
Ideals (A,J,f) has_upper_Zorn_property_wrt RelIncl (Ideals (A,J,f))
proof end;

theorem Th9: :: TOPZARI1:7
for A being non degenerated commutative Ring
for f being Element of A
for J being proper Ideal of A st not f in sqrt J holds
ex m being prime Ideal of A st
( not f in m & J c= m )
proof end;

::[AM] Cor 1.4
theorem Th10: :: TOPZARI1:8
for A being non degenerated commutative Ring
for J being proper Ideal of A ex m being maximal Ideal of A st J c= m
proof end;

theorem Th11: :: TOPZARI1:9
for A being non degenerated commutative Ring
for J being proper Ideal of A ex m being prime Ideal of A st J c= m
proof end;

::[AM] Cor 1.5
theorem :: TOPZARI1:10
for A being non degenerated commutative Ring
for a being Element of A st a is NonUnit of A holds
ex m being maximal Ideal of A st a in m
proof end;

definition
let R be commutative Ring;
func Spectrum R -> Subset-Family of R equals :Def3: :: TOPZARI1:def 5
{ I where I is Ideal of R : ( I is quasi-prime & I <> [#] R ) } if not R is degenerated
otherwise {} ;
coherence
( ( not R is degenerated implies { I where I is Ideal of R : ( I is quasi-prime & I <> [#] R ) } is Subset-Family of R ) & ( R is degenerated implies {} is Subset-Family of R ) )
proof end;
consistency
for b1 being Subset-Family of R holds verum
;
end;

:: deftheorem Def3 defines Spectrum TOPZARI1:def 5 :
for R being commutative Ring holds
( ( not R is degenerated implies Spectrum R = { I where I is Ideal of R : ( I is quasi-prime & I <> [#] R ) } ) & ( R is degenerated implies Spectrum R = {} ) );

definition
let A be non degenerated commutative Ring;
:: original: Spectrum
redefine func Spectrum A -> Subset-Family of A equals :: TOPZARI1:def 6
{ I where I is prime Ideal of A : verum } ;
correctness
coherence
Spectrum A is Subset-Family of A
;
compatibility
for b1 being Subset-Family of A holds
( b1 = Spectrum A iff b1 = { I where I is prime Ideal of A : verum } )
;
proof end;
end;

:: deftheorem defines Spectrum TOPZARI1:def 6 :
for A being non degenerated commutative Ring holds Spectrum A = { I where I is prime Ideal of A : verum } ;

registration
let A be non degenerated commutative Ring;
cluster Spectrum A -> non empty ;
coherence
not Spectrum A is empty
proof end;
end;

definition
let R be commutative Ring;
func m-Spectrum R -> Subset-Family of R equals :Def4: :: TOPZARI1:def 7
{ I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } if not R is degenerated
otherwise {} ;
coherence
( ( not R is degenerated implies { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } is Subset-Family of R ) & ( R is degenerated implies {} is Subset-Family of R ) )
proof end;
consistency
for b1 being Subset-Family of R holds verum
;
end;

:: deftheorem Def4 defines m-Spectrum TOPZARI1:def 7 :
for R being commutative Ring holds
( ( not R is degenerated implies m-Spectrum R = { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } ) & ( R is degenerated implies m-Spectrum R = {} ) );

definition
let A be non degenerated commutative Ring;
:: original: m-Spectrum
redefine func m-Spectrum A -> Subset-Family of the carrier of A equals :: TOPZARI1:def 8
{ I where I is maximal Ideal of A : verum } ;
correctness
coherence
m-Spectrum A is Subset-Family of the carrier of A
;
compatibility
for b1 being Subset-Family of the carrier of A holds
( b1 = m-Spectrum A iff b1 = { I where I is maximal Ideal of A : verum } )
;
proof end;
end;

:: deftheorem defines m-Spectrum TOPZARI1:def 8 :
for A being non degenerated commutative Ring holds m-Spectrum A = { I where I is maximal Ideal of A : verum } ;

registration
let A be non degenerated commutative Ring;
cluster m-Spectrum A -> non empty ;
coherence
not m-Spectrum A is empty
proof end;
end;

definition
let A be non degenerated commutative Ring;
attr A is local means :: TOPZARI1:def 9
ex m being Ideal of A st m-Spectrum A = {m};
end;

:: deftheorem defines local TOPZARI1:def 9 :
for A being non degenerated commutative Ring holds
( A is local iff ex m being Ideal of A st m-Spectrum A = {m} );

definition
let A be non degenerated commutative Ring;
attr A is semi-local means :: TOPZARI1:def 10
m-Spectrum A is finite ;
end;

:: deftheorem defines semi-local TOPZARI1:def 10 :
for A being non degenerated commutative Ring holds
( A is semi-local iff m-Spectrum A is finite );

theorem Th15: :: TOPZARI1:11
for A being non degenerated commutative Ring
for I being Ideal of A
for x being object st x in I & I is proper Ideal of A holds
x is NonUnit of A
proof end;

theorem Th16: :: TOPZARI1:12
for A being non degenerated commutative Ring st ( for m1, m2 being object st m1 in m-Spectrum A & m2 in m-Spectrum A holds
m1 = m2 ) holds
A is local
proof end;

::[AM] prop 1.6 i)
theorem Th17: :: TOPZARI1:13
for A being non degenerated commutative Ring
for J being proper Ideal of A st ( for x being object st x in ([#] A) \ J holds
x is Unit of A ) holds
A is local
proof end;

theorem Th18: :: TOPZARI1:14
for A being non degenerated commutative Ring
for a being Element of A
for m being maximal Ideal of A st a in ([#] A) \ m holds
() + m = [#] A
proof end;

::[AM] prop 1.6 ii)
theorem :: TOPZARI1:15
for A being non degenerated commutative Ring
for m being maximal Ideal of A st ( for a being Element of A st a in m holds
(1. A) + a is Unit of A ) holds
A is local
proof end;

definition
let R be commutative Ring;
let E be Subset of R;
func PrimeIdeals (R,E) -> Subset of () equals :Def5: :: TOPZARI1:def 11
{ p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } if not R is degenerated
otherwise {} ;
coherence
( ( not R is degenerated implies { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } is Subset of () ) & ( R is degenerated implies {} is Subset of () ) )
proof end;
consistency
for b1 being Subset of () holds verum
;
end;

:: deftheorem Def5 defines PrimeIdeals TOPZARI1:def 11 :
for R being commutative Ring
for E being Subset of R holds
( ( not R is degenerated implies PrimeIdeals (R,E) = { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } ) & ( R is degenerated implies PrimeIdeals (R,E) = {} ) );

definition
let A be non degenerated commutative Ring;
let E be Subset of A;
:: original: PrimeIdeals
redefine func PrimeIdeals (A,E) -> Subset of () equals :: TOPZARI1:def 12
{ p where p is prime Ideal of A : E c= p } ;
correctness
coherence
PrimeIdeals (A,E) is Subset of ()
;
compatibility
for b1 being Subset of () holds
( b1 = PrimeIdeals (A,E) iff b1 = { p where p is prime Ideal of A : E c= p } )
;
proof end;
end;

:: deftheorem defines PrimeIdeals TOPZARI1:def 12 :
for A being non degenerated commutative Ring
for E being Subset of A holds PrimeIdeals (A,E) = { p where p is prime Ideal of A : E c= p } ;

registration
let A be non degenerated commutative Ring;
let J be proper Ideal of A;
cluster PrimeIdeals (A,J) -> non empty ;
coherence
not PrimeIdeals (A,J) is empty
proof end;
end;

Th21: for A being non degenerated commutative Ring holds PrimeIdeals (A,{(0. A)}) = Spectrum A
proof end;

Th22: for A being non degenerated commutative Ring
for x being object st x in Spectrum A holds
x is prime Ideal of A

proof end;

theorem Th23: :: TOPZARI1:16
for A being non degenerated commutative Ring
for a being Element of A
for p being prime Ideal of A
for k being non zero Nat st not a in p holds
not a |^ k in p
proof end;

Lm24: for A being non degenerated commutative Ring
for a being Element of A
for n being Nat
for p being prime Ideal of A st a |^ n in p holds
n <> 0

proof end;

definition
let A be non degenerated commutative Ring;
func nilrad A -> Subset of A equals :: TOPZARI1:def 13
{ a where a is nilpotent Element of A : verum } ;
coherence
{ a where a is nilpotent Element of A : verum } is Subset of A
proof end;
end;

:: deftheorem defines nilrad TOPZARI1:def 13 :
for A being non degenerated commutative Ring holds nilrad A = { a where a is nilpotent Element of A : verum } ;

Lm25: for A being non degenerated commutative Ring
for a being Element of A st a is nilpotent holds
a in sqrt {(0. A)}

proof end;

Lm26: for A being non degenerated commutative Ring
for a being Element of A
for n being Nat st a |^ n in {(0. A)} holds
n <> 0

proof end;

theorem Th27: :: TOPZARI1:17
for A being non degenerated commutative Ring holds nilrad A = sqrt {(0. A)}
proof end;

registration
let A be non degenerated commutative Ring;
cluster nilrad A -> non empty ;
coherence
proof end;
end;

registration
let A be non degenerated commutative Ring;
coherence
for b1 being Subset of A st b1 = nilrad A holds
proof end;
end;

registration
let A be non degenerated commutative Ring;
cluster nilrad A -> left-ideal right-ideal for Subset of A;
coherence
for b1 being Subset of A st b1 = nilrad A holds
( b1 is left-ideal & b1 is right-ideal )
proof end;
end;

::::: [AM] Prop 1.14
theorem Th28: :: TOPZARI1:18
for A being non degenerated commutative Ring
for J being proper Ideal of A holds sqrt J = meet (PrimeIdeals (A,J))
proof end;

::::: [AM] Prop 1.8
theorem :: TOPZARI1:19
for A being non degenerated commutative Ring holds nilrad A = meet ()
proof end;

:::[AM] Ex 1.13 i)
theorem Th30: :: TOPZARI1:20
for A being non degenerated commutative Ring
for I being Ideal of A holds I c= sqrt I
proof end;

theorem :: TOPZARI1:21
for A being non degenerated commutative Ring
for I being Ideal of A
for J being proper Ideal of A st I c= J holds
sqrt I c= sqrt J
proof end;

definition
let A be non degenerated commutative Ring;
func J-Rad A -> Subset of A equals :: TOPZARI1:def 14
meet ();
coherence
meet () is Subset of A
;
end;

:: deftheorem defines J-Rad TOPZARI1:def 14 :
for A being non degenerated commutative Ring holds J-Rad A = meet ();

theorem Th32: :: TOPZARI1:22
for A being non degenerated commutative Ring
for S being non empty Subset of A holds PrimeIdeals (A,S) c= Ideals (A,S)
proof end;

theorem Th33: :: TOPZARI1:23
for A being non degenerated commutative Ring
for S being non empty Subset of A holds PrimeIdeals (A,S) = (Ideals (A,S)) /\ ()
proof end;

:: [AM] p.12 Ex15 i)
theorem Th34: :: TOPZARI1:24
for A being non degenerated commutative Ring
for S being non empty Subset of A holds PrimeIdeals (A,S) = PrimeIdeals (A,())
proof end;

theorem Th35: :: TOPZARI1:25
for A being non degenerated commutative Ring
for I being Ideal of A
for p being prime Ideal of A st I c= p holds
sqrt I c= p
proof end;

theorem Th36: :: TOPZARI1:26
for A being non degenerated commutative Ring
for I being Ideal of A
for p being prime Ideal of A st sqrt I c= p holds
I c= p
proof end;

:: [AM] p.12 Ex15 i)
theorem Th37: :: TOPZARI1:27
for A being non degenerated commutative Ring
for S being non empty Subset of A holds PrimeIdeals (A,(sqrt ())) = PrimeIdeals (A,())
proof end;

theorem Th38: :: TOPZARI1:28
for A being non degenerated commutative Ring
for E1, E2 being Subset of A st E2 c= E1 holds
PrimeIdeals (A,E1) c= PrimeIdeals (A,E2)
proof end;

::[AM] p.12 Ex.17 iv) not yet introduce X_f = PrimeIdeals(A,{f})
theorem :: TOPZARI1:29
for A being non degenerated commutative Ring
for J1, J2 being proper Ideal of A holds
( PrimeIdeals (A,J1) = PrimeIdeals (A,J2) iff sqrt J1 = sqrt J2 )
proof end;

::[AM] Prop 1.11 ii) case of n=2
theorem Th40: :: TOPZARI1:30
for A being non degenerated commutative Ring
for I1, I2 being Ideal of A
for p being prime Ideal of A holds
( not I1 *' I2 c= p or I1 c= p or I2 c= p )
proof end;

::[AM] p.12 Ex.15 ii)
theorem Th41A: :: TOPZARI1:31
for A being non degenerated commutative Ring holds PrimeIdeals (A,{(1. A)}) = {}
proof end;

Th41: for A being non degenerated commutative Ring ex E being non empty Subset of A st {} = PrimeIdeals (A,E)
proof end;

::[AM] p.12 Ex.15 ii)
theorem :: TOPZARI1:32
for A being non degenerated commutative Ring holds Spectrum A = PrimeIdeals (A,{(0. A)}) by Th21;

Th42: for A being non degenerated commutative Ring ex E being non empty Subset of A st Spectrum A = PrimeIdeals (A,E)
proof end;

::[AM] p.12 Ex.15 iv)
theorem Th43: :: TOPZARI1:33
for A being non degenerated commutative Ring
for E1, E2 being non empty Subset of A ex E3 being non empty Subset of A st (PrimeIdeals (A,E1)) \/ (PrimeIdeals (A,E2)) = PrimeIdeals (A,E3)
proof end;

::[AM] p.12 Ex.15 iii)
theorem Th44: :: TOPZARI1:34
for A being non degenerated commutative Ring
for G being Subset-Family of () st ( for S being set st S in G holds
ex E being non empty Subset of A st S = PrimeIdeals (A,E) ) holds
ex F being non empty Subset of A st Intersect G = PrimeIdeals (A,F)
proof end;

::[AM] p.12 Ex.15
definition
let A be non degenerated commutative Ring;
func ZariskiTS A -> strict TopSpace means :Def7: :: TOPZARI1:def 15
( the carrier of it = Spectrum A & ( for F being Subset of it holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) );
existence
ex b1 being strict TopSpace st
( the carrier of b1 = Spectrum A & ( for F being Subset of b1 holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) )
proof end;
correctness
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = Spectrum A & ( for F being Subset of b1 holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) & the carrier of b2 = Spectrum A & ( for F being Subset of b2 holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines ZariskiTS TOPZARI1:def 15 :
for A being non degenerated commutative Ring
for b2 being strict TopSpace holds
( b2 = ZariskiTS A iff ( the carrier of b2 = Spectrum A & ( for F being Subset of b2 holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) ) );

registration
let A be non degenerated commutative Ring;
cluster ZariskiTS A -> non empty strict ;
coherence
not ZariskiTS A is empty
proof end;
end;

Lm44: for A being non degenerated commutative Ring
for P being Point of () holds P is prime Ideal of A

proof end;

theorem Th45: :: TOPZARI1:35
for A being non degenerated commutative Ring
for P, Q being Point of () st P <> Q holds
ex V being Subset of () st
( V is open & ( ( P in V & not Q in V ) or ( Q in V & not P in V ) ) )
proof end;

registration
existence
ex b1 being commutative Ring st b1 is degenerated
proof end;
end;

registration
let R be degenerated commutative Ring;
cluster ADTS () -> T_0 ;
coherence
proof end;
end;

::[AM] p.13 Ex18 iv)
registration
let A be non degenerated commutative Ring;
coherence
ZariskiTS A is T_0
proof end;
end;

Lm48: for A, B being non degenerated commutative Ring
for M0 being Ideal of B
for x, y being Element of the carrier of A
for h being Function of A,B st h is RingHomomorphism & x in h " M0 & y in h " M0 holds
x + y in h " M0

proof end;

Lm49: for A, B being non degenerated commutative Ring
for M0 being Ideal of B
for r, x being Element of A
for h being Function of A,B st h is RingHomomorphism & x in h " M0 holds
r * x in h " M0

proof end;

theorem Th50: :: TOPZARI1:36
for A, B being non degenerated commutative Ring
for h being Function of A,B
for M0 being Ideal of B st h is RingHomomorphism holds
h " M0 is Ideal of A
proof end;

theorem Th51: :: TOPZARI1:37
for A, B being non degenerated commutative Ring
for h being Function of A,B
for M0 being prime Ideal of B st h is RingHomomorphism holds
h " M0 is prime Ideal of A
proof end;

:: Spec h is continuous map of ZariskiTS B -> ZariskiTS A
:: associated with a ring homomorphism h:A->B.
::[AM] p.13 Ex22
definition
let A, B be non degenerated commutative Ring;
let h be Function of A,B;
assume A0: h is RingHomomorphism ;
func Spec h -> Function of (),() means :Def9: :: TOPZARI1:def 16
for x being Point of () holds it . x = h " x;
existence
ex b1 being Function of (),() st
for x being Point of () holds b1 . x = h " x
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for x being Point of () holds b1 . x = h " x ) & ( for x being Point of () holds b2 . x = h " x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Spec TOPZARI1:def 16 :
for A, B being non degenerated commutative Ring
for h being Function of A,B st h is RingHomomorphism holds
for b4 being Function of (),() holds
( b4 = Spec h iff for x being Point of () holds b4 . x = h " x );

::[AM] p.13 Ex22 ii)
theorem Th52: :: TOPZARI1:38
for A, B being non degenerated commutative Ring
for h being Function of A,B
for E being Subset of A st h is RingHomomorphism holds
(Spec h) " (PrimeIdeals (A,E)) = PrimeIdeals (B,(h .: E))
proof end;

::[AM] p.13 Ex22 i)
theorem :: TOPZARI1:39
for A, B being non degenerated commutative Ring
for h being Function of A,B st h is RingHomomorphism holds
Spec h is continuous
proof end;