:: {R}ings of {F}ractions and {L}ocalization
:: by Yasushige Watase
::
:: Received January 13, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

:: Zero-divisor. Unit [AM]p2-3

definition

let R be commutative Ring;
let r be Element of R;

attr r is zero_divisible means :Def1: :: RINGFRAC:def 1
ex r1 being Element of R st
( r1 <> 0. R & r * r1 = 0. R );

end;

:: deftheorem Def1 defines zero_divisible RINGFRAC:def 1 :
for R being commutative Ring
for r being Element of R holds
( r is zero_divisible iff ex r1 being Element of R st
( r1 <> 0. R & r * r1 = 0. R ) );

registration

let A be non degenerated commutative Ring;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable zero_divisible for Element of the carrier of A;

existence
ex b₁ being Element of A st b₁ is zero_divisible

proof end;

end;

definition

let A be non degenerated commutative Ring;
mode Zero_Divisor of A is zero_divisible Element of A;

end;

theorem Th1: :: RINGFRAC:1

for A being non degenerated commutative Ring holds 0. A is Zero_Divisor of A

proof end;

theorem Th2: :: RINGFRAC:2

for A being non degenerated commutative Ring holds 1. A is not Zero_Divisor of A

proof end;

definition

let A be non degenerated commutative Ring;

func ZeroDiv_Set A -> Subset of A equals :: RINGFRAC:def 2
{ a where a is Element of A : a is Zero_Divisor of A } ;

coherence
{ a where a is Element of A : a is Zero_Divisor of A } is Subset of A

proof end;

end;

:: deftheorem defines ZeroDiv_Set RINGFRAC:def 2 :
for A being non degenerated commutative Ring holds ZeroDiv_Set A = { a where a is Element of A : a is Zero_Divisor of A } ;

definition

let A be non degenerated commutative Ring;

