:: The First Isomorphism Theorem and Other Properties of Rings
:: by Artur Korni{\l}owicz and Christoph Schwarzweller
::
:: Received November 29, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

definition

let R be non empty set ;
let f be non empty FinSequence of R;
let x be Element of dom f;
:: original: .
redefine func f . x -> Element of R;
coherence
f . x is Element of R

proof end;

end;

registration

let X be set ;
let F1, F2 be X -valued FinSequence;

cluster F1 ^ F2 -> X -valued ;

coherence
F1 ^ F2 is X -valued

proof end;

end;

theorem prod4: :: RING_2:1

for R being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for F being FinSequence of R st ex i being Nat st
( i in dom F & F . i = 0. R ) holds
Product F = 0. R

proof end;

theorem prod5: :: RING_2:2

for R being non degenerated right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for F being FinSequence of R holds
( Product F = 0. R iff ex i being Nat st
( i in dom F & F . i = 0. R ) )

proof end;

definition

let X be set ;
mode Chain of X is sequence of X;

end;

definition

let X be non empty set ;
let C be Chain of X;

attr C is ascending means :asc: :: RING_2:def 1
for i being Nat holds C . i c= C . (i + 1);

attr C is stagnating means :: RING_2:def 2
ex i being Nat st
for j being Nat st j >= i holds
C . j = C . i;

end;

:: deftheorem asc defines ascending RING_2:def 1 :
for X being non empty set
for C being Chain of X holds
( C is ascending iff for i being Nat holds C . i c= C . (i + 1) );

:: deftheorem defines stagnating RING_2:def 2 :
for X being non empty set
for C being Chain of X holds
( C is stagnating iff ex i being Nat st
for j being Nat st j >= i holds
C . j = C . i );

registration

let X be non empty set ;
let x be Element of X;

cluster NAT --> x -> ascending stagnating for Chain of X;

coherence
for b₁ being Chain of X st b₁ = NAT --> x holds
( b₁ is ascending & b₁ is stagnating )

proof end;

end;

registration

let X be non empty set ;

cluster Relation-like NAT -defined X -valued Function-like non empty total quasi_total ascending stagnating for Element of bool [:NAT,X:];

existence
ex b₁ being Chain of X st
( b₁ is ascending & b₁ is stagnating )

proof end;

end;

ch1: for X being non empty set
for C being ascending Chain of X
for x being object
for i, j being Nat st i <= j & x in C . i holds
x in C . j

proof end;

theorem :: RING_2:3

for X being non empty set
for C being ascending Chain of X
for i, j being Nat st i <= j holds
C . i c= C . j by ch1;

definition

let R be Ring;

func Ideals R -> Subset-Family of the carrier of R equals :: RING_2:def 3
{ I where I is Ideal of R : verum } ;

coherence
{ I where I is Ideal of R : verum } is Subset-Family of the carrier of R

proof end;

end;

:: deftheorem defines Ideals RING_2:def 3 :
for R being Ring holds Ideals R = { I where I is Ideal of R : verum } ;

registration

let R be Ring;

cluster Ideals R -> non empty ;

coherence
not Ideals R is empty

proof end;

end;

theorem id2: :: RING_2:4

for R being comRing
for I being Ideal of R
for a being Element of R st a in I holds
{a} -Ideal c= I

proof end;

theorem id1: :: RING_2:5

for R being Ring
for C being ascending Chain of (Ideals R) holds union { (C . i) where i is Nat : verum } is Ideal of R

proof end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_zeroed doubleLoopStr ;

cluster R --> (0. S) -> additive ;

coherence
R --> (0. S) is additive

proof end;

end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

cluster R --> (0. S) -> multiplicative ;

coherence
R --> (0. S) is multiplicative

proof end;

end;

registration

let R be non empty well-unital doubleLoopStr ;
let S be non degenerated well-unital doubleLoopStr ;

cluster R --> (0. S) -> non unity-preserving ;

coherence
not R --> (0. S) is unity-preserving by FUNCOP_1:7;

end;

registration

let R be non empty doubleLoopStr ;

cluster id R -> additive unity-preserving multiplicative ;

coherence
( id R is additive & id R is multiplicative & id R is unity-preserving ) ;

