:: On Primary Ideals. {P}art {I}
:: by Yasushige Watase
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, FUNCT_1, RELAT_1, CARD_3, XBOOLE_0, TARSKI, XCMPLX_0,
STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, CARD_1, MESFUNC1, GROUP_1, ARYTM_1,
FINSEQ_1, SETFAM_1, INT_2, QUOFIELD, BINOP_1, GROUP_4, NUMBERS, IDEAL_1,
ZFMISC_1, FUNCSDOM, CARD_FIL, RING_1, SQUARE_1, BCIALG_2, NEWTON, RING_2,
XXREAL_0, TOPZARI1, ALGSTR_0, LATTICEA, RINGFRAC, EQREL_1, WAYBEL20,
VECTSP10, PARTFUN1, IDEAL_2, ORDINAL4, RAMSEY_1, GCD_1, LATTICE3,
VECTSP_1, CATALG_1, COHSP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, DOMAIN_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
FINSEQ_1, FINSEQOP, EQREL_1, NEWTON, STRUCT_0, ALGSTR_0, RLVECT_1,
GROUP_1, VECTSP_1, BINOM, VECTSP10, IDEAL_1, RING_1, RING_2, TOPZARI1,
RINGFRAC, COHSP_1;
constructors RELSET_1, FINSEQOP, NEWTON, RINGCAT1, MOD_4, GCD_1, BINOM,
COHSP_1, RINGFRAC;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, STRUCT_0, CARD_1,
VECTSP_1, ALGSTR_1, SUBSET_1, ALGSTR_0, RLVECT_1, IDEAL_1, RING_2, MOD_4,
RING_1, TOPZARI1, FINSEQ_1, INT_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
begin :: Preliminaries: Some Properties of Ideals
reserve R for commutative Ring;
reserve A for non degenerated commutative Ring;
reserve I,J,q for Ideal of A;
reserve p for prime Ideal of A;
reserve M,M1,M2 for Ideal of A/q;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Preliminary Propositions on Ideal Operation
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::\\\\\\\\\
theorem :: IDEAL_2:1
for a,b be Ideal of A, p be prime Ideal of A st a /\ b c= p holds
a c= p or b c= p;
definition
let A;
let a be non empty FinSequence of Ideals(A);
let i be Element of dom a;
redefine func a.i -> non empty Subset of A;
end;
registration
let A;
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;
end;
registration
let A;
let a be non empty FinSequence of Ideals(A);
cluster meet (rng a) -> add-closed left-ideal right-ideal for Subset of A;
end;
::[AM]Prop1.11 ii)
theorem :: IDEAL_2:2
for a be non empty FinSequence of Ideals(A), p be prime Ideal of A
holds
meet rng a c= p implies ex i be object st i in dom a & a.i c= p;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Functional Notation of radical Ideal (L % I) = %I.L
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let A;
let I be Ideal of A;
func %I -> Function of bool the carrier of A, bool the carrier of A
means
:: IDEAL_2:def 1
for x be Subset of A holds it.x = (x % I);
end;
theorem :: IDEAL_2:3
for I be proper Ideal of A, F be non empty FinSequence of Ideals(A) holds
rng((%I)*F) <> {} & rng F <> {} &
meet rng((%I)*F) c= the carrier of A;
::[AM]Ex.1.12. iv) (/\F_i % I) = /\(F_i % I)
theorem :: IDEAL_2:4
for I be proper Ideal of A, F be non empty FinSequence of Ideals(A) holds
(%I).(meet rng F) = meet rng((%I)*F);
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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
:: 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);
end;
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;
end;
theorem :: IDEAL_2:5
I ||^ 1 = I & I *' [#]A = I;
theorem :: IDEAL_2:6
for f,g be 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;
theorem :: IDEAL_2:7
for n be Nat st n > 0 holds I||^(n+1) = I *' (I||^n);
::[AM] Ex.1.13 ii)
theorem :: IDEAL_2:8
sqrt I = sqrt(sqrt I);
::[AM] Ex.1.13 iii) sqrt(I*'J) = sqrt(I /\ J) referred to IDEAL_1:92
theorem :: IDEAL_2:9
sqrt(I /\ J) = sqrt(I) /\ sqrt(J);
::[AM] Ex.1.13 iv)
theorem :: IDEAL_2:10
sqrt I = [#]A iff I = [#]A;
::[AM] Ex1.13 v)
theorem :: IDEAL_2:11
sqrt(I+J) = sqrt( sqrt(I)+ sqrt(J));
::[AM] Ex1.13 vi)
theorem :: IDEAL_2:12
for p be prime Ideal of A, n be non zero Nat holds sqrt(p||^n) = p;
::[AM] Prop1.16
theorem :: IDEAL_2:13
sqrt(I),sqrt(J) are_co-prime implies I,J are_co-prime;
theorem :: IDEAL_2:14
for x,y be 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;
theorem :: IDEAL_2:15
for a,x be Element of the carrier of A/q st
x in (canHom(q)).:I holds a*x in (canHom(q)).:I;
theorem :: IDEAL_2:16
(canHom q).:I is Ideal of A/q;
theorem :: IDEAL_2:17
for x,y be Element of the carrier of A st x in (canHom q)"M1 &
y in (canHom q)"M1 holds x + y in (canHom q)"M1;
theorem :: IDEAL_2:18
for r,x be Element of the carrier of A st x in (canHom q)"M1
holds r*x in (canHom q)"M1;
theorem :: IDEAL_2:19
(canHom q)"M1 is Ideal of A;
theorem :: IDEAL_2:20
q c= (canHom q)"M1;
theorem :: IDEAL_2:21
(canHom q).:(canHom q)"M1 = M1;
theorem :: IDEAL_2:22
q c= I implies (canHom q)"((canHom q).:I) = I;
theorem :: IDEAL_2:23
I c= J implies (canHom q).:I c= (canHom q).:J;
theorem :: IDEAL_2:24
M1 c= M2 implies (canHom q)"M1 c= (canHom q)"M2;
theorem :: IDEAL_2:25
(canHom q)"([#](A/q)) = [#]A;
theorem :: IDEAL_2:26
M is proper implies (canHom q)"M is proper;
theorem :: IDEAL_2:27
q c= I & I is maximal implies (canHom q).:I is maximal;
definition let A,q;
func Psi q -> Function of Ideals(A/q), Ideals(A,q) means
:: IDEAL_2:def 3
for x be Element of Ideals (A/q) holds it.x = (canHom q)"x;
end;
registration let A;
let J be proper Ideal of A;
cluster A/J -> non degenerated commutative;
end;
::[AM] Prop1.1
registration let A;
let q be Ideal of A;
cluster Psi q -> one-to-one c=-monotone;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Primary Ideal Definition of quasi-primary/primary/p-primary [AM]Chapter 4
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let A be well-unital non empty doubleLoopStr,
S be Subset of A;
attr S is quasi-primary means
:: IDEAL_2:def 4
for x,y be Element of A st x*y in S holds x in S or y in sqrt S;
end;
definition
let A be well-unital non empty doubleLoopStr,
S be Subset of A;
attr S is primary means
:: IDEAL_2:def 5
S is proper quasi-primary;
end;
registration
let K be well-unital non empty doubleLoopStr;
cluster primary -> proper quasi-primary for Subset of K;
cluster proper quasi-primary -> primary for Subset of K;
end;
theorem :: IDEAL_2:28
for p be Ideal of A holds p is prime implies p is primary;
registration
let A;
cluster prime -> primary for Ideal of A;
end;
registration
let A be non degenerated commutative Ring;
cluster primary for proper Ideal of A;
end;
theorem :: IDEAL_2:29
I is primary iff I <> [#]A &
for x,y be Element of A st x*y in I & not x in I holds y in sqrt I;
theorem :: IDEAL_2:30
(I <> [#]A &
for x,y be Element of A st x*y in I & not x in I holds y in sqrt I)
iff
A/I is non degenerated &
(for z be Element of A/I st z is zero_divisible holds z is nilpotent );
theorem :: IDEAL_2:31
I is primary iff
A/I is non degenerated &
(for x be Element of A/I st x is zero_divisible holds x is nilpotent);
::[AM] prop4.1
registration let A;
let Q be primary Ideal of A;
cluster sqrt Q -> prime;
end;
registration let A;
let I be primary Ideal of A;
cluster zero_divisible -> nilpotent for Element of A/I;
end;
definition let A;
let P,Q be Ideal of A;
attr Q is P-primary means
:: IDEAL_2:def 6
sqrt Q = P;
end;
definition
let A;
func PRIMARY(A)-> Subset-Family of the carrier of A equals
:: IDEAL_2:def 7
the set of all I where I is primary Ideal of A;
end;
registration
let A;
cluster PRIMARY(A) -> non empty;
end;
definition
let A,p;
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};
end;
theorem :: IDEAL_2:32
for q be proper Ideal of A holds
(canHom q).:(sqrt q) = nilrad(A/q);
theorem :: IDEAL_2:33
for q be proper Ideal of A holds
sqrt q is maximal implies A/q is local;
::[AM] Prop4.2
theorem :: IDEAL_2:34
for q be proper Ideal of A holds sqrt q is maximal implies q is primary;
::[AM] Prop4.2 particular case of maximal Ideal
theorem :: IDEAL_2:35
for M be maximal Ideal of A, n be non zero Nat holds M||^n in PRIMARY(A,M);
theorem :: IDEAL_2:36
for q1,q2 be Ideal of A st q1 in PRIMARY(A,p) & q2 in PRIMARY(A,p)
holds q1 /\ q2 in PRIMARY(A,p);
::[AM] Lemma4.3
::: {Fi} is p-primary, F1 /\ F2 /\...../\Fn is p-primary
theorem :: IDEAL_2:37
for p be prime Ideal of A, F be non empty FinSequence of PRIMARY(A,p)
holds meet rng F in PRIMARY(A,p);
theorem :: IDEAL_2:38
for I be proper Ideal of A, x be Element of (sqrt I)
ex m be Nat
st m in {n where n is Element of NAT: not(x|^n in I)} & x|^(m+1) in I;
theorem :: IDEAL_2:39
for I,J be proper Ideal of A holds
I c= J & J c= sqrt I &
(for x, y be Element of A holds x*y in I & not(x in I) implies y in J)
implies
I is primary & sqrt I = J & J is prime;
theorem :: IDEAL_2:40
for Q be proper Ideal of A holds
(for x,y be Element of A holds x*y in Q & not y in sqrt Q implies x in Q)
implies
Q is primary & sqrt Q is prime;
::[AM] Lemma4.4 i)
theorem :: IDEAL_2:41
for q be Ideal of A, x be Element of A
holds x in q implies q % ({x}-Ideal) = [#]A;
::[AM] Lemma4.4 ii)
theorem :: IDEAL_2:42
for q be Ideal of A, x be Element of A st q in PRIMARY(A,p)
holds not(x in q) implies q % ({x}-Ideal) in PRIMARY(A,p);
::[AM] Lemma4.4 iii)
theorem :: IDEAL_2:43
for q be Ideal of A,x be Element of A st q in PRIMARY(A,p)
holds not x in p implies q % ({x}-Ideal) = q;