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

end;
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 );

ex r1 being Element of R st

( r1 <> 0. R & r * r1 = 0. R );

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

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;

ex b_{1} being Element of A st b_{1} is zero_divisible

end;
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

proof end;

definition
end;

definition

let A be non degenerated commutative Ring;

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

end;
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 } ;

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

proof 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 } ;

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

for A being non degenerated commutative Ring holds Non_ZeroDiv_Set A = ([#] A) \ (ZeroDiv_Set A);

registration

let A be non degenerated commutative Ring;

coherence

not ZeroDiv_Set A is empty

not Non_ZeroDiv_Set A is empty

end;
coherence

not ZeroDiv_Set A is empty

proof end;

coherence not Non_ZeroDiv_Set A is empty

proof end;

::::::::::::::::::::::::::::::::::::::::::::::::::::

::: Definition of multiplicatively-closed set

::::::::::::::::::::::::::::::::::::::::::::::::::::

:: [AM] p36

::: Definition of multiplicatively-closed set

::::::::::::::::::::::::::::::::::::::::::::::::::::

:: [AM] p36

registration

let R be commutative Ring;

existence

ex b_{1} being non empty Subset of R st b_{1} is multiplicatively-closed

end;
existence

ex b

proof 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 );

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 b_{1} being non empty multiplicatively-closed Subset of A st b_{1} is without_zero

end;
existence

ex b

proof 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

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 ;

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

Non_ZeroDiv_Set A is multiplicatively-closed

end;
coherence

Non_ZeroDiv_Set A is multiplicatively-closed

proof end;

definition

let R be commutative Ring;

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

end;
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 } ;

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

proof 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 } ;

for R being commutative Ring holds Unit_Set R = { a where a is Element of R : a is Unit of R } ;

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

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 ;

existence

ex b_{1} being Element of R st b_{1} * r = 1. R
by A1, Th10;

uniqueness

for b_{1}, b_{2} being Element of R st b_{1} * r = 1. R & b_{2} * r = 1. R holds

b_{1} = b_{2}

end;
let r be Element of R;

assume A1: r in Unit_Set R ;

existence

ex b

uniqueness

for b

b

proof 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_{3} being Element of R holds

( b_{3} = recip r iff b_{3} * r = 1. R );

for R being commutative Ring

for r being Element of R st r in Unit_Set R holds

for b

( b

definition

let R be commutative Ring;

let u, v be Element of R;

u * (recip u) is Element of R ;

end;
let u, v be Element of R;

::: assume v in Unit_Set(R);

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

:: deftheorem defines [/] RINGFRAC:def 7 :

for R being commutative Ring

for u, v being Element of R holds u [/] v = u * (recip u);

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 ["]) )

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) ["])

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;

ex b_{1} being Subset of [: the carrier of R, the carrier of R:] st

for x being set holds

( x in b_{1} iff ex a, b being Element of R st

( x = [a,b] & b in S ) )

for b_{1}, b_{2} being Subset of [: the carrier of R, the carrier of R:] st ( for x being set holds

( x in b_{1} iff ex a, b being Element of R st

( x = [a,b] & b in S ) ) ) & ( for x being set holds

( x in b_{2} iff ex a, b being Element of R st

( x = [a,b] & b in S ) ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff ex a, b being Element of R st

( x = [a,b] & b in S ) );

ex b

for x being set holds

( x in b

( x = [a,b] & b in S ) )

proof end;

uniqueness for b

( x in b

( x = [a,b] & b in S ) ) ) & ( for x being set holds

( x in b

( x = [a,b] & b in S ) ) ) holds

b

proof 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_{3} being Subset of [: the carrier of R, the carrier of R:] holds

( b_{3} = Frac S iff for x being set holds

( x in b_{3} iff ex a, b being Element of R st

( x = [a,b] & b in S ) ) );

for R being commutative Ring

for S being non empty multiplicatively-closed Subset of R

for b

( b

( x in b

( 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:]

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;

coherence

not Frac S is empty

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

coherence

not Frac S is empty

proof 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;

ex b_{1} being Function of R,(Frac S) st

for o being object st o in the carrier of R holds

b_{1} . o = [o,(1. R)]

for b_{1}, b_{2} being Function of R,(Frac S) st ( for o being object st o in the carrier of R holds

b_{1} . o = [o,(1. R)] ) & ( for o being object st o in the carrier of R holds

b_{2} . o = [o,(1. R)] ) holds

b_{1} = b_{2}

end;
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 for o being object st o in the carrier of R holds

it . o = [o,(1. R)];

ex b

for o being object st o in the carrier of R holds

b

proof end;

uniqueness for b

b

b

b

proof 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_{3} being Function of R,(Frac S) holds

( b_{3} = frac1 S iff for o being object st o in the carrier of R holds

b_{3} . o = [o,(1. R)] );

for R being commutative Ring

for S being non empty multiplicatively-closed Subset of R

for b

( b

b

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;

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

for b_{1}, u, v being Element of Frac S st b_{1} = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] holds

b_{1} = [(((v `1) * (u `2)) + ((u `1) * (v `2))),((v `2) * (u `2))]
;

end;
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))];

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

proof end;

commutativity for b

b

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

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;

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

for b_{1}, u, v being Element of Frac S st b_{1} = [((u `1) * (v `1)),((u `2) * (v `2))] holds

b_{1} = [((v `1) * (u `1)),((v `2) * (u `2))]
;

end;
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))];

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

