:: by Yasushige Watase

::

:: Received October 16, 2018

:: Copyright (c) 2018-2019 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;

{ I where I is Ideal of A : S c= I } is Subset of (Ideals A)

end;
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 } ;

{ I where I is Ideal of A : S c= I } is Subset of (Ideals A)

proof 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 } ;

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;

coherence

not Ideals (A,S) is empty

end;
let S be non empty Subset of A;

coherence

not Ideals (A,S) is empty

proof 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))

for S being non empty Subset of A holds Ideals (A,S) = Ideals (A,(S -Ideal))

proof 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 );

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 ;

existence

ex b_{1} being Element of A st b_{1} is nilpotent

end;
existence

ex b

proof end;

registration
end;

:: Definition of a multiplicatively closed set generated by an element

:: which does not meet a proper Ideal J

:: 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;

coherence

{ (f |^ i) where i is Nat : verum } is Subset of A

end;
let J be proper Ideal of A;

let f be Element of A;

coherence

{ (f |^ i) where i is Nat : verum } is Subset of A

proof 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 } ;

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

end;
let J be proper Ideal of A;

let f be Element of A;

coherence

multClSet (J,f) is multiplicatively-closed

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)}

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;

{ 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)

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

{ 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;

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

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)

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))

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 )

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

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

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

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;

( ( 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 ) )

for b_{1} being Subset-Family of R holds verum
;

end;
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 { I where I is Ideal of R : ( I is quasi-prime & I <> [#] R ) } if not R is degenerated

otherwise {} ;

( ( 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

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

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;

coherence

Spectrum A is Subset-Family of A;

compatibility

for b_{1} being Subset-Family of A holds

( b_{1} = Spectrum A iff b_{1} = { I where I is prime Ideal of A : verum } );

end;
:: original: Spectrum

redefine func Spectrum A -> Subset-Family of A equals :: TOPZARI1:def 6

{ I where I is prime Ideal of A : verum } ;

correctness redefine func Spectrum A -> Subset-Family of A equals :: TOPZARI1:def 6

{ I where I is prime Ideal of A : verum } ;

coherence

Spectrum A is Subset-Family of A;

compatibility

for b

( b

proof 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 } ;

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

registration
end;

definition

let R be commutative Ring;

( ( 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 ) )

for b_{1} being Subset-Family of R holds verum
;

end;
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 { I where I is Ideal of R : ( I is quasi-maximal & I <> [#] R ) } if not R is degenerated

otherwise {} ;

( ( 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

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

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;

coherence

m-Spectrum A is Subset-Family of the carrier of A;

compatibility

for b_{1} being Subset-Family of the carrier of A holds

( b_{1} = m-Spectrum A iff b_{1} = { I where I is maximal Ideal of A : verum } );

end;
:: 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 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 } ;

coherence

m-Spectrum A is Subset-Family of the carrier of A;

compatibility

for b

( b

proof 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 } ;

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

registration
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} );

for A being non degenerated commutative Ring holds

( A is local iff ex m being Ideal of A st m-Spectrum A = {m} );

:: 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 );

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

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

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

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

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

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;

( ( 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) ) )

for b_{1} being Subset of (Spectrum R) holds verum
;

end;
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 { p where p is Ideal of R : ( p is quasi-prime & p <> [#] R & E c= p ) } if not R is degenerated

otherwise {} ;

( ( 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

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

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;

coherence

PrimeIdeals (A,E) is Subset of (Spectrum A);

compatibility

for b_{1} being Subset of (Spectrum A) holds

( b_{1} = PrimeIdeals (A,E) iff b_{1} = { p where p is prime Ideal of A : E c= p } );

end;
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 redefine func PrimeIdeals (A,E) -> Subset of (Spectrum A) equals :: TOPZARI1:def 12

{ p where p is prime Ideal of A : E c= p } ;

coherence

PrimeIdeals (A,E) is Subset of (Spectrum A);

compatibility

for b

( b

proof 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 } ;

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;

coherence

not PrimeIdeals (A,J) is empty

end;
let J be proper Ideal of A;

coherence

not PrimeIdeals (A,J) is empty

proof 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

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;

{ a where a is nilpotent Element of A : verum } is Subset of A

end;
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 } ;

{ a where a is nilpotent Element of A : verum } is Subset of A

proof 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 } ;

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;

registration
end;

registration

let A be non degenerated commutative Ring;

coherence

for b_{1} being Subset of A st b_{1} = nilrad A holds

b_{1} is add-closed

end;
coherence

for b

b

proof end;

registration

let A be non degenerated commutative Ring;

coherence

for b_{1} being Subset of A st b_{1} = nilrad A holds

( b_{1} is left-ideal & b_{1} is right-ideal )

end;
coherence

for b

( b

proof 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))

for J being proper Ideal of A holds sqrt J = meet (PrimeIdeals (A,J))

proof end;

::::: [AM] Prop 1.8

:::[AM] Ex 1.13 i)

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

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
end;

:: deftheorem defines J-Rad TOPZARI1:def 14 :

for A being non degenerated commutative Ring holds J-Rad A = meet (m-Spectrum A);

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)

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)

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))

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

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

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))

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)

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 )

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 )

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)

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

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)

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)

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;

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = Spectrum A & ( for F being Subset of b_{1} holds

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) )

uniqueness

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = Spectrum A & ( for F being Subset of b_{1} holds

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) & the carrier of b_{2} = Spectrum A & ( for F being Subset of b_{2} holds

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) holds

b_{1} = b_{2};

end;
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 ( 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) ) ) );

ex b

( the carrier of b

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) )

proof end;

correctness uniqueness

for b

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) & the carrier of b

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) holds

b

proof end;

:: deftheorem Def7 defines ZariskiTS TOPZARI1:def 15 :

for A being non degenerated commutative Ring

for b_{2} being strict TopSpace holds

( b_{2} = ZariskiTS A iff ( the carrier of b_{2} = Spectrum A & ( for F being Subset of b_{2} holds

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) ) );

for A being non degenerated commutative Ring

for b

( b

( F is closed iff ex E being non empty Subset of A st F = PrimeIdeals (A,E) ) ) ) );

registration
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 ) ) )

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

ex b_{1} being commutative Ring st b_{1} is degenerated
end;

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

proof end;

registration
end;

::[AM] p.13 Ex18 iv)

registration
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

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

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

:: 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 ;

ex b_{1} being Function of (ZariskiTS B),(ZariskiTS A) st

for x being Point of (ZariskiTS B) holds b_{1} . x = h " x

for b_{1}, b_{2} being Function of (ZariskiTS B),(ZariskiTS A) st ( for x being Point of (ZariskiTS B) holds b_{1} . x = h " x ) & ( for x being Point of (ZariskiTS B) holds b_{2} . x = h " x ) holds

b_{1} = b_{2}

end;
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 for x being Point of (ZariskiTS B) holds it . x = h " x;

ex b

for x being Point of (ZariskiTS B) holds b

proof end;

uniqueness for b

b

proof 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_{4} being Function of (ZariskiTS B),(ZariskiTS A) holds

( b_{4} = Spec h iff for x being Point of (ZariskiTS B) holds b_{4} . x = h " x );

for A, B being non degenerated commutative Ring

for h being Function of A,B st h is RingHomomorphism holds

for b

( b

::[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))

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

for h being Function of A,B st h is RingHomomorphism holds

Spec h is continuous

proof end;

:: Definition of Nilpotency