:: On Primary Ideals. {P}art {I}
:: by Yasushige Watase
::
:: Received June 30, 2021
:: Copyright (c) 2021-2026 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, WSIERP_1;
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;
definitions TARSKI, IDEAL_1;
equalities STRUCT_0, FINSEQ_1, ALGSTR_0;
expansions TARSKI, FUNCT_2, IDEAL_1, STRUCT_0, XBOOLE_0, SUBSET_1, TOPZARI1,
RINGFRAC, FUNCT_1, RING_1;
theorems GROUP_1, RLVECT_1, IDEAL_1, FUNCT_2, TARSKI, FUNCT_1, XREAL_1, NAT_1,
RING_1, XBOOLE_0, FINSEQ_1, ORDINAL1, XBOOLE_1, BINOM, RING_2, RELAT_1,
SETFAM_1, TOPZARI1, RINGFRAC, FIELD_1, VECTSP10, VECTSP_2, FINSEQ_5,
PARTFUN1, FINSEQ_3, FINSEQ_2, TOPREALA, CARD_1, INT_1, COHSP_1;
schemes NAT_1, RECDEF_1, INT_1, FUNCT_2;
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 Th1:
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
proof
let a,b be Ideal of A, p be prime Ideal of A;
assume
A1: a /\ b c= p;
a *' b c= a /\ b by IDEAL_1:79; then
a *' b c= p by A1;
hence thesis by TOPZARI1:30;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
a.i in Ideals(A); then
a.i in the set of all I where I is Ideal of A by RING_2:def 3; then
consider ai be Ideal of A such that
A2: ai = a.i;
thus thesis by A2;
end;
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;
coherence
proof
dom a <> {} by RELAT_1:41; then
a.i in rng a by FUNCT_1:3; then
a.i in Ideals(A); then
a.i in the set of all I where I is Ideal of A by RING_2:def 3; then
consider ai be Ideal of A such that
A2: ai = a.i;
thus thesis by A2;
end;
end;
Th3: for a be non empty FinSequence of Ideals(A) holds meet rng a is Ideal of A
proof
let a be non empty FinSequence of Ideals(A);
defpred P[Nat] means
for a be non empty FinSequence of Ideals(A) st len a = $1 holds
meet rng a is Ideal of A;
A1: P[1]
proof
for a be non empty FinSequence of Ideals(A) st len a = 1 holds
meet rng a is Ideal of A
proof
let a be non empty FinSequence of Ideals(A);
assume
A2: len a = 1; then
{1} = dom a by FINSEQ_1:def 3,2; then
1 in dom a by FINSEQ_1:2; then
reconsider e = 1 as Element of dom a;
a = <*a.1*> by A2, FINSEQ_1:40; then
rng a = {a.1} by FINSEQ_1:39; then
meet rng a = a.e by SETFAM_1:10;
hence thesis;
end;
hence thesis;
end;
A5: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A6: P[n];
for a be non empty FinSequence of Ideals(A)
st len a = n+1 holds meet rng a is Ideal of A
proof
let a be non empty FinSequence of Ideals(A);
assume
A7: len a = n+1; then
A8: a = a|n ^<*a/.(n+1)*> by FINSEQ_5:21;
A9: len (a|n) = n by A7,FINSEQ_1:59,NAT_1:11;
reconsider an = a|n as non empty FinSequence of Ideals(A);
reconsider I1 = meet rng an as Ideal of A by A6,A9;
A10: dom a = Seg (n+1) by A7,FINSEQ_1:def 3;
1 <=n+1<=n+1 by NAT_1:11; then
n+1 in dom a by A10; then
reconsider n1 = n + 1 as Element of dom a;
rng <*a/.(n+1)*> = {a/.(n+1)} by FINSEQ_1:39; then
A12: meet rng <*a/.(n+1)*> = a/.(n+1) by SETFAM_1:10
.= a.n1 by A10,PARTFUN1:def 6;
reconsider I2 = meet rng <*a/.n1*> as Ideal of A by A12;
A13: rng an <> {} & rng <*a/.(n+1)*> <> {} by RELAT_1:41;
meet rng a
= meet (rng an \/ rng <*a/.(n+1)*>) by FINSEQ_1:31,A8
.= I1 /\ I2 by A13,SETFAM_1:9;
hence thesis;
end;
hence thesis;
end;
A15: for i being non zero Nat holds P[i] from NAT_1:sch 10(A1,A5);
reconsider n = len a as non zero Nat;
n = len a;
hence thesis by A15;
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;
coherence by Th3;
end;
Th4: for a be non empty FinSequence of Ideals(A), p be prime Ideal of A
st len a = 1 holds
meet rng a c= p implies ex i be object st i in dom a & a.i c= p
proof
let a be non empty FinSequence of Ideals(A), p be prime Ideal of A;
assume
A1: len a = 1; then
A2: {1} = dom a by FINSEQ_1:def 3,FINSEQ_1:2;
a = <*a.1*> by A1,FINSEQ_1:40; then
A4: rng a = {a.1} by FINSEQ_1:39;
assume
A5: meet rng a c= p;
consider i be object such that
A6: i in dom a by A2,XBOOLE_0:def 1;
reconsider i as Nat by A6;
a.i = a.1 by A6,A2,TARSKI:def 1 .= meet rng a by A4,SETFAM_1:10;
hence thesis by A5,A6;
end;
::[AM]Prop1.11 ii)
theorem
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
proof
let a be non empty FinSequence of Ideals(A), p be prime Ideal of A;
defpred P[Nat] means
for a be non empty FinSequence of Ideals(A), p be prime Ideal of A
st len a = $1 holds
meet rng a c= p implies ex i be object st i in dom a & a.i c= p;
A1: P[1] by Th4;
A2: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A3: P[n];
for a be non empty FinSequence of Ideals(A), p be prime Ideal of A
st len a = n+1 holds
(meet rng a c= p implies ex i be object st i in dom a & a.i c= p)
proof
let a be non empty FinSequence of Ideals(A),p be prime Ideal of A;
assume
A4: len a = n+1; then
A5: a = a|n ^<*a/.(n+1)*> by FINSEQ_5:21;
A6: len (a|n) = n by A4,FINSEQ_1:59,NAT_1:11;
reconsider an = a|n as non empty FinSequence of Ideals(A);
A7: dom an = Seg (len an) by FINSEQ_1:def 3 .= Seg n
by A4,FINSEQ_1:59,NAT_1:11;
A8: dom a = Seg (n+1) by A4,FINSEQ_1:def 3;
A9: rng an <> {} & rng <*a/.(n+1)*> <> {} by RELAT_1:41;
A10: meet rng a = meet (rng an \/ rng <*a/.(n+1)*>) by FINSEQ_1:31,A5
.= meet(rng an) /\ meet rng(<*a/.(n+1)*>) by A9,SETFAM_1:9;
meet rng a c= p implies
ex i be object st i in dom a & a.i c= p
proof ::::A
assume
A11: meet rng a c= p;
reconsider I1 = meet(rng an) as Ideal of A by Th3;
reconsider I2 = meet rng(<*a/.(n+1)*>) as Ideal of A by Th3;
per cases by Th1,A11,A10;
suppose I1 c= p; then
consider i be object such that
A13: i in dom an & an.i c= p by A6,A3;
A14: a.i c= p by A13, A5,FINSEQ_1:def 7;
A15: Seg n c= Seg (n+1) by FINSEQ_1:5,NAT_1:11;
consider i1 be object such that
A16: i1 = i and
A17: i1 in dom a & a.i c= p by A14,A13,A7,A8,A15;
thus thesis by A16,A17;
end;
suppose
A18: I2 c= p;
rng <*a/.(n+1)*> = {a/.(n+1)} by FINSEQ_1:39; then
A19: meet rng <*a/.(n+1)*> = a/.(n+1) by SETFAM_1:10
.= a.(n+1) by A8,FINSEQ_1:4,PARTFUN1:def 6;
consider i be object such that
i = n+1 and
A20: i in dom a & a.i c= p by A18,A19,A8,FINSEQ_1:4;
thus thesis by A20;
end;
end;
hence thesis;
end;
hence thesis;
end;
A21: for i being non zero Nat holds P[i] from NAT_1:sch 10(A1,A2);
reconsider n = len a as non zero Nat;
n = len a;
hence thesis by A21;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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
:Def1:
for x be Subset of A holds it.x = (x % I);
existence
proof
deffunc F(Subset of A) = ($1 % I);
ex f being Function of bool the carrier of A, bool the carrier of A st
for X being Subset of A holds f.X = F(X)
from FUNCT_2:sch 4; then
consider f being Function of bool the carrier of A, bool the carrier of A
such that
A1: for X being Subset of A holds f.X = F(X);
take f;
let r be Subset of A;
thus thesis by A1;
end;
uniqueness
proof
let f,g be Function of bool the carrier of A, bool the carrier of A
such that
A2: for X being Subset of A holds f.X = (X % I) and
A3: for X being Subset of A holds g.X = (X % I);
for Y being Subset of A holds f.Y = g.Y
proof
let Y be Subset of A;
f.Y = (Y % I) by A2 .=g.Y by A3;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th6:
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
proof
let I be proper Ideal of A, F be non empty FinSequence of Ideals(A);
reconsider J = meet rng F as Ideal of A by Th3;
A1: rng F c= bool the carrier of A by XBOOLE_1:1; then
reconsider F1 = F as non empty FinSequence of bool the carrier of A
by FINSEQ_1:def 4;
A2: dom %I = bool the carrier of A by FUNCT_2:def 1;
A3: 1 in dom F by FINSEQ_5:6;
1 in dom (%I*F) by A1,A2,RELAT_1:27,A3;
hence thesis by A3,FUNCT_1:3;
end;
::[AM]Ex.1.12. iv) (/\F_i % I) = /\(F_i % I)
theorem
for I be proper Ideal of A, F be non empty FinSequence of Ideals(A) holds
(%I).(meet rng F) = meet rng((%I)*F)
proof
let I be proper Ideal of A, F be non empty FinSequence of Ideals(A);
reconsider J = meet rng F as Ideal of A by Th3;
A1: rng F c= bool the carrier of A by XBOOLE_1:1; then
reconsider F1 = F as non empty FinSequence of bool the carrier of A
by FINSEQ_1:def 4;
A2: dom %I = bool the carrier of A by FUNCT_2:def 1;
A3: dom(%I*F) = dom F by A1,A2,RELAT_1:27;
A4: rng((%I)*F) <> {} by Th6;
A5: rng F c= Ideals(A);
A6: for x be object holds x in (%I).(meet rng F) implies
x in meet rng((%I)*F)
proof
let x be object;
assume x in (%I).(meet rng F); then
A8: x in (J%I) by Def1;
x in {a where a is Element of A: a*I c= J} by A8,IDEAL_1:def 23; then
consider a be Element of A such that
A9: a = x & a*I c= J;
x in meet rng((%I)*F)
proof
assume not x in meet rng((%I)*F); then
consider Y be set such that
A11: Y in rng((%I)*F) & not x in Y by A4,SETFAM_1:def 1;
consider i be object such that
A12: i in dom ((%I)*F) & Y = ((%I)*F).i by A11,FUNCT_1:def 3;
A13: Y = (%I).(F1.i) by A12,FINSEQ_3:120;
reconsider i1 = i as Nat by A12;
i in dom F by A1,A2,RELAT_1:27,A12; then
A14: F.i in rng F by FUNCT_1:def 3;
F.i in Ideals(A) by A14; then
F.i in the set of all I where I is Ideal of A by RING_2:def 3; then
consider Fi be Ideal of A such that
A15: Fi = F.i;
A16: Y = Fi % I by Def1,A13,A15;
meet rng F c= F.i by A14,SETFAM_1:3; then
a*I c= Fi by A9,A15; then
a in {b where b is Element of A: b*I c= Fi};
hence contradiction by A11,A9,A16,IDEAL_1:def 23;
end;
hence thesis;
end;
meet rng((%I)*F) c= (%I).(meet rng F)
proof
let x be object;
assume
A18: x in meet rng((%I)*F); then
consider a be Element of A such that
A19: x = a;
A20: dom((%I)*F1) = dom F1 & len ((%I)*F1) = len F1 &
for i be Nat st i in dom((%I)*F1) holds ((%I)*F1).i = (%I).(F1.i)
by FINSEQ_3:120;
A21: F is Function of dom F, rng F by FUNCT_2:1;
for Y be set st Y in rng F holds a*I c= Y
proof
let Y be set;
assume Y in rng F; then
consider j be object such that
A23: j in dom F & Y = F.j by A21,FUNCT_2:11;
F.j in Ideals(A) by A23,A5,FUNCT_1:3;then
F.j in the set of all I where I is Ideal of A by RING_2:def 3; then
consider Fj be Ideal of A such that
A24: Fj = F.j;
A25: ((%I)*F1).j in rng((%I)*F) by A23,A3,FUNCT_1:def 3;
x in ((%I)*F).j by A25,A18,SETFAM_1:def 1; then
x in (%I).(Fj) by A20,A23, A24; then
A26: x in (Fj%I) by Def1;
a in {b where b is Element of A: b*I c=Fj} by A19,A26,IDEAL_1:def 23;
then
consider b1 be Element of A such that
A27: a = b1 & b1 * I c= Fj;
thus thesis by A23,A24,A27;
end; then
A28: a*I c= meet rng F by Th6,SETFAM_1:5;
x in (%I).(meet rng F)
proof
assume
A29: not x in (%I).(meet rng F);
A30: (%I).(meet rng F) = J%I by Def1;
not(x in {b where b is Element of A: b*I c= J})
by A29,A30,IDEAL_1:def 23;
hence contradiction by A28,A19;
end;
hence thesis;
end;
hence thesis by A6,TARSKI:2;
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:
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
hereby
assume n = 0;
take A = [#]K;
thus A = the carrier of K;
end;
assume
A1: n <> 0;
set D = bool the carrier of K;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
defpred P[set,set,set] means
ex A being Subset of K st A = $2 & $3 = S *' A;
A2: for i being Nat st 1 <= i & i < n1
for x being Element of D ex y being Element of D st P[i,x,y]
proof
let i be Nat such that 1 <= i & i < n1;
let x be Element of D;
take S *' x;
thus thesis;
end;
consider f being FinSequence of D such that
A3: len f = n1 and
A4: f.1 = S or n1 = 0 and
A5: for i being Nat st 1 <= i & i < n1 holds P[i,f.i,f.(i+1)]
from RECDEF_1:sch 4(A2);
take f/.len f, f;
len f in dom f by A1,A3,CARD_1:27,FINSEQ_5:6;
hence f/.len f = f.len f by PARTFUN1:def 6;
thus len f = n by A3;
thus f.1 = S by A1,A4;
let i be Nat such that
A6: i in dom f;
assume i+1 in dom f; then
i+1 <= n1 by A3,FINSEQ_3:25; then
i < n1 by NAT_1:13; then
P[i,f.i,f.(i+1)] by A6,FINSEQ_3:25,A5;
hence thesis by A6,PARTFUN1:def 6;
end;
uniqueness
proof
let S1, S2 be Subset of K;
thus n = 0 & S1 = the carrier of K & S2 = the carrier of K
implies S1 = S2;
assume n <> 0;
given f being FinSequence of bool the carrier of K such that
A10: S1 = f.len f and
A11: len f = n and
A12: f.1 = S and
A13: for i being Nat st i in dom f & i+1 in dom f holds
f.(i+1) = S *' (f/.i);
given g being FinSequence of bool the carrier of K such that
A14: S2 = g.len g and
A15: len g = n and
A16: g.1 = S and
A17: for i being Nat st i in dom g & i+1 in dom g holds
g.(i+1) = S *' (g/.i);
A18: dom f = dom g by A11,A15,FINSEQ_3:29;
for k being Nat st k in dom f holds f.k = g.k
proof
let k be Nat;
defpred P[Nat] means $1 in dom f implies f.$1 = g.$1;
A19: P[0] by FINSEQ_3:24;
A20: for a being Nat st P[a] holds P[a+1]
proof
let a be Nat such that
A21: P[a] and
A22: a+1 in dom f;
per cases;
suppose
A23: a in dom f; then
A24: f/.a = f.a by PARTFUN1:def 6 .= g/.a by A18,A21,A23,PARTFUN1:def 6;
thus f.(a+1) = S *' (f/.a) by A13,A22,A23
.= g.(a+1) by A17,A18,A22,A23,A24;
end;
suppose not a in dom f;
then a = 0 by A22,TOPREALA:2;
hence thesis by A12,A16;
end;
end;
for a being Nat holds P[a] from NAT_1:sch 2(A19,A20);
hence thesis;
end;
hence S1 = S2 by A10,A14,A11,A15,A18,FINSEQ_1:13;
end;
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;
coherence
proof
per cases by NAT_1:6;
suppose
A1: n = 0;
A2: S||^n = the carrier of R by A1,Def2;
thus S||^n is non empty by A1,Def2;
thus S||^n is add-closed by A2;
thus S||^n is left-ideal by A2;
let p, x be Element of R;
thus thesis by A2;
end;
suppose
A3: ex k being Nat st n = k + 1;
then
consider f being FinSequence of bool the carrier of R such that
A4: S||^n = f.len f & len f = n & f.1 = S and
A5: for i being Nat st i in dom f & i+1 in dom f holds
f.(i+1) = S *' (f/.i) by Def2;
defpred P[Nat] means
$1 in dom f implies f.$1 is Ideal of R;
A6: P[0] by FINSEQ_3:24;
A7: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume that
A8: P[m] and
A9: m+1 in dom f;
per cases by A9,TOPREALA:2;
suppose m = 0;
hence thesis by A4;
end;
suppose
A10: m in dom f;
then
A11: f/.m = f.m by PARTFUN1:def 6;
f.(m+1) = S*'(f/.m) by A5,A9,A10;
hence thesis by A10,A8,A11;
end;
end;
A12: for m be Nat holds P[m] from NAT_1:sch 2(A6,A7);
0+1 <= len f by A3,A4,NAT_1:13;
hence thesis by A4,A12,FINSEQ_3:25;
end;
end;
end;
theorem Th8:
I ||^ 1 = I & I *' [#]A = I
proof
set f = <*I*>;
A1: len f = 1 & f.1 = I by FINSEQ_1:40;
A2: for i be Nat st i in dom f & i+1 in dom f holds f.(i+1) = I *' (f/.i)
proof
let i be Nat;
assume
A3: i in dom f & i+1 in dom f;
dom f = {1} by FINSEQ_1:2,38; then
i = 1 & i+1 = 1 by A3,TARSKI:def 1;
hence thesis;
end;
I + [#]A = [#]A by IDEAL_1:74; then
I, [#]A are_co-prime; then
I *' [#]A = I /\ [#]A by IDEAL_1:84 .= I by XBOOLE_1:28;
hence thesis by A1,A2,Def2;
end;
theorem Th9:
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
proof
let f,g be FinSequence of bool the carrier of A;
assume that
A1: 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)) and
A2: (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));
A3: dom f = Seg(len f) by FINSEQ_1:def 3;
A4: dom g = Seg(len g) by FINSEQ_1:def 3;
set f1 = f|(dom g);
A5: dom f1 = dom(f|Seg(len g)) by FINSEQ_1:def 3
.= dom f /\ Seg(len g) by RELAT_1:61
.= Seg (len f) /\ Seg(len g) by FINSEQ_1:def 3
.= Seg(len g) by A1,FINSEQ_1:5,XBOOLE_1:28;
A6: dom f1 = dom g by A5,FINSEQ_1:def 3;
A7: for i being Nat st i in dom f1 & i+1 in dom f1 holds
f1.(i+1) = I *' (f1/.i)
proof
let i be Nat;
assume
A8: i in dom f1 & i+1 in dom f1;
A9: dom f1 c= dom f by A3,A5,A1,FINSEQ_1:5;
A10: f1/.i = f1.i by A8,PARTFUN1:def 6 .= f.i by A8,A6,FUNCT_1:49
.= f/.i by A8,A9,PARTFUN1:def 6;
f1.(i+1) = f.(i+1) by A8,A6,FUNCT_1:49
.= I *' (f1/.i) by A10,A1,A8,A9;
hence thesis;
end;
f1 = g
proof
A11: for k being Nat st k in dom f1 holds f1.k = g.k
proof
let k be Nat;
defpred P[Nat] means $1 in dom f1 implies f1.$1 = g.$1;
A12: P[0]
proof
assume
A13: not P[0];
reconsider F = f1 as FinSequence by A5,FINSEQ_1:def 2;
reconsider x = 0 as object;
x in dom F by A13;
hence contradiction by FINSEQ_3:24;
end;
A15: for a being Nat st P[a] holds P[a+1]
proof
let a be Nat such that
A16: P[a] and
A17: a+1 in dom f1;
per cases;
suppose
A18: a in dom f1; then
A19: f1/.a = f1.a by PARTFUN1:def 6
.= g/.a by A6,A16,A18,PARTFUN1:def 6;
thus f1.(a+1) = I *' (f1/.a) by A7,A17,A18
.= g.(a+1) by A2,A6,A17,A18,A19;
end;
suppose
A20: not a in dom f1;
reconsider F = f1 as FinSequence by A5,FINSEQ_1:def 2;
A21: a in dom F or a = 0 by A17,TOPREALA:2;
A22: 0 < 0 + len g by A1;
1 <= 1 <= len g by A22,NAT_1:19; then
1 in dom g by A4;
hence thesis by A1,A2,A21,A20,FUNCT_1:49;
end;
end;
for a being Nat holds P[a] from NAT_1:sch 2(A12,A15);
hence thesis;
end;
reconsider f1 as FinSequence by A5,FINSEQ_1:def 2;
thus thesis by A5,FINSEQ_1:def 3, A11;
end;
hence thesis;
end;
theorem Th10:
for n be Nat st n > 0 holds I||^(n+1) = I *' (I||^n)
proof
let n be Nat;
assume
A1: n > 0;
consider f be FinSequence of bool the carrier of A such that
A2: I||^(n+1) = f.len f & len f = n+1 & f.1 = I and
A3: for i being Nat st i in dom f & i+1 in dom f holds
f.(i+1) = I *' (f/.i) by Def2;
consider g be FinSequence of bool the carrier of A such that
A4: I||^n = g.len g & len g = n & g.1 = I and
A5: for i being Nat st i in dom g & i+1 in dom g holds
g.(i+1) = I *' (g/.i) by A1,Def2;
A6: len f > len g & len g > 0 by A1,A2,A4,XREAL_1:39;
A7: dom f = Seg(n+1) by A2,FINSEQ_1:def 3;
A8: dom g = Seg(n) by A4,FINSEQ_1:def 3;
A9: 0 < 0 + n by A1;
A10: 1 <=n<=n+1 by NAT_1:19,A9;
1 <= n+1 <= n+1 by NAT_1:12; then
A11: n in dom f & n +1 in dom f by A7,A10;
1 <=n<=n by A9,NAT_1:19; then
A12: n in dom g by A8;
f/.n = f.n by A11,PARTFUN1:def 6 .= (f|(dom g)).n by A12,FUNCT_1:49
.= I||^n by A4,A6,A2,A3,A5,Th9;
hence thesis by A2,A3,A11;
end;
::[AM] Ex.1.13 ii)
theorem
sqrt I = sqrt(sqrt I)
proof
for o be object st o in sqrt(sqrt I) holds o in sqrt I
proof
let o be object;
assume
A1: o in sqrt(sqrt I); then
reconsider o as Element of A;
o in {a where a is Element of A: ex n being Element of NAT st
a|^n in (sqrt I)} by A1,IDEAL_1:def 24; then
consider o1 be Element of A such that
A2: o1 = o and
A3: ex n being Element of NAT st o1|^n in (sqrt I);
consider n1 be Element of NAT such that
A4: o1|^n1 in (sqrt I) by A3;
reconsider x = o1|^n1 as Element of A;
x in {a where a is Element of A: ex n being Element of NAT st
a|^n in I} by A4,IDEAL_1:def 24; then
consider x1 be Element of A such that
A5: x1 = x and
A6: ex m being Element of NAT st x1|^m in I;
consider m1 be Element of NAT such that
A7: x1|^m1 in I by A6;
reconsider nm = n1*m1 as Element of NAT;
o1|^nm in I by A5,A7,BINOM:11; then
o1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in I};
hence thesis by A2,IDEAL_1:def 24;
end; then
sqrt(sqrt I) c= sqrt I;
hence thesis by TOPZARI1:20;
end;
::[AM] Ex.1.13 iii) sqrt(I*'J) = sqrt(I /\ J) referred to IDEAL_1:92
theorem Th12:
sqrt(I /\ J) = sqrt(I) /\ sqrt(J)
proof
A1: for o be object st o in sqrt(I /\ J) holds o in sqrt(I) /\ sqrt(J)
proof
let o be object;
assume
A2: o in sqrt(I /\ J); then
reconsider o as Element of A;
o in {a where a is Element of A: ex n being Element of NAT st
a|^n in (I /\ J)} by A2,IDEAL_1:def 24; then
consider o1 be Element of A such that
A3: o1 = o and
A4: ex n being Element of NAT st o1|^n in I /\ J;
consider n1 be Element of NAT such that
A5: o1|^n1 in I /\ J by A4;
A6: o1|^n1 in I & o1|^n1 in J by A5,XBOOLE_0:def 4; then
o1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in I}; then
A7: o1 in sqrt I by IDEAL_1:def 24;
o1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in J} by A6; then
o1 in sqrt J by IDEAL_1:def 24;
hence thesis by A3,A7,XBOOLE_0:def 4;
end;
sqrt(I) /\ sqrt(J) c= sqrt(I /\ J)
proof
let o be object;
assume
A9: o in sqrt(I) /\ sqrt(J); then
A10: o in sqrt(I) & o in sqrt(J) by XBOOLE_0:def 4;
reconsider o as Element of A by A9;
o in {a where a is Element of A: ex n being Element of NAT st
a|^n in I} by A10,IDEAL_1:def 24; then
consider o1 be Element of A such that
A11: o1 = o and
A12: ex n being Element of NAT st o1|^n in I;
consider n1 be Element of NAT such that
A13: o1|^n1 in I by A12;
o in {a where a is Element of A: ex n being Element of NAT st
a|^n in J} by A10,IDEAL_1:def 24; then
consider o2 be Element of A such that
A14: o2 = o and
A15: ex m being Element of NAT st o2|^m in J;
consider m1 be Element of NAT such that
A16: o2|^m1 in J by A15;
A17: (o1|^n1)*(o1|^m1) = o1|^(n1+m1) by BINOM:10;
reconsider n2 = n1+m1 as Element of NAT;
o1|^n2 in I & o1|^n2 in J by A16, A14,A11, IDEAL_1:def 2, A13,A17;then
o1|^n2 in I /\ J by XBOOLE_0:def 4; then
o1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in I /\ J};
hence thesis by A11,IDEAL_1:def 24;
end;
hence thesis by A1,TARSKI:2;
end;
::[AM] Ex.1.13 iv)
theorem Th13:
sqrt I = [#]A iff I = [#]A
proof
:: =>)
thus sqrt I = [#]A implies I = [#]A
proof
assume sqrt I = [#]A; then
1.A in sqrt I; then
1.A in {a where a is Element of A: ex n being Element of NAT st
a|^n in I} by IDEAL_1:def 24; then
consider o1 be Element of A such that
A3: o1 = 1.A and
A4: ex n being Element of NAT st o1|^n in I;
consider m1 be Element of NAT such that
A5: o1|^m1 in I by A4;
A6: o1|^m1 = 1.A by A3,TOPZARI1:2;
not (I is proper) by A5,A6,IDEAL_1:19;
hence thesis;
end;
:: <=)
thus thesis by TOPZARI1:20;
end;
::[AM] Ex1.13 v)
theorem Th14:
sqrt(I+J) = sqrt( sqrt(I)+ sqrt(J))
proof
:: =>)
A1: for o be object holds o in sqrt(I+J) implies o in sqrt( sqrt(I)+ sqrt(J))
proof
let o be object;
assume o in sqrt(I+J); then
o in {a where a is Element of A: ex n being Element of NAT st
a|^n in I+J} by IDEAL_1:def 24; then
consider o1 be Element of A such that
A3: o1 = o and
A4: ex n being Element of NAT st o1|^n in I+J;
consider m1 be Element of NAT such that
A5: o1|^m1 in I+J by A4;
o1|^m1 in {a + b where a,b is Element of A :
a in I & b in J} by A5,IDEAL_1:def 19; then
consider a1,b1 be Element of A such that
A6: o1|^m1 = a1+b1 and
A7: a1 in I and
A8: b1 in J;
A9: I c= sqrt I by TOPZARI1:20;
A10: J c= sqrt J by TOPZARI1:20;
A11: a1 + b1 in {a + b where a,b is Element of A :
a in sqrt I & b in sqrt J} by A7,A9,A8,A10;
o1|^m1 in sqrt I + sqrt J by A6, A11,IDEAL_1:def 19; then
o1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in sqrt I+ sqrt J};
hence thesis by A3,IDEAL_1:def 24;
end;
:: <=) This has done along with "cluster sqrt I -> add-closed of IDEAL_1";
sqrt( sqrt(I)+ sqrt(J)) c= sqrt(I+J)
proof
let o be object;
assume o in sqrt( sqrt(I)+ sqrt(J)); then
o in {a where a is Element of A: ex n being Element of NAT st
a|^n in sqrt I + sqrt J} by IDEAL_1:def 24; then
consider o1 be Element of A such that
A14: o1 = o and
A15: ex n being Element of NAT st o1|^n in sqrt I+ sqrt J;
consider m1 be Element of NAT such that
A16: o1|^m1 in sqrt I+ sqrt J by A15;
o1|^m1 in {a + b where a,b is Element of A :
a in sqrt I & b in sqrt J} by A16,IDEAL_1:def 19; then
consider a1,b1 be Element of A such that
A17: o1|^m1 = a1+b1 and
A18: a1 in sqrt I and
A19: b1 in sqrt J;
a1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in I} by A18,IDEAL_1:def 24; then
consider a2 be Element of A such that
A20: a2 = a1 and
A21: ex n being Element of NAT st a2|^n in I;
consider n2 be Element of NAT such that
A22: a2|^n2 in I by A21;
b1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in J} by A19,IDEAL_1:def 24; then
consider b2 be Element of A such that
A23: b2 = b1 and
A24: ex m being Element of NAT st b2|^m in J;
consider m2 be Element of NAT such that
A25: b2|^m2 in J by A24;
set p = ((a2,b2) In_Power (n2+m2));
consider f being sequence of the carrier of A such that
A26: Sum p = f.(len p) and
A27: f.0 = 0.A and
A28: for j being Nat, v being Element of A st j < len p &
v = p.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 12;
defpred P[Element of NAT] means f.$1 in I+J;
A29: for i being Element of NAT st 1 <= i & i <= len p holds p.i in I+J
proof
let i be Element of NAT;
assume that
A30: 1 <= i and
A31: i <= len p;
set r = i - 1;
set l = (n2+m2) - r;
1 - 1 <= i - 1 by A30,XREAL_1:9; then
reconsider r as Element of NAT by INT_1:3;
i <= (n2+m2) + 1 by A31,BINOM:def 7; then
r <= ((n2+m2) + 1) - 1 by XREAL_1:9; then
r - r <= (n2+m2) - r by XREAL_1:9; then
reconsider l as Element of NAT by INT_1:3;
i in Seg(len p) by A30,A31; then
A32: i in dom p by FINSEQ_1:def 3; then
A33: p.i = p/.i by PARTFUN1:def 6
.= ((n2+m2) choose r)*a2|^l*b2|^r by A32,BINOM:def 7;
per cases;
suppose
n2 <= l; then
consider k being Nat such that
A34: l = n2 + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
a2|^l = (a2|^n2)*(a2|^k) by A34,BINOM:10; then
a2|^l in I by A22,IDEAL_1:def 2; then
a2|^l in I + J by TARSKI:def 3, IDEAL_1:73;
hence thesis by A33,IDEAL_1:def 3,IDEAL_1:17;
end;
suppose
l < n2;
then
A36: ((n2+m2) + -r) + r < n2 + r by XREAL_1:6;
consider k being Nat such that
A37: r = m2 + k by NAT_1:10,A36,XREAL_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
b2|^r = (b2|^m2)*(b2|^k) by A37,BINOM:10;
then
b2|^r in J by A25,IDEAL_1:def 3; then
b2|^r in I + J by TARSKI:def 3, IDEAL_1:73;
hence thesis by A33,IDEAL_1:def 3;
end;
end;
A38: now
let j be Element of NAT;
assume that
0 <= j and
A39: j < len p;
thus P[j] implies P[j+1]
proof
assume
A40: f.j in I+J;
A41: j + 1 <= len p by A39,NAT_1:13;
1 <= j + 1 by NAT_1:11; then
j + 1 in Seg(len p) by A41; then
j + 1 in dom p by FINSEQ_1:def 3; then
A42: p/.(j+1) = p.(j+1) by PARTFUN1:def 6;
then
A43: p/.(j+1) in I+J by A29,A41,NAT_1:11;
f.(j + 1) = f.j + p/.(j+1) by A28,A39,A42;
hence thesis by A40,A43,IDEAL_1:def 1;
end;
end;
A44: (a2+b2)|^(n2+m2) = Sum((a2,b2) In_Power (n2+m2)) by BINOM:25;
A45: P[0] by A27,IDEAL_1:2;
A46: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from
INT_1:sch 7(A45,A38);
A47: (o1|^m1)|^(n2+m2) in I+J by A17,A23,A20,A44,A26,A46;
reconsider n0 = m1*(n2+m2) as Element of NAT;
A48: o1|^n0 in I + J by A47,BINOM:11;
o1 in {a where a is Element of A: ex n being Element of NAT st
a|^n in I+J} by A48;
hence thesis by A14,IDEAL_1:def 24;
end;
hence thesis by A1,TARSKI:2;
end;
::[AM] Ex1.13 vi)
theorem Th15:
for p be prime Ideal of A, n be non zero Nat holds sqrt(p||^n) = p
proof
let p be prime Ideal of A, n be non zero Nat;
A1: p = sqrt p by TOPZARI1:25,TOPZARI1:20;
defpred P[Nat] means sqrt(p||^$1) = p;
A2: P[1] by A1,Th8;
A3: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A4: P[n];
A5: n > 0;
sqrt (p||^(n+1)) = sqrt (p *' (p||^n)) by A5,Th10
.= sqrt(p /\ (p||^n)) by IDEAL_1:92
.= sqrt(p) /\ sqrt(p||^n) by Th12
.= p by A1,A4;
hence thesis;
end;
for i being non zero Nat holds P[i] from NAT_1:sch 10(A2,A3);
hence thesis;
end;
::[AM] Prop1.16
theorem
sqrt(I),sqrt(J) are_co-prime implies I,J are_co-prime
proof
assume
A1: sqrt(I),sqrt(J) are_co-prime;
sqrt (I +J) = sqrt( sqrt(I)+ sqrt(J)) by Th14 .= [#]A by A1,Th13;
hence thesis by Th13;
end;
Lm1:
for p be prime Ideal of A, n be non zero Nat holds p||^n is proper
proof
let p be prime Ideal of A, n be non zero Nat;
assume
A1: not p||^n is proper;
p = sqrt(p||^n) by Th15 .= [#]A by A1,Th13;
hence contradiction;
end;
theorem Th17:
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
proof
let x,y be Element of the carrier of A/q such that
A1: x in (canHom(q)).:I and
A2: y in (canHom(q)).:I;
consider x0 being object such that
A3: x0 in dom(canHom(q)) and
A4: x0 in I and
A5: x = (canHom(q)).x0 by A1,FUNCT_1:def 6;
consider y0 being object such that
A6: y0 in dom(canHom(q)) and
A7: y0 in I and
A8: y = (canHom(q)).y0 by A2,FUNCT_1:def 6;
A9: dom(canHom(q)) = the carrier of A by FUNCT_2:def 1;
reconsider x1= x0,y1=y0 as Element of A by A3,A6;
A10: (canHom q).x1 = Class(EqRel(A,q),x1) by RING_2:def 5;
A11: (canHom q).y1 = Class(EqRel(A,q),y1) by RING_2:def 5;
A12: x1+y1 in I by A4,A7,IDEAL_1:def 1;
(canHom(q)).(x1+y1) = Class(EqRel(A,q),x1+y1) by RING_2:def 5
.= (canHom q).x1 + (canHom q).y1 by A10,A11,RING_1:13;
hence thesis by A5,A8,A9,FUNCT_1:def 6,A12;
end;
theorem Th18:
for a,x be Element of the carrier of A/q st
x in (canHom(q)).:I holds a*x in (canHom(q)).:I
proof
let a,x be Element of the carrier of A/q such that
A1: x in (canHom(q)).:I;
A2: rng(canHom(q)) = the carrier of A/q by FUNCT_2:def 3;
consider a0 being object such that
A3: a0 in dom(canHom(q)) and
A4: a = (canHom(q)).a0 by A2,FUNCT_1:def 3;
consider x0 being object such that
A5: x0 in dom(canHom(q)) and
A6: x0 in I and
A7: x = (canHom(q)).x0 by A1,FUNCT_1:def 6;
A8: dom(canHom(q)) = the carrier of A by FUNCT_2:def 1;
reconsider a1 = a0 ,x1= x0 as Element of A by A5,A3;
A9: (canHom q).a1 = Class(EqRel(A,q),a1) by RING_2:def 5;
A10: (canHom q).x1 = Class(EqRel(A,q),x1) by RING_2:def 5;
A11: a1*x1 in I by A6,IDEAL_1:def 2;
(canHom(q)).(a1*x1) = Class(EqRel(A,q),a1*x1) by RING_2:def 5
.= (canHom q).a1 * (canHom q).x1 by A9,A10,RING_1:14;
hence thesis by A4, A7, A8,A11, FUNCT_1:def 6;
end;
theorem Th19:
(canHom q).:I is Ideal of A/q
proof
A1: (canHom q).:I is add-closed by Th17;
A2: (canHom q).:I is left-ideal by Th18;
A3: 0.A in I by IDEAL_1:2;
A4: (canHom q).0.A = Class(EqRel(A,q),0.A) by RING_2:def 5
.= 0.(A/q) by RING_1:def 6;
0.A in the carrier of A; then
0.A in dom(canHom q) by FUNCT_2:def 1; then
0.(A/q) in (canHom q).:I by A3,A4,FUNCT_1:def 6;
hence thesis by A1,A2;
end;
theorem Th20:
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
proof
let x,y be Element of the carrier of A such that
A1: x in (canHom q)"M1 and
A2: y in (canHom q)"M1;
A3: (canHom q).x in M1 by A1,FUNCT_1:def 7;
A4: (canHom q).y in M1 by A2,FUNCT_1:def 7;
reconsider a=x,b=y as Element of A;
reconsider x1= Class(EqRel(A,q),a) as Element of A/q by RING_1:12;
reconsider y1= Class(EqRel(A,q),b) as Element of A/q by RING_1:12;
(canHom q).x + (canHom q).y =
x1 + (canHom q).y by RING_2:def 5 .= x1 + y1 by RING_2:def 5
.= Class(EqRel(A,q),a+b) by RING_1:13; then
A5: Class(EqRel(A,q),a+b) in M1 by A3,A4,IDEAL_1:def 1;
A6: (canHom q).(a+b) in M1 by A5,RING_2:def 5;
a+b in A; then
a+b in dom (canHom q) by FUNCT_2:def 1;
hence thesis by A6, FUNCT_1:def 7;
end;
theorem Th21:
for r,x be Element of the carrier of A st x in (canHom q)"M1
holds r*x in (canHom q)"M1
proof
let r,x be Element of the carrier of A such that
A1: x in (canHom q)"M1;
A2: (canHom q).x in M1 by A1,FUNCT_1:def 7;
reconsider a=x,b=r as Element of A;
reconsider x1= Class(EqRel(A,q),a) as Element of A/q by RING_1:12;
reconsider r1= Class(EqRel(A,q),b) as Element of A/q by RING_1:12;
(canHom q).r * (canHom q).x =
r1 * (canHom q).x by RING_2:def 5 .= r1 * x1 by RING_2:def 5
.= Class(EqRel(A,q),a*b) by RING_1:14; then
Class(EqRel(A,q),a*b) in M1 by A2,IDEAL_1:def 2; then
A4: (canHom q).(a*b) in M1 by RING_2:def 5;
a*b in A; then
a*b in dom (canHom q) by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
theorem Th22:
(canHom q)"M1 is Ideal of A
proof
A1: (canHom q)"M1 is add-closed by Th20;
A2: (canHom q)"M1 is left-ideal by Th21;
A3: (canHom q).0.A = Class(EqRel(A,q),0.A) by RING_2:def 5
.= 0.(A/q) by RING_1:def 6;
A4: dom (canHom q) = the carrier of A by FUNCT_2:def 1;
(canHom q).0.A in M1 by A3,IDEAL_1:2; then
0.A in (canHom q)"M1 by A4,FUNCT_1:def 7;
hence thesis by A1,A2;
end;
theorem Th23:
q c= (canHom q)"M1
proof
reconsider m =(canHom q)"M1 as Ideal of A by Th22;
for x be object st x in q holds x in (canHom q)"M1
proof
let x be object;
assume
A1: x in q; then
x in the carrier of A; then
A3: x in dom (canHom q) by FUNCT_2:def 1;
x in ker(canHom q) by A1,RING_2:13; then
x in {v where v is Element of A : (canHom q).v = 0.(A/q)}
by VECTSP10:def 9; then
consider x1 be Element of A such that
A4: x= x1 and
A5: (canHom q).x1 = 0.(A/q);
(canHom q).x in M1 by A5,A4, IDEAL_1:2;
hence thesis by A3, FUNCT_1:def 7;
end;
hence thesis;
end;
theorem Th24:
(canHom q).:(canHom q)"M1 = M1
proof
rng (canHom q) = (the carrier of A/q) by FUNCT_2:def 3;
hence thesis by FUNCT_1:77;
end;
theorem Th25:
q c= I implies (canHom q)"((canHom q).:I) = I
proof
assume q c= I; then
ker(canHom q) = q & q c= I by RING_2:13; then
A2: I + ker(canHom q) c= I by IDEAL_1:75;
(canHom q)"((canHom q).:I) c= I
proof
for x be object st x in (canHom q)"((canHom q).:I) holds x in I
proof
set f = canHom q;
let x be object;
assume
A4: x in f"(f.:I); then
A5: x in dom f & f.x in (f.:I) by FUNCT_1:def 7;
consider x1 be object such that
A6: x1 in dom f and
A7: x1 in I and
A8: f.x = f.x1 by A5,FUNCT_1:def 6;
reconsider a=x,b=x1 as Element of A by A4,A6;
f.a - f.b = 0.(A/q) by A8,RLVECT_1:5; then
f.(a-b) = 0.(A/q) by RING_2:8; then
(a-b) in {v where v is Element of A : f.v = 0.(A/q)}; then
(a-b) in ker f by VECTSP10:def 9; then
consider x3 be object such that
A10: x3 in ker f and
A11: x3 = a-b;
reconsider c = x3 as Element of A by A10;
A12: a = b + c by A11, VECTSP_2:2;
I+ker f={a + b where a,b is Element of A : a in I & b in ker f}
by IDEAL_1:def 19; then
x in I + ker f by A12,A7,A10;
hence thesis by A2;
end;
hence thesis;
end;
hence thesis by FUNCT_2:42;
end;
theorem
I c= J implies (canHom q).:I c= (canHom q).:J
proof
assume
A1: I c= J;
for x be Element of the carrier of A/q st x in (canHom q).:I
holds x in (canHom q).:J
proof
let x be Element of the carrier of A/q;
assume x in (canHom q).:I; then
consider x0 being object such that
A3: x0 in dom canHom(q) and
A4: x0 in I and
A5: x = (canHom(q)).x0 by FUNCT_1:def 6;
thus thesis by A5,A1,A4,A3,FUNCT_1:def 6;
end;
hence thesis;
end;
theorem Th27:
M1 c= M2 implies (canHom q)"M1 c= (canHom q)"M2
proof
assume
A1: M1 c= M2;
for x be Element of the carrier of A st x in (canHom q)"M1
holds x in (canHom q)"M2
proof
let x be Element of the carrier of A;
assume x in (canHom q)"M1; then
x in dom canHom q & (canHom q).x in M1 by FUNCT_1:def 7;
hence thesis by FUNCT_1:def 7,A1;
end;
hence thesis;
end;
theorem Th28:
(canHom q)"([#](A/q)) = [#]A
proof
(canHom q)"([#](A/q)) = (canHom q)"(rng(canHom q))by FUNCT_2:def 3
.= dom(canHom q) by RELAT_1:134 .= [#]A by FUNCT_2:def 1;
hence thesis;
end;
theorem Th29:
M is proper implies (canHom q)"M is proper
proof
assume
A1: M is proper;
assume not (canHom q)"M is proper; then
M = (canHom q).:[#]A by Th24
.= (canHom q).:dom(canHom q) by FUNCT_2:def 1
.= rng(canHom q) by RELAT_1:113 .= [#](A/q) by FUNCT_2:def 3;
hence contradiction by A1;
end;
Lm2:
M1 <> M2 iff (canHom q)"M1 <> (canHom q)"M2
proof
::(=>)
M1 <> M2 implies (canHom q)"M1 <> (canHom q)"M2
proof
assume
A2: M1 <> M2;
assume (canHom q)"M1 = (canHom q)"M2; then
M1 = (canHom q).:(canHom q)"M2 by Th24 .= M2 by Th24;
hence contradiction by A2;
end;
hence thesis;
end;
theorem Th30:
q c= I & I is maximal implies (canHom q).:I is maximal
proof
set M = (canHom q).:I;
reconsider M as Ideal of A/q by Th19;
assume
A1: q c= I & I is maximal;
(canHom q).:I is maximal
proof
assume not (canHom q).:I is maximal; then
per cases;
suppose
not M is proper; then
M = [#](A/q); then
[#]A = (canHom q)"M by Th28 .= I by A1,Th25;
hence contradiction by A1;
end;
suppose
not (M is quasi-maximal); then
consider J be Ideal of A/q such that
A6: M c= J & J <> M & J is proper;
A7: (canHom q)"M <> (canHom q)"J by Lm2,A6;
A8: (canHom q)"J is proper by A6,Th29;
reconsider I2 = (canHom q)"J as Ideal of A by Th22;
(canHom q)"M = I by Th25,A1; then
consider I0 be Ideal of A such that
I0 = I2 and
A9: I c= I0 & I <> I0 & I0 is proper by A6, Th27, A7, A8;
not I is quasi-maximal by A9;
hence contradiction by A1;
end;
end;
hence thesis;
end;
definition let A,q;
func Psi q -> Function of Ideals(A/q), Ideals(A,q) means :Def3:
for x be Element of Ideals (A/q) holds it.x = (canHom q)"x;
existence
proof
defpred P[Element of Ideals (A/q),object] means $2 = (canHom q)"$1;
A1: for x be Element of Ideals (A/q) ex y be Element of Ideals(A,q)
st P[x,y]
proof
let M be Element of Ideals (A/q);
A2: M in Ideals (A/q);
Ideals (A/q) = the set of all a where a is Ideal of A/q by RING_2:def 3;
then
consider J be Ideal of A/q such that
A3: J = M by A2;
A4: (canHom q)"J is Ideal of A by Th22;
q c= (canHom q)"J by Th23; then
(canHom q)"J in { I where I is Ideal of A: q c= I } by A4; then
(canHom q)"M in Ideals(A,q) by A3,TOPZARI1:def 1;
hence thesis;
end;
consider f being Function of Ideals (A/q), Ideals(A,q) such that
A6: for x being Element of Ideals (A/q) holds P[x,f.x] from FUNCT_2:sch 3(A1);
thus thesis by A6;
end;
uniqueness
proof
let f,g be Function of Ideals (A/q), Ideals(A,q);
assume that
A7: for x be Element of Ideals (A/q) holds f.x = (canHom q)"x and
A8: for x be Element of Ideals (A/q) holds g.x = (canHom q)"x;
now
let x be Element of Ideals (A/q);
f.x = (canHom q)"x by A7;
hence f.x = g.x by A8;
end;
hence thesis;
end;
end;
psi:
Psi(q) is one-to-one & Psi(q) is c=-monotone
proof
A1: for x1,x2 be object st x1 in dom Psi(q) & x2 in dom Psi(q)
& (Psi(q)).x1 = (Psi(q)).x2 holds x1 = x2
proof
let x1,x2 be object;
assume
A2: x1 in dom Psi(q) & x2 in dom Psi(q) & (Psi(q)).x1 = (Psi(q)).x2; then
A3: x1 in Ideals (A/q) & x2 in Ideals (A/q); then
A4: x1 in the set of all I where I is Ideal of A/q by RING_2:def 3;
x2 in the set of all I where I is Ideal of A/q by A3,RING_2:def 3;then
consider z2 be Ideal of A/q such that
A5: z2 = x2;
consider z1 be Ideal of A/q such that
A6: z1 = x1 by A4;
A7: (canHom q)"z1 = (Psi(q)).x2 by A2,Def3,A6
.= (canHom q)"z2 by A2,A5,Def3;
z1 = (canHom q).:(canHom q)"z2 by A7,Th24 .= z2 by Th24;
hence thesis by A5,A6;
end;
for x1,x2 be set st x1 in dom(Psi(q)) & x2 in dom(Psi(q)) & x1 c= x2
holds (Psi(q)).x1 c= (Psi(q)).x2
proof
let x1,x2 be set;
assume
A10: x1 in dom(Psi(q)) & x2 in dom(Psi(q)) & x1 c= x2; then
A11: x1 in Ideals (A/q) & x2 in Ideals (A/q); then
A12: x1 in the set of all I where I is Ideal of A/q by RING_2:def 3;
x2 in the set of all I where I is Ideal of A/q by A11,RING_2:def 3;
then
consider z2 be Ideal of A/q such that
A13: z2 = x2;
consider z1 be Ideal of A/q such that
A14: z1 = x1 by A12;
A15: (canHom q)"z1 = (Psi(q)).x1 by A10,Def3,A14;
(canHom q)"z2 = (Psi(q)).x2 by A10,A13,Def3;
hence thesis by A15,A10,A13,A14,Th27;
end;
hence thesis by A1,COHSP_1:def 11;
end;
registration let A;
let J be proper Ideal of A;
cluster A/J -> non degenerated commutative;
coherence by RING_1:16;
end;
::[AM] Prop1.1
registration let A;
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 well-unital non empty doubleLoopStr,
S be Subset of A;
attr S is quasi-primary means
:Def4:
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
S is proper quasi-primary;
end;
registration
let K be well-unital non empty doubleLoopStr;
cluster primary -> proper quasi-primary for Subset of K;
coherence;
cluster proper quasi-primary -> primary for Subset of K;
coherence;
end;
theorem Th32:
for p be Ideal of A holds p is prime implies p is primary
proof
let p be Ideal of A;
assume p is prime; then
reconsider p as prime Ideal of A;
for x,y be Element of A st x*y in p holds x in p or y in sqrt p
proof
let x,y be Element of A;
assume x*y in p; then
A3: x in p or y in p by RING_1:def 1;
p c= sqrt p by TOPZARI1:20;
hence thesis by A3;
end;
hence thesis by Def4;
end;
registration
let A;
cluster prime -> primary for Ideal of A;
coherence by Th32;
end;
registration
let A be non degenerated commutative Ring;
cluster primary for proper Ideal of A;
existence
proof
set m = the maximal Ideal of A;
m is primary;
hence thesis;
end;
end;
theorem Th33:
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
proof
(I <> [#]A &
for a1,a2 be Element of A st a1*a2 in I & not a1 in I holds a2 in sqrt I)
implies I is primary
proof
assume
A1: I <> [#]A &
for a1,a2 be Element of A st a1*a2 in I & not a1 in I
holds a2 in sqrt I; then
A2: I is quasi-primary;
I is proper by A1;
hence thesis by A2;
end;
hence thesis by Def4;
end;
theorem Th34:
(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 )
proof
A1: (I <> [#]A &
for x,y be Element of A st x*y in I & not x in I holds y in sqrt I)
implies
A/I is non degenerated &
(for z be Element of A/I st z is zero_divisible holds z is nilpotent )
proof
assume
A2: (I <> [#]A &
for x,y be Element of A st x*y in I & not x in I holds y in sqrt I);
A3: I is proper by A2;
(for z be Element of A/I st z is zero_divisible holds z is nilpotent)
proof
let z be Element of A/I;
assume z is zero_divisible; then
consider y be Element of (A/I) such that
A5: y <> 0.(A/I) & y*z = 0.(A/I);
consider z0 being Element of A such that
A6: z = Class(EqRel(A,I),z0) by RING_1:11;
consider y0 being Element of A such that
A7: y = Class(EqRel(A,I),y0) by RING_1:11;
A8: not y0 in I
proof
assume y0 in I; then
A10: y0 - 0.A in I;
y = Class(EqRel(A,I),0.A) by A7,A10,RING_1:6
.= 0.(A/I) by RING_1:def 6;
hence contradiction by A5;
end;
Class(EqRel(A,I),0.A) = 0.(A/I) by RING_1:def 6
.= Class(EqRel(A,I),y0*z0) by A5,A6,A7,RING_1:14; then
y0*z0 - 0.A in I by RING_1:6; then
A12: z0 in sqrt I by A8,A2;
z0 in {a where a is Element of A:ex n being Element of NAT
st a|^n in I} by A12,IDEAL_1:def 24; then
consider z1 be Element of A such that
A13: z1 = z0 and
A14: ex n being Element of NAT st z1|^n in I;
consider n1 be Element of NAT such that
A15: z1|^n1 in I by A14;
z0|^n1 - 0.A in I by A15, A13; then
A16: Class(EqRel(A,I),z0|^n1) = Class(EqRel(A,I),0.A) by RING_1:6
.= 0.(A/I) by RING_1:def 6;
n1 <> 0
proof
assume n1 = 0; then
A18: z0|^n1 = 1_A by BINOM:8 .= 1.A;
not I is proper by A15,A13,A18,IDEAL_1:19;
hence contradiction by A2;
end; then
reconsider n1 as non zero Nat;
z|^n1 = 0.(A/I) by A16,A6,FIELD_1:2;
hence thesis;
end;
hence thesis by A3;
end;
A/I is non degenerated &
(for z be Element of A/I st z is zero_divisible holds z is nilpotent)
implies
(I <> [#]A &
for x1,y1 be Element of A st x1*y1 in I & not x1 in I holds y1 in sqrt I)
proof
assume
A19: A/I is non degenerated &
(for z be Element of A/I st z is zero_divisible holds z is nilpotent);
for x1,y1 be Element of A st x1*y1 in I & not x1 in I
holds y1 in sqrt I
proof
let x1,y1 be Element of A;
assume
A20: x1*y1 in I & not x1 in I; then
A21: y1*x1 - 0.A in I;
reconsider z = Class(EqRel(A,I),x1) as Element of A/I by RING_1:12;
reconsider y = Class(EqRel(A,I),y1) as Element of A/I by RING_1:12;
A22: z <> 0.(A/I)
proof
assume z = 0.(A/I); then
Class(EqRel(A,I),x1) = Class(EqRel(A,I),0.A) by RING_1:def 6;
then
x1 - 0.A in I by RING_1:6;
hence contradiction by A20;
end;
y*z = Class(EqRel(A,I),y1*x1) by RING_1:14 .= Class(EqRel(A,I),0.A)
by A21,RING_1:6 .= 0.(A/I) by RING_1:def 6; then
y is zero_divisible by A22; then
y is nilpotent by A19; then
consider n being non zero Nat such that
A25: y|^n = 0.(A/I);
Class(EqRel(A,I),y1|^n) = 0.(A/I) by A25,FIELD_1:2
.= Class(EqRel(A,I),0.A) by RING_1:def 6; then
A26: y1|^n - 0.A in I by RING_1:6;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider I as Subset of A;
y1|^n1 in I by A26; then
y1 in {a where a is Element of A :
ex n be Element of NAT st a|^n in I};
hence thesis by IDEAL_1:def 24;
end;
hence thesis by A19;
end;
hence thesis by A1;
end;
theorem Th35:
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)
proof
A1: I is primary implies
A/I is non degenerated &
(for x be Element of A/I st x is zero_divisible holds x is nilpotent)
proof
assume I is primary; then
I <> [#]A & for x1,y1 be Element of A st x1*y1 in I & not x1 in I holds
y1 in sqrt I by Th33;
hence thesis by Th34;
end;
A/I is non degenerated &
(for x be Element of A/I st x is zero_divisible holds x is nilpotent)
implies I is primary
proof
assume A/I is non degenerated &
(for x be Element of A/I st x is zero_divisible holds x is nilpotent);
then
(I <> [#]A &
for x,y be Element of A st x*y in I & not x in I holds y in sqrt I)
by Th34;
hence thesis by Th33;
end;
hence thesis by A1;
end;
Th36:
for Q be primary Ideal of A holds
sqrt Q is prime & for P be prime Ideal of A st Q c= P holds sqrt Q c= P
proof
let Q be primary Ideal of A;
for x,y be Element of A st x*y in sqrt Q holds x in sqrt Q or y in sqrt Q
proof
set M = {a where a is Element of A: ex n be Element of NAT st a|^n in Q};
let x,y be Element of A;
assume x*y in sqrt Q; then
x*y in M by IDEAL_1:def 24; then
consider z be Element of A such that
A2: z = x*y and
A3: ex n being Element of NAT st z|^n in Q;
consider n1 be Element of NAT such that
A4: z|^n1 in Q by A3;
A5: (x|^n1)*(y|^n1) in Q by A4,A2,BINOM:9;
x in sqrt Q or y in sqrt Q
proof
per cases by A5,Def4;
suppose
(x|^n1) in Q; then
x in M;
hence thesis by IDEAL_1:def 24;
end;
suppose
(y|^n1) in sqrt Q; then
(y|^n1) in M by IDEAL_1:def 24; then
consider y1 be Element of A such that
A9: y1 = (y|^n1) and
A10: ex m being Element of NAT st y1|^m in Q;
consider m1 be Element of NAT such that
A11: y1|^m1 in Q by A10;
reconsider n2 = n1*m1 as Element of NAT;
A12: y|^n2 in Q by A9,A11,BINOM:11;
y in M by A12;
hence thesis by IDEAL_1:def 24;
end;
end;
hence thesis;
end; then
A14: sqrt Q is quasi-prime;
consider P be prime Ideal of A such that
A15: Q c= P by TOPZARI1:9;
P c< [#]A; then
A17: sqrt Q is proper by A15,TOPZARI1:25,XBOOLE_1:59;
for P be prime Ideal of A st Q c= P holds sqrt Q c= P
proof
let P be prime Ideal of A;
assume Q c= P; then
P in {p where p is prime Ideal of A: Q c=p }; then
P in PrimeIdeals(A,Q) by TOPZARI1:def 12; then
A19: meet PrimeIdeals(A,Q) c= P by SETFAM_1:3;
reconsider Q as proper Ideal of A;
thus thesis by A19,TOPZARI1:18;
end;
hence thesis by A14,A17;
end;
::[AM] prop4.1
registration let A;
let Q be primary Ideal of A;
cluster sqrt Q -> prime;
coherence by Th36;
end;
registration let A;
let I be primary Ideal of A;
cluster zero_divisible -> nilpotent for Element of A/I;
coherence by Th35;
end;
definition let A;
let P,Q be Ideal of A;
attr Q is P-primary means
sqrt Q = P;
end;
definition
let A;
func PRIMARY(A)-> Subset-Family of the carrier of A equals
the set of all I where I is primary Ideal of A;
coherence
proof
set M = the set of all I where I is primary Ideal of A;
now let x be object;
assume x in M; then
ex I being primary Ideal of A st x = I;
hence x in bool the carrier of A;
end;
then M c= bool the carrier of A;
hence thesis;
end;
end;
registration
let A;
cluster PRIMARY(A) -> non empty;
coherence
proof
the maximal Ideal of A in the set of all I where I is primary Ideal of A;
hence thesis;
end;
end;
definition
let A,p;
func PRIMARY(A,p) -> non empty Subset of PRIMARY(A) equals
{I where I is primary Ideal of A: I is p-primary};
coherence
proof
reconsider p1 = p as primary Ideal of A;
sqrt p1 = p by TOPZARI1:25,TOPZARI1:20; then
p1 is p-primary; then
A1: p1 in {I where I is primary Ideal of A: I is p-primary};
{I where I is primary Ideal of A: I is p-primary } c= PRIMARY(A)
proof
set X = {I where I is primary Ideal of A: I is p-primary };
let x be object;
assume x in X;
then
consider x1 be primary Ideal of A such that
A2: x1 = x and
x1 is p-primary;
thus thesis by A2;
end;
hence thesis by A1;
end;
end;
theorem Th37:
for q be proper Ideal of A holds
(canHom q).:(sqrt q) = nilrad(A/q)
proof
let q be proper Ideal of A;
A1: for x be object st x in nilrad (A/q) holds x in (canHom q).:(sqrt q)
proof
let x be object;
assume x in nilrad (A/q); then
x in sqrt({0.(A/q)}) by TOPZARI1:17; then
x in {a where a is Element of A/q: ex n being
Element of NAT st a|^n in {0.(A/q)}} by IDEAL_1:def 24; then
consider x1 be Element of A/q such that
A3: x1 = x and
A4: ex n being Element of NAT st x1|^n in {0.(A/q)};
consider n1 be Element of NAT such that
A5: x1|^n1 in {0.(A/q)} by A4;
consider y1 being Element of A such that
A6: x1 = Class(EqRel(A,q),y1) by RING_1:11;
A7: x1 = (canHom q).y1 by A6,RING_2:def 5;
Class(EqRel(A,q),0.A) = 0.(A/q) by RING_1:def 6
.= x1|^n1 by A5,TARSKI:def 1
.= Class(EqRel(A,q),y1|^n1) by A6,FIELD_1:2; then
y1|^n1 - 0.A in q by RING_1:6; then
y1 in {a where a is Element of A:
ex n being Element of NAT st a|^n in q}; then
A8: y1 in sqrt q by IDEAL_1:def 24;
dom canHom q = [#]A by FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 6,A7,A8;
end;
(canHom q).:(sqrt q) c= nilrad (A/q)
proof
let x be object;
assume x in (canHom q).:(sqrt q); then
consider x1 be object such that
A11: x1 in dom canHom q and
A12: x1 in sqrt q and
A13: x = (canHom q).x1 by FUNCT_1:def 6;
reconsider x1 as Element of A by A11;
A14: x1 in {a where a is Element of A:
ex n being Element of NAT st a|^n in q} by A12,IDEAL_1:def 24;
consider x0 be Element of A such that
A15: x0 = x1 and
A16: ex n being Element of NAT st x0|^n in q by A14;
consider n1 be Element of NAT such that
A17: x0|^n1 in q by A16;
A18: x0|^n1 - 0.A in q by A17;
A19: x = Class(EqRel(A,q),x0) by A13,A15,RING_2:def 5;
x in rng (canHom q) by A11, A13,FUNCT_1:def 3; then
reconsider y = x as Element of A/q;
y|^n1 = Class(EqRel(A,q),x0|^n1) by A19,FIELD_1:2
.= Class(EqRel(A,q),0.A) by A18,RING_1:6 .= 0.(A/q) by RING_1:def 6;
then
y|^n1 in {0.(A/q)} by TARSKI:def 1; then
y in {a where a is Element of A/q: ex n being
Element of NAT st a|^n in {0.(A/q)}}; then
y in sqrt {0.(A/q)} by IDEAL_1:def 24;
hence thesis by TOPZARI1:17;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th38:
for q be proper Ideal of A holds
sqrt q is maximal implies A/q is local
proof
let q be proper Ideal of A;
set m = sqrt q;
set E = {I where I is Ideal of (A/q):
I is quasi-maximal & I <> [#](A/q)};
assume
A1: m is maximal;
A2: (canHom q).:m = nilrad(A/q) by Th37;
for m1,m2 be object st m1 in m-Spectrum (A/q) & m2 in m-Spectrum (A/q)
holds m1 = m2
proof
let m1,m2 be object;
assume m1 in m-Spectrum (A/q) & m2 in m-Spectrum (A/q); then
A4: m1 in E & m2 in E by TOPZARI1:def 7; then
consider M1 be Ideal of A/q such that
A5: M1 = m1 and
A6: M1 is quasi-maximal & M1 <> [#](A/q);
consider M2 be Ideal of A/q such that
A7: M2 = m2 and
A8: M2 is quasi-maximal & M2 <> [#](A/q) by A4;
A9: M1 is proper by A6;
A10: M2 is proper by A8;
set S = {I where I is Ideal of A/q: I is quasi-prime & I <> [#](A/q)};
H: Spectrum(A/q) = the set of all I where I is prime Ideal of (A/q)
by TOPZARI1:def 6; then
M1 in Spectrum (A/q) by A6,A9; then
meet Spectrum (A/q) c= M1 by SETFAM_1:3; then
A11: nilrad (A/q) c= M1 by TOPZARI1:19;
set M = nilrad (A/q);
M is maximal by A1,TOPZARI1:20,Th30,A2; then
A12: M is proper quasi-maximal; then
A13: M1 = M or M1 is non proper by A11;
M2 in Spectrum (A/q) by H,A8,A10; then
meet Spectrum (A/q) c= M2 by SETFAM_1:3; then
nilrad (A/q) c= M2 by TOPZARI1:19; then
A15: M2 = M or M2 is non proper by A12;
m1 = m2
proof
assume
A16: m1 <> m2;
per cases by A13,A15;
suppose
M1 = M & M2 = M;
hence contradiction by A16,A5,A7;
end;
suppose
M1 = M & M2 = [#](A/q);
hence contradiction by A8;
end;
suppose
M1 = [#](A/q) & M2=M;
hence contradiction by A6;
end;
suppose
M1 = [#](A/q) & M2= [#](A/q);
hence contradiction by A16,A5,A7;
end;
end;
hence thesis;
end;
hence thesis by TOPZARI1:12;
end;
Lm3:
for r,r1 be Element of R holds
r1 in Unit_Set(R) implies ex r2 be Element of R st r1*r2 = 1.R
proof
let r,r1 be Element of R;
assume
A1: r1 in Unit_Set(R);
r1 in {a where a is Element of R: a is Unit of R } by A1,RINGFRAC:def 5;
then
consider r be Element of [#]R such that
A2: r1 = r & r is Unit of R;
reconsider r1 as Element of R;
{r1}-Ideal = [#]R by A2,RING_2:20; then
A3: 1.R in {r1}-Ideal;
{r1}-Ideal = the set of all r1*r where r is Element of R by IDEAL_1:64;
hence thesis by A3;
end;
::[AM] Prop4.2
theorem Th39:
for q be proper Ideal of A holds sqrt q is maximal implies q is primary
proof
let q be proper Ideal of A;
set m = sqrt q;
assume
A1: m is maximal; then
A2: (canHom q).:m is maximal by TOPZARI1:20,Th30;
reconsider M = (canHom q).:m as Ideal of A/q by Th19;
A3: A/q is local by A1,Th38;
for x be Element of A/q st x is zero_divisible holds x is nilpotent
proof
let x be Element of A/q;
assume
A4: x is zero_divisible;
x is NonUnit of A/q
proof
assume not x is NonUnit of A/q; then
x in {a where a is Element of A/q: a is Unit of A/q }; then
x in Unit_Set(A/q) by RINGFRAC:def 5; then
consider a1 be Element of A/q such that
A6: x*a1 = 1.(A/q) by Lm3;
consider y be Element of A/q such that
A7: y <> 0.(A/q) & y*x = 0.(A/q) by A4;
y = y*1.(A/q) .= (y*x)*a1 by A6,GROUP_1:def 3 .= 0.(A/q) by A7;
hence contradiction by A7;
end; then
consider m1 be maximal Ideal of A/q such that
A8: x in m1 by TOPZARI1:10;
set S = {I where I is Ideal of A/q: I is quasi-maximal & I <> [#](A/q)};
M in S by A2; then
A9: M in m-Spectrum (A/q) by TOPZARI1:def 7;
m1 in S; then
A10: m1 in m-Spectrum (A/q) by TOPZARI1:def 7;
consider M0 be Ideal of A/q such that
A11: m-Spectrum (A/q) = {M0} by A3;
M = M0 by A9,A11,TARSKI:def 1 .= m1 by A10,A11,TARSKI:def 1; then
x in nilrad(A/q) by Th37,A8; then
x in the set of all a where a is nilpotent Element of A/q
by TOPZARI1:def 13; then
consider x0 be nilpotent Element of A/q such that
A13: x0 = x;
thus thesis by A13;
end;
hence thesis by Th35;
end;
::[AM] Prop4.2 particular case of maximal Ideal
theorem
for M be maximal Ideal of A, n be non zero Nat holds M||^n in PRIMARY(A,M)
proof
let M be maximal Ideal of A, n be non zero Nat;
reconsider q = M||^n as proper Ideal of A by Lm1;
sqrt q is maximal by Th15; then
reconsider Mn = M||^n as primary Ideal of A by Th39;
Mn is M-primary by Th15;
hence thesis;
end;
theorem Th41:
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)
proof
let q1,q2 be Ideal of A;
set M = {I where I is primary Ideal of A: I is p-primary };
assume
A1: q1 in PRIMARY(A,p) & q2 in PRIMARY(A,p); then
consider Q1 be primary Ideal of A such that
A2: Q1 = q1 and
A3: Q1 is p-primary;
A4: Q1 <> [#]A;
consider Q2 be primary Ideal of A such that
A5: Q2 = q2 and
A6: Q2 is p-primary by A1;
set Q3 = Q1 /\ Q2;
A7: sqrt Q3 = sqrt(Q1) /\ sqrt (Q2) by Th12;
A8: Q3 <> [#]A by A4, XBOOLE_1:17;
A9: for x,y be Element of A st x*y in Q3 & not x in Q3 holds y in sqrt Q3
proof
let x,y be Element of A;
assume
A10: x*y in Q3 & not x in Q3;
assume not y in sqrt Q3; then
A12: not (y in sqrt(Q1) /\ sqrt (Q2)) by Th12;
per cases by A10,XBOOLE_0:def 4;
suppose
x*y in Q3 & not(x in Q1); then
x*y in Q1 & not(x in Q1) by XBOOLE_0:def 4;
hence contradiction by A3,A6,A12,Def4;
end;
suppose
x*y in Q3 & not(x in Q2); then
x*y in Q2 & not(x in Q2) by XBOOLE_0:def 4;
hence contradiction by A3,A6,A12,Def4;
end;
end;
reconsider Q3 as primary Ideal of A by A9,A8,Th33;
Q3 is p-primary by A3,A6,A7;
hence thesis by A2,A5;
end;
::[AM] Lemma4.3
::: {Fi} is p-primary, F1 /\ F2 /\...../\Fn is p-primary
theorem
for p be prime Ideal of A, F be non empty FinSequence of PRIMARY(A,p)
holds meet rng F in PRIMARY(A,p)
proof
let p be prime Ideal of A, F be non empty FinSequence of PRIMARY(A,p);
set q = meet rng F;
meet rng F in PRIMARY(A,p)
proof
:: By Induction of len F
A1: len F <> 0;
defpred P[Nat] means for F be non empty FinSequence of PRIMARY(A,p) st
$1 = len F holds meet rng F in PRIMARY(A,p);
A2: for n be Nat st n>=1 holds P[n] implies P[n+1]
proof
let n be Nat such that
A3: n>=1 and
A4: P[n];
for F be non empty FinSequence of PRIMARY(A,p) st
n+1 = len F holds meet rng F in PRIMARY(A,p)
proof
let F be non empty FinSequence of PRIMARY(A,p);
assume
A5: n+1 = len F;
len F <> 0; then
consider G be FinSequence of PRIMARY(A,p),
q be Element of PRIMARY(A,p) such that
A6: F = G^<*q*> by FINSEQ_2:19;
A7: Seg(len <*q*>) = dom <*q*> by FINSEQ_1:def 3
.= Seg 1 by FINSEQ_1:def 8;
A8: len F = len G + len <*q*> by A6,FINSEQ_1:22
.= len G + 1 by A7,FINSEQ_1:6;
reconsider G as non empty FinSequence of PRIMARY(A,p) by A3,A5,A8;
A9: meet rng G in PRIMARY(A,p) by A4,A5,A8;
dom G = Seg n by A5,A8,FINSEQ_1:def 3; then
A10: 1 in dom G by A3;
dom <*q*> = Seg 1 by FINSEQ_1:def 8; then
A12: rng G <> {} & rng <*q*> <> {} by A10,RELAT_1:42;
q in {I where I is primary Ideal of A:I is p-primary}; then
consider q1 be primary Ideal of A such that
A13: q1 = q & q1 is p-primary;
consider q2 be primary Ideal of A such that
A14: q2 = meet rng G & q2 is p-primary by A9;
q2 /\ q1 in {I where I is primary Ideal of A: I is p-primary}
by A13,A9,A14,Th41; then
consider q3 be primary Ideal of A such that
A15: q3 = q2 /\ q1 and
A16: q3 is p-primary;
A17: meet rng F = meet(rng(G) \/ rng <*q*>) by A6,FINSEQ_1:31
.= meet(rng(G)) /\ meet(rng <*q*>) by A12,SETFAM_1:9
.= meet(rng(G)) /\ meet {q} by FINSEQ_1:38
.= q3 by A15, A14,A13,SETFAM_1:10;
reconsider Q = meet rng F as primary Ideal of A by A17;
thus thesis by A17,A16;
end;
hence thesis;
end;
A18: P[1]
proof
for F be non empty FinSequence of PRIMARY(A,p) st
1 = len F holds meet rng F in PRIMARY(A,p)
proof
let F be non empty FinSequence of PRIMARY(A,p);
assume 1 = len F; then
A20: dom F = {1} by FINSEQ_1:2,def 3; then
A21: rng F = {F.1} by FUNCT_1:4;
A22: meet rng F = meet {F.1} by A20,FUNCT_1:4 .= F.1 by SETFAM_1:10;
F.1 in {F.1} by TARSKI:def 1;
hence thesis by A22,A21;
end;
hence thesis;
end;
for n be Nat st n>=1 holds P[n] from NAT_1:sch 8(A18,A2);
hence thesis by A1,NAT_1:14;
end;
hence thesis;
end;
theorem Th43:
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
proof
let I be proper Ideal of A, x be Element of sqrt I;
set C = {n where n is Element of NAT: not(x|^n in I)};
x in sqrt I; then
x in {a where a is Element of A: ex n being Element of NAT st
a|^n in I} by IDEAL_1:def 24; then
consider x1 be Element of A such that
A1: x1 = x and
A2: ex n being Element of NAT st x1|^n in I;
consider n1 being Element of NAT such that
A3: x1|^n1 in I by A2;
reconsider n1 as Element of NAT;
A4: not(n1 in {n where n is Element of NAT: not(x|^n in I)})
proof
assume n1 in {n where n is Element of NAT: not(x|^n in I)}; then
consider n0 be Element of NAT such that
A6: n0 = n1 & not(x|^n0 in I);
thus contradiction by A3,A1,A6;
end;
assume
A7: not(ex m be Nat st m in {n where n is Element of NAT: not(x|^n in I)}
& x|^(m+1) in I);
A8: 0 in {n where n is Element of NAT: not(x|^n in I)}
proof
set n = 0;
x|^n = 1_A by BINOM:8 .= 1.A; then
not x|^n in I by IDEAL_1:19;
hence thesis;
end;
{n where n is Element of NAT: not(x|^n in I)} = NAT
proof
defpred P[Nat] means
$1 in {n where n is Element of NAT: not(x|^n in I)};
A12: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n]; then
not (x|^(n+1) in I) by A7;
hence thesis;
end;
A15: P[0] by A8;
for n be Nat holds P[n] from NAT_1:sch 2(A15,A12); then
H: NAT c= {n where n is Element of NAT: not(x|^n in I)};
{n where n is Element of NAT: not(x|^n in I)} c= NAT
proof
now let o be object;
assume o in {n where n is Element of NAT: not(x|^n in I)};
then consider n be Element of NAT such that
I: n = o & not(x|^n in I);
thus o in NAT by I;
end;
hence thesis;
end;
hence thesis by H;
end;
hence contradiction by A4;
end;
theorem Th44:
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
proof
let I,J be proper Ideal of A;
assume that
A1: I c= J & J c= sqrt I and
A2: for x, y be Element of A holds x*y in I & not(x in I) implies y in J;
for x,y be Element of A st x*y in I & not (x in I) holds y in sqrt I
by A1,A2; then
A3: I is primary by Def4;
sqrt I c= J
proof
let x be object;
assume x in sqrt I; then
reconsider x0 = x as Element of sqrt I;
consider m be Nat such that
A5: m in {n where n is Element of NAT: not(x0|^n in I)} &
x0|^(m+1) in I by Th43;
consider m0 be Element of NAT such that
A6: m0 = m & not(x0|^m0 in I) by A5;
per cases by NAT_1:25;
suppose
m = 0; then
x0|^(m+1) = x0 by BINOM:8;
hence thesis by A1,A5;
end;
suppose
1 <= m;
reconsider x0 as Element of A;
x0|^(m+1) = (x0|^m)*(x0|^1) by BINOM:10
.= (x0|^m)*x0 by BINOM:8;
hence thesis by A2,A5,A6;
end;
end; then
sqrt I = J by A1;
hence thesis by A3;
end;
theorem Th45:
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
proof
let Q be proper Ideal of A;
assume
A3: for x,y be Element of A
holds x*y in Q & not y in sqrt Q implies x in Q;
not 1.A in sqrt Q by TOPZARI1:3; then
sqrt Q is proper; then
reconsider P = sqrt Q as proper Ideal of A;
reconsider Q as proper Ideal of A;
A2: Q c= P & P c= sqrt Q by TOPZARI1:20;
for x,y be Element of A holds x*y in Q & not(x in Q) implies y in P
by A3;
hence thesis by A2,Th44;
end;
::[AM] Lemma4.4 i)
theorem
for q be Ideal of A, x be Element of A
holds x in q implies q % ({x}-Ideal) = [#]A
proof
let q be Ideal of A, x be Element of A;
set I = {x}-Ideal;
x in q implies (q %I) = [#]A
proof
assume
A2: x in q;
1.A in (q % I)
proof
q = q-Ideal by IDEAL_1:44; then
A4: I c= q by A2,IDEAL_1:67;
1.A*I c= q by A4,IDEAL_1:71; then
1.A in {a where a is Element of A: a*({x}-Ideal) c= q};
hence thesis by IDEAL_1:def 23;
end; then
not (q % I) is proper by IDEAL_1:19;
hence thesis;
end;
hence thesis;
end;
::[AM] Lemma4.4 ii)
theorem
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)
proof
let q be Ideal of A, x be Element of A;
assume
A1: q in PRIMARY(A,p);
set I = {x}-Ideal;
consider q1 be primary Ideal of A such that
A2: q1 = q and
A3: q1 is p-primary by A1;
set M = {a where a is Element of A: a*I c= q};
reconsider J = (q % I) as Ideal of A;
not(x in q) implies (q % I) in PRIMARY(A,p)
proof
assume
A4: not x in q;
not 1.A in (q % I)
proof
assume 1.A in (q % I); then
1.A in M by IDEAL_1:def 23; then
consider y1 being Element of A such that
A6: 1.A = y1 and
A7: y1*I c= q;
I c= q by A7,A6,IDEAL_1:71;
hence contradiction by A4,IDEAL_1:66;
end; then
A9: (q % I) is proper;
for y be Element of A holds y in (q % I) implies y in p
proof
let y be Element of A;
assume y in (q % I); then
y in M by IDEAL_1:def 23; then
consider y1 being Element of A such that
A11: y1= y and
A12: y1*I c= q;
x in I by IDEAL_1:66; then
A14: y1*x in {y1*i where i is Element of A : i in I};
y1*x in y1*I by A14,IDEAL_1:def 18;
hence thesis by A11, A3, Th33, A4, A2, A12;
end; then
A16: q % I c= p;
A17: p = sqrt (q % I) by A16,TOPZARI1:25, A3,A2,A9,TOPZARI1:21,IDEAL_1:85;
:::::::::::: to prove (q % I) is primary
set Q = (q % I);
reconsider Q as proper Ideal of A by A9;
A18: for a,b be Element of A st a*b in Q & not b in p holds a in Q
proof
let a,b be Element of A;
assume
A19: a*b in Q & not b in p; then
a*b in M by IDEAL_1:def 23; then
consider ab1 being Element of A such that
A20: ab1 = a*b and
A21: ab1*I c= q1 by A2;
A22: for i be Element of A st i in I holds a*i in q1
proof
let i be Element of A;
assume i in I; then
ab1*i in {ab1*i1 where i1 is Element of A : i1 in I}; then
A24: ab1*i in ab1*I by IDEAL_1:def 18;
(a*b)*i = (i*a)*b by GROUP_1:def 3;
hence thesis by A3,Def4,A20,A21,A24,A19;
end;
a*I c= q
proof
for z be object holds z in a*I implies z in q1
proof
let z be object;
assume z in a*I; then
z in {a*i1 where i1 is Element of A : i1 in I}
by IDEAL_1:def 18; then
consider i0 be Element of A such that
A27: z = a*i0 and
A28: i0 in I;
thus thesis by A27,A28,A22;
end;
hence thesis by A2;
end; then
a in {y where y is Element of A: y*I c= q};
hence thesis by IDEAL_1:def 23;
end;
reconsider Q as primary Ideal of A by A18,A17,Th45;
Q is p-primary by A17;
hence thesis;
end;
hence thesis;
end;
::[AM] Lemma4.4 iii)
theorem
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
proof
let q be Ideal of A, x be Element of A;
assume
A1: q in PRIMARY(A,p);
set I = {x}-Ideal;
set M = {a where a is Element of A: a*I c= q};
consider Q be primary Ideal of A such that
A2: Q = q and
A3: Q is p-primary by A1;
not(x in p) implies (q % I) = q
proof
assume
A4: not x in p;
A5: for o be object holds o in (q % I) implies o in q
proof
let o be object;
assume o in q % I; then
o in M by IDEAL_1:def 23; then
consider o1 being Element of A such that
A7: o1 = o and
A8: o1*I c= q;
x in I by IDEAL_1:66; then
o1*x in {o1*i1 where i1 is Element of A : i1 in I}; then
o1*x in o1*I by IDEAL_1:def 18;
hence thesis by A7,Def4,A2,A3,A4,A8;
end;
q % I c= q by A5;
hence thesis by IDEAL_1:85;
end;
hence thesis;
end;