end;

registration

let R be non empty doubleLoopStr ;

cluster id R -> monomorphism epimorphism ;

coherence
( id R is RingMonomorphism & id R is RingEpimorphism ) ;

end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_zeroed doubleLoopStr ;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive for Element of bool [: the carrier of R, the carrier of S:];

existence
ex b₁ being Function of R,S st b₁ is additive

proof end;

end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total multiplicative for Element of bool [: the carrier of R, the carrier of S:];

existence
ex b₁ being Function of R,S st b₁ is multiplicative

proof end;

end;

registration

let R, S be non empty well-unital doubleLoopStr ;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total unity-preserving for Element of bool [: the carrier of R, the carrier of S:];

existence
ex b₁ being Function of R,S st b₁ is unity-preserving

proof end;

end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive multiplicative for Element of bool [: the carrier of R, the carrier of S:];

existence
ex b₁ being Function of R,S st
( b₁ is additive & b₁ is multiplicative )

proof end;

end;

definition

let R, S be Ring;

attr S is R -homomorphic means :defhom: :: RING_2:def 4
ex f being Function of R,S st f is RingHomomorphism ;

end;

:: deftheorem defhom defines -homomorphic RING_2:def 4 :
for R, S being Ring holds
( S is R -homomorphic iff ex f being Function of R,S st f is RingHomomorphism );

registration

let R be Ring;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -homomorphic

proof end;

end;

registration

let R be comRing;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative commutative V124() V125() V126() V127() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -homomorphic

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -homomorphic

proof end;

end;

registration

let R be Field;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative commutative V124() V125() V126() V127() domRing-like gcd-like Euclidian R -homomorphic for doubleLoopStr ;

existence
ex b₁ being Field st b₁ is R -homomorphic

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative commutative V124() V125() V126() V127() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being comRing st b₁ is R -homomorphic

proof end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() R -homomorphic for doubleLoopStr ;

existence
ex b₁ being Ring st b₁ is R -homomorphic

proof end;

end;

registration

let R be Ring;
let S be R -homomorphic Ring;

cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive unity-preserving multiplicative for Element of bool [: the carrier of R, the carrier of S:];

existence
ex b₁ being Function of R,S st
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving )

proof end;

end;

definition

let R be Ring;
let S be R -homomorphic Ring;
mode Homomorphism of R,S is additive unity-preserving multiplicative Function of R,S;

end;

registration

let R, S, T be Ring;
let f be unity-preserving Function of R,S;
let g be unity-preserving Function of S,T;

cluster f * g -> unity-preserving for Function of R,T;

coherence
for b₁ being Function of R,T st b₁ = g * f holds
b₁ is unity-preserving

proof end;

end;

registration

let R be Ring;
let S be R -homomorphic Ring;

cluster non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative S -homomorphic -> R -homomorphic S -homomorphic for doubleLoopStr ;

coherence
for b₁ being S -homomorphic Ring holds b₁ is R -homomorphic

proof end;

end;

notation

let R, S be non empty doubleLoopStr ;
synonym R,S are_isomorphic for R is_ringisomorph_to S;

end;

theorem hom1: :: RING_2:6

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S holds f . (0. R) = 0. S

proof end;

theorem hom4a: :: RING_2:7

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S
for x being Element of R holds f . (- x) = - (f . x)

proof end;

theorem hom4: :: RING_2:8

for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S
for x, y being Element of R holds f . (x - y) = (f . x) - (f . y)

proof end;

theorem hom2: :: RING_2:9

for R being non empty right_unital doubleLoopStr
for S being non empty right_complementable right-distributive right_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
for f being multiplicative Function of R,S holds
( f . (1. R) = 0. S or f . (1. R) = 1. S )

proof end;

hom3: for E, F being Field
for f being additive multiplicative Function of E,F holds
( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )

proof end;

theorem :: RING_2:10

for E, F being Field
for f being additive multiplicative Function of E,F holds
( f . (1. E) = 0. F iff f = E --> (0. F) )

proof end;

theorem hom3a: :: RING_2:11

for E, F being Field
for f being additive multiplicative Function of E,F holds
( f . (1. E) = 1. F iff f is monomorphism )

