begin
theorem Th1:
theorem Th2:
theorem Th3:
begin
:: deftheorem Def1 defines quasi-prime RING_1:def 1 :
for K being non empty multMagma
for S being Subset of K holds
( S is quasi-prime iff for a, b being Element of K holds
( not a * b in S or a in S or b in S ) );
:: deftheorem Def2 defines prime RING_1:def 2 :
for K being non empty multLoopStr
for S being Subset of K holds
( S is prime iff ( S is proper & S is quasi-prime ) );
:: deftheorem Def3 defines quasi-maximal RING_1:def 3 :
for R being non empty doubleLoopStr
for I being Subset of R holds
( I is quasi-maximal iff for J being Ideal of R holds
( not I c= J or J = I or not J is proper ) );
:: deftheorem Def4 defines maximal RING_1:def 4 :
for R being non empty doubleLoopStr
for I being Subset of R holds
( I is maximal iff ( I is proper & I is quasi-maximal ) );
theorem
begin
Lm1:
for R being Ring
for I being Ideal of R ex E being Equivalence_Relation of the carrier of R st
for x, y being set 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 ) ) )
definition
let R be
Ring;
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
ex b1 being Relation of R st
for a, b being Element of R holds
( [a,b] in b1 iff a - b in I )
uniqueness
for b1, b2 being Relation of R st ( for a, b being Element of R holds
( [a,b] in b1 iff a - b in I ) ) & ( for a, b being Element of R holds
( [a,b] in b2 iff a - b in I ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines EqRel RING_1:def 5 :
for R being Ring
for I being Ideal of R
for b3 being Relation of R holds
( b3 = EqRel (R,I) iff for a, b being Element of R holds
( [a,b] in b3 iff a - b in I ) );
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem
begin
definition
let R be
Ring;
let I be
Ideal of
R;
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
ex b1 being strict doubleLoopStr st
( the carrier of b1 = Class (EqRel (R,I)) & 1. b1 = Class ((EqRel (R,I)),(1. R)) & 0. b1 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b1 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b1 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) )
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = Class (EqRel (R,I)) & 1. b1 = Class ((EqRel (R,I)),(1. R)) & 0. b1 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b1 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b1 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b1 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) & the carrier of b2 = Class (EqRel (R,I)) & 1. b2 = Class ((EqRel (R,I)),(1. R)) & 0. b2 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b2 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b2 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b2 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b2 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines QuotientRing RING_1:def 6 :
for R being Ring
for I being Ideal of R
for b3 being strict doubleLoopStr holds
( b3 = QuotientRing (R,I) iff ( the carrier of b3 = Class (EqRel (R,I)) & 1. b3 = Class ((EqRel (R,I)),(1. R)) & 0. b3 = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b3 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b3 . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b3 ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b3 . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) ) );
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
Lm2:
now
let R be
Ring;
for I being Ideal of R
for e being Element of (R / I) st e = Class ((EqRel (R,I)),(1_ R)) holds
for h being Element of (R / I) holds
( h * e = h & e * h = h )let I be
Ideal of
R;
for e being Element of (R / I) st e = Class ((EqRel (R,I)),(1_ R)) holds
for h being Element of (R / I) holds
( h * e = h & e * h = h )set E =
EqRel (
R,
I);
let e be
Element of
(R / I);
( e = Class ((EqRel (R,I)),(1_ R)) implies for h being Element of (R / I) holds
( h * e = h & e * h = h ) )assume A1:
e = Class (
(EqRel (R,I)),
(1_ R))
;
for h being Element of (R / I) holds
( h * e = h & e * h = h )let h be
Element of
(R / I);
( h * e = h & e * h = h )consider a being
Element of
R such that A2:
e = Class (
(EqRel (R,I)),
a)
by Th11;
consider b being
Element of
R such that A3:
h = Class (
(EqRel (R,I)),
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:43
.=
(b * a) - b
by VECTSP_1:def 13
;
A7:
b * (a - (1_ R)) in I
by A4, IDEAL_1:def 2;
thus h * e =
Class (
(EqRel (R,I)),
(b * a))
by A2, A3, Th14
.=
h
by A3, A7, A6, Th6
;
e * h = hA8:
(a - (1_ R)) * b =
(a * b) - ((1_ R) * b)
by VECTSP_1:45
.=
(a * b) - b
by VECTSP_1:def 19
;
thus e * h =
Class (
(EqRel (R,I)),
(a * b))
by A2, A3, Th14
.=
h
by A3, A5, A8, Th6
;
verum
end;
theorem
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem