Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

The Field of Quotients Over an Integral Domain

by
Christoph Schwarzweller

MML identifier: QUOFIELD
[ Mizar article, MML identifier index ]

```environ

vocabulary RLVECT_1, VECTSP_1, MCART_1, VECTSP_2, BINOP_1, LATTICES, SETFAM_1,
FUNCSDOM, ARYTM_3, BOOLE, ARYTM_1, FUNCT_1, RELAT_1, PRE_TOPC, GRCAT_1,
COHSP_1, ENDALG, SUBSET_1, QUOFIELD;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MCART_1, FUNCT_1,
FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, RLVECT_1, VECTSP_2, VECTSP_1,
BINOP_1, PRE_TOPC, TOPS_2, FUNCSDOM, GRCAT_1, ENDALG, GCD_1;
constructors DOMAIN_1, BINOP_1, GCD_1, TOPS_2, GRCAT_1, ENDALG, ALGSTR_2;
clusters STRUCT_0, RELSET_1, SUBSET_1, GCD_1, ALGSTR_1, VECTSP_1, XBOOLE_0;
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;

definition 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
let I be non degenerated non empty multLoopStr_0;
let u be Element of Q.I;
redefine func u`1 -> Element of I;
redefine func u`2 -> Element of I;
end;

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

canceled;

theorem :: QUOFIELD:4
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

theorem :: QUOFIELD:5
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) & pmult(u,v) = pmult(v,u);

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;
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:6
for I being non degenerated commutative (non empty multLoopStr_0)
for u being Element of Q.I holds u in QClass.u;

definition 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:7
for I being non degenerated non empty multLoopStr_0 holds
Quot.I is non empty;

definition let I be non degenerated non empty multLoopStr_0;
cluster Quot.I -> non empty;
end;

theorem :: QUOFIELD:8
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:9
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Quot.I holds u meets v implies u = v;

::: Definition of Quotient Field Addition and Multiplication

begin

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;

canceled;

theorem :: QUOFIELD:11
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Q.I holds

theorem :: QUOFIELD:12
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:13
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds

theorem :: QUOFIELD:14
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:15
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:16
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:17
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds

theorem :: QUOFIELD:18
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds

theorem :: QUOFIELD:19
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds

theorem :: QUOFIELD:20
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:21
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:22
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds

theorem :: QUOFIELD:23
for I being non degenerated domRing-like commutative Ring

theorem :: QUOFIELD:24
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds

theorem :: QUOFIELD:25
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:26
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:27
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:28
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds

theorem :: QUOFIELD:29
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds

theorem :: QUOFIELD:30
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds

theorem :: QUOFIELD:31
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;

::: Definition of Quotient Field

begin

definition
let I be non degenerated domRing-like commutative Ring;
func the_Field_of_Quotients(I) -> strict doubleLoopStr equals
:: QUOFIELD:def 16
end;

definition
let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) -> non empty;
end;

theorem :: QUOFIELD:32
for I being non degenerated domRing-like commutative Ring holds
the carrier of the_Field_of_Quotients(I) = Quot.I &
the mult of the_Field_of_Quotients(I) = quotmult(I) &
the Zero of the_Field_of_Quotients(I) = q0.I &
the unity of the_Field_of_Quotients(I) = q1.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

theorem :: QUOFIELD:34
for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I) holds

theorem :: QUOFIELD:35
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:36
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:37
for I being non degenerated domRing-like commutative Ring
for u,v being Element of the_Field_of_Quotients(I) holds

definition let I be non degenerated domRing-like commutative Ring;
right_complementable;
end;

theorem :: QUOFIELD:38
for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I) holds

theorem :: QUOFIELD:39
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);

theorem :: QUOFIELD:40
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:41
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:42
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:43
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;

canceled;

theorem :: QUOFIELD:45
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:46
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:47
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:48
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:49
for I being non degenerated domRing-like commutative Ring holds
Abelian commutative associative left_unital distributive
Field-like non degenerated (non empty doubleLoopStr);

definition let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) ->
Abelian commutative associative left_unital distributive
Field-like non degenerated;
end;

theorem :: QUOFIELD:50
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

definition
cluster -> domRing-like right_unital
commutative associative left_unital
distributive Field-like non degenerated(non empty doubleLoopStr));
end;

definition
Abelian commutative associative left_unital
distributive Field-like non degenerated (non empty doubleLoopStr);
end;

definition
let F be commutative associative left_unital distributive
Field-like (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:51
for F being non degenerated Field-like 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:52
for F being non degenerated Field-like 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);

::: Definition of Ring Homomorphism

begin

definition let R,S be non empty doubleLoopStr;
let f be map of R, S;
canceled 3;

attr f is RingHomomorphism means
:: QUOFIELD:def 21
end;

definition let R,S be non empty doubleLoopStr;
cluster RingHomomorphism -> additive multiplicative unity-preserving
map of R, S;
cluster additive multiplicative unity-preserving -> RingHomomorphism
map of R, S;
end;

definition let R,S be non empty doubleLoopStr;
let f be map of R, S;
attr f is RingEpimorphism means
:: QUOFIELD:def 22
f is RingHomomorphism & rng f = the carrier of S;

attr f is RingMonomorphism means
:: QUOFIELD:def 23
f is RingHomomorphism & f is one-to-one;
synonym f is embedding;
end;

definition let R,S be non empty doubleLoopStr;
let f be map of R, S;
attr f is RingIsomorphism means
:: QUOFIELD:def 24
f is RingMonomorphism RingEpimorphism;
end;

definition let R,S be non empty doubleLoopStr;
cluster RingIsomorphism -> RingMonomorphism RingEpimorphism map of R, S;
cluster RingMonomorphism RingEpimorphism -> RingIsomorphism map of R, S;
end;

theorem :: QUOFIELD:53
for R,S being Ring
for f being map of R, S st f is RingHomomorphism holds
f.(0.R) = 0.S;

theorem :: QUOFIELD:54
for R,S being Ring
for f being map of R, S st f is RingMonomorphism
for x being Element of R holds
f.x = 0.S iff x = 0.R;

theorem :: QUOFIELD:55
for R,S being non degenerated Field-like commutative Ring
for f being map of R, S st f is RingHomomorphism
for x being Element of R st x <> 0.R holds
f.(x") = (f.x)";

theorem :: QUOFIELD:56
for R,S being non degenerated Field-like commutative Ring
for f being map 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:57
for R,S,T being Ring
for f being map of R, S st f is RingHomomorphism
for g being map of S, T st g is RingHomomorphism holds
g*f is RingHomomorphism;

theorem :: QUOFIELD:58
for R being non empty doubleLoopStr
holds id R is RingHomomorphism;

definition let R be non empty doubleLoopStr;
cluster id R -> RingHomomorphism;
end;

definition let R,S be non empty doubleLoopStr;
pred R is_embedded_in S means
:: QUOFIELD:def 25
ex f being map 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 26
ex f being map of R, S st f is RingIsomorphism;
symmetry;
end;

::: Properties of the Field of Quotients

begin

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 27
[x,y];
end;

definition let I be non degenerated domRing-like commutative Ring;
func canHom(I) -> map of I, the_Field_of_Quotients(I) means
:: QUOFIELD:def 28
for x being Element of I holds
it.x = QClass.(quotient(x,1_ I));
end;

theorem :: QUOFIELD:59
for I being non degenerated domRing-like commutative Ring holds
canHom(I) is RingHomomorphism;

theorem :: QUOFIELD:60
for I being non degenerated domRing-like commutative Ring holds
canHom(I) is embedding;

theorem :: QUOFIELD:61
for I being non degenerated domRing-like commutative Ring holds
I is_embedded_in the_Field_of_Quotients(I);

theorem :: QUOFIELD:62
for F being non degenerated Field-like domRing-like commutative Ring holds
F is_ringisomorph_to the_Field_of_Quotients(F);

definition let I be non degenerated domRing-like commutative Ring;
cluster the_Field_of_Quotients(I) ->
domRing-like right_unital right-distributive;
end;

theorem :: QUOFIELD:63
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 map of I, F;
pred I has_Field_of_Quotients_Pair F,f means
:: QUOFIELD:def 29
f is RingMonomorphism &
for F' being add-associative right_zeroed right_complementable
Abelian commutative associative left_unital distributive
Field-like non degenerated (non empty doubleLoopStr)
for f' being map of I, F' st f' is RingMonomorphism holds
ex h being map of F, F' st h is RingHomomorphism &
h*f = f' &
for h' being map of F, F'
st h' is RingHomomorphism & h'*f = f'
holds h' = h;
end;

theorem :: QUOFIELD:64
for I being non degenerated domRing-like commutative Ring holds
ex F being add-associative right_zeroed right_complementable
Abelian commutative associative left_unital distributive
Field-like non degenerated (non empty doubleLoopStr)
st ex f being map of I, F st I has_Field_of_Quotients_Pair F,f;

theorem :: QUOFIELD:65
for I being domRing-like commutative Ring
for F,F' being add-associative right_zeroed right_complementable
Abelian commutative associative left_unital distributive
Field-like non degenerated (non empty doubleLoopStr)
for f being map of I, F
for f' being map of I, F'
st I has_Field_of_Quotients_Pair F,f &
I has_Field_of_Quotients_Pair F',f'
holds F is_ringisomorph_to F';
```