proof end;

commutativity for b

b

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

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;

coherence

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

coherence

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

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

let x, y be Element of Frac S;

coherence

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

coherence

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

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

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

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)

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)

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;

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

let x, y be Element of Frac S;

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

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

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

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

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

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;

ex b_{1} being Equivalence_Relation of (Frac S) st

for u, v being Element of Frac S holds

( [u,v] in b_{1} iff u,v Fr_Eq S )

for b_{1}, b_{2} being Equivalence_Relation of (Frac S) st ( for u, v being Element of Frac S holds

( [u,v] in b_{1} iff u,v Fr_Eq S ) ) & ( for u, v being Element of Frac S holds

( [u,v] in b_{2} iff u,v Fr_Eq S ) ) holds

b_{1} = b_{2}

end;
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 for u, v being Element of Frac S holds

( [u,v] in it iff u,v Fr_Eq S );

ex b

for u, v being Element of Frac S holds

( [u,v] in b

proof end;

uniqueness for b

( [u,v] in b

( [u,v] in b

b

proof 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_{3} being Equivalence_Relation of (Frac S) holds

( b_{3} = EqRel S iff for u, v being Element of Frac S holds

( [u,v] in b_{3} iff u,v Fr_Eq S ) );

for R being commutative Ring

for S being non empty multiplicatively-closed Subset of R

for b

( b

( [u,v] in b

:::registration

::: let R,S;

::: cluster EqRel(S) -> non empty total symmetric transitive;

::: coherence;

:::end;

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

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 )

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

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

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

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;

coherence

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

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

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

coherence

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

proof end;

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

proof 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)];

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)];

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

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;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = Class (EqRel S) & 1. b_{1} = Class ((EqRel S),(1. (R,S))) & 0. b_{1} = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b_{1} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b_{1} . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b_{1} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b_{1} . (x,y) = Class ((EqRel S),(a * b)) ) ) )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = Class (EqRel S) & 1. b_{1} = Class ((EqRel S),(1. (R,S))) & 0. b_{1} = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b_{1} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b_{1} . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b_{1} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b_{1} . (x,y) = Class ((EqRel S),(a * b)) ) ) & the carrier of b_{2} = Class (EqRel S) & 1. b_{2} = Class ((EqRel S),(1. (R,S))) & 0. b_{2} = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b_{2} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b_{2} . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b_{2} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b_{2} . (x,y) = Class ((EqRel S),(a * b)) ) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) ) );

ex b

( the carrier of b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b

proof end;

uniqueness for b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b

b

proof 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_{3} being strict doubleLoopStr holds

( b_{3} = FracRing S iff ( the carrier of b_{3} = Class (EqRel S) & 1. b_{3} = Class ((EqRel S),(1. (R,S))) & 0. b_{3} = Class ((EqRel S),(0. (R,S))) & ( for x, y being Element of b_{3} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b_{3} . (x,y) = Class ((EqRel S),(a + b)) ) ) & ( for x, y being Element of b_{3} ex a, b being Element of Frac S st

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b_{3} . (x,y) = Class ((EqRel S),(a * b)) ) ) ) );