proof end;

registration

let E, F be Field;

cluster Function-like quasi_total additive unity-preserving multiplicative -> monomorphism for Element of bool [: the carrier of E, the carrier of F:];

coherence
for b₁ being Function of E,F st b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving holds
b₁ is monomorphism by hom3a;

end;

definition

let R be Ring;
let I be Ideal of R;

func canHom I -> Function of R,(R / I) means :defhomI: :: RING_2:def 5
for a being Element of R holds it . a = Class ((EqRel (R,I)),a);

existence
ex b₁ being Function of R,(R / I) st
for a being Element of R holds b₁ . a = Class ((EqRel (R,I)),a)

proof end;

uniqueness
for b₁, b₂ being Function of R,(R / I) st ( for a being Element of R holds b₁ . a = Class ((EqRel (R,I)),a) ) & ( for a being Element of R holds b₂ . a = Class ((EqRel (R,I)),a) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defhomI defines canHom RING_2:def 5 :
for R being Ring
for I being Ideal of R
for b₃ being Function of R,(R / I) holds
( b₃ = canHom I iff for a being Element of R holds b₃ . a = Class ((EqRel (R,I)),a) );

registration

let R be Ring;
let I be Ideal of R;

cluster canHom I -> additive unity-preserving multiplicative ;

coherence
( canHom I is additive & canHom I is multiplicative & canHom I is unity-preserving )

proof end;

end;

registration

let R be Ring;
let I be Ideal of R;

cluster canHom I -> epimorphism ;

coherence
canHom I is RingEpimorphism

proof end;

end;

registration

let R be Ring;
let I be Ideal of R;

cluster QuotientRing (R,I) -> R -homomorphic ;

coherence
R / I is R -homomorphic

proof end;

end;

registration

let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
let f be additive Function of R,S;

cluster ker f -> non empty ;

coherence
not ker f is empty

proof end;

end;

ker1: for R, S being non empty doubleLoopStr
for f being Function of R,S
for x being Element of R st x in ker f holds
f . x = 0. S

proof end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let f be additive Function of R,S;

cluster ker f -> add-closed ;

coherence
ker f is add-closed

proof end;

end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
let f be multiplicative Function of R,S;

cluster ker f -> left-ideal ;

coherence
ker f is left-ideal

proof end;

end;

registration

let R be non empty doubleLoopStr ;
let S be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let f be multiplicative Function of R,S;

cluster ker f -> right-ideal ;

coherence
ker f is right-ideal

proof end;

end;

registration

let R be non empty well-unital doubleLoopStr ;
let S be non degenerated well-unital doubleLoopStr ;
let f be unity-preserving Function of R,S;

cluster ker f -> proper ;

coherence
ker f is proper

proof end;

end;

theorem ker0: :: RING_2:12

for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S holds
( f is monomorphism iff ker f = {(0. R)} )

proof end;

theorem kercanhomI: :: RING_2:13

for R being Ring
for I being Ideal of R holds ker (canHom I) = I

proof end;

theorem :: RING_2:14

for R being Ring
for I being Subset of R holds
( I is Ideal of R iff ex S being b₁ -homomorphic Ring ex f being Homomorphism of R,S st ker f = I )

proof end;

T0: for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S holds 0. S in rng f

proof end;

T1: for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S holds 1. S in rng f

proof end;

T3: for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S holds rng f is Preserv of the addF of S

proof end;

T4: for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S holds rng f is Preserv of the multF of S

proof end;

definition

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;

func Image f -> strict doubleLoopStr means :defim: :: RING_2:def 6
( the carrier of it = rng f & the addF of it = the addF of S || (rng f) & the multF of it = the multF of S || (rng f) & the OneF of it = 1. S & the ZeroF of it = 0. S );

existence
ex b₁ being strict doubleLoopStr st
( the carrier of b₁ = rng f & the addF of b₁ = the addF of S || (rng f) & the multF of b₁ = the multF of S || (rng f) & the OneF of b₁ = 1. S & the ZeroF of b₁ = 0. S )

proof end;

uniqueness
for b₁, b₂ being strict doubleLoopStr st the carrier of b₁ = rng f & the addF of b₁ = the addF of S || (rng f) & the multF of b₁ = the multF of S || (rng f) & the OneF of b₁ = 1. S & the ZeroF of b₁ = 0. S & the carrier of b₂ = rng f & the addF of b₂ = the addF of S || (rng f) & the multF of b₂ = the multF of S || (rng f) & the OneF of b₂ = 1. S & the ZeroF of b₂ = 0. S holds
b₁ = b₂ ;

end;

:: deftheorem defim defines Image RING_2:def 6 :
for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S
for b₄ being strict doubleLoopStr holds
( b₄ = Image f iff ( the carrier of b₄ = rng f & the addF of b₄ = the addF of S || (rng f) & the multF of b₄ = the multF of S || (rng f) & the OneF of b₄ = 1. S & the ZeroF of b₄ = 0. S ) );

T5: for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S
for a, b being Element of (Image f)
for x, y being Element of S st a = x & b = y holds
( a + b = x + y & a * b = x * y )

proof end;

T6: for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S
for a being Element of (Image f) ex x being Element of R st f . x = a

proof end;

registration

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;

cluster Image f -> non empty strict ;

coherence
not Image f is empty

proof end;

end;

registration

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;

cluster Image f -> right_complementable strict Abelian add-associative right_zeroed ;

coherence
( Image f is Abelian & Image f is add-associative & Image f is right_zeroed & Image f is right_complementable )

proof end;

end;

registration

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;

cluster Image f -> strict well-unital distributive associative ;

coherence
( Image f is associative & Image f is well-unital & Image f is distributive )

proof end;

end;

registration

let R be comRing;
let S be R -homomorphic comRing;
let f be Homomorphism of R,S;

cluster Image f -> strict commutative ;

coherence
Image f is commutative

proof end;

end;

definition

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;
:: original: Image
redefine func Image f -> strict Subring of S;
coherence
Image f is strict Subring of S

proof end;

end;

definition

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;

func canHom f -> Function of (R / (ker f)),(Image f) means :ch: :: RING_2:def 7
for a being Element of R holds it . (Class ((EqRel (R,(ker f))),a)) = f . a;

existence
ex b₁ being Function of (R / (ker f)),(Image f) st
for a being Element of R holds b₁ . (Class ((EqRel (R,(ker f))),a)) = f . a

proof end;

uniqueness
for b₁, b₂ being Function of (R / (ker f)),(Image f) st ( for a being Element of R holds b₁ . (Class ((EqRel (R,(ker f))),a)) = f . a ) & ( for a being Element of R holds b₂ . (Class ((EqRel (R,(ker f))),a)) = f . a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem ch defines canHom RING_2:def 7 :
for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S
for b₄ being Function of (R / (ker f)),(Image f) holds
( b₄ = canHom f iff for a being Element of R holds b₄ . (Class ((EqRel (R,(ker f))),a)) = f . a );

registration

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;

cluster canHom f -> additive unity-preserving multiplicative ;

coherence
( canHom f is additive & canHom f is multiplicative & canHom f is unity-preserving )

proof end;

end;

registration

let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;

cluster canHom f -> monomorphism epimorphism ;

coherence
( canHom f is RingMonomorphism & canHom f is RingEpimorphism )

proof end;

end;

theorem :: RING_2:15

for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S holds R / (ker f), Image f are_isomorphic

proof end;

theorem :: RING_2:16

for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S st f is onto holds
R / (ker f),S are_isomorphic

proof end;

theorem :: RING_2:17

for R being Ring holds R / {(0. R)},R are_isomorphic

proof end;

registration

let R be Ring;

cluster QuotientRing (R,([#] R)) -> trivial ;

coherence
R / ([#] R) is trivial

proof end;

end;

registration

let L be non empty right_unital multLoopStr ;

cluster unital for Element of the carrier of L;

existence
ex b₁ being Element of L st b₁ is unital

proof end;

end;

definition

let L be non empty right_unital multLoopStr ;
mode Unit of L is unital Element of L;

end;

registration

let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;

cluster left_add-cancelable right_add-cancelable add-cancelable right_complementable non unital for Element of the carrier of L;

existence
not for b₁ being Element of L holds b₁ is unital

proof end;

end;

definition

let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;
mode NonUnit of L is non unital Element of L;

end;

registration

let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;

cluster 0. L -> non unital ;

coherence
not 0. L is unital

proof end;

end;

registration

let L be non empty right_unital multLoopStr ;

cluster 1. L -> unital ;

coherence
1. L is unital

proof end;

end;

registration

let L be non degenerated right_complementable left-distributive right_unital add-associative right_zeroed doubleLoopStr ;

cluster unital -> non zero for Element of the carrier of L;

coherence
for b₁ being Unit of L holds not b₁ is zero ;

end;

registration

let F be Field;

cluster non zero -> non zero unital for Element of the carrier of F;

coherence
for b₁ being non zero Element of F holds b₁ is unital

proof end;

end;

registration

let R be domRing;
let u, v be unital Element of R;

cluster u * v -> unital ;

coherence
u * v is unital

proof end;

end;

theorem div0: :: RING_2:18

for R being comRing
for a, b being Element of R holds
( a divides b iff b in {a} -Ideal )

proof end;

theorem div1: :: RING_2:19

for R being comRing
for a, b being Element of R holds
( a divides b iff {b} -Ideal c= {a} -Ideal )

proof end;

theorem div2: :: RING_2:20

for R being comRing
for a being Element of R holds
( a is Unit of R iff {a} -Ideal = [#] R )

proof end;

theorem div3: :: RING_2:21

for R being comRing
for a, b being Element of R holds
( a is_associated_to b iff {a} -Ideal = {b} -Ideal ) by div1;

definition

let R be non empty right_unital doubleLoopStr ;
let x be Element of R;

attr x is prime means :defprim: :: RING_2:def 8
( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds
( not x divides a * b or x divides a or x divides b ) ) );

attr x is irreducible means :: RING_2:def 9
( x <> 0. R & x is not Unit of R & ( for a being Element of R holds
( not a divides x or a is Unit of R or a is_associated_to x ) ) );

end;

:: deftheorem defprim defines prime RING_2:def 8 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is prime iff ( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds
( not x divides a * b or x divides a or x divides b ) ) ) );

:: deftheorem defines irreducible RING_2:def 9 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is irreducible iff ( x <> 0. R & x is not Unit of R & ( for a being Element of R holds
( not a divides x or a is Unit of R or a is_associated_to x ) ) ) );

notation

let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
antonym reducible x for irreducible ;

end;

registration

let R be non empty right_unital doubleLoopStr ;

cluster non prime for Element of the carrier of R;

existence
not for b₁ being Element of R holds b₁ is prime

proof end;

end;

lemintr: for x, y being Integer
for a, b being Element of INT.Ring st x <> 0 & x = a & y = b holds
( x divides y iff a divides b )

proof end;

registration

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable V106() integer complex ext-real V192() prime for Element of the carrier of INT.Ring;

existence
ex b₁ being Element of INT.Ring st b₁ is prime

proof end;

end;

registration

let R be non empty right_unital doubleLoopStr ;

cluster prime -> non zero non unital for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is prime holds
( not b₁ is zero & not b₁ is unital ) ;

cluster irreducible -> non zero non unital for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is irreducible holds
( not b₁ is zero & not b₁ is unital ) ;

end;

registration

let R be domRing;

cluster prime -> irreducible for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is prime holds
b₁ is irreducible

proof end;

end;

registration

let F be Field;

cluster -> reducible for Element of the carrier of F;

coherence
for b₁ being Element of F holds b₁ is reducible ;

end;

definition

let R be non empty right_unital doubleLoopStr ;

func IRR R -> Subset of R equals :: RING_2:def 10
{ x where x is Element of R : x is irreducible } ;

coherence
{ x where x is Element of R : x is irreducible } is Subset of R

proof end;

end;

:: deftheorem defines IRR RING_2:def 10 :
for R being non empty right_unital doubleLoopStr holds IRR R = { x where x is Element of R : x is irreducible } ;

registration

let F be Field;

cluster IRR F -> empty ;

coherence
IRR F is empty

proof end;

end;

theorem ass0: :: RING_2:22

for R being domRing
for c being non zero Element of R
for b, a, d being Element of R st a * b is_associated_to c * d & a is_associated_to c holds
b is_associated_to d

proof end;

theorem ass1: :: RING_2:23

for R being domRing
for a, b being Element of R st a is irreducible & b is_associated_to a holds
b is irreducible

proof end;

theorem thpr: :: RING_2:24

for R being non degenerated comRing
for a being non zero Element of R holds
( a is prime iff {a} -Ideal is prime )

proof end;

theorem maxirr: :: RING_2:25

for R being non degenerated comRing
for a being non zero Element of R st {a} -Ideal is maximal holds
a is irreducible

proof end;

registration

cluster non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative -> PID for doubleLoopStr ;

coherence
for b₁ being Field holds b₁ is PID

proof end;

end;

registration

cluster non empty PID for doubleLoopStr ;

existence
ex b₁ being non empty doubleLoopStr st b₁ is PID

proof end;

end;

definition

mode PIDomain is PID domRing;

end;

theorem maxirr2: :: RING_2:26

for R being PIDomain
for a being non zero Element of R holds
( {a} -Ideal is maximal iff a is irreducible )

proof end;

registration

let R be PIDomain;

cluster irreducible -> prime for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is irreducible holds
b₁ is prime

proof end;

end;

registration

cluster non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative Euclidian -> PID for doubleLoopStr ;

coherence
for b₁ being comRing st b₁ is Euclidian holds
b₁ is PID by IDEAL_1:94;

end;

registration

let R be PIDomain;

cluster Function-like quasi_total ascending -> stagnating for Element of bool [:NAT,(Ideals R):];

coherence
for b₁ being Chain of (Ideals R) st b₁ is ascending holds
b₁ is stagnating

proof end;

end;

definition

let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
let F be non empty FinSequence of R;

pred F is_a_factorization_of x means :: RING_2:def 11
( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) );

end;

:: deftheorem defines is_a_factorization_of RING_2:def 11 :
for R being non empty right_unital doubleLoopStr
for x being Element of R
for F being non empty FinSequence of R holds
( F is_a_factorization_of x iff ( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) ) );

definition

let R be non empty right_unital doubleLoopStr ;
let x be Element of R;

attr x is factorizable means :: RING_2:def 12
ex F being non empty FinSequence of R st F is_a_factorization_of x;

end;

:: deftheorem defines factorizable RING_2:def 12 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is factorizable iff ex F being non empty FinSequence of R st F is_a_factorization_of x );

definition

let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
assume AS: x is factorizable ;

mode Factorization of x -> non empty FinSequence of R means :ddf: :: RING_2:def 13
it is_a_factorization_of x;

existence
ex b₁ being non empty FinSequence of R st b₁ is_a_factorization_of x by AS;

end;

:: deftheorem ddf defines Factorization RING_2:def 13 :
for R being non empty right_unital doubleLoopStr
for x being Element of R st x is factorizable holds
for b₃ being non empty FinSequence of R holds
( b₃ is Factorization of x iff b₃ is_a_factorization_of x );

definition

let R be non empty right_unital doubleLoopStr ;
let x be Element of R;

attr x is uniquely_factorizable means :: RING_2:def 14
( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) );

end;

:: deftheorem defines uniquely_factorizable RING_2:def 14 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is uniquely_factorizable iff ( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) ) );

