:: Quotient Rings
:: by Artur Korni{\l}owicz
::
:: Received December 7, 2005
:: Copyright (c) 2005-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 RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_1, ARYTM_3,
SUPINF_2, RELAT_1, INT_2, CARD_FIL, TARSKI, GROUP_4, IDEAL_1, VECTSP_2,
GROUP_1, FUNCSDOM, EQREL_1, STRUCT_0, WAYBEL20, PARTFUN1, RELAT_2,
SETWISEO, FUNCT_1, MESFUNC1, BINOP_1, VECTSP_1, LATTICES, WELLORD2,
ORDERS_1, WELLORD1, RING_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETWISEO, RELAT_1, RELSET_1, FUNCT_1,
PARTFUN1, ALG_1, RELAT_2, EQREL_1, WELLORD1, WELLORD2, ORDERS_1, BINOP_1,
DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_2,
IDEAL_1;
constructors WELLORD1, WELLORD2, BINOP_1, SETWISEO, ORDERS_1, EQREL_1, GCD_1,
IDEAL_1, DOMAIN_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSUB_1, EQREL_1, STRUCT_0,
VECTSP_1, ALGSTR_1, QUOFIELD, IDEAL_1;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, RELAT_1, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2,
IDEAL_1, ORDERS_1, STRUCT_0, ALGSTR_0;
equalities WELLORD1, STRUCT_0, ALGSTR_0;
expansions TARSKI, XBOOLE_0, GROUP_1, VECTSP_1, VECTSP_2, IDEAL_1, ORDERS_1,
STRUCT_0;
theorems VECTSP_1, TARSKI, FUNCT_1, RLVECT_1, VECTSP_2, XBOOLE_0, FUNCT_2,
BINOP_1, ZFMISC_1, GROUP_1, IDEAL_1, RELAT_1, EQREL_1, SETWISEO,
ORDERS_1, WELLORD2, RELAT_2, SUBSET_1;
schemes EQREL_1, BINOP_1;
begin :: Preliminaries
theorem Th1:
for L being add-associative right_zeroed right_complementable
non empty addLoopStr, a, b being Element of L holds a - b + b = a
proof
let L be add-associative right_zeroed right_complementable non empty
addLoopStr, a, b be Element of L;
thus a-b+b = a+(-b+b) by RLVECT_1:def 3
.= a+0.L by RLVECT_1:5
.= a by RLVECT_1:def 4;
end;
theorem Th2:
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr, b, c being Element of L holds c = b - (b - c)
proof
let L be add-associative right_zeroed right_complementable Abelian non
empty addLoopStr, b, c be Element of L;
set a = b - c;
a+c-a = c-a+a by RLVECT_1:28
.= c by Th1;
hence thesis by Th1;
end;
theorem Th3:
for L being add-associative right_zeroed right_complementable Abelian
non empty addLoopStr,
a, b, c being Element of L holds a - b - (c - b) = a - c
proof
let L be add-associative right_zeroed right_complementable Abelian non
empty addLoopStr, a, b, c be Element of L;
thus a-b-(c-b) = a-b-c+b by RLVECT_1:29
.= a-b+b-c by RLVECT_1:28
.= a-(b-b)-c by RLVECT_1:29
.= a-0.L-c by RLVECT_1:15
.= a-c by RLVECT_1:13;
end;
begin :: Ideals
definition
let K be non empty multMagma, S be Subset of K;
attr S is quasi-prime means
for a, b being Element of K st a*b in S holds a in S or b in S;
end;
definition
let K be non empty multLoopStr, S be Subset of K;
attr S is prime means
S is proper quasi-prime;
end;
definition
let R be non empty doubleLoopStr;
let I be Subset of R;
attr I is quasi-maximal means
for J being Ideal of R st I c= J holds J = I or J is non proper;
end;
definition
let R be non empty doubleLoopStr;
let I be Subset of R;
attr I is maximal means
I is proper quasi-maximal;
end;
registration
let K be non empty multLoopStr;
cluster prime -> proper quasi-prime for Subset of K;
coherence;
cluster proper quasi-prime -> prime for Subset of K;
coherence;
end;
registration
let R be non empty doubleLoopStr;
cluster maximal -> proper quasi-maximal for Subset of R;
coherence;
cluster proper quasi-maximal -> maximal for Subset of R;
coherence;
end;
registration
let R be non empty addLoopStr;
cluster [#]R -> add-closed;
coherence;
end;
registration
let R be non empty multMagma;
cluster [#]R -> left-ideal right-ideal;
coherence;
end;
theorem
for R being domRing holds {0.R} is prime
proof
let R be domRing;
not 1_R in {0.R} by TARSKI:def 1;
hence {0.R} is proper by IDEAL_1:19;
let a, b be Element of R;
assume a*b in {0.R};
then a*b = 0.R by TARSKI:def 1;
then a = 0.R or b = 0.R by VECTSP_2:def 1;
hence thesis by TARSKI:def 1;
end;
begin :: Equivalence Relation
reserve R for Ring,
I for Ideal of R,
a, b for Element of R;
Lm1: for R being add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr,
I being Ideal of R ex E being Equivalence_Relation of the carrier of R st
for x, y being object holds [x,y] in E iff x in the carrier of
R & y in the carrier of R & ex P, Q being Element of R st P = x & Q = y & P-Q
in I
proof
let R be add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr, I be Ideal of R;
defpred P[object,object] means
ex P,Q being Element of R st P = $1 & Q = $2 & P-Q
in I;
A1: for x,y being object st P[x,y] holds P[y,x]
proof
let x,y be object;
given P,Q being Element of R such that
A2: P = x & Q = y & P-Q in I;
take Q,P;
-(P-Q) = Q-P by RLVECT_1:33;
hence thesis by A2,IDEAL_1:13;
end;
A3: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z]
proof
let x,y,z be object;
assume P[x,y];
then consider P,Q being Element of R such that
A4: P = x & Q = y & P-Q in I;
assume P[y,z];
then consider W,S being Element of R such that
A5: W = y & S = z & W-S in I;
take P,S;
P-Q+(Q-S) = P-Q+Q-S by RLVECT_1:28
.= P-S by Th1;
hence thesis by A4,A5,IDEAL_1:def 1;
end;
A6: for x being object st x in the carrier of R holds P[x,x]
proof
let x be object;
assume x in the carrier of R;
then reconsider x as Element of R;
x-x = 0.R by RLVECT_1:15;
hence thesis by IDEAL_1:2;
end;
thus ex EqR being Equivalence_Relation of the carrier of R st
for x,y being object
holds [x,y] in EqR iff x in the carrier of R & y in the carrier of R & P[x,
y] from EQREL_1:sch 1(A6,A1,A3);
end;
definition
let R be add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr;
let I be Ideal of R;
func EqRel(R,I) -> Relation of R means
:Def5:
for a, b being Element of R holds [a,b] in it iff a-b in I;
existence
proof
consider E being Equivalence_Relation of the carrier of R such that
A1: for x, y being object holds [x,y] in E iff x in the carrier of R & y
in the carrier of R & ex P, Q being Element of R st P = x & Q = y & P-Q in I
by Lm1;
take E;
let a, b be Element of R;
thus [a,b] in E implies a-b in I
proof
assume [a,b] in E;
then ex P, Q being Element of R st P = a & Q = b & P-Q in I by A1;
hence thesis;
end;
thus thesis by A1;
end;
uniqueness
proof
let A, B be Relation of R such that
A2: for a, b being Element of R holds [a,b] in A iff a-b in I and
A3: for a, b being Element of R holds [a,b] in B iff a-b in I;
let x, y be object;
thus [x,y] in A implies [x,y] in B
proof
assume
A4: [x,y] in A;
then reconsider x, y as Element of R by ZFMISC_1:87;
x-y in I by A2,A4;
hence thesis by A3;
end;
assume
A5: [x,y] in B;
then reconsider x, y as Element of R by ZFMISC_1:87;
x-y in I by A3,A5;
hence thesis by A2;
end;
end;
registration
let R be add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr;
let I be Ideal of R;
cluster EqRel(R,I) -> non empty total symmetric transitive;
coherence
proof
set A = EqRel(R,I);
consider B being Equivalence_Relation of the carrier of R such that
A1: for x, y being object holds [x,y] in B iff x in the carrier of R & y
in the carrier of R & ex P, Q being Element of R st P = x & Q = y & P-Q in I
by Lm1;
A = B
proof
let x, y be object;
thus [x,y] in A implies [x,y] in B
proof
assume
A2: [x,y] in A;
then reconsider x, y as Element of R by ZFMISC_1:87;
x-y in I by A2,Def5;
hence thesis by A1;
end;
assume [x,y] in B;
then ex P, Q being Element of R st P = x & Q = y & P-Q in I by A1;
hence thesis by Def5;
end;
hence thesis by EQREL_1:9,RELAT_1:40;
end;
end;
theorem Th5:
for R being add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr
for I being Ideal of R, a,b being Element of R
holds a in Class(EqRel(R,I),b) iff a-b in I
proof
let R be add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr;
let I be Ideal of R, a,b be Element of R;
set E = EqRel(R,I);
hereby
assume a in Class(E,b);
then [a,b] in E by EQREL_1:19;
hence a-b in I by Def5;
end;
assume a-b in I;
then [a,b] in E by Def5;
hence thesis by EQREL_1:19;
end;
theorem Th6:
for R being add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr
for I being Ideal of R, a,b being Element of R
holds Class(EqRel(R,I),a) = Class(EqRel(R,I),b) iff a-b in I
proof
let R be add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr;
let I be Ideal of R, a,b be Element of R;
set E = EqRel(R,I);
thus Class(E,a) = Class(E,b) implies a-b in I
proof
assume Class(E,a) = Class(E,b);
then a in Class(E,b) by EQREL_1:23;
hence thesis by Th5;
end;
assume a-b in I;
then a in Class(E,b) by Th5;
hence thesis by EQREL_1:23;
end;
theorem Th7:
Class(EqRel(R,[#]R),a) = the carrier of R
proof
set E = EqRel(R,[#]R);
thus Class(E,a) c= the carrier of R;
let x be object;
assume x in the carrier of R;
then reconsider x as Element of R;
x-a in [#]R;
then [x,a] in E by Def5;
hence thesis by EQREL_1:19;
end;
theorem
Class EqRel(R,[#]R) = {the carrier of R}
proof
set E = EqRel(R,[#]R);
thus Class E c= {the carrier of R}
proof
let A be object;
assume A in Class E;
then consider x being object such that
A1: x in the carrier of R and
A2: A = Class(E,x) by EQREL_1:def 3;
reconsider x as Element of R by A1;
Class(E,x) = the carrier of R
proof
thus Class(E,x) c= the carrier of R;
let a be object;
assume a in the carrier of R;
then reconsider a as Element of R;
a-x in [#]R;
then [a,x] in E by Def5;
hence thesis by EQREL_1:19;
end;
hence thesis by A2,TARSKI:def 1;
end;
let A be object;
assume A in {the carrier of R};
then A = the carrier of R by TARSKI:def 1
.= Class(E,0.R) by Th7;
hence thesis by EQREL_1:def 3;
end;
theorem Th9:
Class(EqRel(R,{0.R}),a) = {a}
proof
set E = EqRel(R,{0.R});
thus Class(E,a) c= {a}
proof
let A be object;
assume
A1: A in Class(E,a);
then reconsider A as Element of R;
[A,a] in E by A1,EQREL_1:19;
then A-a in {0.R} by Def5;
then A-a = 0.R by TARSKI:def 1;
then A = a by RLVECT_1:21;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {a};
then
A2: x = a by TARSKI:def 1;
a-a = 0.R & 0.R in {0.R} by RLVECT_1:15,TARSKI:def 1;
then [x,a] in E by A2,Def5;
hence thesis by EQREL_1:19;
end;
theorem
Class EqRel(R,{0.R}) = rng singleton the carrier of R
proof
set E = EqRel(R,{0.R});
set f = singleton the carrier of R;
A1: dom f = the carrier of R by FUNCT_2:def 1;
thus Class E c= rng f
proof
let A be object;
assume A in Class E;
then consider x being object such that
A2: x in the carrier of R and
A3: A = Class(E,x) by EQREL_1:def 3;
reconsider x as Element of R by A2;
A4: Class(E,x) = {x}
proof
thus Class(E,x) c= {x}
proof
let a be object;
assume
A5: a in Class(E,x);
then reconsider a as Element of R;
[a,x] in E by A5,EQREL_1:19;
then a-x in {0.R} by Def5;
then a-x = 0.R by TARSKI:def 1;
then a = x by RLVECT_1:21;
hence thesis by TARSKI:def 1;
end;
let a be object;
x-x = 0.R by RLVECT_1:15;
then
A6: x-x in {0.R} by TARSKI:def 1;
assume a in {x};
then a = x by TARSKI:def 1;
then [a,x] in E by A6,Def5;
hence thesis by EQREL_1:19;
end;
f.x = {x} by SETWISEO:def 6;
hence thesis by A1,A3,A4,FUNCT_1:def 3;
end;
let A be object;
assume A in rng f;
then consider w being object such that
A7: w in dom f and
A8: f.w = A by FUNCT_1:def 3;
f.w = {w} by A7,SETWISEO:def 6
.= Class(E,w) by A7,Th9;
hence thesis by A7,A8,EQREL_1:def 3;
end;
begin :: Quotient Ring
reserve R for add-associative right_zeroed right_complementable Abelian
distributive left_unital non empty doubleLoopStr;
reserve I for Ideal of R;
definition
let R, I;
::$N Quotient ring
::$L https://en.wikipedia.org/wiki/Quotient_ring Quotient ring
func QuotientRing(R,I) -> strict doubleLoopStr means
:Def6:
the carrier of it = Class EqRel(R,I) &
1.it = Class(EqRel(R,I),1.R) &
0.it = Class(EqRel(R,I),0.R) &
(for x, y being Element of it
ex a, b being Element of R st
x = Class(EqRel(R,I),a) & y = Class(EqRel(R,I),b) &
(the addF of it).(x,y) = Class(EqRel(R,I),a+b)) &
for x, y being Element of it
ex a, b being Element of R st
x = Class(EqRel(R,I),a) & y = Class(EqRel(R,I),b) &
(the multF of it).(x,y) = Class(EqRel(R,I),a*b);
existence
proof
set E = EqRel(R,I);
set A = Class E;
defpred P[set,set,set] means ex P,Q being Element of R st $1 = Class(E,P)
& $2 = Class(E,Q) & $3 = Class(E,P+Q);
defpred R[set,set,set] means ex P,Q being Element of R st $1 = Class(E,P)
& $2 = Class(E,Q) & $3 = Class(E,P*Q);
reconsider u = Class(EqRel(R,I),1.R) as Element of A by EQREL_1:def 3;
reconsider z = Class(EqRel(R,I),0.R) as Element of A by EQREL_1:def 3;
A1: for x, y being Element of A ex z being Element of A st P[x,y,z]
proof
let x, y be Element of A;
consider P being object such that
A2: P in the carrier of R and
A3: x = Class(E,P) by EQREL_1:def 3;
consider Q being object such that
A4: Q in the carrier of R and
A5: y = Class(E,Q) by EQREL_1:def 3;
reconsider P,Q as Element of R by A2,A4;
Class(E,P+Q) is Element of A by EQREL_1:def 3;
hence thesis by A3,A5;
end;
consider g being BinOp of A such that
A6: for a,b being Element of A holds P[a,b,g.(a,b)] from BINOP_1:sch 3
(A1);
A7: for x,y being Element of A ex z being Element of A st R[x,y,z]
proof
let x, y be Element of A;
consider P being object such that
A8: P in the carrier of R and
A9: x = Class(E,P) by EQREL_1:def 3;
consider Q being object such that
A10: Q in the carrier of R and
A11: y = Class(E,Q) by EQREL_1:def 3;
reconsider P,Q as Element of R by A8,A10;
Class(E,P*Q) is Element of A by EQREL_1:def 3;
hence thesis by A9,A11;
end;
consider h being BinOp of A such that
A12: for a,b being Element of A holds R[a,b,h.(a,b)] from BINOP_1:sch
3(A7);
take doubleLoopStr(#A,g,h,u,z#);
thus thesis by A6,A12;
end;
uniqueness
proof
set E = EqRel(R,I);
let X, Y be strict doubleLoopStr such that
A13: the carrier of X = Class E and
A14: 1.X = Class(E,1.R) & 0.X = Class(E,0.R) and
A15: for x, y being Element of X ex a, b being Element of R st x =
Class(E,a) & y = Class(E,b) & (the addF of X).(x,y) = Class(E,a+b) and
A16: for x, y being Element of X ex a, b being Element of R st x =
Class(E,a) & y = Class(E,b) & (the multF of X).(x,y) = Class(E,a*b) and
A17: the carrier of Y = Class E and
A18: 1.Y = Class(E,1.R) & 0.Y = Class(E,0.R) and
A19: for x, y being Element of Y ex a, b being Element of R st x =
Class(E,a) & y = Class(E,b) & (the addF of Y).(x,y) = Class(E,a+b) and
A20: for x, y being Element of Y ex a, b being Element of R st x =
Class(E,a) & y = Class(E,b) & (the multF of Y).(x,y) = Class(E,a*b);
A21: for x, y being Element of X holds (the multF of X).(x,y) = (the multF
of Y).(x,y)
proof
let x, y be Element of X;
consider a, b being Element of R such that
A22: x = Class(E,a) and
A23: y = Class(E,b) and
A24: (the multF of X).(x,y) = Class(E,a*b) by A16;
consider a1, b1 being Element of R such that
A25: x = Class(E,a1) and
A26: y = Class(E,b1) and
A27: (the multF of Y).(x,y) = Class(E,a1*b1) by A13,A17,A20;
b-b1 in I by A23,A26,Th6;
then
A28: a1*(b-b1) in I by IDEAL_1:def 2;
A29: (a-a1)*b + a1*(b-b1) = a*b-a1*b + a1*(b-b1) by VECTSP_1:13
.= a*b-a1*b + (a1*b-a1*b1) by VECTSP_1:11
.= a*b-a1*b+a1*b-a1*b1 by RLVECT_1:28
.= a*b-a1*b1 by Th1;
a-a1 in I by A22,A25,Th6;
then (a-a1)*b in I by IDEAL_1:def 3;
then (a-a1)*b + a1*(b-b1) in I by A28,IDEAL_1:def 1;
hence thesis by A24,A27,A29,Th6;
end;
for x, y being Element of X holds (the addF of X).(x,y) = (the addF
of Y).(x,y)
proof
let x, y be Element of X;
consider a, b being Element of R such that
A30: x = Class(E,a) & y = Class(E,b) and
A31: (the addF of X).(x,y) = Class(E,a+b) by A15;
consider a1, b1 being Element of R such that
A32: x = Class(E,a1) & y = Class(E,b1) and
A33: (the addF of Y).(x,y) = Class(E,a1+b1) by A13,A17,A19;
a-a1 in I & b-b1 in I by A30,A32,Th6;
then
A34: a-a1+(b-b1) in I by IDEAL_1:def 1;
a+b-(a1+b1) = a+b-a1-b1 by RLVECT_1:27
.= a-a1+b-b1 by RLVECT_1:28
.= a-a1+(b-b1) by RLVECT_1:28;
hence thesis by A31,A33,A34,Th6;
end;
then the addF of X = the addF of Y by A13,A17,BINOP_1:2;
hence thesis by A13,A14,A17,A18,A21,BINOP_1:2;
end;
end;
notation
let R, I;
synonym R/I for QuotientRing(R,I);
end;
registration
let R, I;
cluster R/I -> non empty;
coherence
proof
the carrier of R/I = Class EqRel(R,I) by Def6;
hence the carrier of R/I is non empty;
end;
end;
reserve a,b for Element of R;
reserve x, y for Element of R/I;
theorem Th11:
ex a being Element of R st x = Class(EqRel(R,I),a)
proof
the carrier of R/I = Class EqRel(R,I) by Def6;
then x in Class EqRel(R,I);
then ex a being object
st a in the carrier of R & x = Class(EqRel(R,I),a) by
EQREL_1:def 3;
hence thesis;
end;
theorem Th12:
Class(EqRel(R,I),a) is Element of R/I
proof
the carrier of R/I = Class EqRel(R,I) by Def6;
hence thesis by EQREL_1:def 3;
end;
theorem Th13:
x = Class(EqRel(R,I),a) & y = Class(EqRel(R,I),b) implies
x+y = Class(EqRel(R,I),a+b)
proof
consider a1, b1 being Element of R such that
A1: x = Class(EqRel(R,I),a1) & y = Class(EqRel(R,I),b1) and
A2: (the addF of R/I).(x,y) = Class(EqRel(R,I),a1+b1) by Def6;
A3: a1-a+(b1-b) = a1-a+b1-b by RLVECT_1:28
.= a1+b1-a-b by RLVECT_1:28
.= a1+b1-(a+b) by RLVECT_1:27;
assume x = Class(EqRel(R,I),a) & y = Class(EqRel(R,I),b);
then a1-a in I & b1-b in I by A1,Th6;
then a1+b1-(a+b) in I by A3,IDEAL_1:def 1;
hence thesis by A2,Th6;
end;
theorem Th14:
x = Class(EqRel(R,I),a) & y = Class(EqRel(R,I),b) implies
x*y = Class(EqRel(R,I),a*b)
proof
assume that
A1: x = Class(EqRel(R,I),a) and
A2: y = Class(EqRel(R,I),b);
consider a1, b1 being Element of R such that
A3: x = Class(EqRel(R,I),a1) and
A4: y = Class(EqRel(R,I),b1) and
A5: (the multF of R/I).(x,y) = Class(EqRel(R,I),a1*b1) by Def6;
b1-b in I by A2,A4,Th6;
then
A6: a1*(b1-b) in I by IDEAL_1:def 2;
(a1-a)*b = a1*b-a*b & a1*(b1-b) = a1*b1-a1*b by VECTSP_1:11,13;
then
A7: a1*(b1-b)+(a1-a)*b = a1*b1-a1*b+a1*b-a*b by RLVECT_1:28
.= a1*b1-(a*b) by Th1;
a1-a in I by A1,A3,Th6;
then (a1-a)*b in I by IDEAL_1:def 3;
then (a1-a)*b+a1*(b1-b) in I by A6,IDEAL_1:def 1;
hence thesis by A5,A7,Th6;
end;
Lm2: now
let R be Ring, I be Ideal of R;
set E = EqRel(R,I);
let e be Element of R/I such that
A1: e = Class(E,1_R);
let h be Element of R/I;
consider a being Element of R such that
A2: e = Class(E,a) by Th11;
consider b being Element of R such that
A3: h = Class(E,b) by Th11;
A4: a-1_R in I by A1,A2,Th6;
then
A5: (a-1_R)*b in I by IDEAL_1:def 3;
A6: b*(a-1_R) = b*a-b*1_R by VECTSP_1:11
.= b*a-b;
A7: b*(a-1_R) in I by A4,IDEAL_1:def 2;
thus h * e = Class(E,b*a) by A2,A3,Th14
.= h by A3,A7,A6,Th6;
A8: (a-1_R)*b = a*b-1_R*b by VECTSP_1:13
.= a*b-b;
thus e * h = Class(E,a*b) by A2,A3,Th14
.= h by A3,A5,A8,Th6;
end;
theorem
Class(EqRel(R,I),1.R) = 1.(R/I) by Def6;
registration
let R be Ring, I be Ideal of R;
cluster R/I -> Abelian add-associative right_zeroed right_complementable
associative well-unital distributive;
coherence
proof
set g = the addF of R/I;
set E = EqRel(R,I);
hereby
let x, y be Element of R/I;
consider a being Element of R such that
A1: x = Class(E,a) by Th11;
consider b being Element of R such that
A2: y = Class(E,b) by Th11;
thus x + y = Class(E,a+b) by A1,A2,Th13
.= y + x by A1,A2,Th13;
end;
hereby
let x, y, z be Element of R/I;
consider a being Element of R such that
A3: x = Class(E,a) by Th11;
consider b being Element of R such that
A4: y = Class(E,b) by Th11;
consider bc being Element of R such that
A5: y+z = Class(E,bc) by Th11;
consider c being Element of R such that
A6: z = Class(E,c) by Th11;
y+z = Class(E,b+c) by A4,A6,Th13;
then
A7: bc-(b+c) in I by A5,Th6;
consider ab being Element of R such that
A8: x+y = Class(E,ab) by Th11;
x+y = Class(E,a+b) by A3,A4,Th13;
then ab-(a+b) in I by A8,Th6;
then
A9: ab-(a+b)-(bc-(b+c)) in I by A7,IDEAL_1:15;
A10: ab-(a+b)-(bc-(b+c)) = ab-(a+b)-bc+(b+c) by RLVECT_1:29
.= ab-(a+b)+(b+c)-bc by RLVECT_1:28
.= ab-a-b+(b+c)-bc by RLVECT_1:27
.= ab-a-b+b+c-bc by RLVECT_1:def 3
.= ab-a+c-bc by Th1
.= ab+c-a-bc by RLVECT_1:28
.= ab+c-(a+bc) by RLVECT_1:27;
thus (x+y)+z = Class(E,ab+c) by A6,A8,Th13
.= Class(E,a+bc) by A9,A10,Th6
.= x+(y+z) by A3,A5,Th13;
end;
hereby
let v be Element of R/I;
consider a, b being Element of R such that
A11: v = Class(E,a) and
A12: 0.(R/I) = Class(E,b) and
A13: g.(v,0.(R/I)) = Class(E,a+b) by Def6;
A14: b-0.R = b by RLVECT_1:13;
A15: a+b-a = a-a+b by RLVECT_1:28
.= 0.R+b by RLVECT_1:15
.= b by RLVECT_1:def 4;
0.(R/I) = Class(E,0.R) by Def6;
then b-0.R in I by A12,Th6;
hence v + 0.(R/I) = v by A11,A13,A14,A15,Th6;
end;
thus R/I is right_complementable
proof
let v be Element of R/I;
consider a, b being Element of R such that
A16: v = Class(E,a) and
0.(R/I) = Class(E,b) and
g.(v,0.(R/I)) = Class(E,a+b) by Def6;
reconsider w = Class(E,-a) as Element of R/I by Th12;
take w;
A17: 0.(R/I) = Class(E,0.R) by Def6;
thus v + w = Class(E,a+-a) by A16,Th13
.= 0.(R/I) by A17,RLVECT_1:def 10;
end;
hereby
let x, y, z be Element of R/I;
consider a being Element of R such that
A18: x = Class(E,a) by Th11;
consider ab being Element of R such that
A19: x*y = Class(E,ab) by Th11;
consider c being Element of R such that
A20: z = Class(E,c) by Th11;
consider b being Element of R such that
A21: y = Class(E,b) by Th11;
x*y = Class(E,a*b) by A18,A21,Th14;
then ab - a*b in I by A19,Th6;
then
A22: (ab - a*b)*c in I by IDEAL_1:def 3;
consider bc being Element of R such that
A23: y*z = Class(E,bc) by Th11;
y*z = Class(E,b*c) by A21,A20,Th14;
then bc - b*c in I by A23,Th6;
then
A24: a*(bc - b*c) in I by IDEAL_1:def 2;
A25: (ab - a*b)*c = ab*c - a*b*c & a*(bc - b*c) = a*bc - a*(b*c) by
VECTSP_1:11,13;
a*(b*c) = a*b*c & ab*c - a*b*c - (a*bc - a*b*c) = ab*c - a*bc by Th3,
GROUP_1:def 3;
then
A26: ab*c - a*bc in I by A22,A24,A25,IDEAL_1:15;
thus (x*y)*z = Class(E,ab*c) by A20,A19,Th14
.= Class(E,a*bc) by A26,Th6
.= x*(y*z) by A18,A23,Th14;
end;
1.R = 1_R & Class(E,1.R) = 1.(R/I) by Def6;
hence for x being Element of R/I holds x*1.(R/I) = x & 1.(R/I)*x = x by Lm2
;
let x, y, z be Element of R/I;
consider a being Element of R such that
A27: x = Class(E,a) by Th11;
consider ab being Element of R such that
A28: x*y = Class(E,ab) by Th11;
consider ca being Element of R such that
A29: z*x = Class(E,ca) by Th11;
consider c being Element of R such that
A30: z = Class(E,c) by Th11;
z*x = Class(E,c*a) by A27,A30,Th14;
then
A31: c*a - ca in I by A29,Th6;
consider b being Element of R such that
A32: y = Class(E,b) by Th11;
x*y = Class(E,a*b) by A27,A32,Th14;
then
A33: ab-a*b in I by A28,Th6;
consider ac being Element of R such that
A34: x*z = Class(E,ac) by Th11;
x*z = Class(E,a*c) by A27,A30,Th14;
then
A35: ac-a*c in I by A34,Th6;
consider bc being Element of R such that
A36: y+z = Class(E,bc) by Th11;
y+z = Class(E,b+c) by A32,A30,Th13;
then
A37: bc-(b+c) in I by A36,Th6;
then
A38: (bc-(b+c))*a in I by IDEAL_1:def 3;
a*(bc-(b+c)) in I by A37,IDEAL_1:def 2;
then a*(bc-(b+c)) - (ab-a*b) in I by A33,IDEAL_1:15;
then
A39: a*(bc-(b+c)) - (ab-a*b) - (ac-a*c) in I by A35,IDEAL_1:15;
A40: a*(bc-(b+c)) - (ab-a*b) - (ac-a*c) = a*bc-a*(b+c) - (ab-a*b) - (ac-a*
c) by VECTSP_1:11
.= a*bc-(a*b+a*c) - (ab-a*b) - (ac-a*c) by VECTSP_1:def 2
.= a*bc-a*b-a*c - (ab-a*b) - (ac-a*c) by RLVECT_1:27
.= a*bc-a*b-a*c-ab+a*b - (ac-a*c) by RLVECT_1:29
.= a*bc-a*b-a*c-ab+a*b-ac+a*c by RLVECT_1:29
.= a*bc-a*b-a*c+a*b-ab-ac+a*c by RLVECT_1:28
.= a*bc-a*b+a*b-a*c-ab-ac+a*c by RLVECT_1:28
.= a*bc-a*c-ab-ac+a*c by Th1
.= a*bc-a*c-ab+a*c-ac by RLVECT_1:28
.= a*bc-a*c+a*c-ab-ac by RLVECT_1:28
.= a*bc-ab-ac by Th1
.= a*bc-(ab+ac) by RLVECT_1:27;
thus x*(y+z) = Class(E,a*bc) by A27,A36,Th14
.= Class(E,ab+ac) by A39,A40,Th6
.= x*y+x*z by A28,A34,Th13;
consider ba being Element of R such that
A41: y*x = Class(E,ba) by Th11;
y*x = Class(E,b*a) by A27,A32,Th14;
then b*a - ba in I by A41,Th6;
then (bc-(b+c))*a + (b*a-ba) in I by A38,IDEAL_1:def 1;
then
A42: (bc-(b+c))*a + (b*a-ba) + (c*a-ca) in I by A31,IDEAL_1:def 1;
A43: (bc-(b+c))*a + (b*a-ba) + (c*a-ca) = bc*a-(b+c)*a + (b*a-ba) + (c*a-
ca) by VECTSP_1:13
.= bc*a-(b*a+c*a) + (b*a-ba) + (c*a-ca) by VECTSP_1:def 3
.= bc*a-b*a-c*a + (b*a-ba) + (c*a-ca) by RLVECT_1:27
.= bc*a-b*a-c*a+b*a-ba + (c*a-ca) by RLVECT_1:28
.= bc*a-b*a-c*a+b*a-ba+c*a-ca by RLVECT_1:28
.= bc*a-b*a+b*a-c*a-ba+c*a-ca by RLVECT_1:28
.= bc*a-c*a-ba+c*a-ca by Th1
.= bc*a-c*a+c*a-ba-ca by RLVECT_1:28
.= bc*a-ba-ca by Th1
.= bc*a - (ba+ca) by RLVECT_1:27;
thus (y+z)*x = Class(E,bc*a) by A27,A36,Th14
.= Class(E,ba+ca) by A42,A43,Th6
.= y*x+z*x by A41,A29,Th13;
end;
end;
registration
let R be commutative Ring, I be Ideal of R;
cluster R/I -> commutative;
coherence
proof
set E = EqRel(R,I);
let x, y be Element of R/I;
consider a being Element of R such that
A1: x = Class(E,a) by Th11;
consider b being Element of R such that
A2: y = Class(E,b) by Th11;
thus x*y = Class(E,a*b) by A1,A2,Th14
.= y*x by A1,A2,Th14;
end;
end;
theorem Th16:
for R being Ring, I being Ideal of R
holds I is proper iff R/I is non degenerated
proof
let R be Ring, I be Ideal of R;
set E = EqRel(R,I);
A1: 1.R-0.R = 1.R by RLVECT_1:13;
A2: 0.(R/I) = Class(E,0.R) & 1.(R/I) = Class(E,1.R) by Def6;
thus I is proper implies R/I is non degenerated
by A2,Th6,A1,IDEAL_1:19;
assume
A3: R/I is non degenerated;
assume not I is proper;
then 1.R in I by IDEAL_1:19;
hence thesis by A2,A1,A3,Th6;
end;
theorem Th17:
I is quasi-prime iff R/I is domRing-like
proof
set E = EqRel(R,I);
A1: Class(E,0.R) = 0.(R/I) by Def6;
thus I is quasi-prime implies R/I is domRing-like
proof
assume
A2: I is quasi-prime;
let x, y be Element of R/I such that
A3: x*y = 0.(R/I);
consider a being Element of R such that
A4: x = Class(E,a) by Th11;
consider b being Element of R such that
A5: y = Class(E,b) by Th11;
x*y = Class(E,a*b) by A4,A5,Th14;
then a*b-0.R = a*b & a*b-0.R in I by A1,A3,Th6,RLVECT_1:13;
then
A6: a in I or b in I by A2;
a-0.R = a & b-0.R = b by RLVECT_1:13;
hence thesis by A1,A4,A5,A6,Th6;
end;
assume
A7: R/I is domRing-like;
let a, b be Element of R;
reconsider x = Class(E,a), y = Class(E,b) as Element of R/I by Th12;
A8: a*b-0.R = a*b by RLVECT_1:13;
A9: Class(E,a*b) = x*y by Th14;
assume a*b in I;
then Class(E,a*b) = Class(E,0.R) by A8,Th6;
then x = 0.(R/I) or y = 0.(R/I) by A1,A7,A9;
then a-0.R in I or b-0.R in I by A1,Th6;
hence thesis by RLVECT_1:13;
end;
theorem
for R being commutative Ring, I being Ideal of R holds
I is prime iff R/I is domRing by Th16,Th17;
theorem Th19:
for R being Ring, I being Ideal of R st
R is commutative & I is quasi-maximal holds R/I is almost_left_invertible
proof
let R be Ring, I be Ideal of R;
set E = EqRel(R,I);
assume that
A1: R is commutative and
A2: I is quasi-maximal;
let x be Element of R/I such that
A3: x <> 0.(R/I);
consider a being Element of R such that
A4: x = Class(E,a) by Th11;
set M = {a*r+s where r, s is Element of R: s in I};
M c= the carrier of R
proof
let k be object;
assume k in M;
then ex r, s being Element of R st k = a*r+s & s in I;
hence thesis;
end;
then reconsider M as Subset of R;
A5: 0.R in I by IDEAL_1:2;
A6: M is left-ideal
proof
let p, x be Element of R;
assume x in M;
then consider r, s being Element of R such that
A7: x = a*r+s and
A8: s in I;
A9: p*s in I by A8,IDEAL_1:def 2;
a*(r*p)+p*s = a*r*p+p*s by GROUP_1:def 3
.= a*r*p+s*p by A1
.= x*p by A7,VECTSP_1:def 3
.= p*x by A1;
hence thesis by A9;
end;
A10: I c= M
proof
let i be object;
assume i in I;
then reconsider i as Element of I;
a*0.R+i = 0.R+i
.= i by RLVECT_1:def 4;
hence thesis;
end;
A11: M is right-ideal
proof
let p, x be Element of R;
assume x in M;
then consider r, s being Element of R such that
A12: x = a*r+s and
A13: s in I;
A14: p*s in I by A13,IDEAL_1:def 2;
a*(r*p)+p*s = a*r*p+p*s by GROUP_1:def 3
.= a*r*p+s*p by A1
.= x*p by A12,VECTSP_1:def 3;
hence thesis by A14;
end;
A15: M is add-closed
proof
let c, d be Element of R;
assume c in M;
then consider rc, sc being Element of R such that
A16: c = a*rc+sc and
A17: sc in I;
assume d in M;
then consider rd, sd being Element of R such that
A18: d = a*rd+sd and
A19: sd in I;
A20: a*(rc+rd)+(sc+sd) = a*rc+a*rd+(sc+sd) by VECTSP_1:def 2
.= a*rc+a*rd+sc+sd by RLVECT_1:def 3
.= a*rc+sc+a*rd+sd by RLVECT_1:def 3
.= c+d by A16,A18,RLVECT_1:def 3;
sc+sd in I by A17,A19,IDEAL_1:def 1;
hence c+d in M by A20;
end;
A21: now
A22: a-0.R = a by RLVECT_1:13;
assume a in I;
then Class(E,a) = Class(E,0.R) by A22,Th6
.= 0.(R/I) by Def6;
hence contradiction by A3,A4;
end;
a*1.R+0.R = a+0.R
.= a by RLVECT_1:def 4;
then a in M by A5;
then M is non proper by A2,A15,A6,A11,A21,A10;
then M = the carrier of R by SUBSET_1:def 6;
then 1.R in M;
then consider b, m being Element of R such that
A23: 1.R = a*b+m and
A24: m in I;
A25: m = 1.R-a*b by A23,VECTSP_2:2;
reconsider y = Class(E,b) as Element of R/I by Th12;
take y;
A26: Class(E,1.R) = 1.(R/I) by Def6;
thus y*x = Class(E,b*a) by A4,Th14
.= Class(E,a*b) by A1
.= 1.(R/I) by A24,A25,A26,Th6;
end;
theorem Th20:
for R being Ring, I being Ideal of R
st R/I is almost_left_invertible holds I is quasi-maximal
proof
let R be Ring, I be Ideal of R;
set E = EqRel(R,I);
assume
A1: R/I is almost_left_invertible;
given J being Ideal of R such that
A2: I c= J and
A3: J <> I and
A4: J is proper;
not J c= I by A2,A3;
then consider a being object such that
A5: a in J and
A6: not a in I;
reconsider a as Element of R by A5;
reconsider x = Class(E,a) as Element of R/I by Th12;
A7: Class(E,0.R) = 0.(R/I) by Def6;
now
assume x = 0.(R/I);
then a-0.R in I by A7,Th6;
hence contradiction by A6,RLVECT_1:13;
end;
then consider y being Element of R/I such that
A8: y*x = 1.(R/I) by A1;
consider b being Element of R such that
A9: y = Class(E,b) by Th11;
A10: Class(E,1.R) = 1.(R/I) by Def6;
y*x = Class(E,b*a) by A9,Th14;
then
A11: b*a-1.R in I by A10,A8,Th6;
A12: 1.R = b*a-(b*a-1.R) by Th2;
b*a in J by A5,IDEAL_1:def 2;
then 1.R in J by A2,A11,A12,IDEAL_1:15;
hence thesis by A4,IDEAL_1:19;
end;
theorem
for R being commutative Ring, I being Ideal of R holds
I is maximal iff R/I is Skew-Field by Th16,Th19,Th20;
registration
let R be non degenerated commutative Ring;
cluster maximal -> prime for Ideal of R;
coherence
proof
let I be Ideal of R;
assume
A1: I is proper quasi-maximal;
then R/I is almost_left_invertible non degenerated by Th16,Th19;
hence I is proper quasi-prime by A1,Th17;
end;
end;
::$N Krull's theorem
::$L https://en.wikipedia.org/wiki/Krull's_theorem Krull's theorem
registration
let R be non degenerated Ring;
cluster maximal for Ideal of R;
existence
proof
set S = {A where A is Ideal of R: A is proper};
set P = RelIncl S;
A1: P is_antisymmetric_in S by WELLORD2:21;
A2: field P = S by WELLORD2:def 1;
A3: S has_upper_Zorn_property_wrt P
proof
let Y be set such that
A4: Y c= S and
A5: P |_2 Y is being_linear-order;
per cases;
suppose
A6: Y is empty;
take x = {0.R}-Ideal;
now
assume x is non proper;
then
A7: x = the carrier of R by SUBSET_1:def 6;
x = {0.R} by IDEAL_1:47;
then 1.R = 0.R by A7,TARSKI:def 1;
hence contradiction;
end;
hence x in S;
thus thesis by A6;
end;
suppose
Y is non empty;
then consider e being object such that
A8: e in Y;
take x = union Y;
x c= the carrier of R
proof
let a be object;
assume a in x;
then consider Z being set such that
A9: a in Z and
A10: Z in Y by TARSKI:def 4;
Z in S by A4,A10;
then ex A being Ideal of R st Z = A & A is proper;
hence thesis by A9;
end;
then reconsider B = x as Subset of R;
A11: B is right-ideal
proof
let p, a be Element of R;
assume a in B;
then consider Aa being set such that
A12: a in Aa and
A13: Aa in Y by TARSKI:def 4;
Aa in S by A4,A13;
then consider Ia being Ideal of R such that
A14: Aa = Ia and
Ia is proper;
a*p in Ia & Ia c= B by A12,A13,A14,IDEAL_1:def 3,ZFMISC_1:74;
hence thesis;
end;
A15: B is left-ideal
proof
let p, a be Element of R;
assume a in B;
then consider Aa being set such that
A16: a in Aa and
A17: Aa in Y by TARSKI:def 4;
Aa in S by A4,A17;
then consider Ia being Ideal of R such that
A18: Aa = Ia and
Ia is proper;
p*a in Ia & Ia c= B by A16,A17,A18,IDEAL_1:def 2,ZFMISC_1:74;
hence thesis;
end;
A19: now
assume B is non proper;
then 1.R in B by A15,IDEAL_1:19;
then consider Aa being set such that
A20: 1.R in Aa and
A21: Aa in Y by TARSKI:def 4;
Aa in S by A4,A21;
then ex Ia being Ideal of R st Aa = Ia & Ia is proper;
hence contradiction by A20,IDEAL_1:19;
end;
A22: B is add-closed
proof
A23: field (P |_2 Y) = Y by A2,A4,ORDERS_1:71;
let a, b be Element of R;
A24: now
let A be Ideal of R;
assume a in A & b in A;
then
A25: a+b in A by IDEAL_1:def 1;
assume A in Y;
hence a+b in B by A25,TARSKI:def 4;
end;
assume a in B;
then consider Aa being set such that
A26: a in Aa and
A27: Aa in Y by TARSKI:def 4;
Aa in S by A4,A27;
then
A28: ex Ia being Ideal of R st Aa = Ia & Ia is proper;
assume b in B;
then consider Ab being set such that
A29: b in Ab and
A30: Ab in Y by TARSKI:def 4;
P |_2 Y is connected by A5;
then P |_2 Y is_connected_in field (P |_2 Y) by RELAT_2:def 14;
then
[Aa,Ab] in P |_2 Y or [Ab,Aa] in P |_2 Y or Aa = Ab by A27,A30,A23,
RELAT_2:def 6;
then [Aa,Ab] in P or [Ab,Aa] in P or Aa = Ab by XBOOLE_0:def 4;
then
A31: Aa c= Ab or Ab c= Aa by A4,A27,A30,WELLORD2:def 1;
Ab in S by A4,A30;
then ex Ib being Ideal of R st Ab = Ib & Ib is proper;
hence a+b in B by A26,A27,A29,A30,A24,A28,A31;
end;
e in S by A4,A8;
then consider A being Ideal of R such that
A32: e = A and
A is proper;
ex q being object st q in A by XBOOLE_0:def 1;
then B is non empty by A8,A32,TARSKI:def 4;
hence
A33: x in S by A22,A15,A11,A19;
let y be set;
assume
A34: y in Y;
then y c= x by ZFMISC_1:74;
hence thesis by A4,A33,A34,WELLORD2:def 1;
end;
end;
P is_reflexive_in S & P is_transitive_in S by WELLORD2:19,20;
then P partially_orders S by A1;
then consider x being set such that
A35: x is_maximal_in P by A2,A3,ORDERS_1:63;
A36: x in field P by A35;
then consider I being Ideal of R such that
A37: x = I and
A38: I is proper by A2;
take I;
thus I is proper by A38;
let J be Ideal of R such that
A39: I c= J;
now
assume J is proper;
then
A40: J in S;
then [I,J] in P by A2,A36,A37,A39,WELLORD2:def 1;
hence I = J by A2,A35,A37,A40;
end;
hence thesis;
end;
end;
registration
let R be non degenerated commutative Ring;
cluster maximal for Ideal of R;
existence
proof
set I = the maximal Ideal of R;
take I;
thus thesis;
end;
end;
registration
let R be non degenerated commutative Ring, I be quasi-prime Ideal of R;
cluster R/I -> domRing-like;
coherence by Th17;
end;
registration
let R be non degenerated commutative Ring, I be quasi-maximal Ideal of R;
cluster R/I -> almost_left_invertible;
coherence by Th19;
end;