:: {Z}ariski {T}opology
:: by Yasushige Watase
::
:: Received October 16, 2018
:: 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 (Ideals A) 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 (Ideals A)

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,(S -Ideal))

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 ;

cluster 0. A -> nilpotent ;

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 b₁ being Element of A st b₁ 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;

cluster multClSet (J,f) -> multiplicatively-closed ;

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 (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)) = {} ) } ;

coherence
{ I where I is Subset of A : ( I is proper Ideal of A & J c= I & I /\ (multClSet (J,f)) = {} ) } is Subset of (Ideals A)

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 b₁ 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 b₁ being Subset-Family of A holds
( b₁ = Spectrum A iff b₁ = { 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 b₁ 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 b₁ being Subset-Family of the carrier of A holds
( b₁ = m-Spectrum A iff b₁ = { 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
({a} -Ideal) + 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 (Spectrum R) 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 (Spectrum R) ) & ( R is degenerated implies {} is Subset of (Spectrum R) ) )

proof end;

consistency
for b₁ being Subset of (Spectrum R) 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 (Spectrum A) equals :: TOPZARI1:def 12
{ p where p is prime Ideal of A : E c= p } ;

correctness
coherence
PrimeIdeals (A,E) is Subset of (Spectrum A);
compatibility
for b₁ being Subset of (Spectrum A) holds
( b₁ = PrimeIdeals (A,E) iff b₁ = { 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
not nilrad A is empty

proof end;

end;

registration

let A be non degenerated commutative Ring;

cluster nilrad A -> add-closed for Subset of A;

coherence
for b₁ being Subset of A st b₁ = nilrad A holds
b₁ is add-closed

proof end;

end;

registration

let A be non degenerated commutative Ring;

cluster nilrad A -> left-ideal right-ideal for Subset of A;

coherence
for b₁ being Subset of A st b₁ = nilrad A holds
( b₁ is left-ideal & b₁ 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 (Spectrum A)

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 (m-Spectrum A);

coherence
meet (m-Spectrum A) is Subset of A ;

end;

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

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)) /\ (Spectrum A)

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,(S -Ideal))

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 (S -Ideal))) = PrimeIdeals (A,(S -Ideal))

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 (Spectrum A) 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 b₁ being strict TopSpace st
( the carrier of b₁ = Spectrum A & ( for F being Subset of b₁ holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) )

proof end;

correctness
uniqueness
for b₁, b₂ being strict TopSpace st the carrier of b₁ = Spectrum A & ( for F being Subset of b₁ holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) & the carrier of b₂ = Spectrum A & ( for F being Subset of b₂ holds
( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def7 defines ZariskiTS TOPZARI1:def 15 :
for A being non degenerated commutative Ring
for b₂ being strict TopSpace holds
( b₂ = ZariskiTS A iff ( the carrier of b₂ = Spectrum A & ( for F being Subset of b₂ 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 (ZariskiTS A) 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 (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 ) ) )

proof end;

registration

cluster non empty degenerated left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable V127() V128() V129() V134() unital associative commutative V166() V167() V168() V169() V170() V171() V184() V185() V186() V187() for doubleLoopStr ;

existence
ex b₁ being commutative Ring st b₁ is degenerated

proof end;

end;

registration

let R be degenerated commutative Ring;

cluster ADTS (Spectrum R) -> T_0 ;

coherence
ADTS (Spectrum R) is T_0

proof end;

end;

::[AM] p.13 Ex18 iv)

registration

let A be non degenerated commutative Ring;

cluster ZariskiTS A -> strict T_0 ;

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 (ZariskiTS B),(ZariskiTS A) means :Def9: :: TOPZARI1:def 16
for x being Point of (ZariskiTS B) holds it . x = h " x;

existence
ex b₁ being Function of (ZariskiTS B),(ZariskiTS A) st
for x being Point of (ZariskiTS B) holds b₁ . x = h " x

proof end;

uniqueness
for b₁, b₂ being Function of (ZariskiTS B),(ZariskiTS A) st ( for x being Point of (ZariskiTS B) holds b₁ . x = h " x ) & ( for x being Point of (ZariskiTS B) holds b₂ . x = h " x ) holds
b₁ = b₂

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 b₄ being Function of (ZariskiTS B),(ZariskiTS A) holds
( b₄ = Spec h iff for x being Point of (ZariskiTS B) holds b₄ . 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;