func Non_ZeroDiv_Set A -> Subset of A equals :: RINGFRAC:def 3
([#] A) \ (ZeroDiv_Set A);

coherence
([#] A) \ (ZeroDiv_Set A) is Subset of A ;

end;

:: deftheorem defines Non_ZeroDiv_Set RINGFRAC:def 3 :
for A being non degenerated commutative Ring holds Non_ZeroDiv_Set A = ([#] A) \ (ZeroDiv_Set A);

registration

let A be non degenerated commutative Ring;

cluster ZeroDiv_Set A -> non empty ;

coherence
not ZeroDiv_Set A is empty

proof end;

cluster Non_ZeroDiv_Set A -> non empty ;

coherence
not Non_ZeroDiv_Set A is empty

proof end;

end;

theorem Th3: :: RINGFRAC:3

for A being non degenerated commutative Ring holds not 0. A in Non_ZeroDiv_Set A

proof end;

theorem Th4: :: RINGFRAC:4

for A being non degenerated commutative Ring st A is domRing holds
{(0. A)} = ZeroDiv_Set A

proof end;

::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Definition of multiplicatively-closed set
::::::::::::::::::::::::::::::::::::::::::::::::::::
:: [AM] p36

theorem Th5: :: RINGFRAC:5

for R being commutative Ring holds {(1. R)} is multiplicatively-closed

proof end;

registration

let R be commutative Ring;

cluster non empty multiplicatively-closed for Element of bool the carrier of R;

existence
ex b₁ being non empty Subset of R st b₁ is multiplicatively-closed

proof end;

end;

definition

let A be non degenerated commutative Ring;
let V be Subset of A;

attr V is without_zero means :: RINGFRAC:def 4
not 0. A in V;

end;

:: deftheorem defines without_zero RINGFRAC:def 4 :
for A being non degenerated commutative Ring
for V being Subset of A holds
( V is without_zero iff not 0. A in V );

registration

let A be non degenerated commutative Ring;

cluster non empty multiplicatively-closed without_zero for Element of bool the carrier of A;

existence
ex b₁ being non empty multiplicatively-closed Subset of A st b₁ is without_zero

proof end;

end;

Lm5: for A being non degenerated commutative Ring
for o being object st o in Spectrum A holds
o is prime Ideal of A

proof end;

::Example.1.1)of [AM] p38

theorem Th6: :: RINGFRAC:6

for A being non degenerated commutative Ring
for p being Element of Spectrum A holds ([#] A) \ p is multiplicatively-closed

proof end;

::Example.1.3)of [AM] p38

theorem :: RINGFRAC:7

for A being non degenerated commutative Ring
for a being Element of A
for J being proper Ideal of A holds multClSet (J,a) is multiplicatively-closed ;

registration

let A be non degenerated commutative Ring;

cluster Non_ZeroDiv_Set A -> multiplicatively-closed ;

coherence
Non_ZeroDiv_Set A is multiplicatively-closed

proof end;

end;

definition

let R be commutative Ring;

func Unit_Set R -> Subset of R equals :: RINGFRAC:def 5
{ a where a is Element of R : a is Unit of R } ;

coherence
{ a where a is Element of R : a is Unit of R } is Subset of R

proof end;

end;

:: deftheorem defines Unit_Set RINGFRAC:def 5 :
for R being commutative Ring holds Unit_Set R = { a where a is Element of R : a is Unit of R } ;

registration

let R be commutative Ring;

cluster Unit_Set R -> non empty ;

coherence
not Unit_Set R is empty

proof end;

end;

Th9: for R being commutative Ring
for r1 being Element of R st r1 in Unit_Set R holds
ex r2 being Element of R st r1 * r2 = 1. R

proof end;

Th10: for R being commutative Ring
for r1 being Element of R st r1 in Unit_Set R holds
ex r2 being Element of R st r2 * r1 = 1. R

proof end;

theorem Th11: :: RINGFRAC:8

for R being commutative Ring
for r1 being Element of R st r1 in Unit_Set R holds
r1 is right_mult-cancelable

proof end;

definition

let R be commutative Ring;
let r be Element of R;
assume A1: r in Unit_Set R ;

func recip r -> Element of R means :Def2: :: RINGFRAC:def 6
it * r = 1. R;

existence
ex b₁ being Element of R st b₁ * r = 1. R by A1, Th10;
uniqueness
for b₁, b₂ being Element of R st b₁ * r = 1. R & b₂ * r = 1. R holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines recip RINGFRAC:def 6 :
for R being commutative Ring
for r being Element of R st r in Unit_Set R holds
for b₃ being Element of R holds
( b₃ = recip r iff b₃ * r = 1. R );

notation

let R be commutative Ring;
let r be Element of R;
synonym r ["] for recip r;

end;

definition

let R be commutative Ring;
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);

coherence
u * (recip u) is Element of R ;

end;

:: deftheorem defines [/] RINGFRAC:def 7 :
for R being commutative Ring
for u, v being Element of R holds u [/] v = u * (recip u);

theorem Th12: :: RINGFRAC:9

for R, R1 being commutative Ring
for f being Function of R,R1
for u being Unit of R
for v being Element of R st f is RingHomomorphism holds
( f . u is Unit of R1 & (f . u) ["] = f . (u ["]) )

proof end;

theorem :: RINGFRAC:10

for R, R1 being commutative Ring
for f being Function of R,R1
for u being Unit of R
for v being Element of R st f is RingHomomorphism holds
f . (v * (u ["])) = (f . v) * ((f . u) ["])

proof end;

:: Definition of Pairs

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

func Frac S -> Subset of [: the carrier of R, the carrier of R:] means :Def3: :: 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 ) );

existence
ex b₁ being Subset of [: the carrier of R, the carrier of R:] st
for x being set holds
( x in b₁ iff ex a, b being Element of R st
( x = [a,b] & b in S ) )

proof end;

uniqueness
for b₁, b₂ being Subset of [: the carrier of R, the carrier of R:] st ( for x being set holds
( x in b₁ iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ) & ( for x being set holds
( x in b₂ iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Frac RINGFRAC:def 8 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being Subset of [: the carrier of R, the carrier of R:] holds
( b₃ = Frac S iff for x being set holds
( x in b₃ iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) );

theorem Th15: :: RINGFRAC:11

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds Frac S = [:([#] R),S:]

proof end;

registration

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

cluster Frac S -> non empty ;

coherence
not Frac S is empty

proof end;

end;

Lm16: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x being object st x in the carrier of R holds
[x,(1. R)] in Frac S

proof end;

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

func frac1 S -> Function of R,(Frac S) means :Def4: :: RINGFRAC:def 9
for o being object st o in the carrier of R holds
it . o = [o,(1. R)];

existence
ex b₁ being Function of R,(Frac S) st
for o being object st o in the carrier of R holds
b₁ . o = [o,(1. R)]

proof end;

uniqueness
for b₁, b₂ being Function of R,(Frac S) st ( for o being object st o in the carrier of R holds
b₁ . o = [o,(1. R)] ) & ( for o being object st o in the carrier of R holds
b₂ . o = [o,(1. R)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines frac1 RINGFRAC:def 9 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being Function of R,(Frac S) holds
( b₃ = frac1 S iff for o being object st o in the carrier of R holds
b₃ . o = [o,(1. R)] );

Lm17: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x being Element of Frac S holds
( x `1 in R & x `2 in S )

proof end;

Th18: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for u being Element of Frac S holds u `2 in S

proof end;

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;
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))];

coherence
[(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Frac S

proof end;

commutativity
for b₁, u, v being Element of Frac S st b₁ = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] holds
b₁ = [(((v `1) * (u `2)) + ((u `1) * (v `2))),((v `2) * (u `2))] ;

end;

:: deftheorem defines Fracadd RINGFRAC:def 10 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for u, v being Element of Frac S holds Fracadd (u,v) = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))];

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;
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))];

coherence
[((u `1) * (v `1)),((u `2) * (v `2))] is Element of Frac S

proof end;

commutativity
for b₁, u, v being Element of Frac S st b₁ = [((u `1) * (v `1)),((u `2) * (v `2))] holds
b₁ = [((v `1) * (u `1)),((v `2) * (u `2))] ;

end;

:: deftheorem defines Fracmult RINGFRAC:def 11 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for u, v being Element of Frac S holds Fracmult (u,v) = [((u `1) * (v `1)),((u `2) * (v `2))];

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;
let x, y be Element of Frac S;

func x + y -> Element of Frac S equals :: RINGFRAC:def 12
Fracadd (x,y);

coherence
Fracadd (x,y) is Element of Frac S ;

func x * y -> Element of Frac S equals :: RINGFRAC:def 13
Fracmult (x,y);

coherence
Fracmult (x,y) is Element of Frac S ;

end;

:: deftheorem defines + RINGFRAC:def 12 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S holds x + y = Fracadd (x,y);

:: deftheorem defines * RINGFRAC:def 13 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S holds x * y = Fracmult (x,y);

theorem Th19: :: RINGFRAC:12

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S holds Fracadd (x,(Fracadd (y,z))) = Fracadd ((Fracadd (x,y)),z)

proof end;

theorem Th20: :: RINGFRAC:13

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S holds Fracmult (x,(Fracmult (y,z))) = Fracmult ((Fracmult (x,y)),z)

proof end;

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;
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;

:: deftheorem defines Fr_Eq RINGFRAC:def 14 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S holds
( x,y Fr_Eq S iff ex s1 being Element of R st
( s1 in S & (((x `1) * (y `2)) - ((y `1) * (x `2))) * s1 = 0. R ) );

theorem :: RINGFRAC:14

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S st 0. R in S holds
x,y Fr_Eq S

proof end;

theorem Th22: :: RINGFRAC:15

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x being Element of Frac S holds x,x Fr_Eq S

proof end;

theorem Th23: :: RINGFRAC:16

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S st x,y Fr_Eq S holds
y,x Fr_Eq S

proof end;

theorem Th24: :: RINGFRAC:17

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S st x,y Fr_Eq S & y,z Fr_Eq S holds
x,z Fr_Eq S

proof end;

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

func EqRel S -> Equivalence_Relation of (Frac S) means :Def5: :: RINGFRAC:def 15
for u, v being Element of Frac S holds
( [u,v] in it iff u,v Fr_Eq S );

existence
ex b₁ being Equivalence_Relation of (Frac S) st
for u, v being Element of Frac S holds
( [u,v] in b₁ iff u,v Fr_Eq S )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of (Frac S) st ( for u, v being Element of Frac S holds
( [u,v] in b₁ iff u,v Fr_Eq S ) ) & ( for u, v being Element of Frac S holds
( [u,v] in b₂ iff u,v Fr_Eq S ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines EqRel RINGFRAC:def 15 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being Equivalence_Relation of (Frac S) holds
( b₃ = EqRel S iff for u, v being Element of Frac S holds
( [u,v] in b₃ iff u,v Fr_Eq S ) );

:::registration
::: let R,S;
::: cluster EqRel(S) -> non empty total symmetric transitive;
::: coherence;
:::end;

theorem Th25: :: RINGFRAC:18

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S holds
( x in Class ((EqRel S),y) iff x,y Fr_Eq S )

proof end;

theorem Th26: :: RINGFRAC:19

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of Frac S holds
( Class ((EqRel S),x) = Class ((EqRel S),y) iff x,y Fr_Eq S )

proof end;

theorem Th27: :: RINGFRAC:20

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for u, v, x, y being Element of Frac S st x,u Fr_Eq S & y,v Fr_Eq S holds
Fracmult (x,y), Fracmult (u,v) Fr_Eq S

proof end;

theorem Th28: :: RINGFRAC:21

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for u, v, x, y being Element of Frac S st x,u Fr_Eq S & y,v Fr_Eq S holds
Fracadd (x,y), Fracadd (u,v) Fr_Eq S

proof end;

theorem Th29: :: RINGFRAC:22

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S holds (x + y) * z,(x * z) + (y * z) Fr_Eq S

proof end;

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

func 0. (R,S) -> Element of Frac S equals :: RINGFRAC:def 16
[(0. R),(1. R)];

coherence
[(0. R),(1. R)] is Element of Frac S

proof end;

func 1. (R,S) -> Element of Frac S equals :: RINGFRAC:def 17
[(1. R),(1. R)];

coherence
[(1. R),(1. R)] is Element of Frac S

proof end;

end;

:: deftheorem defines 0. RINGFRAC:def 16 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds 0. (R,S) = [(0. R),(1. R)];

:: deftheorem defines 1. RINGFRAC:def 17 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds 1. (R,S) = [(1. R),(1. R)];

theorem Th30: :: RINGFRAC:23

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x being Element of Frac S
for s being Element of S st x = [s,s] holds
x, 1. (R,S) Fr_Eq S

proof end;

definition

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

func FracRing S -> strict doubleLoopStr means :Def6: :: 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)) ) ) );

existence
ex b₁ being strict doubleLoopStr st
( the carrier of b₁ = Class (EqRel S) & 1. b₁ = Class ((EqRel S),(1. (R,S))) & 0. b₁ = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b₁ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b₁ . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b₁ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b₁ . (x,y) = Class ((EqRel S),(a * b)) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict doubleLoopStr st the carrier of b₁ = Class (EqRel S) & 1. b₁ = Class ((EqRel S),(1. (R,S))) & 0. b₁ = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b₁ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b₁ . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b₁ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b₁ . (x,y) = Class ((EqRel S),(a * b)) ) ) & the carrier of b₂ = Class (EqRel S) & 1. b₂ = Class ((EqRel S),(1. (R,S))) & 0. b₂ = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b₂ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b₂ . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b₂ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b₂ . (x,y) = Class ((EqRel S),(a * b)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines FracRing RINGFRAC:def 18 :
for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for b₃ being strict doubleLoopStr holds
( b₃ = FracRing S iff ( the carrier of b₃ = Class (EqRel S) & 1. b₃ = Class ((EqRel S),(1. (R,S))) & 0. b₃ = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b₃ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b₃ . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b₃ ex a, b being Element of Frac S st
( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b₃ . (x,y) = Class ((EqRel S),(a * b)) ) ) ) );

notation

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;
synonym S ~ R for FracRing S;

end;

registration

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

cluster FracRing S -> non empty strict ;

coherence
not S ~ R is empty

proof end;

end;

:: Example 2) of [AM] p38

theorem Th31: :: RINGFRAC:24

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds
( 0. R in S iff S ~ R is degenerated )

proof end;

theorem Th32: :: RINGFRAC:25

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x being Element of (S ~ R) ex a being Element of Frac S st x = Class ((EqRel S),a)

proof end;

theorem Th33: :: RINGFRAC:26

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for a, b being Element of Frac S
for x, y being Element of (S ~ R) st x = Class ((EqRel S),a) & y = Class ((EqRel S),b) holds
x * y = Class ((EqRel S),(a * b))

proof end;

theorem Th34: :: RINGFRAC:27

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of (S ~ R) holds x * y = y * x

proof end;

theorem Th35: :: RINGFRAC:28

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for a, b being Element of Frac S
for x, y being Element of (S ~ R) st x = Class ((EqRel S),a) & y = Class ((EqRel S),b) holds
x + y = Class ((EqRel S),(a + b))

proof end;

Lm36: for R being commutative Ring
for r1, r2 being Element of R
for S being non empty multiplicatively-closed Subset of R holds Fracadd (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 + r2) Fr_Eq S

proof end;

Lm37: for R being commutative Ring
for r1, r2 being Element of R
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of (S ~ R) st x = Class ((EqRel S),((frac1 S) . r1)) & y = Class ((EqRel S),((frac1 S) . r2)) holds
x + y = Class ((EqRel S),((frac1 S) . (r1 + r2)))

proof end;

Lm38: for R being commutative Ring
for r1, r2 being Element of R
for S being non empty multiplicatively-closed Subset of R holds Fracmult (((frac1 S) . r1),((frac1 S) . r2)),(frac1 S) . (r1 * r2) Fr_Eq S

proof end;

Lm39: for R being commutative Ring
for r1, r2 being Element of R
for S being non empty multiplicatively-closed Subset of R
for x, y being Element of (S ~ R) st x = Class ((EqRel S),((frac1 S) . r1)) & y = Class ((EqRel S),((frac1 S) . r2)) holds
x * y = Class ((EqRel S),((frac1 S) . (r1 * r2)))

proof end;

theorem Th40: :: RINGFRAC:29

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds S ~ R is Ring

proof end;

registration

let R be commutative Ring;
let S be non empty multiplicatively-closed Subset of R;

cluster FracRing S -> right_complementable strict well-unital distributive Abelian add-associative right_zeroed associative commutative ;

coherence
( S ~ R is commutative & S ~ R is Abelian & S ~ R is add-associative & S ~ R is right_zeroed & S ~ R is right_complementable & S ~ R is associative & S ~ R is well-unital & S ~ R is distributive ) by Th34, Th40;

end;

Lm41: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for a being Element of Frac S holds Class ((EqRel S),a) is Element of (S ~ R)

proof end;

Lm42: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for a being Element of Frac S st a `1 = a `2 holds
Class ((EqRel S),a) = 1. (S ~ R)

proof end;

Lm43: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds Class ((EqRel S),((frac1 S) . (1. R))) = 1. (S ~ R)

proof end;

Lm44: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for o being object st o in the carrier of R holds
Class ((EqRel S),((frac1 S) . o)) in the carrier of (S ~ R)

proof end;

Lm45: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for a being Element of Frac S st a `1 in S holds
Class ((EqRel S),a) is Unit of (S ~ R)

proof end;

Lm46: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for s being Element of S holds Class ((EqRel S),[s,(1. R)]) is Unit of (S ~ R)

proof end;

theorem Th46: :: RINGFRAC:30

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for z being Element of (S ~ R) ex r1, r2 being Element of R st
( r2 in S & z = Class ((EqRel S),[r1,r2]) )

proof end;

definition

let A be non degenerated commutative Ring;
let S be non empty multiplicatively-closed without_zero Subset of A;

func canHom S -> Function of A,(S ~ A) means :Def7: :: RINGFRAC:def 19
for o being object st o in the carrier of A holds
it . o = Class ((EqRel S),((frac1 S) . o));

existence
ex b₁ being Function of A,(S ~ A) st
for o being object st o in the carrier of A holds
b₁ . o = Class ((EqRel S),((frac1 S) . o))

proof end;

uniqueness
for b₁, b₂ being Function of A,(S ~ A) st ( for o being object st o in the carrier of A holds
b₁ . o = Class ((EqRel S),((frac1 S) . o)) ) & ( for o being object st o in the carrier of A holds
b₂ . o = Class ((EqRel S),((frac1 S) . o)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines canHom RINGFRAC:def 19 :
for A being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for b₃ being Function of A,(S ~ A) holds
( b₃ = canHom S iff for o being object st o in the carrier of A holds
b₃ . o = Class ((EqRel S),((frac1 S) . o)) );

registration

let A be non degenerated commutative Ring;
let S be non empty multiplicatively-closed without_zero Subset of A;

cluster canHom S -> additive unity-preserving multiplicative ;

coherence
( canHom S is additive & canHom S is multiplicative & canHom S is unity-preserving )

proof end;

end;

theorem Lm49: :: RINGFRAC:31

for A being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for a, b being Element of A holds (canHom S) . (a - b) = ((canHom S) . a) - ((canHom S) . b)

proof end;

theorem Lm50: :: RINGFRAC:32

for A being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A st not 0. A in S holds
ker (canHom S) c= ZeroDiv_Set A

proof end;

theorem :: RINGFRAC:33

for A being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A st not 0. A in S & A is domRing holds
( ker (canHom S) = {(0. A)} & canHom S is one-to-one )

proof end;

definition

let A be non degenerated commutative Ring;
let p be Element of Spectrum A;

func Loc (A,p) -> Subset of A equals :: RINGFRAC:def 20
([#] A) \ p;

coherence
([#] A) \ p is Subset of A ;

end;

:: deftheorem defines Loc RINGFRAC:def 20 :
for A being non degenerated commutative Ring
for p being Element of Spectrum A holds Loc (A,p) = ([#] A) \ p;

Th52: for A being non degenerated commutative Ring
for p being Element of Spectrum A holds 1. A in Loc (A,p)

proof end;

registration

let A be non degenerated commutative Ring;
let p be Element of Spectrum A;

cluster Loc (A,p) -> non empty ;

coherence
not Loc (A,p) is empty by Th52;

cluster Loc (A,p) -> multiplicatively-closed ;

coherence
Loc (A,p) is multiplicatively-closed by Th6;

cluster Loc (A,p) -> without_zero ;

coherence
Loc (A,p) is without_zero

proof end;

end;

definition

let A be non degenerated commutative Ring;
let p be Element of Spectrum A;

func A ~ p -> Ring equals :: RINGFRAC:def 21
(Loc (A,p)) ~ A;

correctness
coherence
(Loc (A,p)) ~ A is Ring;
;

end;

:: deftheorem defines ~ RINGFRAC:def 21 :
for A being non degenerated commutative Ring
for p being Element of Spectrum A holds A ~ p = (Loc (A,p)) ~ A;

registration

let A be non degenerated commutative Ring;
let p be Element of Spectrum A;

cluster A ~ p -> non degenerated ;

coherence
not A ~ p is degenerated

proof end;

cluster A ~ p -> commutative ;

coherence
A ~ p is commutative ;

end;

definition

let A be non degenerated commutative Ring;
let p be Element of Spectrum A;

func Loc-Ideal p -> Subset of ([#] (A ~ p)) equals :: RINGFRAC:def 22
{ y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } ;

coherence
{ y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } is Subset of ([#] (A ~ p))

proof end;

end;

:: deftheorem defines Loc-Ideal RINGFRAC:def 22 :
for A being non degenerated commutative Ring
for p being Element of Spectrum A holds Loc-Ideal p = { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } ;

registration

let A be non degenerated commutative Ring;
let p be Element of Spectrum A;

cluster Loc-Ideal p -> non empty ;

coherence
not Loc-Ideal p is empty

proof end;

end;

theorem Th53: :: RINGFRAC:34

for A being non degenerated commutative Ring
for p being Element of Spectrum A holds Loc-Ideal p is proper Ideal of (A ~ p)

proof end;

theorem Th54: :: RINGFRAC:35

for A being non degenerated commutative Ring
for p being Element of Spectrum A
for x being object st x in ([#] (A ~ p)) \ (Loc-Ideal p) holds
x is Unit of (A ~ p)

proof end;

theorem :: RINGFRAC:36

for A being non degenerated commutative Ring
for p being Element of Spectrum A holds
( A ~ p is local & Loc-Ideal p is maximal Ideal of (A ~ p) )

proof end;

theorem Th56: :: RINGFRAC:37

for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B
for s being Element of S st f is RingHomomorphism & f .: S c= Unit_Set B holds
f . s is Unit of B

proof end;

:: Prop 3.1 of [AM] p37.

definition

let A, B be non degenerated commutative Ring;
let S be non empty multiplicatively-closed without_zero Subset of A;
let f be Function of A,B;
assume A1: ( f is RingHomomorphism & f .: S c= Unit_Set B ) ;

func Univ_Map (S,f) -> Function of (S ~ A),B means :Def8: :: 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) ["]) );

existence
ex b₁ being Function of (S ~ A),B st
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]) & b₁ . x = (f . a) * ((f . s) ["]) )

proof end;

uniqueness
for b₁, b₂ being Function of (S ~ A),B st ( 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]) & b₁ . x = (f . a) * ((f . s) ["]) ) ) & ( 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]) & b₂ . x = (f . a) * ((f . s) ["]) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Univ_Map RINGFRAC:def 23 :
for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
for b₅ being Function of (S ~ A),B holds
( b₅ = Univ_Map (S,f) iff 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]) & b₅ . x = (f . a) * ((f . s) ["]) ) );

theorem Th57: :: RINGFRAC:38

for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
Univ_Map (S,f) is additive

proof end;

theorem Th58: :: RINGFRAC:39

for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
Univ_Map (S,f) is multiplicative

proof end;

theorem Th59: :: RINGFRAC:40

for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
Univ_Map (S,f) is unity-preserving

proof end;

theorem :: RINGFRAC:41

for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
Univ_Map (S,f) is RingHomomorphism by Th57, Th58, Th59;

theorem Th61: :: RINGFRAC:42

for A, B being non degenerated commutative Ring
for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
f = (Univ_Map (S,f)) * (canHom S)

proof end;

:: Total Quotient Ring of R is S~R & S = {the all non zero-divisors}
:: Exercise 9. i) from [AM] p.44

definition

let A be non degenerated commutative Ring;

func Total-Quotient-Ring A -> Ring equals :: RINGFRAC:def 24
(Non_ZeroDiv_Set A) ~ A;

correctness
coherence
(Non_ZeroDiv_Set A) ~ A is Ring;
;

end;

:: deftheorem defines Total-Quotient-Ring RINGFRAC:def 24 :
for A being non degenerated commutative Ring holds Total-Quotient-Ring A = (Non_ZeroDiv_Set A) ~ A;

registration

let A be non degenerated commutative Ring;

cluster Total-Quotient-Ring A -> non degenerated ;

coherence
not Total-Quotient-Ring A is degenerated

proof end;

end;

::Prop1.2 i)<-> ii)[AM] p.3

theorem :: RINGFRAC:43

for A being non degenerated commutative Ring st A is Field holds
Ideals A = {{(0. A)}, the carrier of A}

proof end;

theorem Lm63: :: RINGFRAC:44

for A being domRing holds
( Non_ZeroDiv_Set A = ([#] A) \ {(0. A)} & Non_ZeroDiv_Set A is non empty multiplicatively-closed without_zero Subset of A )

proof end;

theorem Th64: :: RINGFRAC:45

for A being domRing
for a being Element of A holds
( a in Non_ZeroDiv_Set A iff a <> 0. A )

proof end;

:: Remark of [AM] p.37

theorem Th65: :: RINGFRAC:46

for A being domRing holds Total-Quotient-Ring A is Field

proof end;

theorem :: RINGFRAC:47

for A being domRing holds the_Field_of_Quotients A is_ringisomorph_to Total-Quotient-Ring A

proof end;