registration

let R be non empty right_unital doubleLoopStr ;

cluster uniquely_factorizable -> factorizable for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is uniquely_factorizable holds
b₁ is factorizable ;

end;

registration

let R be domRing;

cluster factorizable -> non zero non unital for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is factorizable holds
( not b₁ is zero & not b₁ is unital )

proof end;

end;

fact1: for R being non empty right_unital doubleLoopStr
for a being Element of R holds
( a is irreducible iff <*a*> is_a_factorization_of a )

proof end;

registration

let R be non empty right_unital doubleLoopStr ;

cluster irreducible -> factorizable for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is irreducible holds
b₁ is factorizable

proof end;

end;

theorem :: RING_2:27

for R being non empty right_unital doubleLoopStr
for a being Element of R holds
( a is irreducible iff <*a*> is_a_factorization_of a ) by fact1;

theorem fact2: :: RING_2:28

for R being non empty well-unital associative doubleLoopStr
for a, b being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds
F ^ G is_a_factorization_of a * b

proof end;

lemfactunique1: for R being domRing
for a, b, x being Element of R
for F being non empty FinSequence of R st x is prime & x divides a & a is_associated_to b & F is_a_factorization_of b holds
ex i being Element of dom F st F . i is_associated_to x

proof end;

lemfactunique: for R being PIDomain
for x, y being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
ex p being Function of (dom F),(dom G) st
( p is bijective & ( for i being Element of dom F holds G . (p . i) is_associated_to F . i ) )

