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