Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### The Field of Quotients Over an Integral Domain

**by****Christoph Schwarzweller**- Received May 4, 1998
- 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 padd(u,padd(v,w)) = padd(padd(u,v),w) & padd(u,v) = padd(v,u); 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; 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: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 qadd(QClass.u,QClass.v) = QClass.(padd(u,v)); 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 qadd(u,qadd(v,w)) = qadd(qadd(u,v),w) & qadd(u,v) = qadd(v,u); 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 qmult(qadd(u,v),w) = qadd(qmult(u,w),qmult(v,w)); theorem :: QUOFIELD:18 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:19 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: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 (quotadd(I)).((quotadd(I)).(u,v),w) = (quotadd(I)).(u,(quotadd(I)).(v,w)); theorem :: QUOFIELD:23 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:24 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: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 (quotmult(I)).((quotadd(I)).(u,v),w) = (quotadd(I)).((quotmult(I)).(u,w),(quotmult(I)).(v,w)); theorem :: QUOFIELD:29 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:30 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: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 doubleLoopStr (# Quot.I,quotadd(I),quotmult(I),q1.I,q0.I #); 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 add of the_Field_of_Quotients(I) = quotadd(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 (quotadd(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 (quotaddinv(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 (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 u + v = (quotadd(I)).(u,v); definition let I be non degenerated domRing-like commutative Ring; cluster the_Field_of_Quotients(I) -> add-associative right_zeroed 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 -u = (quotaddinv(I)).(u); 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 the_Field_of_Quotients(I) is add-associative right_zeroed right_complementable 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 (add-associative right_zeroed right_complementable commutative associative left_unital distributive Field-like non degenerated(non empty doubleLoopStr)); end; definition cluster add-associative right_zeroed right_complementable 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 f is additive multiplicative unity-preserving; 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';

Back to top