proof end;

registration

let R be PIDomain;

cluster factorizable -> uniquely_factorizable for Element of the carrier of R;

coherence
for b₁ being Element of R st b₁ is factorizable holds
b₁ is uniquely_factorizable

proof end;

end;

definition

let R be non degenerated Ring;

attr R is factorial means :df: :: RING_2:def 15
for a being non zero Element of R st a is NonUnit of R holds
a is uniquely_factorizable ;

end;

:: deftheorem df defines factorial RING_2:def 15 :
for R being non degenerated Ring holds
( R is factorial iff for a being non zero Element of R st a is NonUnit of R holds
a is uniquely_factorizable );

registration

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V115() unital associative V124() V125() V126() V127() factorial for doubleLoopStr ;

existence
ex b₁ being non degenerated Ring st b₁ is factorial

proof end;

end;

registration

let R be non degenerated factorial Ring;

cluster non zero non unital -> factorizable for Element of the carrier of R;

coherence
for b₁ being Element of R st not b₁ is zero & not b₁ is unital holds
b₁ is factorizable

proof end;

end;

definition

mode FactorialRing is non degenerated factorial Ring;

end;

registration

cluster non empty non degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative PID domRing-like -> factorial for doubleLoopStr ;

coherence
for b₁ being domRing st b₁ is PID holds
b₁ is factorial

