:: by Yasushige Watase

::

:: Received June 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

theorem Th1: :: IDEAL_2:1

for A being non degenerated commutative Ring

for a, b being Ideal of A

for p being prime Ideal of A holds

( not a /\ b c= p or a c= p or b c= p )

for a, b being Ideal of A

for p being prime Ideal of A holds

( not a /\ b c= p or a c= p or b c= p )

proof end;

definition

let A be non degenerated commutative Ring;

let a be non empty FinSequence of Ideals A;

let i be Element of dom a;

:: original: .

redefine func a . i -> non empty Subset of A;

coherence

a . i is non empty Subset of A

end;
let a be non empty FinSequence of Ideals A;

let i be Element of dom a;

:: original: .

redefine func a . i -> non empty Subset of A;

coherence

a . i is non empty Subset of A

proof end;

registration

let A be non degenerated commutative Ring;

let a be non empty FinSequence of Ideals A;

let i be Element of dom a;

coherence

for b_{1} being Subset of A st b_{1} = a . i holds

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

end;
let a be non empty FinSequence of Ideals A;

let i be Element of dom a;

coherence

for b

( b

proof end;

Th3: for A being non degenerated commutative Ring

for a being non empty FinSequence of Ideals A holds meet (rng a) is Ideal of A

proof end;

registration

let A be non degenerated commutative Ring;

let a be non empty FinSequence of Ideals A;

coherence

for b_{1} being Subset of A st b_{1} = meet (rng a) holds

( b_{1} is add-closed & b_{1} is left-ideal & b_{1} is right-ideal )
by Th3;

end;
let a be non empty FinSequence of Ideals A;

coherence

for b

( b

Th4: for A being non degenerated commutative Ring

for a being non empty FinSequence of Ideals A

for p being prime Ideal of A st len a = 1 & meet (rng a) c= p holds

ex i being object st

( i in dom a & a . i c= p )

proof end;

::[AM]Prop1.11 ii)

theorem :: IDEAL_2:2

for A being non degenerated commutative Ring

for a being non empty FinSequence of Ideals A

for p being prime Ideal of A st meet (rng a) c= p holds

ex i being object st

( i in dom a & a . i c= p )

for a being non empty FinSequence of Ideals A

for p being prime Ideal of A st meet (rng a) c= p holds

ex i being object st

( i in dom a & a . i c= p )

proof end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

:: Functional Notation of radical Ideal (L % I) = %I.L

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

:: Functional Notation of radical Ideal (L % I) = %I.L

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition

let A be non degenerated commutative Ring;

let I be Ideal of A;

ex b_{1} being Function of (bool the carrier of A),(bool the carrier of A) st

for x being Subset of A holds b_{1} . x = x % I

for b_{1}, b_{2} being Function of (bool the carrier of A),(bool the carrier of A) st ( for x being Subset of A holds b_{1} . x = x % I ) & ( for x being Subset of A holds b_{2} . x = x % I ) holds

b_{1} = b_{2}

end;
let I be Ideal of A;

func % I -> Function of (bool the carrier of A),(bool the carrier of A) means :Def1: :: IDEAL_2:def 1

for x being Subset of A holds it . x = x % I;

existence for x being Subset of A holds it . x = x % I;

ex b

for x being Subset of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines % IDEAL_2:def 1 :

for A being non degenerated commutative Ring

for I being Ideal of A

for b_{3} being Function of (bool the carrier of A),(bool the carrier of A) holds

( b_{3} = % I iff for x being Subset of A holds b_{3} . x = x % I );

for A being non degenerated commutative Ring

for I being Ideal of A

for b

( b

theorem Th6: :: IDEAL_2:3

for A being non degenerated commutative Ring

for I being proper Ideal of A

for F being non empty FinSequence of Ideals A holds

( rng ((% I) * F) <> {} & rng F <> {} & meet (rng ((% I) * F)) c= the carrier of A )

for I being proper Ideal of A

for F being non empty FinSequence of Ideals A holds

( rng ((% I) * F) <> {} & rng F <> {} & meet (rng ((% I) * F)) c= the carrier of A )

proof end;

::[AM]Ex.1.12. iv) (/\F_i % I) = /\(F_i % I)

theorem :: IDEAL_2:4

for A being non degenerated commutative Ring

for I being proper Ideal of A

for F being non empty FinSequence of Ideals A holds (% I) . (meet (rng F)) = meet (rng ((% I) * F))

for I being proper Ideal of A

for F being non empty FinSequence of Ideals A holds (% I) . (meet (rng F)) = meet (rng ((% I) * F))

proof end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

:: redefine power of Ideal form FVALUAT1:def 4

:: func S |^ n -> Subset of K

:: due to a conflict of function symobol function |^

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

:: redefine power of Ideal form FVALUAT1:def 4

:: func S |^ n -> Subset of K

:: due to a conflict of function symobol function |^

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition

let K be non empty doubleLoopStr ;

let S be Subset of K;

let n be Nat;

for b_{1} being Subset of K holds verum
;

existence

( ( n = 0 implies ex b_{1} being Subset of K st b_{1} = the carrier of K ) & ( not n = 0 implies ex b_{1} being Subset of K ex f being FinSequence of bool the carrier of K st

( b_{1} = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) ) )

for b_{1}, b_{2} being Subset of K holds

( ( n = 0 & b_{1} = the carrier of K & b_{2} = the carrier of K implies b_{1} = b_{2} ) & ( not n = 0 & ex f being FinSequence of bool the carrier of K st

( b_{1} = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st

( b_{2} = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) implies b_{1} = b_{2} ) )

end;
let S be Subset of K;

let n be Nat;

func S ||^ n -> Subset of K means :Def2: :: IDEAL_2:def 2

it = the carrier of K if n = 0

otherwise ex f being FinSequence of bool the carrier of K st

( it = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) );

consistency it = the carrier of K if n = 0

otherwise ex f being FinSequence of bool the carrier of K st

( it = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) );

