:: {R}ings of {F}ractions and {L}ocalization
:: by Yasushige Watase
::
:: 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;
existence
ex b1 being Element of A st b1 is zero_divisible
proof end;
end;

definition 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) \ ();
coherence
([#] 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) \ ();

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 b1 being non empty Subset of R st b1 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;
existence
ex b1 being non empty multiplicatively-closed Subset of A st b1 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;
coherence
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 b1 being Element of R st b1 * r = 1. R
by ;
uniqueness
for b1, b2 being Element of R st b1 * r = 1. R & b2 * r = 1. R holds
b1 = b2
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 b3 being Element of R holds
( b3 = recip r iff b3 * 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 * ();
coherence
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 * ();

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 b1 being Subset of [: the carrier of R, the carrier of R:] st
for x being set holds
( x in b1 iff ex a, b being Element of R st
( x = [a,b] & b in S ) )
proof end;
uniqueness
for b1, b2 being Subset of [: the carrier of R, the carrier of R:] st ( for x being set holds
( x in b1 iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ) holds
b1 = b2
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 b3 being Subset of [: the carrier of R, the carrier of R:] holds
( b3 = Frac S iff for x being set holds
( x in b3 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 b1 being Function of R,(Frac S) st
for o being object st o in the carrier of R holds
b1 . o = [o,(1. R)]
proof end;
uniqueness
for b1, b2 being Function of R,(Frac S) st ( for o being object st o in the carrier of R holds
b1 . o = [o,(1. R)] ) & ( for o being object st o in the carrier of R holds
b2 . o = [o,(1. R)] ) holds
b1 = b2
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 b3 being Function of R,(Frac S) holds
( b3 = frac1 S iff for o being object st o in the carrier of R holds
b3 . 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 b1, u, v being Element of Frac S st b1 = [(((u 1) * (v 2)) + ((v 1) * (u 2))),((u 2) * (v 2))] holds
b1 = [(((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 b1, u, v being Element of Frac S st b1 = [((u 1) * (v 1)),((u 2) * (v 2))] holds
b1 = [((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
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
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 b1 being Equivalence_Relation of (Frac S) st
for u, v being Element of Frac S holds
( [u,v] in b1 iff u,v Fr_Eq S )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of (Frac S) st ( for u, v being Element of Frac S holds
( [u,v] in b1 iff u,v Fr_Eq S ) ) & ( for u, v being Element of Frac S holds
( [u,v] in b2 iff u,v Fr_Eq S ) ) holds
b1 = b2
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 b3 being Equivalence_Relation of (Frac S) holds
( b3 = EqRel S iff for u, v being Element of Frac S holds
( [u,v] in b3 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 ((),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 ((),x) = Class ((),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
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 () & 1. it = Class ((),(1. (R,S))) & 0. it = Class ((),(0. (R,S))) & ( for x, y being Element of it ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the addF of it . (x,y) = Class ((),(a + b)) ) ) & ( for x, y being Element of it ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the multF of it . (x,y) = Class ((),(a * b)) ) ) );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = Class () & 1. b1 = Class ((),(1. (R,S))) & 0. b1 = Class ((),(0. (R,S))) & ( for x, y being Element of b1 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the addF of b1 . (x,y) = Class ((),(a + b)) ) ) & ( for x, y being Element of b1 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the multF of b1 . (x,y) = Class ((),(a * b)) ) ) )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = Class () & 1. b1 = Class ((),(1. (R,S))) & 0. b1 = Class ((),(0. (R,S))) & ( for x, y being Element of b1 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the addF of b1 . (x,y) = Class ((),(a + b)) ) ) & ( for x, y being Element of b1 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the multF of b1 . (x,y) = Class ((),(a * b)) ) ) & the carrier of b2 = Class () & 1. b2 = Class ((),(1. (R,S))) & 0. b2 = Class ((),(0. (R,S))) & ( for x, y being Element of b2 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the addF of b2 . (x,y) = Class ((),(a + b)) ) ) & ( for x, y being Element of b2 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the multF of b2 . (x,y) = Class ((),(a * b)) ) ) holds
b1 = b2
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 b3 being strict doubleLoopStr holds
( b3 = FracRing S iff ( the carrier of b3 = Class () & 1. b3 = Class ((),(1. (R,S))) & 0. b3 = Class ((),(0. (R,S))) & ( for x, y being Element of b3 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the addF of b3 . (x,y) = Class ((),(a + b)) ) ) & ( for x, y being Element of b3 ex a, b being Element of Frac S st
( x = Class ((),a) & y = Class ((),b) & the multF of b3 . (x,y) = Class ((),(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 ((),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 ((),a) & y = Class ((),b) holds
x * y = Class ((),(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 ((),a) & y = Class ((),b) holds
x + y = Class ((),(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 ((() . r1),(() . r2)),() . (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 ((),(() . r1)) & y = Class ((),(() . r2)) holds
x + y = Class ((),(() . (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 ((() . r1),(() . r2)),() . (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 ((),(() . r1)) & y = Class ((),(() . r2)) holds
x * y = Class ((),(() . (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;
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 ;
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 ((),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 ((),a) = 1. (S ~ R)

proof end;

Lm43: for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R holds Class ((),(() . (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 ((),(() . 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 ((),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 ((),[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 ((),[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 ((),(() . o));
existence
ex b1 being Function of A,(S ~ A) st
for o being object st o in the carrier of A holds
b1 . o = Class ((),(() . o))
proof end;
uniqueness
for b1, b2 being Function of A,(S ~ A) st ( for o being object st o in the carrier of A holds
b1 . o = Class ((),(() . o)) ) & ( for o being object st o in the carrier of A holds
b2 . o = Class ((),(() . o)) ) holds
b1 = b2
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 b3 being Function of A,(S ~ A) holds
( b3 = canHom S iff for o being object st o in the carrier of A holds
b3 . o = Class ((),(() . o)) );

registration
let A be non degenerated commutative Ring;
let S be non empty multiplicatively-closed without_zero Subset of A;
coherence
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 () . (a - b) = (() . a) - (() . 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 () 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 () = {(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;
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)) \ () 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 ((),[a,s]) & it . x = (f . a) * ((f . s) ["]) );
existence
ex b1 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 ((),[a,s]) & b1 . x = (f . a) * ((f . s) ["]) )
proof end;
uniqueness
for b1, b2 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 ((),[a,s]) & b1 . 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 ((),[a,s]) & b2 . x = (f . a) * ((f . s) ["]) ) ) holds
b1 = b2
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 b5 being Function of (S ~ A),B holds
( b5 = 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 ((),[a,s]) & b5 . 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
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 ;

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)) * ()
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;
correctness
coherence
() ~ A is Ring
;
;
end;

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

registration
let A be non degenerated commutative Ring;
coherence
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
proof end;