proof end;

end;

definition

let L be Field;
let p be Polynomial of L;

func deg* p -> Nat equals :S: :: RING_2:def 16
deg p if p <> 0_. L
otherwise 0 ;

coherence
( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) )

proof end;

consistency
for b₁ being Nat holds verum ;

end;

:: deftheorem S defines deg* RING_2:def 16 :
for L being Field
for p being Polynomial of L holds
( ( p <> 0_. L implies deg* p = deg p ) & ( not p <> 0_. L implies deg* p = 0 ) );

definition

let L be Field;

func deg* L -> Function of (Polynom-Ring L),NAT means :T: :: RING_2:def 17
for p being Polynomial of L holds it . p = deg* p;

existence
ex b₁ being Function of (Polynom-Ring L),NAT st
for p being Polynomial of L holds b₁ . p = deg* p

proof end;

uniqueness
for b₁, b₂ being Function of (Polynom-Ring L),NAT st ( for p being Polynomial of L holds b₁ . p = deg* p ) & ( for p being Polynomial of L holds b₂ . p = deg* p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem T defines deg* RING_2:def 17 :
for L being Field
for b₂ being Function of (Polynom-Ring L),NAT holds
( b₂ = deg* L iff for p being Polynomial of L holds b₂ . p = deg* p );

theorem degA: :: RING_2:29

for L being Field
for p being Polynomial of L
for q being non zero Polynomial of L holds deg (p mod q) < deg q

proof end;

theorem thEucl1: :: RING_2:30

for L being Field
for p being Element of (Polynom-Ring L)
for q being non zero Element of (Polynom-Ring L) ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or (deg* L) . r < (deg* L) . q ) )

proof end;

thEucl2: for L being Field ex f being Function of (Polynom-Ring L),NAT st
for p, q being Element of (Polynom-Ring L) st q <> 0. (Polynom-Ring L) holds
ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) )

proof end;

registration

let L be Field;

cluster Polynom-Ring L -> Euclidian ;

coherence
Polynom-Ring L is Euclidian

proof end;

end;

definition

let L be Field;
:: original: deg*
redefine func deg* L -> DegreeFunction of Polynom-Ring L;
coherence
deg* L is DegreeFunction of Polynom-Ring L

proof end;

end;