:: Quotient Rings
:: by Artur Korni{\l}owicz
::
:: Received December 7, 2005
:: Copyright (c) 2005 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 :Def1: :: 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 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 ) );

definition

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

end;

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

definition

let R be non empty doubleLoopStr ;
let I be Subset of R;
attr I is quasi-maximal means :Def3: :: 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 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 ) );

definition

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

end;

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

registration

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

end;

registration

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

end;

registration

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

proof end;

end;

registration

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

proof end;

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 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 ) ) )

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 b₁ being Relation of R st
for a, b being Element of R holds
( [a,b] in b₁ iff a - b in I )

proof end;

uniqueness
for b₁, b₂ being Relation of R st ( for a, b being Element of R holds
( [a,b] in b₁ iff a - b in I ) ) & ( for a, b being Element of R holds
( [a,b] in b₂ iff a - b in I ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines EqRel RING_1:def 5 :

for R being Ring
for I being Ideal of R
for b₃ being Relation of R holds
( b₃ = EqRel R,I iff for a, b being Element of R holds
( [a,b] in b₃ iff a - b in I ) );

registration

let R be Ring;
let I be Ideal of R;
cluster EqRel R,I -> non empty symmetric transitive total ;
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;
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 b₁ being strict doubleLoopStr st
( the carrier of b₁ = Class (EqRel R,I) & 1. b₁ = Class (EqRel R,I),(1. R) & 0. b₁ = Class (EqRel R,I),(0. R) & ( for x, y being Element of b₁ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of b₁ . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of b₁ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of b₁ . x,y = Class (EqRel R,I),(a * b) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict doubleLoopStr st the carrier of b₁ = Class (EqRel R,I) & 1. b₁ = Class (EqRel R,I),(1. R) & 0. b₁ = Class (EqRel R,I),(0. R) & ( for x, y being Element of b₁ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of b₁ . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of b₁ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of b₁ . x,y = Class (EqRel R,I),(a * b) ) ) & the carrier of b₂ = Class (EqRel R,I) & 1. b₂ = Class (EqRel R,I),(1. R) & 0. b₂ = Class (EqRel R,I),(0. R) & ( for x, y being Element of b₂ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of b₂ . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of b₂ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of b₂ . x,y = Class (EqRel R,I),(a * b) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines QuotientRing RING_1:def 6 :

for R being Ring
for I being Ideal of R
for b₃ being strict doubleLoopStr holds
( b₃ = QuotientRing R,I iff ( the carrier of b₃ = Class (EqRel R,I) & 1. b₃ = Class (EqRel R,I),(1. R) & 0. b₃ = Class (EqRel R,I),(0. R) & ( for x, y being Element of b₃ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the addF of b₃ . x,y = Class (EqRel R,I),(a + b) ) ) & ( for x, y being Element of b₃ ex a, b being Element of R st
( x = Class (EqRel R,I),a & y = Class (EqRel R,I),b & the multF of b₃ . 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

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: b * (a - (1_ R)) in I by IDEAL_1:def 2;
A6: b * (a - (1_ R)) = (b * a) - (b * (1_ R)) by VECTSP_1:43
.= (b * a) - b by VECTSP_1:def 13 ;
thus h * e = Class (EqRel R,I),(b * a) by A2, A3, Th14
.= h by A3, A5, A6, Th6 ; :: thesis: e * h = h
A7: (a - (1_ R)) * b in I by A4, IDEAL_1:def 3;
A8: (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, A7, 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 associative well-unital distributive Abelian add-associative right_zeroed ;
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 )

proof end;

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 )

proof end;

registration

let R be non degenerated commutative Ring;
cluster maximal -> prime Element of K34(the carrier of R);
coherence
for b₁ being Ideal of R st b₁ is maximal holds
b₁ is prime

proof end;

end;

registration

let R be non degenerated Ring;
cluster maximal Element of K34(the carrier of R);
existence
ex b₁ being Ideal of R st b₁ is maximal

proof end;

end;

registration

let R be non degenerated commutative Ring;
cluster maximal Element of K34(the carrier of R);
existence
ex b₁ being Ideal of R st b₁ 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;