for R being commutative Ring

for S being non empty multiplicatively-closed Subset of R

for b

( b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the addF of b

( x = Class ((EqRel S),a) & y = Class ((EqRel S),b) & the multF of b

notation

let R be commutative Ring;

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

synonym S ~ R for FracRing S;

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

synonym S ~ R for FracRing S;

registration

let R be commutative Ring;

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

coherence

not S ~ R is empty

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

coherence

not S ~ R is empty

proof 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 )

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)

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))

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

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))

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

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;

( 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;
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;

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]) )

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;

ex b_{1} being Function of A,(S ~ A) st

for o being object st o in the carrier of A holds

b_{1} . o = Class ((EqRel S),((frac1 S) . o))

for b_{1}, b_{2} being Function of A,(S ~ A) st ( for o being object st o in the carrier of A holds

b_{1} . o = Class ((EqRel S),((frac1 S) . o)) ) & ( for o being object st o in the carrier of A holds

b_{2} . o = Class ((EqRel S),((frac1 S) . o)) ) holds

b_{1} = b_{2}

end;
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 for o being object st o in the carrier of A holds

it . o = Class ((EqRel S),((frac1 S) . o));

ex b

for o being object st o in the carrier of A holds

b

proof end;

uniqueness for b

b

b

b

proof 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_{3} being Function of A,(S ~ A) holds

( b_{3} = canHom S iff for o being object st o in the carrier of A holds

b_{3} . o = Class ((EqRel S),((frac1 S) . o)) );

for A being non degenerated commutative Ring

for S being non empty multiplicatively-closed without_zero Subset of A

for b

( b

b

registration

let A be non degenerated commutative Ring;

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

coherence

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

end;
let S be non empty multiplicatively-closed without_zero Subset of A;

coherence

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

proof 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)

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

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 )

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;

coherence

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

end;
let p be Element of Spectrum A;

coherence

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

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

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;

coherence

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

coherence

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

coherence

Loc (A,p) is without_zero

end;
let p be Element of Spectrum A;

coherence

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

coherence

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

coherence

Loc (A,p) is without_zero

proof end;

definition

let A be non degenerated commutative Ring;

let p be Element of Spectrum A;

correctness

coherence

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

;

end;
let p be Element of Spectrum A;

correctness

coherence

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

;

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

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;

coherence

not A ~ p is degenerated

A ~ p is commutative ;

end;
let p be Element of Spectrum A;

coherence

not A ~ p is degenerated

proof end;

coherence A ~ p is commutative ;

definition

let A be non degenerated commutative Ring;

let p be Element of Spectrum A;

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

end;
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) ) } ;

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

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

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;

coherence

not Loc-Ideal p is empty

end;
let p be Element of Spectrum A;

coherence

not Loc-Ideal p is empty

proof 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)

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)

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) )

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

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

ex b_{1} 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_{1} . x = (f . a) * ((f . s) ["]) )

for b_{1}, b_{2} 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_{1} . 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_{2} . x = (f . a) * ((f . s) ["]) ) ) holds

b_{1} = b_{2}

end;
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 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) ["]) );

ex b

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

proof end;

uniqueness for b

ex a, s being Element of A st

( s in S & x = Class ((EqRel S),[a,s]) & b

ex a, s being Element of A st

( s in S & x = Class ((EqRel S),[a,s]) & b

b

proof 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_{5} being Function of (S ~ A),B holds

( b_{5} = 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_{5} . x = (f . a) * ((f . s) ["]) ) );

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

( b

ex a, s being Element of A st

( s in S & x = Class ((EqRel S),[a,s]) & b

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

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

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

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;

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)

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

:: Exercise 9. i) from [AM] p.44

definition
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;

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;

coherence

not Total-Quotient-Ring A is degenerated

end;
coherence

not Total-Quotient-Ring A is degenerated

proof 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}

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 )

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

proof end;

:: Remark of [AM] p.37