IDEAL_2: On Primary Ideals. {P}art {I}

:: On Primary Ideals. {P}art {I}
:: by Yasushige Watase
::
:: Received June 30, 2021
:: 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

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;

cluster a . i -> add-closed left-ideal right-ideal for Subset of A;

coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines % IDEAL_2:def 1 :

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

proof end;

uniqueness

proof end;

end;

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

registration

let R be Ring;
let S be Ideal of R;
let n be Nat;

cluster S ||^ n -> non empty add-closed left-ideal right-ideal ;

coherence

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

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)

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

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

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

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

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

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

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

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

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

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

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

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 = (canHom q) " x;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Psi IDEAL_2:def 3 :

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 by RING_1:16;

end;

::[AM] Prop1.1

registration

let A be non degenerated commutative Ring;
let q be Ideal of A;

cluster Psi q -> one-to-one c=-monotone ;

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

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 :

registration

let K be non empty well-unital doubleLoopStr ;

cluster primary -> proper quasi-primary for Element of K10( the carrier of K);

coherence ;

cluster proper quasi-primary -> primary for Element of K10( the carrier of K);

coherence ;

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 by Th32;

end;

registration

let A be non degenerated commutative Ring;

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

existence

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

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

proof end;

end;

:: deftheorem defines PRIMARY IDEAL_2:def 7 :

registration

let A be non degenerated commutative Ring;

cluster PRIMARY A -> non empty ;

coherence

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 (PRIMARY A) equals :: IDEAL_2:def 8
{ I where I is primary Ideal of A : I is p -primary } ;

coherence

proof end;

end;

:: deftheorem defines PRIMARY IDEAL_2:def 8 :

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)

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

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

proof end;