:: The Field of Quotients over an Integral Domain
:: by Christoph Schwarzweller
::
:: Received May 4, 1998
:: Copyright (c) 1998-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 XBOOLE_0, STRUCT_0, SUBSET_1, ZFMISC_1, SUPINF_2, ALGSTR_0,
MESFUNC1, MCART_1, VECTSP_2, RELAT_1, ARYTM_3, BINOP_1, RLVECT_1,
LATTICES, SETFAM_1, FUNCSDOM, GROUP_1, ARYTM_1, FUNCT_1, VECTSP_1,
MSSUBFAM, TARSKI, QUOFIELD, FUNCT_2, FDIFF_1, MOD_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, XTUPLE_0, MCART_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, BINOP_1, DOMAIN_1,
STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_2, VECTSP_1, TOPS_2,
GRCAT_1, GCD_1, GROUP_6, RINGCAT1, MOD_4;
constructors DOMAIN_1, TOPS_2, GRCAT_1, GROUP_6, GCD_1, ALGSTR_1, RELSET_1,
XTUPLE_0, RINGCAT1, MOD_4;
registrations SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, VECTSP_1, ALGSTR_1,
GCD_1, XTUPLE_0, RINGCAT1, MOD_4;
requirements SUBSET, BOOLE;
begin :: Definition of Pairs
definition
let I be non empty ZeroStr;
func Q.I -> Subset of [:the carrier of I,the carrier of I:] means
:: QUOFIELD:def 1
for u being set holds
u in it iff ex a,b being Element of I st u = [a,b] & b <> 0.I;
end;
theorem :: QUOFIELD:1
for I being non degenerated non empty multLoopStr_0 holds Q.I is non empty;
registration
let I be non degenerated non empty multLoopStr_0;
cluster Q.I -> non empty;
end;
theorem :: QUOFIELD:2
for I being non degenerated non empty multLoopStr_0 for u being
Element of Q.I holds u`2 <> 0.I;
:: Definition and some Properties of Pair Addition and Multiplication
definition
let I be non degenerated domRing-like non empty doubleLoopStr;
let u,v be Element of Q.I;
func padd(u,v) -> Element of Q.I equals
:: QUOFIELD:def 2
[u`1 * v`2 + v`1 * u`2, u`2 * v`2];
end;
definition
let I be non degenerated domRing-like non empty doubleLoopStr;
let u,v be Element of Q.I;
func pmult(u,v) -> Element of Q.I equals
:: QUOFIELD:def 3
[u`1 * v`1, u`2 * v`2];
end;
theorem :: QUOFIELD:3
for I being non degenerated domRing-like associative commutative
Abelian add-associative distributive non empty doubleLoopStr for u,v,w being
Element of Q.I holds padd(u,padd(v,w)) = padd(padd(u,v),w);
theorem :: QUOFIELD:4
for I being non degenerated domRing-like associative commutative
Abelian non empty doubleLoopStr for u,v,w being Element of Q.I holds pmult(u,
pmult(v,w)) = pmult(pmult(u,v),w);
definition
let I be non degenerated domRing-like associative commutative Abelian
add-associative distributive non empty doubleLoopStr;
let u, v be Element of Q.I;
redefine func padd(u,v);
commutativity;
end;
definition
let I be non degenerated domRing-like associative commutative Abelian non
empty doubleLoopStr;
let u, v be Element of Q.I;
redefine func pmult(u,v);
commutativity;
end;
:: Definition of Classes of Pairs
definition
let I be non degenerated non empty multLoopStr_0;
let u be Element of Q.I;
func QClass.u -> Subset of Q.I means
:: QUOFIELD:def 4
for z being Element of Q.I holds z in it iff z`1 * u`2 = z`2 * u`1;
end;
theorem :: QUOFIELD:5
for I being non degenerated commutative non empty multLoopStr_0
for u being Element of Q.I holds u in QClass.u;
registration
let I be non degenerated commutative non empty multLoopStr_0;
let u be Element of Q.I;
cluster QClass.u -> non empty;
end;
definition
let I be non degenerated non empty multLoopStr_0;
func Quot.I -> Subset-Family of Q.I means
:: QUOFIELD:def 5
for A being Subset of Q.I
holds A in it iff ex u being Element of Q.I st A = QClass.u;
end;
theorem :: QUOFIELD:6
for I being non degenerated non empty multLoopStr_0 holds Quot.
I is non empty;
registration
let I be non degenerated non empty multLoopStr_0;
cluster Quot.I -> non empty;
end;
theorem :: QUOFIELD:7
for I being non degenerated domRing-like commutative Ring for u,v
being Element of Q.I holds (ex w being Element of Quot.I st u in w & v in w)
implies u`1 * v`2 = v`1 * u`2;
theorem :: QUOFIELD:8
for I being non degenerated domRing-like commutative Ring for u,v
being Element of Quot.I holds u meets v implies u = v;
begin :: Definition of Quotient Field Addition and Multiplication
definition
let I be non degenerated domRing-like commutative Ring;
let u,v be Element of Quot.I;
func qadd(u,v) -> Element of Quot.I means
:: QUOFIELD:def 6
for z being Element of Q.I
holds z in it iff ex a,b being Element of Q.I st a in u & b in v & z`1 * (a`2 *
b`2) = z`2 * (a`1 * b`2 + b`1 * a`2);
end;
definition
let I be non degenerated domRing-like commutative Ring;
let u,v be Element of Quot.I;
func qmult(u,v) -> Element of Quot.I means
:: QUOFIELD:def 7
for z being Element of Q.I
holds z in it iff ex a,b being Element of Q.I st a in u & b in v & z`1 * (a`2 *
b`2) = z`2 * (a`1 * b`1);
end;
definition
let I be non degenerated non empty multLoopStr_0;
let u be Element of Q.I;
redefine func QClass.u -> Element of Quot.I;
end;
theorem :: QUOFIELD:9
for I being non degenerated domRing-like commutative Ring for u,
v being Element of Q.I holds qadd(QClass.u,QClass.v) = QClass.(padd(u,v));
theorem :: QUOFIELD:10
for I being non degenerated domRing-like commutative Ring for u,
v being Element of Q.I holds qmult(QClass.u,QClass.v) = QClass.(pmult(u,v));
:: Properties of Quotient Field Addition and Multiplication
definition
let I be non degenerated domRing-like commutative Ring;
func q0.I -> Element of Quot.I means
:: QUOFIELD:def 8
for z being Element of Q.I holds z in it iff z`1 = 0.I;
end;
definition
let I be non degenerated domRing-like commutative Ring;
func q1.I -> Element of Quot.I means
:: QUOFIELD:def 9
for z being Element of Q.I holds z in it iff z`1 = z`2;
end;
definition
let I be non degenerated domRing-like commutative Ring;
let u be Element of Quot.I;
func qaddinv(u) -> Element of Quot.I means
:: QUOFIELD:def 10
for z being Element of Q.
I holds z in it iff ex a being Element of Q.I st a in u & z`1 * a`2 = z`2 * (-(
a`1));
end;
definition
let I be non degenerated domRing-like commutative Ring;
let u be Element of Quot.I;
assume
u <> q0.I;
func qmultinv(u) -> Element of Quot.I means
:: QUOFIELD:def 11
for z being Element of
Q.I holds z in it iff ex a being Element of Q.I st a in u & z`1 * a`1 = z`2 * a
`2;
end;
theorem :: QUOFIELD:11
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds qadd(u,qadd(v,w)) = qadd(qadd(u,v),w) & qadd(
u,v) = qadd(v,u);
theorem :: QUOFIELD:12
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds qadd(u,q0.I) = u & qadd(q0.I,u) = u;
theorem :: QUOFIELD:13
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds qmult(u,qmult(v,w)) = qmult(qmult(u,v),w) &
qmult(u,v) = qmult(v,u);
theorem :: QUOFIELD:14
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds qmult(u,q1.I) = u & qmult(q1.I,u) = u;
theorem :: QUOFIELD:15
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds qmult(qadd(u,v),w) = qadd(qmult(u,w),qmult(v,
w));
theorem :: QUOFIELD:16
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds qmult(u,qadd(v,w)) = qadd(qmult(u,v),qmult(u,
w));
theorem :: QUOFIELD:17
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds qadd(u,qaddinv(u)) = q0.I & qadd(qaddinv(u),u) =
q0.I;
theorem :: QUOFIELD:18
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I st u <> q0.I holds qmult(u,qmultinv(u)) = q1.I & qmult(
qmultinv(u),u) = q1.I;
theorem :: QUOFIELD:19
for I being non degenerated domRing-like commutative Ring holds q1.I <> q0.I;
:: Redefinition of the Operations' Types
definition
let I be non degenerated domRing-like commutative Ring;
func quotadd(I) -> BinOp of Quot.I means
:: QUOFIELD:def 12
for u,v being Element of Quot.I holds it.(u,v) = qadd(u,v);
end;
definition
let I be non degenerated domRing-like commutative Ring;
func quotmult(I) -> BinOp of Quot.I means
:: QUOFIELD:def 13
for u,v being Element of Quot.I holds it.(u,v) = qmult(u,v);
end;
definition
let I be non degenerated domRing-like commutative Ring;
func quotaddinv(I) -> UnOp of Quot.I means
:: QUOFIELD:def 14
for u being Element of Quot.I holds it.(u) = qaddinv(u);
end;
definition
let I be non degenerated domRing-like commutative Ring;
func quotmultinv(I) -> UnOp of Quot.I means
:: QUOFIELD:def 15
for u being Element of Quot.I holds it.(u) = qmultinv(u);
end;
theorem :: QUOFIELD:20
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds (quotadd(I)).((quotadd(I)).(u,v),w) = (
quotadd(I)).(u,(quotadd(I)).(v,w));
theorem :: QUOFIELD:21
for I being non degenerated domRing-like commutative Ring for u,
v being Element of Quot.I holds (quotadd(I)).(u,v) = (quotadd(I)).(v,u);
theorem :: QUOFIELD:22
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds (quotadd(I)).(u,q0.I) = u & (quotadd(I)).(q0.I,u)
= u;
theorem :: QUOFIELD:23
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds (quotmult(I)).((quotmult(I)).(u,v),w) = (
quotmult(I)).(u,(quotmult(I)).(v,w));
theorem :: QUOFIELD:24
for I being non degenerated domRing-like commutative Ring for u,
v being Element of Quot.I holds (quotmult(I)).(u,v)=(quotmult(I)).(v,u);
theorem :: QUOFIELD:25
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds (quotmult(I)).(u,q1.I) = u & (quotmult(I)).(q1.I,
u) = u;
theorem :: QUOFIELD:26
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds (quotmult(I)).((quotadd(I)).(u,v),w) = (
quotadd(I)).((quotmult(I)).(u,w),(quotmult(I)).(v,w));
theorem :: QUOFIELD:27
for I being non degenerated domRing-like commutative Ring for u,
v,w being Element of Quot.I holds (quotmult(I)).(u,(quotadd(I)).(v,w)) = (
quotadd(I)).((quotmult(I)).(u,v),(quotmult(I)).(u,w));
theorem :: QUOFIELD:28
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I holds (quotadd(I)).(u,(quotaddinv(I)).(u)) = q0.I & (
quotadd(I)).((quotaddinv(I)).(u),u) = q0.I;
theorem :: QUOFIELD:29
for I being non degenerated domRing-like commutative Ring for u
being Element of Quot.I st u <> q0.I holds (quotmult(I)).(u,(quotmultinv(I)).(u
)) = q1.I & (quotmult(I)).((quotmultinv(I)).(u),u) = q1.I;
begin :: Definition of Quotient Field
definition
let I be non degenerated domRing-like commutative Ring;
func the_Field_of_Quotients(I) -> strict doubleLoopStr equals
:: QUOFIELD:def 16
doubleLoopStr
(# Quot.I,quotadd(I),quotmult(I),q1.I,q0.I #);
end;
registration
let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) -> non empty;
end;
theorem :: QUOFIELD:30
for I being non degenerated domRing-like commutative Ring holds the
carrier of the_Field_of_Quotients(I) = Quot.I & the addF of
the_Field_of_Quotients(I) = quotadd(I) & the multF of the_Field_of_Quotients(I)
= quotmult(I) & 0.the_Field_of_Quotients(I) = q0.I & 1.the_Field_of_Quotients(I
) = q1.I;
theorem :: QUOFIELD:31
for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds (quotadd(I)).(u,v) is Element
of the_Field_of_Quotients(I);
theorem :: QUOFIELD:32
for I being non degenerated domRing-like commutative Ring for u
being Element of the_Field_of_Quotients(I) holds (quotaddinv(I)).(u) is Element
of the_Field_of_Quotients(I);
theorem :: QUOFIELD:33
for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds (quotmult(I)).(u,v) is Element
of the_Field_of_Quotients(I);
theorem :: QUOFIELD:34
for I being non degenerated domRing-like commutative Ring for u being
Element of the_Field_of_Quotients(I) holds (quotmultinv(I)).(u) is Element of
the_Field_of_Quotients(I);
theorem :: QUOFIELD:35
for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds u + v = (quotadd(I)).(u,v);
registration
let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) -> add-associative right_zeroed
right_complementable;
end;
theorem :: QUOFIELD:36
for I being non degenerated domRing-like commutative Ring for u being
Element of the_Field_of_Quotients(I) holds -u = (quotaddinv(I)).(u);
theorem :: QUOFIELD:37
for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds u * v = (quotmult(I)).(u,v);
registration
let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) -> commutative;
end;
registration
let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) -> well-unital;
end;
theorem :: QUOFIELD:38
for I being non degenerated domRing-like commutative Ring holds 1.
the_Field_of_Quotients(I) = q1.I & 0.the_Field_of_Quotients(I) = q0.I;
theorem :: QUOFIELD:39
for I being non degenerated domRing-like commutative Ring for u,v,w
being Element of the_Field_of_Quotients(I) holds (u + v) + w = u + (v + w);
theorem :: QUOFIELD:40
for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds u + v = v + u;
theorem :: QUOFIELD:41
for I being non degenerated domRing-like commutative Ring for u being
Element of the_Field_of_Quotients(I) holds u + 0.the_Field_of_Quotients(I) = u;
theorem :: QUOFIELD:42
for I being non degenerated domRing-like commutative Ring for u being
Element of the_Field_of_Quotients(I) holds 1.the_Field_of_Quotients(I) * u = u;
theorem :: QUOFIELD:43
for I being non degenerated domRing-like commutative Ring for u,v
being Element of the_Field_of_Quotients(I) holds u * v = v * u;
theorem :: QUOFIELD:44
for I being non degenerated domRing-like commutative Ring for u,v,w
being Element of the_Field_of_Quotients(I) holds (u * v) * w = u * (v * w);
theorem :: QUOFIELD:45
for I being non degenerated domRing-like commutative Ring for u
being Element of the_Field_of_Quotients(I) st u <> 0.the_Field_of_Quotients(I)
ex v being Element of the_Field_of_Quotients(I) st u * v = 1.
the_Field_of_Quotients(I);
theorem :: QUOFIELD:46
for I being non degenerated domRing-like commutative Ring holds
the_Field_of_Quotients(I) is add-associative right_zeroed right_complementable
Abelian associative unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr;
registration
let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) -> Abelian associative distributive
almost_left_invertible non degenerated;
end;
theorem :: QUOFIELD:47
for I being non degenerated domRing-like commutative Ring for x
being Element of the_Field_of_Quotients(I) st x <> 0.the_Field_of_Quotients(I)
for a being Element of I st a <> 0.I for u being Element of Q.I st x = QClass.u
& u = [a,1.I] for v being Element of Q.I st v = [1.I,a] holds x" = QClass.v;
:: Field is Integral Domain
registration
cluster -> domRing-like right_unital for add-associative right_zeroed
right_complementable commutative associative well-unital distributive
almost_left_invertible non empty doubleLoopStr;
end;
registration
cluster add-associative right_zeroed right_complementable Abelian
commutative associative left_unital distributive almost_left_invertible non
degenerated for non empty doubleLoopStr;
end;
definition
let F be commutative associative well-unital distributive
almost_left_invertible non empty doubleLoopStr;
let x, y be Element of F;
func x/y -> Element of F equals
:: QUOFIELD:def 17
x * y";
end;
theorem :: QUOFIELD:48
for F being non degenerated almost_left_invertible commutative
Ring for a,b,c,d being Element of F st b <> 0.F & d <> 0.F holds (a/b) * (c/d)
= (a * c) / (b * d);
theorem :: QUOFIELD:49
for F being non degenerated almost_left_invertible commutative
Ring for a,b,c,d being Element of F st b <> 0.F & d <> 0.F holds (a/b) + (c/d)
= (a*d + c*b) / (b * d);
begin :: Definition of Ring Homomorphism
notation
let R,S be non empty doubleLoopStr;
let f be Function of R, S;
synonym f is RingHomomorphism for f is linear;
synonym f is RingEpimorphism for f is epimorphism;
synonym f is RingMonomorphism for f is monomorphism;
end;
notation
let R,S be non empty doubleLoopStr;
let f be Function of R, S;
synonym f is embedding for f is RingMonomorphism;
synonym f is RingIsomorphism for f is isomorphism;
end;
theorem :: QUOFIELD:50
for R,S being Ring for f being Function of R, S st
f is RingHomomorphism holds f.(0.R) = 0.S;
theorem :: QUOFIELD:51
for R,S being Ring for f being Function of R, S st f is
RingMonomorphism for x being Element of R holds f.x = 0.S iff x = 0.R;
theorem :: QUOFIELD:52
for R,S being non degenerated almost_left_invertible commutative
Ring for f being Function of R, S st f is RingHomomorphism for x being Element
of R st x <> 0.R holds f.(x") = (f.x)";
theorem :: QUOFIELD:53
for R,S being non degenerated almost_left_invertible commutative
Ring for f being Function of R, S st f is RingHomomorphism for x,y being
Element of R st y <> 0.R holds f.(x * y") = f.x * (f.y)";
theorem :: QUOFIELD:54
for R,S,T being Ring for f being Function of R, S st f is
RingHomomorphism for g being Function of S, T st g is RingHomomorphism holds g*
f is RingHomomorphism;
theorem :: QUOFIELD:55
for R being non empty doubleLoopStr holds id R is RingHomomorphism;
registration
let R be non empty doubleLoopStr;
cluster id R -> RingHomomorphism;
end;
definition
::$CD 4
let R,S be non empty doubleLoopStr;
pred R is_embedded_in S means
:: QUOFIELD:def 22
ex f being Function of R, S st f is RingMonomorphism;
end;
definition
let R,S be non empty doubleLoopStr;
pred R is_ringisomorph_to S means
:: QUOFIELD:def 23
ex f being Function of R, S st f is RingIsomorphism;
symmetry;
end;
begin :: Properties of the Field of Quotients
definition
let I be non empty ZeroStr;
let x, y be Element of I;
assume
y <> 0.I;
func quotient(x,y) -> Element of Q.I equals
:: QUOFIELD:def 24
[x,y];
end;
definition
let I be non degenerated domRing-like commutative Ring;
func canHom(I) -> Function of I, the_Field_of_Quotients(I) means
:: QUOFIELD:def 25
for x being Element of I holds it.x = QClass.(quotient(x,1.I));
end;
theorem :: QUOFIELD:56
for I being non degenerated domRing-like commutative Ring holds
canHom(I) is RingHomomorphism;
theorem :: QUOFIELD:57
for I being non degenerated domRing-like commutative Ring holds
canHom(I) is embedding;
theorem :: QUOFIELD:58
for I being non degenerated domRing-like commutative Ring holds I
is_embedded_in the_Field_of_Quotients(I);
theorem :: QUOFIELD:59
for F being non degenerated almost_left_invertible domRing-like
commutative Ring holds F is_ringisomorph_to the_Field_of_Quotients(F);
registration
let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) -> domRing-like right_unital
right-distributive;
end;
theorem :: QUOFIELD:60
for I being non degenerated domRing-like commutative Ring holds
the_Field_of_Quotients(the_Field_of_Quotients(I)) is_ringisomorph_to
the_Field_of_Quotients(I);
:: Universal Property of Fields of Quotients
definition
let I, F be non empty doubleLoopStr;
let f be Function of I, F;
pred I has_Field_of_Quotients_Pair F,f means
:: QUOFIELD:def 26
f is RingMonomorphism &
for F9 being add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr for f9 being Function of I, F9 st f9 is
RingMonomorphism holds ex h being Function of F, F9 st h is RingHomomorphism &
h*f = f9 & for h9 being Function of F, F9 st h9 is RingHomomorphism & h9*f = f9
holds h9 = h;
end;
theorem :: QUOFIELD:61
for I being non degenerated domRing-like commutative Ring holds ex F
being add-associative right_zeroed right_complementable Abelian commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr st ex f being Function of I, F st I
has_Field_of_Quotients_Pair F,f;
theorem :: QUOFIELD:62
for I being domRing-like commutative Ring for F,F9 being
add-associative right_zeroed right_complementable Abelian commutative
associative well-unital distributive almost_left_invertible non degenerated
non empty doubleLoopStr for f being Function of I, F for f9 being Function of
I, F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,
f9 holds F is_ringisomorph_to F9;