:: Quotient Rings
:: by Artur Korni{\l}owicz
::
:: Received December 7, 2005
:: Copyright (c) 2005-2016 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;