for b

existence

( ( n = 0 implies ex b

( b

f . (i + 1) = S *' (f /. i) ) ) ) )

proof end;

uniqueness for b

( ( n = 0 & b

( b

f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st

( b

f . (i + 1) = S *' (f /. i) ) ) implies b

proof end;

:: deftheorem Def2 defines ||^ IDEAL_2:def 2 :

for K being non empty doubleLoopStr

for S being Subset of K

for n being Nat

for b_{4} being Subset of K holds

( ( n = 0 implies ( b_{4} = S ||^ n iff b_{4} = the carrier of K ) ) & ( not n = 0 implies ( b_{4} = S ||^ n iff ex f being FinSequence of bool the carrier of K st

( b_{4} = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) ) ) );

for K being non empty doubleLoopStr

for S being Subset of K

for n being Nat

for b

( ( n = 0 implies ( b

( b

f . (i + 1) = S *' (f /. i) ) ) ) ) );

registration

let R be Ring;

let S be Ideal of R;

let n be Nat;

coherence

( not S ||^ n is empty & S ||^ n is add-closed & S ||^ n is left-ideal & S ||^ n is right-ideal )

end;
let S be Ideal of R;

let n be Nat;

coherence

( not S ||^ n is empty & S ||^ n is add-closed & S ||^ n is left-ideal & S ||^ n is right-ideal )

proof end;

theorem Th8: :: IDEAL_2:5

for A being non degenerated commutative Ring

for I being Ideal of A holds

( I ||^ 1 = I & I *' ([#] A) = I )

for I being Ideal of A holds

( I ||^ 1 = I & I *' ([#] A) = I )

proof end;

theorem Th9: :: IDEAL_2:6

for A being non degenerated commutative Ring

for I being Ideal of A

for f, g being FinSequence of bool the carrier of A st len f >= len g & len g > 0 & I ||^ (len f) = f . (len f) & f . 1 = I & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = I *' (f /. i) ) & I ||^ (len g) = g . (len g) & g . 1 = I & ( for i being Nat st i in dom g & i + 1 in dom g holds

g . (i + 1) = I *' (g /. i) ) holds

f | (dom g) = g

for I being Ideal of A

for f, g being FinSequence of bool the carrier of A st len f >= len g & len g > 0 & I ||^ (len f) = f . (len f) & f . 1 = I & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = I *' (f /. i) ) & I ||^ (len g) = g . (len g) & g . 1 = I & ( for i being Nat st i in dom g & i + 1 in dom g holds

g . (i + 1) = I *' (g /. i) ) holds

f | (dom g) = g

proof end;

theorem Th10: :: IDEAL_2:7

for A being non degenerated commutative Ring

for I being Ideal of A

for n being Nat st n > 0 holds

I ||^ (n + 1) = I *' (I ||^ n)

for I being Ideal of A

for n being Nat st n > 0 holds

I ||^ (n + 1) = I *' (I ||^ n)

proof end;

::[AM] Ex.1.13 ii)

::[AM] Ex.1.13 iii) sqrt(I*'J) = sqrt(I /\ J) referred to IDEAL_1:92

theorem Th12: :: IDEAL_2:9

for A being non degenerated commutative Ring

for I, J being Ideal of A holds sqrt (I /\ J) = (sqrt I) /\ (sqrt J)

for I, J being Ideal of A holds sqrt (I /\ J) = (sqrt I) /\ (sqrt J)

proof end;

::[AM] Ex.1.13 iv)

theorem Th13: :: IDEAL_2:10

for A being non degenerated commutative Ring

for I being Ideal of A holds

( sqrt I = [#] A iff I = [#] A )

for I being Ideal of A holds

( sqrt I = [#] A iff I = [#] A )

proof end;

::[AM] Ex1.13 v)

theorem Th14: :: IDEAL_2:11

for A being non degenerated commutative Ring

for I, J being Ideal of A holds sqrt (I + J) = sqrt ((sqrt I) + (sqrt J))

for I, J being Ideal of A holds sqrt (I + J) = sqrt ((sqrt I) + (sqrt J))

proof end;

::[AM] Ex1.13 vi)

theorem Th15: :: IDEAL_2:12

for A being non degenerated commutative Ring

for p being prime Ideal of A

for n being non zero Nat holds sqrt (p ||^ n) = p

for p being prime Ideal of A

for n being non zero Nat holds sqrt (p ||^ n) = p

proof end;

::[AM] Prop1.16

theorem :: IDEAL_2:13

for A being non degenerated commutative Ring

for I, J being Ideal of A st sqrt I, sqrt J are_co-prime holds

I,J are_co-prime

for I, J being Ideal of A st sqrt I, sqrt J are_co-prime holds

I,J are_co-prime

proof end;

Lm1: for A being non degenerated commutative Ring

for p being prime Ideal of A

for n being non zero Nat holds p ||^ n is proper

proof end;

theorem Th17: :: IDEAL_2:14

for A being non degenerated commutative Ring

for I, q being Ideal of A

for x, y being Element of the carrier of (A / q) st x in (canHom q) .: I & y in (canHom q) .: I holds

x + y in (canHom q) .: I

for I, q being Ideal of A

for x, y being Element of the carrier of (A / q) st x in (canHom q) .: I & y in (canHom q) .: I holds

x + y in (canHom q) .: I

proof end;

theorem Th18: :: IDEAL_2:15

for A being non degenerated commutative Ring

for I, q being Ideal of A

for a, x being Element of the carrier of (A / q) st x in (canHom q) .: I holds

a * x in (canHom q) .: I

for I, q being Ideal of A

for a, x being Element of the carrier of (A / q) st x in (canHom q) .: I holds

a * x in (canHom q) .: I

proof end;

theorem Th19: :: IDEAL_2:16

for A being non degenerated commutative Ring

for I, q being Ideal of A holds (canHom q) .: I is Ideal of (A / q)

for I, q being Ideal of A holds (canHom q) .: I is Ideal of (A / q)

proof end;

theorem Th20: :: IDEAL_2:17

for A being non degenerated commutative Ring

for q being Ideal of A

for M1 being Ideal of (A / q)

for x, y being Element of the carrier of A st x in (canHom q) " M1 & y in (canHom q) " M1 holds

x + y in (canHom q) " M1

for q being Ideal of A

for M1 being Ideal of (A / q)

for x, y being Element of the carrier of A st x in (canHom q) " M1 & y in (canHom q) " M1 holds

x + y in (canHom q) " M1

proof end;

theorem Th21: :: IDEAL_2:18

for A being non degenerated commutative Ring

for q being Ideal of A

for M1 being Ideal of (A / q)

for r, x being Element of the carrier of A st x in (canHom q) " M1 holds

r * x in (canHom q) " M1

for q being Ideal of A

for M1 being Ideal of (A / q)

for r, x being Element of the carrier of A st x in (canHom q) " M1 holds

r * x in (canHom q) " M1

proof end;

theorem Th22: :: IDEAL_2:19

for A being non degenerated commutative Ring

for q being Ideal of A

for M1 being Ideal of (A / q) holds (canHom q) " M1 is Ideal of A

for q being Ideal of A

for M1 being Ideal of (A / q) holds (canHom q) " M1 is Ideal of A

proof end;

theorem Th23: :: IDEAL_2:20

for A being non degenerated commutative Ring

for q being Ideal of A

for M1 being Ideal of (A / q) holds q c= (canHom q) " M1

for q being Ideal of A

for M1 being Ideal of (A / q) holds q c= (canHom q) " M1

proof end;

theorem Th24: :: IDEAL_2:21

for A being non degenerated commutative Ring

for q being Ideal of A

for M1 being Ideal of (A / q) holds (canHom q) .: ((canHom q) " M1) = M1

for q being Ideal of A

for M1 being Ideal of (A / q) holds (canHom q) .: ((canHom q) " M1) = M1

proof end;

theorem Th25: :: IDEAL_2:22

for A being non degenerated commutative Ring

for I, q being Ideal of A st q c= I holds

(canHom q) " ((canHom q) .: I) = I

for I, q being Ideal of A st q c= I holds

(canHom q) " ((canHom q) .: I) = I

proof end;

theorem :: IDEAL_2:23

for A being non degenerated commutative Ring

for I, J, q being Ideal of A st I c= J holds

(canHom q) .: I c= (canHom q) .: J

for I, J, q being Ideal of A st I c= J holds

(canHom q) .: I c= (canHom q) .: J

proof end;

theorem Th27: :: IDEAL_2:24

for A being non degenerated commutative Ring

for q being Ideal of A

for M1, M2 being Ideal of (A / q) st M1 c= M2 holds

(canHom q) " M1 c= (canHom q) " M2

for q being Ideal of A

for M1, M2 being Ideal of (A / q) st M1 c= M2 holds

(canHom q) " M1 c= (canHom q) " M2

proof end;

theorem Th28: :: IDEAL_2:25

for A being non degenerated commutative Ring

for q being Ideal of A holds (canHom q) " ([#] (A / q)) = [#] A

for q being Ideal of A holds (canHom q) " ([#] (A / q)) = [#] A

proof end;

theorem Th29: :: IDEAL_2:26

for A being non degenerated commutative Ring

for q being Ideal of A

for M being Ideal of (A / q) st M is proper holds

(canHom q) " M is proper

for q being Ideal of A

for M being Ideal of (A / q) st M is proper holds

(canHom q) " M is proper

proof end;

Lm2: for A being non degenerated commutative Ring

for q being Ideal of A

for M1, M2 being Ideal of (A / q) holds

( M1 <> M2 iff (canHom q) " M1 <> (canHom q) " M2 )

proof end;

theorem Th30: :: IDEAL_2:27

for A being non degenerated commutative Ring

for I, q being Ideal of A st q c= I & I is maximal holds

(canHom q) .: I is maximal

for I, q being Ideal of A st q c= I & I is maximal holds

(canHom q) .: I is maximal

proof end;

definition

let A be non degenerated commutative Ring;

let q be Ideal of A;

ex b_{1} being Function of (Ideals (A / q)),(Ideals (A,q)) st

for x being Element of Ideals (A / q) holds b_{1} . x = (canHom q) " x

for b_{1}, b_{2} being Function of (Ideals (A / q)),(Ideals (A,q)) st ( for x being Element of Ideals (A / q) holds b_{1} . x = (canHom q) " x ) & ( for x being Element of Ideals (A / q) holds b_{2} . x = (canHom q) " x ) holds

b_{1} = b_{2}

end;
let q be Ideal of A;

func Psi q -> Function of (Ideals (A / q)),(Ideals (A,q)) means :Def3: :: IDEAL_2:def 3

for x being Element of Ideals (A / q) holds it . x = (canHom q) " x;

existence for x being Element of Ideals (A / q) holds it . x = (canHom q) " x;

ex b

for x being Element of Ideals (A / q) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines Psi IDEAL_2:def 3 :

for A being non degenerated commutative Ring

for q being Ideal of A

for b_{3} being Function of (Ideals (A / q)),(Ideals (A,q)) holds

( b_{3} = Psi q iff for x being Element of Ideals (A / q) holds b_{3} . x = (canHom q) " x );

for A being non degenerated commutative Ring

for q being Ideal of A

for b

( b

psi: for A being non degenerated commutative Ring

for q being Ideal of A holds

( Psi q is one-to-one & Psi q is c=-monotone )

proof end;

registration

let A be non degenerated commutative Ring;

let J be proper Ideal of A;

coherence

( not A / J is degenerated & A / J is commutative ) by RING_1:16;

end;
let J be proper Ideal of A;

coherence

( not A / J is degenerated & A / J is commutative ) by RING_1:16;

::[AM] Prop1.1

registration

let A be non degenerated commutative Ring;

let q be Ideal of A;

coherence

( Psi q is one-to-one & Psi q is c=-monotone ) by psi;

end;
let q be Ideal of A;

coherence

( Psi q is one-to-one & Psi q is c=-monotone ) by psi;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

:: Primary Ideal Definition of quasi-primary/primary/p-primary [AM]Chapter 4

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

:: Primary Ideal Definition of quasi-primary/primary/p-primary [AM]Chapter 4

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition

let A be non empty well-unital doubleLoopStr ;

let S be Subset of A;

end;
let S be Subset of A;

attr S is quasi-primary means :Def4: :: IDEAL_2:def 4

for x, y being Element of A holds

( not x * y in S or x in S or y in sqrt S );

for x, y being Element of A holds

( not x * y in S or x in S or y in sqrt S );

:: deftheorem Def4 defines quasi-primary IDEAL_2:def 4 :

for A being non empty well-unital doubleLoopStr

for S being Subset of A holds

( S is quasi-primary iff for x, y being Element of A holds

( not x * y in S or x in S or y in sqrt S ) );

for A being non empty well-unital doubleLoopStr

for S being Subset of A holds

( S is quasi-primary iff for x, y being Element of A holds

( not x * y in S or x in S or y in sqrt S ) );

:: deftheorem defines primary IDEAL_2:def 5 :

for A being non empty well-unital doubleLoopStr

for S being Subset of A holds

( S is primary iff ( S is proper & S is quasi-primary ) );

for A being non empty well-unital doubleLoopStr

for S being Subset of A holds

( S is primary iff ( S is proper & S is quasi-primary ) );

registration

let K be non empty well-unital doubleLoopStr ;

coherence

for b_{1} being Subset of K st b_{1} is primary holds

( b_{1} is proper & b_{1} is quasi-primary )
;

coherence

for b_{1} being Subset of K st b_{1} is proper & b_{1} is quasi-primary holds

b_{1} is primary
;

end;
coherence

for b

( b

coherence

for b

b

theorem Th32: :: IDEAL_2:28

for A being non degenerated commutative Ring

for p being Ideal of A st p is prime holds

p is primary

for p being Ideal of A st p is prime holds

p is primary

proof end;

registration

let A be non degenerated commutative Ring;

for b_{1} being Ideal of A st b_{1} is prime holds

b_{1} is primary
by Th32;

end;
cluster non empty add-closed left-ideal right-ideal prime -> primary for Element of K10( the carrier of A);

coherence for b

b

registration

let A be non degenerated commutative Ring;

ex b_{1} being proper Ideal of A st b_{1} is primary

end;
cluster non empty proper add-closed left-ideal right-ideal primary for Element of K10( the carrier of A);

existence ex b

proof end;

theorem Th33: :: IDEAL_2:29

for A being non degenerated commutative Ring

for I being Ideal of A holds

( I is primary iff ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds

y in sqrt I ) ) )

for I being Ideal of A holds

( I is primary iff ( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds

y in sqrt I ) ) )

proof end;

theorem Th34: :: IDEAL_2:30

for A being non degenerated commutative Ring

for I being Ideal of A holds

( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds

y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds

z is nilpotent ) ) )

for I being Ideal of A holds

( I <> [#] A & ( for x, y being Element of A st x * y in I & not x in I holds

y in sqrt I ) iff ( not A / I is degenerated & ( for z being Element of (A / I) st z is zero_divisible holds

z is nilpotent ) ) )

proof end;

theorem Th35: :: IDEAL_2:31

for A being non degenerated commutative Ring

for I being Ideal of A holds

( I is primary iff ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds

x is nilpotent ) ) )

for I being Ideal of A holds

( I is primary iff ( not A / I is degenerated & ( for x being Element of (A / I) st x is zero_divisible holds

x is nilpotent ) ) )

proof end;

Th36: for A being non degenerated commutative Ring

for Q being primary Ideal of A holds

( sqrt Q is prime & ( for P being prime Ideal of A st Q c= P holds

sqrt Q c= P ) )

proof end;

::[AM] prop4.1

registration

let A be non degenerated commutative Ring;

let Q be primary Ideal of A;

coherence

sqrt Q is prime by Th36;

end;
let Q be primary Ideal of A;

coherence

sqrt Q is prime by Th36;

registration

let A be non degenerated commutative Ring;

let I be primary Ideal of A;

coherence

for b_{1} being Element of (A / I) st b_{1} is zero_divisible holds

b_{1} is nilpotent
by Th35;

end;
let I be primary Ideal of A;

coherence

for b

b

:: deftheorem defines -primary IDEAL_2:def 6 :

for A being non degenerated commutative Ring

for P, Q being Ideal of A holds

( Q is P -primary iff sqrt Q = P );

for A being non degenerated commutative Ring

for P, Q being Ideal of A holds

( Q is P -primary iff sqrt Q = P );

definition

let A be non degenerated commutative Ring;

{ I where I is primary Ideal of A : verum } is Subset-Family of the carrier of A

end;
func PRIMARY A -> Subset-Family of the carrier of A equals :: IDEAL_2:def 7

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

coherence { I where I is primary Ideal of A : verum } ;

{ I where I is primary Ideal of A : verum } is Subset-Family of the carrier of A

proof end;

:: deftheorem defines PRIMARY IDEAL_2:def 7 :

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

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

registration
end;

definition

let A be non degenerated commutative Ring;

let p be prime Ideal of A;

{ I where I is primary Ideal of A : I is p -primary } is non empty Subset of (PRIMARY A)

end;
let p be prime Ideal of A;

func PRIMARY (A,p) -> non empty Subset of (PRIMARY A) equals :: IDEAL_2:def 8

{ I where I is primary Ideal of A : I is p -primary } ;

coherence { I where I is primary Ideal of A : I is p -primary } ;

{ I where I is primary Ideal of A : I is p -primary } is non empty Subset of (PRIMARY A)

proof end;

:: deftheorem defines PRIMARY IDEAL_2:def 8 :

for A being non degenerated commutative Ring

for p being prime Ideal of A holds PRIMARY (A,p) = { I where I is primary Ideal of A : I is p -primary } ;

for A being non degenerated commutative Ring

for p being prime Ideal of A holds PRIMARY (A,p) = { I where I is primary Ideal of A : I is p -primary } ;

theorem Th37: :: IDEAL_2:32

for A being non degenerated commutative Ring

for q being proper Ideal of A holds (canHom q) .: (sqrt q) = nilrad (A / q)

for q being proper Ideal of A holds (canHom q) .: (sqrt q) = nilrad (A / q)

proof end;

theorem Th38: :: IDEAL_2:33

for A being non degenerated commutative Ring

for q being proper Ideal of A st sqrt q is maximal holds

A / q is local

for q being proper Ideal of A st sqrt q is maximal holds

A / q is local

proof end;

Lm3: for R being commutative Ring

for r, r1 being Element of R st r1 in Unit_Set R holds

ex r2 being Element of R st r1 * r2 = 1. R

proof end;

::[AM] Prop4.2

theorem Th39: :: IDEAL_2:34

for A being non degenerated commutative Ring

for q being proper Ideal of A st sqrt q is maximal holds

q is primary

for q being proper Ideal of A st sqrt q is maximal holds

q is primary

proof end;

::[AM] Prop4.2 particular case of maximal Ideal

theorem :: IDEAL_2:35

for A being non degenerated commutative Ring

for M being maximal Ideal of A

for n being non zero Nat holds M ||^ n in PRIMARY (A,M)

for M being maximal Ideal of A

for n being non zero Nat holds M ||^ n in PRIMARY (A,M)

proof end;

theorem Th41: :: IDEAL_2:36

for A being non degenerated commutative Ring

for p being prime Ideal of A

for q1, q2 being Ideal of A st q1 in PRIMARY (A,p) & q2 in PRIMARY (A,p) holds

q1 /\ q2 in PRIMARY (A,p)

for p being prime Ideal of A

for q1, q2 being Ideal of A st q1 in PRIMARY (A,p) & q2 in PRIMARY (A,p) holds

q1 /\ q2 in PRIMARY (A,p)

proof end;

::[AM] Lemma4.3

::: {Fi} is p-primary, F1 /\ F2 /\...../\Fn is p-primary

::: {Fi} is p-primary, F1 /\ F2 /\...../\Fn is p-primary

theorem :: IDEAL_2:37

for A being non degenerated commutative Ring

for p being prime Ideal of A

for F being non empty FinSequence of PRIMARY (A,p) holds meet (rng F) in PRIMARY (A,p)

for p being prime Ideal of A

for F being non empty FinSequence of PRIMARY (A,p) holds meet (rng F) in PRIMARY (A,p)

proof end;

theorem Th43: :: IDEAL_2:38

for A being non degenerated commutative Ring

for I being proper Ideal of A

for x being Element of sqrt I ex m being Nat st

( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )

for I being proper Ideal of A

for x being Element of sqrt I ex m being Nat st

( m in { n where n is Element of NAT : not x |^ n in I } & x |^ (m + 1) in I )

proof end;

theorem Th44: :: IDEAL_2:39

for A being non degenerated commutative Ring

for I, J being proper Ideal of A st I c= J & J c= sqrt I & ( for x, y being Element of A st x * y in I & not x in I holds

y in J ) holds

( I is primary & sqrt I = J & J is prime )

for I, J being proper Ideal of A st I c= J & J c= sqrt I & ( for x, y being Element of A st x * y in I & not x in I holds

y in J ) holds

( I is primary & sqrt I = J & J is prime )

proof end;

theorem Th45: :: IDEAL_2:40

for A being non degenerated commutative Ring

for Q being proper Ideal of A st ( for x, y being Element of A st x * y in Q & not y in sqrt Q holds

x in Q ) holds

( Q is primary & sqrt Q is prime )

for Q being proper Ideal of A st ( for x, y being Element of A st x * y in Q & not y in sqrt Q holds

x in Q ) holds

( Q is primary & sqrt Q is prime )

proof end;

::[AM] Lemma4.4 i)

theorem :: IDEAL_2:41

for A being non degenerated commutative Ring

for q being Ideal of A

for x being Element of A st x in q holds

q % ({x} -Ideal) = [#] A

for q being Ideal of A

for x being Element of A st x in q holds

q % ({x} -Ideal) = [#] A

proof end;

::[AM] Lemma4.4 ii)

theorem :: IDEAL_2:42

for A being non degenerated commutative Ring

for p being prime Ideal of A

for q being Ideal of A

for x being Element of A st q in PRIMARY (A,p) & not x in q holds

q % ({x} -Ideal) in PRIMARY (A,p)

for p being prime Ideal of A

for q being Ideal of A

for x being Element of A st q in PRIMARY (A,p) & not x in q holds

q % ({x} -Ideal) in PRIMARY (A,p)

proof end;

::[AM] Lemma4.4 iii)

theorem :: IDEAL_2:43

for A being non degenerated commutative Ring

for p being prime Ideal of A

for q being Ideal of A

for x being Element of A st q in PRIMARY (A,p) & not x in p holds

q % ({x} -Ideal) = q

for p being prime Ideal of A

for q being Ideal of A

for x being Element of A st q in PRIMARY (A,p) & not x in p holds

q % ({x} -Ideal) = q

proof end;

::: Preliminary Propositions on Ideal Operation

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::\\\\\\\\\