:: On Primary Ideals. {P}art {I}
:: by Yasushige Watase
::
:: Copyright (c) 2021 Association of Mizar Users

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Preliminary Propositions on Ideal Operation
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::\\\\\\\\\
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 )
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
proof end;
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 b1 being Subset of A st b1 = a . i holds
( b1 is add-closed & b1 is left-ideal & b1 is right-ideal )
proof end;
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;
cluster meet (rng a) -> add-closed left-ideal right-ideal for Subset of A;
coherence
for b1 being Subset of A st b1 = meet (rng a) holds
( b1 is add-closed & b1 is left-ideal & b1 is right-ideal )
by Th3;
end;

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

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Functional Notation of radical Ideal (L % I) = %I.L
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let A be non degenerated commutative Ring;
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
ex b1 being Function of (bool the carrier of A),(bool the carrier of A) st
for x being Subset of A holds b1 . x = x % I
proof end;
uniqueness
for b1, b2 being Function of (bool the carrier of A),(bool the carrier of A) st ( for x being Subset of A holds b1 . x = x % I ) & ( for x being Subset of A holds b2 . x = x % I ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines % IDEAL_2:def 1 :
for A being non degenerated commutative Ring
for I being Ideal of A
for b3 being Function of (bool the carrier of A),(bool the carrier of A) holds
( b3 = % I iff for x being Subset of A holds b3 . x = x % I );

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

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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;
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
for b1 being Subset of K holds verum
;
existence
( ( n = 0 implies ex b1 being Subset of K st b1 = the carrier of K ) & ( not n = 0 implies ex b1 being Subset of K ex f being FinSequence of bool the carrier of K st
( b1 = 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) ) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of K holds
( ( n = 0 & b1 = the carrier of K & b2 = the carrier of K implies b1 = b2 ) & ( not n = 0 & ex f being FinSequence of bool the carrier of K st
( b1 = 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
( b2 = 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 b1 = b2 ) )
proof end;
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 b4 being Subset of K holds
( ( n = 0 implies ( b4 = S ||^ n iff b4 = the carrier of K ) ) & ( not n = 0 implies ( b4 = S ||^ n iff ex f being FinSequence of bool the carrier of K st
( b4 = 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) ) ) ) ) );

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

::[AM] Ex.1.13 ii)
theorem :: IDEAL_2:8
for A being non degenerated commutative Ring
for I being Ideal of A holds sqrt I = sqrt (sqrt I)
proof end;

::[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)
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 )
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))
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
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
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 () .: I & y in () .: I holds
x + y in () .: 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 () .: I holds
a * x in () .: I
proof end;

theorem Th19: :: IDEAL_2:16
for A being non degenerated commutative Ring
for I, q being Ideal of A holds () .: 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 () " M1 & y in () " M1 holds
x + y in () " 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 () " M1 holds
r * x in () " 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 () " 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= () " 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 () .: (() " 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
() " (() .: 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
() .: I c= () .: 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
() " M1 c= () " M2
proof end;

theorem Th28: :: IDEAL_2:25
for A being non degenerated commutative Ring
for q being Ideal of A holds () " ([#] (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
() " 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 () " M1 <> () " 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
() .: I is maximal
proof end;

definition
let A be non degenerated commutative Ring;
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 = () " x;
existence
ex b1 being Function of (Ideals (A / q)),(Ideals (A,q)) st
for x being Element of Ideals (A / q) holds b1 . x = () " x
proof end;
uniqueness
for b1, b2 being Function of (Ideals (A / q)),(Ideals (A,q)) st ( for x being Element of Ideals (A / q) holds b1 . x = () " x ) & ( for x being Element of Ideals (A / q) holds b2 . x = () " x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Psi IDEAL_2:def 3 :
for A being non degenerated commutative Ring
for q being Ideal of A
for b3 being Function of (Ideals (A / q)),(Ideals (A,q)) holds
( b3 = Psi q iff for x being Element of Ideals (A / q) holds b3 . x = () " x );

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;
cluster QuotientRing (A,J) -> non degenerated commutative ;
coherence
( not A / J is degenerated & A / J is commutative )
by RING_1:16;
end;

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

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

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

definition
let A be non empty well-unital doubleLoopStr ;
let S be Subset of A;
attr S is primary means :: IDEAL_2:def 5
( S is proper & S is quasi-primary );
end;

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

registration
let K be non empty well-unital doubleLoopStr ;
cluster primary -> proper quasi-primary for Element of K10( the carrier of K);
coherence
for b1 being Subset of K st b1 is primary holds
( b1 is proper & b1 is quasi-primary )
;
cluster proper quasi-primary -> primary for Element of K10( the carrier of K);
coherence
for b1 being Subset of K st b1 is proper & b1 is quasi-primary holds
b1 is primary
;
end;

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

registration
let A be non degenerated commutative Ring;
cluster non empty add-closed left-ideal right-ideal prime -> primary for Element of K10( the carrier of A);
coherence
for b1 being Ideal of A st b1 is prime holds
b1 is primary
by Th32;
end;

registration
let A be non degenerated commutative Ring;
existence
ex b1 being proper Ideal of A st b1 is primary
proof end;
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 ) ) )
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 ) ) )
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 ) ) )
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;
cluster sqrt Q -> prime ;
coherence
sqrt Q is prime
by Th36;
end;

registration
let A be non degenerated commutative Ring;
let I be primary Ideal of A;
cluster zero_divisible -> nilpotent for Element of the carrier of (A / I);
coherence
for b1 being Element of (A / I) st b1 is zero_divisible holds
b1 is nilpotent
by Th35;
end;

definition
let A be non degenerated commutative Ring;
let P, Q be Ideal of A;
attr Q is P -primary means :: IDEAL_2:def 6
sqrt Q = P;
end;

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

definition
let A be non degenerated commutative Ring;
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 } is Subset-Family of the carrier of A
proof end;
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 } ;

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

definition
let A be non degenerated commutative Ring;
let p be prime Ideal of A;
func PRIMARY (A,p) -> non empty Subset of () 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 } is non empty Subset of ()
proof end;
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 } ;

theorem Th37: :: IDEAL_2:32
for A being non degenerated commutative Ring
for q being proper Ideal of A holds () .: (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
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
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)
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)
proof end;

::[AM] Lemma4.3
::: {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)
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 )
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 )
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 )
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 % () = [#] 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 % () 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 % () = q
proof end;