:: Quotient Rings
:: by Artur Korni{\l}owicz
::
:: Received December 7, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


theorem Th1: :: RING_1:1
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of L holds (a - b) + b = a
proof end;

theorem Th2: :: RING_1:2
for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for b, c being Element of L holds c = b - (b - c)
proof end;

theorem Th3: :: RING_1:3
for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a, b, c being Element of L holds (a - b) - (c - b) = a - c
proof end;

definition
let K be non empty multMagma ;
let S be Subset of K;
attr S is quasi-prime means :: RING_1:def 1
 for a, b being Element of K holds
( not a * b in S or a in S or b in S );
end;

:: deftheorem 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 ) );

definition
let K be non empty multLoopStr ;
let S be Subset of K;
attr S is prime means :: RING_1:def 2
( S is proper & S is quasi-prime );
end;

:: deftheorem 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 ) );

definition
let R be non empty doubleLoopStr ;
let I be Subset of R;
attr I is quasi-maximal means :: RING_1:def 3
 for J being Ideal of R holds
( not I c= J or J = I or not J is proper );
end;

:: deftheorem 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 ) );

definition
let R be non empty doubleLoopStr ;
let I be Subset of R;
attr I is maximal means :: RING_1:def 4
( I is proper & I is quasi-maximal );
end;

:: deftheorem 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 ) );

registration
let K be non empty multLoopStr ;
cluster prime -> proper quasi-prime for Element of K34( the carrier of K);
coherence
for b1 being Subset of K st b1 is prime holds
( b1 is proper & b1 is quasi-prime ) ;
cluster proper quasi-prime -> prime for Element of K34( the carrier of K);
coherence
for b1 being Subset of K st b1 is proper & b1 is quasi-prime holds
b1 is prime ;
end;

registration
let R be non empty doubleLoopStr ;
cluster maximal -> proper quasi-maximal for Element of K34( the carrier of R);
coherence
for b1 being Subset of R st b1 is maximal holds
( b1 is proper & b1 is quasi-maximal ) ;
cluster proper quasi-maximal -> maximal for Element of K34( the carrier of R);
coherence
for b1 being Subset of R st b1 is proper & b1 is quasi-maximal holds
b1 is maximal ;
end;

registration
let R be non empty addLoopStr ;
cluster [#] R -> add-closed ;
coherence
[#] R is add-closed ;
end;

registration
let R be non empty multMagma ;
cluster [#] R -> left-ideal right-ideal ;
coherence
( [#] R is left-ideal & [#] R is right-ideal ) ;
end;

theorem :: RING_1:4
for R being domRing holds {(0. R)} is prime
proof end;

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

definition
let R be Ring;
let I be Ideal of R;
func EqRel (R,I) -> Relation of R means :Def5: :: RING_1:def 5
 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 )
proof end;
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
proof end;
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 ) );

registration
let R be Ring;
let I be Ideal of R;
cluster EqRel (R,I) -> non empty total symmetric transitive ;
coherence
( not EqRel (R,I) is empty & EqRel (R,I) is total & EqRel (R,I) is symmetric & EqRel (R,I) is transitive )
proof end;
end;

theorem Th5: :: RING_1:5
for R being Ring
for I being Ideal of R
for a, b being Element of R holds
( a in Class ((EqRel (R,I)),b) iff a - b in I )
proof end;

theorem Th6: :: RING_1:6
for R being Ring
for I being Ideal of R
for a, b being Element of R holds
( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )
proof end;

theorem Th7: :: RING_1:7
for R being Ring
for a being Element of R holds Class ((EqRel (R,([#] R))),a) = the carrier of R
proof end;

theorem :: RING_1:8
for R being Ring holds Class (EqRel (R,([#] R))) = { the carrier of R}
proof end;

theorem Th9: :: RING_1:9
for R being Ring
for a being Element of R holds Class ((EqRel (R,{(0. R)})),a) = {a}
proof end;

theorem :: RING_1:10
for R being Ring holds Class (EqRel (R,{(0. R)})) = rng (singleton the carrier of R)
proof end;

definition
let R be Ring;
let I be Ideal of R;
:: WP: Quotient ring
func QuotientRing (R,I) -> strict doubleLoopStr means :Def6: :: RING_1:def 6
( 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)) ) ) )
proof end;
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
proof end;
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)) ) ) ) );

notation
let R be Ring;
let I be Ideal of R;
synonym R / I for QuotientRing (R,I);
end;

registration
let R be Ring;
let I be Ideal of R;
cluster QuotientRing (R,I) -> non empty strict ;
coherence
not R / I is empty
proof end;
end;

theorem Th11: :: RING_1:11
for R being Ring
for I being Ideal of R
for x being Element of (R / I) ex a being Element of R st x = Class ((EqRel (R,I)),a)
proof end;

theorem Th12: :: RING_1:12
for R being Ring
for I being Ideal of R
for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)
proof end;

