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