:: Quotient Rings :: by Artur Korni{\l}owicz :: :: Received December 7, 2005 :: Copyright (c) 2005-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 RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_1, ARYTM_3, SUPINF_2, RELAT_1, INT_2, CARD_FIL, TARSKI, GROUP_4, IDEAL_1, VECTSP_2, GROUP_1, FUNCSDOM, EQREL_1, STRUCT_0, WAYBEL20, PARTFUN1, RELAT_2, SETWISEO, FUNCT_1, MESFUNC1, BINOP_1, VECTSP_1, LATTICES, WELLORD2, ORDERS_1, WELLORD1, RING_1; notations TARSKI, XBOOLE_0, SUBSET_1, SETWISEO, RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, ALG_1, RELAT_2, EQREL_1, WELLORD1, WELLORD2, ORDERS_1, BINOP_1, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_2, IDEAL_1; constructors WELLORD1, WELLORD2, BINOP_1, SETWISEO, ORDERS_1, EQREL_1, GCD_1, IDEAL_1, DOMAIN_1, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSUB_1, EQREL_1, STRUCT_0, VECTSP_1, ALGSTR_1, QUOFIELD, IDEAL_1; requirements BOOLE, SUBSET; begin :: Preliminaries theorem :: RING_1:1 for L being add-associative right_zeroed right_complementable non empty addLoopStr, a, b being Element of L holds a - b + b = a; theorem :: RING_1:2 for L being add-associative right_zeroed right_complementable Abelian non empty addLoopStr, b, c being Element of L holds c = b - (b - c); theorem :: RING_1:3 for L being add-associative right_zeroed right_complementable Abelian non empty addLoopStr, a, b, c being Element of L holds a - b - (c - b ) = a - c; begin :: Ideals definition let K be non empty multMagma, S be Subset of K; attr S is quasi-prime means :: RING_1:def 1 for a, b being Element of K st a*b in S holds a in S or b in S; end; definition let K be non empty multLoopStr, S be Subset of K; attr S is prime means :: RING_1:def 2 S is proper quasi-prime; end; 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 st I c= J holds J = I or J is non proper; end; 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 quasi-maximal; end; registration let K be non empty multLoopStr; cluster prime -> proper quasi-prime for Subset of K; cluster proper quasi-prime -> prime for Subset of K; end; registration let R be non empty doubleLoopStr; cluster maximal -> proper quasi-maximal for Subset of R; cluster proper quasi-maximal -> maximal for Subset of R; end; registration let R be non empty addLoopStr; cluster [#]R -> add-closed; end; registration let R be non empty multMagma; cluster [#]R -> left-ideal right-ideal; end; theorem :: RING_1:4 for R being domRing holds {0.R} is prime; begin :: Equivalence Relation reserve R for Ring, I for Ideal of R, a, b for Element of R; definition let R be Ring, I be Ideal of R; func EqRel(R,I) -> Relation of R means :: RING_1:def 5 for a, b being Element of R holds [a,b] in it iff a-b in I; end; registration let R be Ring, I be Ideal of R; cluster EqRel(R,I) -> non empty total symmetric transitive; end; theorem :: RING_1:5 a in Class(EqRel(R,I),b) iff a-b in I; theorem :: RING_1:6 Class(EqRel(R,I),a) = Class(EqRel(R,I),b) iff a-b in I; theorem :: RING_1:7 Class(EqRel(R,[#]R),a) = the carrier of R; theorem :: RING_1:8 Class EqRel(R,[#]R) = {the carrier of R}; theorem :: RING_1:9 Class(EqRel(R,{0.R}),a) = {a}; theorem :: RING_1:10 Class EqRel(R,{0.R}) = rng singleton the carrier of R; begin :: Quotient Ring definition let R be Ring, I be Ideal of R; ::$N Quotient ring func QuotientRing(R,I) -> strict doubleLoopStr means :: 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); end; notation let R be Ring, I be Ideal of R; synonym R/I for QuotientRing(R,I); end; registration let R be Ring, I be Ideal of R; cluster R/I -> non empty; end; reserve x, y for Element of R/I; theorem :: RING_1:11 ex a being Element of R st x = Class(EqRel(R,I),a); theorem :: RING_1:12 Class(EqRel(R,I),a) is Element of R/I; theorem :: RING_1:13 x = Class(EqRel(R,I),a) & y = Class(EqRel(R,I),b) implies x+y = Class(EqRel(R,I),a+b); theorem :: RING_1:14 x = Class(EqRel(R,I),a) & y = Class(EqRel(R,I),b) implies x*y = Class(EqRel(R,I),a*b); theorem :: RING_1:15 Class(EqRel(R,I),1.R) = 1.(R/I); registration let R be Ring, I be Ideal of R; cluster R/I -> Abelian add-associative right_zeroed right_complementable associative well-unital distributive; end; registration let R be commutative Ring, I be Ideal of R; cluster R/I -> commutative; end; theorem :: RING_1:16 I is proper iff R/I is non degenerated; theorem :: RING_1:17 I is quasi-prime iff R/I is domRing-like; theorem :: RING_1:18 for R being commutative Ring, I being Ideal of R holds I is prime iff R/I is domRing; theorem :: RING_1:19 R is commutative & I is quasi-maximal implies R/I is almost_left_invertible; theorem :: RING_1:20 R/I is almost_left_invertible implies I is quasi-maximal; theorem :: RING_1:21 for R being commutative Ring, I being Ideal of R holds I is maximal iff R/I is Skew-Field; registration let R be non degenerated commutative Ring; cluster maximal -> prime for Ideal of R; end; ::$N Krull's theorem registration let R be non degenerated Ring; cluster maximal for Ideal of R; end; registration let R be non degenerated commutative Ring; cluster maximal for Ideal of R; end; registration let R be non degenerated commutative Ring, I be quasi-prime Ideal of R; cluster R/I -> domRing-like; end; registration let R be non degenerated commutative Ring, I be quasi-maximal Ideal of R; cluster R/I -> almost_left_invertible; end;