theorem Th13: :: RING_1:13
for R being Ring
for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
proof end;

theorem Th14: :: RING_1:14
for R being Ring
for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x * y = Class ((EqRel (R,I)),(a * b))
proof end;

Lm2: now :: thesis: for R being 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 R be Ring; :: thesis: 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; :: thesis: 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); :: thesis: ( 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)) ; :: thesis: for h being Element of (R / I) holds
( h * e = h & e * h = h )
let h be Element of (R / I); :: thesis: ( 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:11
.= (b * a) - b ;
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 ; :: thesis: e * h = h
A8: (a - (1_ R)) * b = (a * b) - ((1_ R) * b) by VECTSP_1:13
.= (a * b) - b ;
thus e * h = Class ((EqRel (R,I)),(a * b)) by A2, A3, Th14
.= h by A3, A5, A8, Th6 ; :: thesis: verum
end;

theorem :: RING_1:15
for R being Ring
for I being Ideal of R holds Class ((EqRel (R,I)),(1. R)) = 1. (R / I) by Def6;

registration
let R be Ring;
let I be Ideal of R;
cluster QuotientRing (R,I) -> right_complementable strict well-unital distributive Abelian add-associative right_zeroed associative ;
coherence
( R / I is Abelian & R / I is add-associative & R / I is right_zeroed & R / I is right_complementable & R / I is associative & R / I is well-unital & R / I is distributive )
proof end;
end;

registration
let R be commutative Ring;
let I be Ideal of R;
cluster QuotientRing (R,I) -> strict commutative ;
coherence
R / I is commutative
proof end;
end;

theorem Th16: :: RING_1:16
for R being Ring
for I being Ideal of R holds
( I is proper iff not R / I is degenerated )
proof end;

theorem Th17: :: RING_1:17
for R being Ring
for I being Ideal of R holds
( I is quasi-prime iff R / I is domRing-like )
proof end;

theorem :: RING_1:18
for R being commutative Ring
for I being Ideal of R holds
( I is prime iff R / I is domRing ) by Th16, Th17;

theorem Th19: :: RING_1:19
for R being Ring
for I being Ideal of R st R is commutative & I is quasi-maximal holds
R / I is almost_left_invertible
proof end;

theorem Th20: :: RING_1:20
for R being Ring
for I being Ideal of R st R / I is almost_left_invertible holds
I is quasi-maximal
proof end;

theorem :: RING_1:21
for R being commutative Ring
for 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 non empty add-closed left-ideal right-ideal maximal -> prime for Element of K34( the carrier of R);
coherence
for b1 being Ideal of R st b1 is maximal holds
b1 is prime
proof end;
end;

:: WP: Krull's theorem
registration
let R be non degenerated Ring;
cluster non empty add-closed left-ideal right-ideal maximal for Element of K34( the carrier of R);
existence
ex b1 being Ideal of R st b1 is maximal
proof end;
end;

registration
let R be non degenerated commutative Ring;
cluster non empty add-closed left-ideal right-ideal maximal for Element of K34( the carrier of R);
existence
ex b1 being Ideal of R st b1 is maximal
proof end;
end;

registration
let R be non degenerated commutative Ring;
let I be quasi-prime Ideal of R;
cluster QuotientRing (R,I) -> strict domRing-like ;
coherence
R / I is domRing-like by Th17;
end;

registration
let R be non degenerated commutative Ring;
let I be quasi-maximal Ideal of R;
cluster QuotientRing (R,I) -> almost_left_invertible strict ;
coherence
R / I is almost_left_invertible by Th19;
end;