:: {R}ings of {F}ractions and {L}ocalization :: by Yasushige Watase :: :: Received January 13, 2020 :: Copyright (c) 2020-2021 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 ARYTM_3, FUNCT_1, RELAT_1, RLVECT_1, VECTSP_1, ALGSTR_0, XBOOLE_0, TARSKI, VECTSP_2, VECTSP10, STRUCT_0, SUBSET_1, SUPINF_2, MESFUNC1, GROUP_1, ARYTM_1, QUOFIELD, MSSUBFAM, BINOP_1, LATTICES, IDEAL_1, C0SP1, EQREL_1, ZFMISC_1, FUNCSDOM, WAYBEL20, CARD_FIL, RING_2, MCART_1, INT_2, TOPZARI1, FREEALG, FUNCT_2, XCMPLX_0, LATTICEA, RING_1, GROUP_4, RINGFRAC, VALUED_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, EQREL_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, QUOFIELD, GCD_1, GROUP_6, IDEAL_1, VECTSP10, C0SP1, RING_1, RING_2, TOPZARI1; constructors BINOP_1, SETWISEO, ORDERS_1, EQREL_1, GCD_1, IDEAL_1, DOMAIN_1, RELSET_1, BINOM, RINGCAT1, MOD_4, QUOFIELD, TOPZARI1; registrations SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, VECTSP_1, ALGSTR_1, XTUPLE_0, MOD_4, QUOFIELD, XBOOLE_0, ALGSTR_0, RLVECT_1, IDEAL_1, RING_1, RING_2, FOMODEL0, EQREL_1, TOPZARI1; requirements SUBSET, BOOLE; begin :: Preliminaries: Zero Divisors, Units, multiplicatively-closed Set reserve R,R1 for commutative Ring; reserve A,B for non degenerated commutative Ring; reserve o,o1,o2 for object; reserve r,r1,r2 for Element of R; reserve a,a1,a2,b,b1 for Element of A; reserve f for Function of R, R1; reserve p for Element of Spectrum A; :: Zero-divisor. Unit [AM]p2-3 definition let R be commutative Ring; let r be Element of R; attr r is zero_divisible means :: RINGFRAC:def 1 ex r1 be Element of R st r1 <> 0.R & r*r1 = 0.R; end; registration let A be non degenerated commutative Ring; cluster zero_divisible for Element of A; end; definition let A; mode Zero_Divisor of A is zero_divisible Element of A; end; theorem :: RINGFRAC:1 0.A is Zero_Divisor of A; theorem :: RINGFRAC:2 1.A is not Zero_Divisor of A; definition let A; func ZeroDiv_Set(A) -> Subset of A equals :: RINGFRAC:def 2 {a where a is Element of A: a is Zero_Divisor of A}; end; definition let A; func Non_ZeroDiv_Set(A) -> Subset of A equals :: RINGFRAC:def 3 [#]A \ ZeroDiv_Set(A); end; registration let A; cluster ZeroDiv_Set(A) -> non empty; cluster Non_ZeroDiv_Set(A) -> non empty; end; theorem :: RINGFRAC:3 not 0.A in Non_ZeroDiv_Set(A); theorem :: RINGFRAC:4 A is domRing implies {0.A} = ZeroDiv_Set(A); :::::::::::::::::::::::::::::::::::::::::::::::::::: ::: Definition of multiplicatively-closed set :::::::::::::::::::::::::::::::::::::::::::::::::::: :: [AM] p36 theorem :: RINGFRAC:5 {1.R} is multiplicatively-closed; registration let R; cluster multiplicatively-closed for non empty Subset of R; end; definition let A; let V be Subset of A; attr V is without_zero means :: RINGFRAC:def 4 not 0.A in V; end; registration let A; cluster without_zero for non empty multiplicatively-closed Subset of A; end; ::Example.1.1)of [AM] p38 theorem :: RINGFRAC:6 [#]A \ p is multiplicatively-closed; ::Example.1.3)of [AM] p38 theorem :: RINGFRAC:7 for J be proper Ideal of A holds multClSet(J,a) is multiplicatively-closed; registration let A; cluster Non_ZeroDiv_Set(A) -> multiplicatively-closed; end; definition let R; func Unit_Set(R) -> Subset of R equals :: RINGFRAC:def 5 {a where a is Element of R: a is Unit of R }; end; registration let R; cluster Unit_Set(R) -> non empty; end; theorem :: RINGFRAC:8 r1 in Unit_Set(R) implies r1 is right_mult-cancelable; definition let R; let r be Element of R; assume r in Unit_Set(R); func recip(r) -> Element of R means :: RINGFRAC:def 6 it * r = 1.R; end; notation let R; let r be Element of R; synonym r["] for recip(r); end; definition let R; let u,v be Element of R; ::: assume v in Unit_Set(R); func u[/]v -> Element of R equals :: RINGFRAC:def 7 u*(recip(u)); end; theorem :: RINGFRAC:9 for u be Unit of R, v be Element of R holds f is RingHomomorphism implies f.u is Unit of R1 & (f.u)["] = f.(u["]); theorem :: RINGFRAC:10 for u be Unit of R, v be Element of R holds f is RingHomomorphism implies f.(v*(u["])) = (f.v)*((f.u)["]); begin :: Equivalence Relation of Fraction reserve S for non empty multiplicatively-closed Subset of R; :: Definition of Pairs definition let R, S; func Frac(S) -> Subset of [:the carrier of R,the carrier of R:] means :: RINGFRAC:def 8 for x being set holds x in it iff ex a,b being Element of R st x = [a,b] & b in S; end; theorem :: RINGFRAC:11 Frac(S) = [:[#]R,S:]; registration let R,S; cluster Frac(S) -> non empty; end; definition let R,S; func frac1(S) -> Function of R, Frac(S) means :: RINGFRAC:def 9 for o be object st o in the carrier of R holds it.o = [o,1.R]; end; reserve u,v,w,x,y,z for Element of Frac(S); definition let R,S; let u,v be Element of Frac(S); func Fracadd(u,v) -> Element of Frac(S) equals :: RINGFRAC:def 10 [u`1 * v`2 + v`1 * u`2, u`2 * v`2]; commutativity; end; definition let R,S; let u,v be Element of Frac(S); func Fracmult(u,v) -> Element of Frac(S) equals :: RINGFRAC:def 11 [u`1 * v`1, u`2 * v`2]; commutativity; end; definition let R,S,x,y; func x+y -> Element of Frac(S) equals :: RINGFRAC:def 12 Fracadd(x,y); func x*y -> Element of Frac(S) equals :: RINGFRAC:def 13 Fracmult(x,y); end; theorem :: RINGFRAC:12 Fracadd(x,Fracadd(y,z)) = Fracadd(Fracadd(x,y),z); theorem :: RINGFRAC:13 Fracmult(x,Fracmult(y,z)) = Fracmult(Fracmult(x,y),z); definition let R,S; let x,y be Element of Frac(S); pred x,y Fr_Eq S means :: RINGFRAC:def 14 ex s1 being Element of R st s1 in S & (x`1 * y`2 - y`1 * x`2) * s1 = 0.R; end; theorem :: RINGFRAC:14 0.R in S implies x,y Fr_Eq S; theorem :: RINGFRAC:15 x,x Fr_Eq S; theorem :: RINGFRAC:16 x,y Fr_Eq S implies y,x Fr_Eq S; theorem :: RINGFRAC:17 x,y Fr_Eq S & y,z Fr_Eq S implies x,z Fr_Eq S; definition let R,S; func EqRel(S) -> Equivalence_Relation of Frac(S) means :: RINGFRAC:def 15 [u,v] in it iff u,v Fr_Eq S; end; :::registration ::: let R,S; ::: cluster EqRel(S) -> non empty total symmetric transitive; ::: coherence; :::end; theorem :: RINGFRAC:18 x in Class(EqRel(S),y) iff x,y Fr_Eq S; theorem :: RINGFRAC:19 Class(EqRel(S),x) = Class(EqRel(S),y) iff x,y Fr_Eq S; theorem :: RINGFRAC:20 x,u Fr_Eq S & y,v Fr_Eq S implies Fracmult(x,y),Fracmult(u,v) Fr_Eq S; theorem :: RINGFRAC:21 x,u Fr_Eq S & y,v Fr_Eq S implies Fracadd(x,y),Fracadd(u,v) Fr_Eq S; theorem :: RINGFRAC:22 (x+y)*z, x*z + y*z Fr_Eq S; definition let R,S; func 0.(R,S) -> Element of Frac(S) equals :: RINGFRAC:def 16 [0.R, 1.R]; func 1.(R,S) -> Element of Frac(S) equals :: RINGFRAC:def 17 [1.R, 1.R]; end; theorem :: RINGFRAC:23 for s be Element of S holds x=[s,s] implies x,1.(R,S) Fr_Eq S; begin :: Constraction of Ring of Fraction definition let R, S; func FracRing(S) -> strict doubleLoopStr means :: RINGFRAC:def 18 the carrier of it = Class EqRel(S) & 1.it = Class(EqRel(S),1.(R,S)) & 0.it = Class(EqRel(S),0.(R,S)) & (for x, y being Element of it ex a, b being Element of Frac(S) st x = Class(EqRel(S),a) & y = Class(EqRel(S),b) & (the addF of it).(x,y) = Class(EqRel(S),a+b) ) & for x, y being Element of it ex a, b being Element of Frac(S) st x = Class(EqRel(S),a) & y = Class(EqRel(S),b) & (the multF of it).(x,y) = Class(EqRel(S),a*b ); end; notation let R,S; synonym S~R for FracRing(S); end; registration let R, S; cluster S~R -> non empty; end; :: Example 2) of [AM] p38 theorem :: RINGFRAC:24 0.R in S iff S~R is degenerated; reserve a, b, c for Element of Frac(S); reserve x, y, z for Element of S~R; theorem :: RINGFRAC:25 for x holds ex a being Element of Frac(S) st x = Class(EqRel(S),a); theorem :: RINGFRAC:26 x = Class(EqRel(S),a) & y = Class(EqRel(S),b) implies x*y = Class(EqRel(S),a*b); theorem :: RINGFRAC:27 x*y = y*x; theorem :: RINGFRAC:28 x = Class(EqRel(S),a) & y = Class(EqRel(S),b) implies x+y = Class(EqRel(S),a+b); theorem :: RINGFRAC:29 S~R is Ring; registration let R,S; cluster S~R -> commutative Abelian add-associative right_zeroed right_complementable associative well-unital distributive; end; theorem :: RINGFRAC:30 for z holds ex r1,r2 be Element of R st r2 in S & z = Class(EqRel(S),[r1,r2]); :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: ::::::: canHom(obj1) obj1: multiclosed set of a Ring ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: reserve S for without_zero non empty multiplicatively-closed Subset of A; definition let A,S; func canHom(S) -> Function of A, S~A means :: RINGFRAC:def 19 for o be object st o in the carrier of A holds it.o = Class(EqRel(S),(frac1(S)).o); end; registration let A,S; cluster canHom(S) -> additive multiplicative unity-preserving; end; theorem :: RINGFRAC:31 for a,b being Element of A holds (canHom(S)).(a-b) = (canHom(S)).a - (canHom(S)).b; theorem :: RINGFRAC:32 not 0.A in S implies ker canHom(S) c= ZeroDiv_Set(A); theorem :: RINGFRAC:33 not 0.A in S & A is domRing implies ker canHom(S) = {0.A} & canHom(S) is one-to-one; begin ::Localization in terms of Prime Ideal reserve p for Element of Spectrum A; definition let A,p; func Loc(A,p) -> Subset of A equals :: RINGFRAC:def 20 [#]A \ p; end; registration let A, p; cluster Loc(A,p) -> non empty; cluster Loc(A,p) -> multiplicatively-closed; cluster Loc(A,p) -> without_zero; end; definition let A,p; func A~p -> Ring equals :: RINGFRAC:def 21 (Loc(A,p))~A; end; registration let A,p; cluster A~p -> non degenerated; cluster A~p -> commutative; end; definition let A,p; func Loc-Ideal(p) -> Subset of [#](A~p) equals :: RINGFRAC:def 22 {y where y is Element of A~p : ex a be Element of Frac(Loc(A,p)) st a in [:p,Loc(A,p):] & y = Class(EqRel(Loc(A,p)),a) }; end; registration let A,p; cluster Loc-Ideal(p) -> non empty; end; reserve a,m,n for Element of A~p; theorem :: RINGFRAC:34 Loc-Ideal(p) is proper Ideal of A~p; theorem :: RINGFRAC:35 for x be object holds x in [#](A~p) \ Loc-Ideal(p) implies x is Unit of A~p; theorem :: RINGFRAC:36 A~p is local & Loc-Ideal(p) is maximal Ideal of A~p; begin :: Universal Property of Ring of Fraction :::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: for any f st f.S c= Unit_Set(B) !ex g:S~A->B st f = g*canHom :: f:A ------> B :: \ / :: canHom \ # / !ex Univ_Map(S,f): S~R ---> B :: \ / :: S~A ::::::::::::::::::::::::::::::::::::::::::::::::::::::: reserve f for Function of A,B; theorem :: RINGFRAC:37 for s be Element of S holds f is RingHomomorphism & f.:S c= Unit_Set(B) implies f.s is Unit of B; :: Prop 3.1 of [AM] p37. definition let A,B,S,f; assume f is RingHomomorphism & f.:S c= Unit_Set(B); func Univ_Map(S,f) -> Function of S~A, B means :: RINGFRAC:def 23 for x being object st x in the carrier of S~A holds ex a,s being Element of A st s in S & x = Class(EqRel(S),[a,s]) & it.x = (f.a)*((f.s)["]); end; theorem :: RINGFRAC:38 f is RingHomomorphism & f.:S c= Unit_Set(B) implies Univ_Map(S,f) is additive; theorem :: RINGFRAC:39 f is RingHomomorphism & f.:S c= Unit_Set(B) implies Univ_Map(S,f) is multiplicative; theorem :: RINGFRAC:40 f is RingHomomorphism & f.:S c= Unit_Set(B) implies Univ_Map(S,f) is unity-preserving; theorem :: RINGFRAC:41 f is RingHomomorphism & f.:S c= Unit_Set(B) implies Univ_Map(S,f) is RingHomomorphism; theorem :: RINGFRAC:42 f is RingHomomorphism & f.:S c= Unit_Set(B) implies f = ((Univ_Map(S,f))*(canHom(S))); begin :: The total-quotient ring and The Quotient Field of Integral Domain. :: Total Quotient Ring of R is S~R & S = {the all non zero-divisors} :: Exercise 9. i) from [AM] p.44 definition let A; func Total-Quotient-Ring(A) -> Ring equals :: RINGFRAC:def 24 (Non_ZeroDiv_Set(A))~A; end; registration let A; cluster Total-Quotient-Ring(A) -> non degenerated; end; reserve x for object; ::Prop1.2 i)<-> ii)[AM] p.3 theorem :: RINGFRAC:43 A is Field implies Ideals(A) = {{0.A}, the carrier of A}; reserve A for domRing; theorem :: RINGFRAC:44 Non_ZeroDiv_Set(A) = [#]A \ {0.A} & Non_ZeroDiv_Set(A) is without_zero non empty multiplicatively-closed Subset of A; theorem :: RINGFRAC:45 for a be Element of A holds a in Non_ZeroDiv_Set(A) iff a <> 0.A; :: Remark of [AM] p.37 theorem :: RINGFRAC:46 Total-Quotient-Ring(A) is Field; reserve x for Element of Q.A, y for object; theorem :: RINGFRAC:47 for A be domRing holds the_Field_of_Quotients(A) is_ringisomorph_to Total-Quotient-Ring(A);