:: The Field of Quotients over an Integral Domain
:: by Christoph Schwarzweller
::
:: Received May 4, 1998
:: Copyright (c) 1998 Association of Mizar Users
definition
let I be non
empty ZeroStr ;
func Q. I -> Subset of
[:the carrier of I,the carrier of I:] means :
Def1:
:: 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 ) );
existence
ex b1 being Subset of [:the carrier of I,the carrier of I:] st
for u being set holds
( u in b1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) )
uniqueness
for b1, b2 being Subset of [:the carrier of I,the carrier of I:] st ( for u being set holds
( u in b1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) & ( for u being set holds
( u in b2 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Q. QUOFIELD:def 1 :
theorem Th1: :: QUOFIELD:1
theorem Th2: :: QUOFIELD:2
Lm1:
for I being non empty non degenerated multLoopStr_0
for u being Element of Q. I holds
( u `1 is Element of I & u `2 is Element of I )
;
:: deftheorem defines padd QUOFIELD:def 2 :
:: deftheorem defines pmult QUOFIELD:def 3 :
theorem :: QUOFIELD:3
canceled;
theorem Th4: :: QUOFIELD:4
theorem Th5: :: QUOFIELD:5
:: deftheorem Def4 defines QClass. QUOFIELD:def 4 :
theorem Th6: :: QUOFIELD:6
:: deftheorem Def5 defines Quot. QUOFIELD:def 5 :
theorem Th7: :: QUOFIELD:7
theorem Th8: :: QUOFIELD:8
theorem Th9: :: QUOFIELD:9
:: deftheorem Def6 defines qadd QUOFIELD:def 6 :
:: deftheorem Def7 defines qmult QUOFIELD:def 7 :
theorem :: QUOFIELD:10
canceled;
theorem Th11: :: QUOFIELD:11
theorem Th12: :: QUOFIELD:12
:: deftheorem Def8 defines q0. QUOFIELD:def 8 :
:: deftheorem Def9 defines q1. QUOFIELD:def 9 :
:: deftheorem Def10 defines qaddinv QUOFIELD:def 10 :
:: deftheorem Def11 defines qmultinv QUOFIELD:def 11 :
theorem Th13: :: QUOFIELD:13
theorem Th14: :: QUOFIELD:14
theorem Th15: :: QUOFIELD:15
theorem Th16: :: QUOFIELD:16
theorem Th17: :: QUOFIELD:17
theorem Th18: :: QUOFIELD:18
theorem Th19: :: QUOFIELD:19
theorem Th20: :: QUOFIELD:20
theorem Th21: :: QUOFIELD:21
definition
let I be non
degenerated commutative domRing-like Ring;
func quotadd I -> BinOp of
Quot. I means :
Def12:
:: QUOFIELD:def 12
for
u,
v being
Element of
Quot. I holds
it . u,
v = qadd u,
v;
existence
ex b1 being BinOp of Quot. I st
for u, v being Element of Quot. I holds b1 . u,v = qadd u,v
uniqueness
for b1, b2 being BinOp of Quot. I st ( for u, v being Element of Quot. I holds b1 . u,v = qadd u,v ) & ( for u, v being Element of Quot. I holds b2 . u,v = qadd u,v ) holds
b1 = b2
end;
:: deftheorem Def12 defines quotadd QUOFIELD:def 12 :
definition
let I be non
degenerated commutative domRing-like Ring;
func quotmult I -> BinOp of
Quot. I means :
Def13:
:: QUOFIELD:def 13
for
u,
v being
Element of
Quot. I holds
it . u,
v = qmult u,
v;
existence
ex b1 being BinOp of Quot. I st
for u, v being Element of Quot. I holds b1 . u,v = qmult u,v
uniqueness
for b1, b2 being BinOp of Quot. I st ( for u, v being Element of Quot. I holds b1 . u,v = qmult u,v ) & ( for u, v being Element of Quot. I holds b2 . u,v = qmult u,v ) holds
b1 = b2
end;
:: deftheorem Def13 defines quotmult QUOFIELD:def 13 :
:: deftheorem Def14 defines quotaddinv QUOFIELD:def 14 :
:: deftheorem Def15 defines quotmultinv QUOFIELD:def 15 :
theorem Th22: :: QUOFIELD:22
theorem Th23: :: QUOFIELD:23
theorem Th24: :: QUOFIELD:24
theorem Th25: :: QUOFIELD:25
theorem Th26: :: QUOFIELD:26
theorem Th27: :: QUOFIELD:27
theorem Th28: :: QUOFIELD:28
theorem Th29: :: QUOFIELD:29
theorem Th30: :: QUOFIELD:30
theorem Th31: :: QUOFIELD:31
:: deftheorem defines the_Field_of_Quotients QUOFIELD:def 16 :
theorem :: QUOFIELD:32
theorem :: QUOFIELD:33
theorem Th34: :: QUOFIELD:34
theorem :: QUOFIELD:35
theorem :: QUOFIELD:36
theorem :: QUOFIELD:37
Lm2:
for I being non degenerated commutative domRing-like Ring holds
( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )
theorem :: QUOFIELD:38
theorem :: QUOFIELD:39
Lm3:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty commutative doubleLoopStr
Lm4:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is well-unital
theorem :: QUOFIELD:40
theorem :: QUOFIELD:41
theorem :: QUOFIELD:42
theorem :: QUOFIELD:43
theorem :: QUOFIELD:44
canceled;
theorem :: QUOFIELD:45
theorem :: QUOFIELD:46
theorem :: QUOFIELD:47
theorem Th48: :: QUOFIELD:48
theorem Th49: :: QUOFIELD:49
theorem Th50: :: QUOFIELD:50
:: deftheorem defines / QUOFIELD:def 17 :
theorem Th51: :: QUOFIELD:51
theorem Th52: :: QUOFIELD:52
:: deftheorem QUOFIELD:def 18 :
canceled;
:: deftheorem QUOFIELD:def 19 :
canceled;
:: deftheorem QUOFIELD:def 20 :
canceled;
:: deftheorem Def21 defines RingHomomorphism QUOFIELD:def 21 :
:: deftheorem Def22 defines RingEpimorphism QUOFIELD:def 22 :
:: deftheorem Def23 defines RingMonomorphism QUOFIELD:def 23 :
:: deftheorem Def24 defines RingIsomorphism QUOFIELD:def 24 :
theorem Th53: :: QUOFIELD:53
theorem Th54: :: QUOFIELD:54
theorem Th55: :: QUOFIELD:55
theorem Th56: :: QUOFIELD:56
theorem Th57: :: QUOFIELD:57
theorem Th58: :: QUOFIELD:58
:: deftheorem Def25 defines is_embedded_in QUOFIELD:def 25 :
:: deftheorem Def26 defines is_ringisomorph_to QUOFIELD:def 26 :
:: deftheorem Def27 defines quotient QUOFIELD:def 27 :
:: deftheorem Def28 defines canHom QUOFIELD:def 28 :
theorem Th59: :: QUOFIELD:59
theorem Th60: :: QUOFIELD:60
theorem :: QUOFIELD:61
theorem Th62: :: QUOFIELD:62
theorem :: QUOFIELD:63
:: deftheorem Def29 defines has_Field_of_Quotients_Pair QUOFIELD:def 29 :
theorem :: QUOFIELD:64
theorem :: QUOFIELD:65