:: 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 b₁ being Subset of K st b₁ is prime holds
( b₁ is proper & b₁ is quasi-prime ) ;

cluster proper quasi-prime -> prime for 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 ;

end;

registration

let R be non empty doubleLoopStr ;

cluster maximal -> proper quasi-maximal for 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 ) ;

cluster proper quasi-maximal -> maximal for 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 ;

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

:: 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 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 :: 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 b₁ being Ideal of R st b₁ is maximal holds
b₁ is prime

proof end;

end;

:: 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 b₁ being Ideal of R st b₁ 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 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;