:: The First Isomorphism Theorem and Other Properties of Rings
:: by Artur Korni{\l}owicz and Christoph Schwarzweller
::
:: Received November 29, 2014
:: Copyright (c) 2014-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, FUNCT_1, RELAT_1, RLVECT_1, GCD_1, WELLORD1, ORDINAL4,
VECTSP_1, CARD_3, ALGSTR_0, XBOOLE_0, TARSKI, INT_1, FUNCT_2, TREES_2,
XCMPLX_0, VECTSP_2, VECTSP10, STRUCT_0, SUBSET_1, SUPINF_2, REARRAN1,
NAT_1, CARD_1, MESFUNC1, INT_3, GROUP_1, ARYTM_1, FINSEQ_1, SETFAM_1,
INT_2, YELLOW_8, QUOFIELD, MSSUBFAM, BINOP_1, GROUP_4, GROUP_6, MOD_4,
LATTICES, HURWITZ, NUMBERS, IDEAL_1, REALSET1, C0SP1, RATFUNC1, EQREL_1,
POLYNOM1, POLYNOM3, ZFMISC_1, FUNCSDOM, WAYBEL20, CARD_FIL, RING_1,
RING_2, PARTFUN1, FINSEQ_3, WAYBEL_6, FUNCOP_1, XXREAL_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, REALSET1,
FINSEQ_1, VFUNCT_1, ORDINAL1, EQREL_1, XCMPLX_0, XXREAL_0, NAT_1, INT_1,
INT_2, INT_3, NUMBERS, VECTSP_1, VECTSP_2, QUOFIELD, STRUCT_0, ALGSTR_0,
GROUP_1, RLVECT_1, GCD_1, POLYNOM3, HURWITZ, IDEAL_1, GROUP_4, GROUP_6,
VECTSP10, MOD_4, C0SP1, RATFUNC1, RING_1;
constructors RING_1, C0SP1, BINOM, RELSET_1, GCD_1, QUOFIELD, BINOP_2,
VFUNCT_1, RATFUNC1, MOD_4, GROUP_6, REALSET1, INT_3, RINGCAT1, GROUP_4,
HURWITZ, VECTSP10, INT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, MEMBERED,
FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, SUBSET_1, RELAT_1, FUNCT_2,
ALGSTR_0, RLVECT_1, QUOFIELD, REALSET1, VFUNCT_1, RATFUNC1, IDEAL_1,
MOD_4, RINGCAT1, RING_1, C0SP1, XCMPLX_0, XXREAL_0, INT_3, VALUED_0,
FUNCT_1, PARTFUN1, CARD_1, GRCAT_1, GROUP_6;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin :: Preliminaries
definition
let R be non empty set;
let f be non empty FinSequence of R;
let x be Element of dom f;
redefine func f.x -> Element of R;
end;
registration
let X be set;
let F1,F2 be X-valued FinSequence;
cluster F1 ^ F2 -> X-valued;
end;
theorem :: RING_2:1
for R being add-associative right_zeroed right_complementable
distributive well-unital non empty doubleLoopStr,
F being FinSequence of R
st ex i being Nat st i in dom F & F.i = 0.R holds Product F = 0.R;
theorem :: RING_2:2
for R being add-associative right_zeroed right_complementable well-unital
distributive domRing-like non degenerated doubleLoopStr,
F being FinSequence of R
holds Product F = 0.R iff ex i being Nat st i in dom F & F.i = 0.R;
definition
let X be set;
mode Chain of X is sequence of X;
end;
definition
let X be non empty set,
C be Chain of X;
attr C is ascending means
:: 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;
registration
let X be non empty set;
let x be Element of X;
cluster NAT --> x -> ascending stagnating for Chain of X;
end;
registration
let X be non empty set;
cluster ascending stagnating for Chain of X;
end;
theorem :: RING_2:3
for X being non empty set,
C be ascending Chain of X,
i,j being Nat st i <= j holds C.i c= C.j;
definition
let R be Ring;
func Ideals R -> Subset-Family of the carrier of R equals
:: RING_2:def 3
the set of all I where I is Ideal of R;
end;
registration
let R be Ring;
cluster Ideals R -> non empty;
end;
theorem :: RING_2:4
for R being comRing,
I being Ideal of R,
a being Element of R holds a in I implies {a}-Ideal c= I;
theorem :: RING_2:5
for R being Ring,
C being ascending Chain of Ideals(R)
holds union the set of all C.i where i is Nat is Ideal of R;
registration
let R be non empty doubleLoopStr,
S be right_zeroed non empty doubleLoopStr;
cluster R --> 0.S -> additive;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
cluster R --> 0.S -> multiplicative;
end;
registration
let R be well-unital non empty doubleLoopStr,
S be well-unital non degenerated doubleLoopStr;
cluster R --> 0.S -> non unity-preserving;
end;
registration
let R be non empty doubleLoopStr;
cluster id R -> additive multiplicative unity-preserving;
end;
registration
let R be non empty doubleLoopStr;
cluster id R -> monomorphism epimorphism;
end;
registration
let R be non empty doubleLoopStr,
S be right_zeroed non empty doubleLoopStr;
cluster additive for Function of R,S;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
cluster multiplicative for Function of R,S;
end;
registration
let R,S be well-unital non empty doubleLoopStr;
cluster unity-preserving for Function of R,S;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
cluster additive multiplicative for Function of R,S;
end;
begin :: Homomorphisms, Kernel and Image
definition
let R,S be Ring;
attr S is R-homomorphic means
:: RING_2:def 4
ex f being Function of R,S st f is RingHomomorphism;
end;
registration
let R be Ring;
cluster R-homomorphic for Ring;
end;
registration
let R be comRing;
cluster R-homomorphic for comRing;
cluster R-homomorphic for Ring;
end;
registration
let R be Field;
cluster R-homomorphic for Field;
cluster R-homomorphic for comRing;
cluster R-homomorphic for Ring;
end;
registration
let R be Ring,
S be R-homomorphic Ring;
cluster additive multiplicative unity-preserving for Function of R,S;
end;
definition
let R be Ring,
S be R-homomorphic Ring;
mode Homomorphism of R,S is
additive multiplicative unity-preserving 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 g * f -> unity-preserving for Function of R,T;
end;
registration
let R be Ring,
S be R-homomorphic Ring;
cluster -> R-homomorphic for S-homomorphic Ring;
end;
notation
let R,S be non empty doubleLoopStr;
synonym R,S are_isomorphic for R is_ringisomorph_to S;
end;
theorem :: RING_2:6
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S
holds f.(0.R) = 0.S;
theorem :: RING_2:7
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S
for x being Element of R
holds f.(-x) = - f.x;
theorem :: RING_2:8
for R being add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr,
f being additive Function of R,S
for x,y being Element of R holds f.(x-y) = f.x - f.y;
theorem :: RING_2:9
for R being right_unital non empty doubleLoopStr,
S being add-associative right_zeroed right_complementable right_unital
Abelian right-distributive domRing-like non empty doubleLoopStr,
f being multiplicative Function of R,S
holds f.(1.R) = 0.S or f.(1.R) = 1.S;
theorem :: RING_2:10
for E,F being Field,
f being additive multiplicative Function of E,F
holds f.(1.E) = 0.F iff f = E --> 0.F;
theorem :: RING_2:11
for E,F being Field,
f being additive multiplicative Function of E,F
holds f.(1.E) = 1.F iff f is monomorphism;
registration
let E,F be Field;
cluster additive multiplicative unity-preserving -> monomorphism
for Function of E,F;
end;
definition
let R be Ring,
I be Ideal of R;
func canHom I -> Function of R, R/I means
:: RING_2:def 5
for a being Element of R holds it.a = Class(EqRel(R,I),a);
end;
registration
let R be Ring,
I be Ideal of R;
cluster canHom I -> additive multiplicative unity-preserving;
end;
registration
let R be Ring,
I be Ideal of R;
cluster canHom I -> epimorphism;
end;
registration
let R be Ring,
I be Ideal of R;
cluster R/I -> R-homomorphic;
end;
registration
let R be add-associative right_zeroed right_complementable
non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let f be additive Function of R,S;
cluster ker f -> non empty;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
non empty doubleLoopStr;
let f be additive Function of R,S;
cluster ker f -> add-closed;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let f be multiplicative Function of R,S;
cluster ker f -> left-ideal;
end;
registration
let R be non empty doubleLoopStr,
S be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
let f be multiplicative Function of R,S;
cluster ker f -> right-ideal;
end;
registration
let R be well-unital non empty doubleLoopStr,
S be well-unital non degenerated doubleLoopStr;
let f be unity-preserving Function of R,S;
cluster ker f -> proper;
end;
theorem :: RING_2:12
for R being Ring,
S being R-homomorphic Ring,
f being Homomorphism of R,S
holds f is monomorphism iff ker f = {0.R};
theorem :: RING_2:13
for R being Ring,
I being Ideal of R holds ker(canHom I) = I;
theorem :: RING_2:14
for R being Ring,
I being Subset of R
holds I is Ideal of R iff
ex S being R-homomorphic Ring,
f being Homomorphism of R,S st ker f = I;
definition
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
func Image f -> strict doubleLoopStr means
:: 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;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster Image f -> non empty;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster Image f -> Abelian add-associative right_zeroed right_complementable;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster Image f -> associative well-unital distributive;
end;
registration
let R be comRing,
S be R-homomorphic comRing,
f be Homomorphism of R,S;
cluster Image f -> commutative;
end;
definition
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
redefine func Image f -> strict Subring of S;
end;
definition
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
func canHom f -> Function of R/(ker f), Image f means
:: RING_2:def 7
for a being Element of R holds it.Class(EqRel(R,ker f),a) = f.a;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster canHom f -> additive multiplicative unity-preserving;
end;
registration
let R be Ring,
S be R-homomorphic Ring,
f be Homomorphism of R,S;
cluster canHom f -> monomorphism epimorphism;
end;
theorem :: RING_2:15
for R being Ring,
S being R-homomorphic Ring,
f being Homomorphism of R,S holds R/(ker f), Image f are_isomorphic;
theorem :: RING_2:16
for R being Ring,
S being R-homomorphic Ring,
f being Homomorphism of R,S
holds f is onto implies R/(ker f), S are_isomorphic;
theorem :: RING_2:17
for R being Ring holds R/{0.R}, R are_isomorphic;
registration
let R be Ring;
cluster R / [#]R -> trivial;
end;
begin :: Units and Non Units
registration
let L be right_unital non empty multLoopStr;
cluster unital for Element of L;
end;
definition
let L be right_unital non empty multLoopStr;
mode Unit of L is unital Element of L;
end;
registration
let L be add-associative right_zeroed right_complementable
left-distributive non degenerated doubleLoopStr;
cluster non unital for Element of L;
end;
definition
let L be add-associative right_zeroed right_complementable
left-distributive non degenerated doubleLoopStr;
mode NonUnit of L is non unital Element of L;
end;
registration
let L be add-associative right_zeroed right_complementable
left-distributive non degenerated doubleLoopStr;
cluster 0.L -> non unital;
end;
registration
let L be right_unital non empty multLoopStr;
cluster 1.L -> unital;
end;
registration
let L be add-associative right_zeroed right_complementable
left-distributive right_unital non degenerated doubleLoopStr;
cluster -> non zero for Unit of L;
end;
registration
let F be Field;
cluster -> unital for non zero Element of F;
end;
registration
let R be domRing,
u,v be unital Element of R;
cluster u * v -> unital;
end;
theorem :: RING_2:18
for R being comRing,
a,b being Element of R
holds a divides b iff b in {a}-Ideal;
theorem :: RING_2:19
for R being comRing,
a,b being Element of R
holds a divides b iff {b}-Ideal c= {a}-Ideal;
theorem :: RING_2:20
for R being comRing,
a being Element of R
holds a is Unit of R iff {a}-Ideal = [#] R;
theorem :: RING_2:21
for R being comRing,
a,b being Element of R
holds a is_associated_to b iff {a}-Ideal = {b}-Ideal;
begin :: Prime and Irreducible Elements
definition
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
attr x is prime means
:: RING_2:def 8
x <> 0.R & not x is Unit of R &
for a,b being Element of R st x divides a * b
holds (x divides a or x divides b);
attr x is irreducible means
:: RING_2:def 9
x <> 0.R & not x is Unit of R &
for a being Element of R st a divides x
holds (a is Unit of R or a is_associated_to x);
end;
notation
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
antonym x is reducible for x is irreducible;
end;
registration
let R be right_unital non empty doubleLoopStr;
cluster non prime for Element of R;
end;
registration
cluster prime for Element of INT.Ring;
end;
registration
let R be right_unital non empty doubleLoopStr;
cluster prime -> non zero non unital for Element of R;
cluster irreducible -> non zero non unital for Element of R;
end;
registration
let R be domRing;
cluster prime -> irreducible for Element of R;
end;
registration
let F be Field;
cluster -> reducible for Element of F;
end;
definition
let R be right_unital non empty doubleLoopStr;
func IRR R -> Subset of R equals
:: RING_2:def 10
{ x where x is Element of R : x is irreducible };
end;
registration
let F be Field;
cluster IRR F -> empty;
end;
theorem :: RING_2:22
for R being domRing,
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;
theorem :: RING_2:23
for R being domRing,
a,b being Element of R
st a is irreducible & b is_associated_to a holds b is irreducible;
theorem :: RING_2:24
for R being non degenerated comRing,
a being non zero Element of R
holds a is prime iff {a}-Ideal is prime;
theorem :: RING_2:25
for R being non degenerated comRing,
a being non zero Element of R
holds {a}-Ideal is maximal implies a is irreducible;
begin :: Principal Ideal Domains and Factorial Rings
registration
cluster -> PID for Field;
end;
registration
cluster PID for non empty doubleLoopStr;
end;
definition
mode PIDomain is PID domRing;
end;
theorem :: RING_2:26
for R being PIDomain,
a being non zero Element of R
holds {a}-Ideal is maximal iff a is irreducible;
registration
let R be PIDomain;
cluster irreducible -> prime for Element of R;
end;
registration
cluster Euclidian -> PID for comRing;
end;
registration
let R be PIDomain;
cluster ascending -> stagnating for Chain of Ideals(R);
end;
definition
let R be right_unital non empty 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;
definition
let R be right_unital non empty 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;
definition
let R be right_unital non empty doubleLoopStr;
let x be Element of R;
assume x is factorizable;
mode Factorization of x -> non empty FinSequence of R means
:: RING_2:def 13
it is_a_factorization_of x;
end;
definition
let R be right_unital non empty 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;
registration
let R be right_unital non empty doubleLoopStr;
cluster uniquely_factorizable -> factorizable for Element of R;
end;
registration
let R be domRing;
cluster factorizable -> non zero non unital for Element of R;
end;
registration
let R be right_unital non empty doubleLoopStr;
cluster irreducible -> factorizable for Element of R;
end;
theorem :: RING_2:27
for R being right_unital non empty doubleLoopStr,
a being Element of R
holds a is irreducible iff <*a*> is_a_factorization_of a;
theorem :: RING_2:28
for R being well-unital associative non empty doubleLoopStr,
a,b being Element of R,
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;
registration
let R be PIDomain;
cluster factorizable -> uniquely_factorizable for Element of R;
end;
definition
let R be non degenerated Ring;
attr R is factorial means
:: RING_2:def 15
for a being non zero Element of R
st a is NonUnit of R holds a is uniquely_factorizable;
end;
registration
cluster factorial for non degenerated Ring;
end;
registration
let R be factorial non degenerated Ring;
cluster non zero non unital -> factorizable for Element of R;
end;
definition
mode FactorialRing is factorial non degenerated Ring;
end;
registration
cluster PID -> factorial for domRing;
end;
begin :: Polynomial Rings over Fields
definition
let L be Field;
let p be Polynomial of L;
func deg* p -> Nat equals
:: RING_2:def 16
deg p if p <> 0_.L otherwise 0;
end;
definition
let L be Field;
func deg* L -> Function of Polynom-Ring L,NAT means
:: RING_2:def 17
for p being Polynomial of L holds it.p = deg* p;
end;
theorem :: 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;
theorem :: RING_2:30
for L being Field,
p being Element of Polynom-Ring L,
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);
registration
let L be Field;
cluster Polynom-Ring L -> Euclidian;
end;
definition
let L be Field;
redefine func deg* L -> DegreeFunction of Polynom-Ring L;
end;