:: by Micha{\l} Muzalewski

::

:: Received December 5, 1991

:: Copyright (c) 1991-2016 Association of Mizar Users

definition

let G, H be non empty doubleLoopStr ;

let IT be Function of G,H;

end;
let IT be Function of G,H;

attr IT is linear means :: RINGCAT1:def 1

( IT is additive & IT is multiplicative & IT is unity-preserving );

( IT is additive & IT is multiplicative & IT is unity-preserving );

:: deftheorem defines linear RINGCAT1:def 1 :

for G, H being non empty doubleLoopStr

for IT being Function of G,H holds

( IT is linear iff ( IT is additive & IT is multiplicative & IT is unity-preserving ) );

for G, H being non empty doubleLoopStr

for IT being Function of G,H holds

( IT is linear iff ( IT is additive & IT is multiplicative & IT is unity-preserving ) );

registration

let G, H be non empty doubleLoopStr ;

for b_{1} being Function of G,H st b_{1} is linear holds

( b_{1} is additive & b_{1} is multiplicative & b_{1} is unity-preserving )
;

for b_{1} being Function of G,H st b_{1} is additive & b_{1} is multiplicative & b_{1} is unity-preserving holds

b_{1} is linear
;

end;
cluster V6() V31( the carrier of G, the carrier of H) linear -> unity-preserving multiplicative additive for Element of bool [: the carrier of G, the carrier of H:];

coherence for b

( b

cluster V6() V31( the carrier of G, the carrier of H) unity-preserving multiplicative additive -> linear for Element of bool [: the carrier of G, the carrier of H:];

coherence for b

b

theorem Th1: :: RINGCAT1:1

for G1, G2, G3 being non empty doubleLoopStr

for f being Function of G1,G2

for g being Function of G2,G3 st f is linear & g is linear holds

g * f is linear

for f being Function of G1,G2

for g being Function of G2,G3 st f is linear & g is linear holds

g * f is linear

proof end;

::

:: 1b. Morphisms of rings

::

:: 1b. Morphisms of rings

::

definition

attr c_{1} is strict ;

struct RingMorphismStr -> ;

aggr RingMorphismStr(# Dom, Cod, Fun #) -> RingMorphismStr ;

sel Dom c_{1} -> Ring;

sel Cod c_{1} -> Ring;

sel Fun c_{1} -> Function of the Dom of c_{1}, the Cod of c_{1};

end;
struct RingMorphismStr -> ;

aggr RingMorphismStr(# Dom, Cod, Fun #) -> RingMorphismStr ;

sel Dom c

sel Cod c

sel Fun c

definition

let f be RingMorphismStr ;

coherence

the Dom of f is Ring ;

coherence

the Cod of f is Ring ;

coherence

the Fun of f is Function of the Dom of f, the Cod of f ;

end;
coherence

the Dom of f is Ring ;

coherence

the Cod of f is Ring ;

coherence

the Fun of f is Function of the Dom of f, the Cod of f ;

Lm1: for G being non empty doubleLoopStr holds id G is linear

proof end;

registration
end;

:: deftheorem Def5 defines RingMorphism-like RINGCAT1:def 5 :

for IT being RingMorphismStr holds

( IT is RingMorphism-like iff fun IT is linear );

for IT being RingMorphismStr holds

( IT is RingMorphism-like iff fun IT is linear );

registration

existence

ex b_{1} being RingMorphismStr st

( b_{1} is strict & b_{1} is RingMorphism-like )

end;
ex b

( b

proof end;

:: deftheorem defines ID RINGCAT1:def 6 :

for G being Ring holds ID G = RingMorphismStr(# G,G,(id G) #);

for G being Ring holds ID G = RingMorphismStr(# G,G,(id G) #);

definition

let G, H be Ring;

reflexivity

for G being Ring ex F being RingMorphism st

( dom F = G & cod F = G )

end;
reflexivity

for G being Ring ex F being RingMorphism st

( dom F = G & cod F = G )

proof end;

:: deftheorem defines <= RINGCAT1:def 7 :

for G, H being Ring holds

( G <= H iff ex F being RingMorphism st

( dom F = G & cod F = H ) );

for G, H being Ring holds

( G <= H iff ex F being RingMorphism st

( dom F = G & cod F = H ) );

Lm2: for F being RingMorphism holds RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is RingMorphism-like

proof end;

definition

let G, H be Ring;

assume A1: G <= H ;

ex b_{1} being strict RingMorphism st

( dom b_{1} = G & cod b_{1} = H )

end;
assume A1: G <= H ;

mode Morphism of G,H -> strict RingMorphism means :Def8: :: RINGCAT1:def 8

( dom it = G & cod it = H );

existence ( dom it = G & cod it = H );

ex b

( dom b

proof end;

:: deftheorem Def8 defines Morphism RINGCAT1:def 8 :

for G, H being Ring st G <= H holds

for b_{3} being strict RingMorphism holds

( b_{3} is Morphism of G,H iff ( dom b_{3} = G & cod b_{3} = H ) );

for G, H being Ring st G <= H holds

for b

( b

registration
end;

definition

let G be Ring;

:: original: ID

redefine func ID G -> strict Morphism of G,G;

coherence

ID G is strict Morphism of G,G

end;
:: original: ID

redefine func ID G -> strict Morphism of G,G;

coherence

ID G is strict Morphism of G,G

proof end;

Lm3: for F being RingMorphism holds the Fun of F is linear

proof end;

Lm4: for G, H being Ring

for f being strict RingMorphismStr st dom f = G & cod f = H & fun f is linear holds

f is Morphism of G,H

proof end;

Lm5: for G, H being Ring

for f being Function of G,H st f is linear holds

RingMorphismStr(# G,H,f #) is Morphism of G,H

proof end;

Lm6: for F being RingMorphism ex G, H being Ring st

( G <= H & dom F = G & cod F = H & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) is Morphism of G,H )

proof end;

theorem Th2: :: RINGCAT1:2

for g, f being RingMorphism st dom g = cod f holds

ex G1, G2, G3 being Ring st

( G1 <= G2 & G2 <= G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 )

ex G1, G2, G3 being Ring st

( G1 <= G2 & G2 <= G3 & RingMorphismStr(# the Dom of g, the Cod of g, the Fun of g #) is Morphism of G2,G3 & RingMorphismStr(# the Dom of f, the Cod of f, the Fun of f #) is Morphism of G1,G2 )

proof end;

Lm7: for G, H being Ring

for F being Morphism of G,H st G <= H holds

ex f being Function of G,H st

( F = RingMorphismStr(# G,H,f #) & f is linear )

proof end;

Lm8: for G, H being Ring

for F being Morphism of G,H st G <= H holds

ex f being Function of G,H st F = RingMorphismStr(# G,H,f #)

proof end;

theorem :: RINGCAT1:4

for F being strict RingMorphism ex G, H being Ring ex f being Function of G,H st

( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )

( F is Morphism of G,H & F = RingMorphismStr(# G,H,f #) & f is linear )

proof end;

definition

let G, F be RingMorphism;

assume A1: dom G = cod F ;

ex b_{1} being strict RingMorphism st

for G1, G2, G3 being Ring

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b_{1} = RingMorphismStr(# G1,G3,(g * f) #)

for b_{1}, b_{2} being strict RingMorphism st ( for G1, G2, G3 being Ring

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b_{1} = RingMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being Ring

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b_{2} = RingMorphismStr(# G1,G3,(g * f) #) ) holds

b_{1} = b_{2}

end;
assume A1: dom G = cod F ;

func G * F -> strict RingMorphism means :Def9: :: RINGCAT1:def 9

for G1, G2, G3 being Ring

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

it = RingMorphismStr(# G1,G3,(g * f) #);

existence for G1, G2, G3 being Ring

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

it = RingMorphismStr(# G1,G3,(g * f) #);

ex b

for G1, G2, G3 being Ring

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b

proof end;

uniqueness for b

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b

b

proof end;

:: deftheorem Def9 defines * RINGCAT1:def 9 :

for G, F being RingMorphism st dom G = cod F holds

for b_{3} being strict RingMorphism holds

( b_{3} = G * F iff for G1, G2, G3 being Ring

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b_{3} = RingMorphismStr(# G1,G3,(g * f) #) );

for G, F being RingMorphism st dom G = cod F holds

for b

( b

for g being Function of G2,G3

for f being Function of G1,G2 st RingMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = RingMorphismStr(# G2,G3,g #) & RingMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = RingMorphismStr(# G1,G2,f #) holds

b

theorem Th6: :: RINGCAT1:6

for G1, G2, G3 being Ring

for G being Morphism of G2,G3

for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds

G * F is Morphism of G1,G3

for G being Morphism of G2,G3

for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds

G * F is Morphism of G1,G3

proof end;

definition

let G1, G2, G3 be Ring;

let G be Morphism of G2,G3;

let F be Morphism of G1,G2;

assume A1: ( G1 <= G2 & G2 <= G3 ) ;

coherence

G * F is strict Morphism of G1,G3 by A1, Th6;

end;
let G be Morphism of G2,G3;

let F be Morphism of G1,G2;

assume A1: ( G1 <= G2 & G2 <= G3 ) ;

coherence

G * F is strict Morphism of G1,G3 by A1, Th6;

:: deftheorem Def10 defines *' RINGCAT1:def 10 :

for G1, G2, G3 being Ring

for G being Morphism of G2,G3

for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds

G *' F = G * F;

for G1, G2, G3 being Ring

for G being Morphism of G2,G3

for F being Morphism of G1,G2 st G1 <= G2 & G2 <= G3 holds

G *' F = G * F;

theorem Th7: :: RINGCAT1:7

for f, g being strict RingMorphism st dom g = cod f holds

ex G1, G2, G3 being Ring ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st

( f = RingMorphismStr(# G1,G2,f0 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) )

ex G1, G2, G3 being Ring ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st

( f = RingMorphismStr(# G1,G2,f0 #) & g = RingMorphismStr(# G2,G3,g0 #) & g * f = RingMorphismStr(# G1,G3,(g0 * f0) #) )

proof end;

theorem Th8: :: RINGCAT1:8

for f, g being strict RingMorphism st dom g = cod f holds

( dom (g * f) = dom f & cod (g * f) = cod g )

( dom (g * f) = dom f & cod (g * f) = cod g )

proof end;

theorem Th9: :: RINGCAT1:9

for G1, G2, G3, G4 being Ring

for f being Morphism of G1,G2

for g being Morphism of G2,G3

for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds

h * (g * f) = (h * g) * f

for f being Morphism of G1,G2

for g being Morphism of G2,G3

for h being Morphism of G3,G4 st G1 <= G2 & G2 <= G3 & G3 <= G4 holds

h * (g * f) = (h * g) * f

proof end;

theorem Th10: :: RINGCAT1:10

for f, g, h being strict RingMorphism st dom h = cod g & dom g = cod f holds

h * (g * f) = (h * g) * f

h * (g * f) = (h * g) * f

proof end;

theorem :: RINGCAT1:11

for G being Ring holds

( dom (ID G) = G & cod (ID G) = G & ( for f being strict RingMorphism st cod f = G holds

(ID G) * f = f ) & ( for g being strict RingMorphism st dom g = G holds

g * (ID G) = g ) )

( dom (ID G) = G & cod (ID G) = G & ( for f being strict RingMorphism st cod f = G holds

(ID G) * f = f ) & ( for g being strict RingMorphism st dom g = G holds

g * (ID G) = g ) )

proof end;

::

:: 2. Domains of rings

::

:: 2. Domains of rings

::

definition

let IT be set ;

end;
attr IT is Ring_DOMAIN-like means :Def11: :: RINGCAT1:def 11

for x being Element of IT holds x is strict Ring;

for x being Element of IT holds x is strict Ring;

:: deftheorem Def11 defines Ring_DOMAIN-like RINGCAT1:def 11 :

for IT being set holds

( IT is Ring_DOMAIN-like iff for x being Element of IT holds x is strict Ring );

for IT being set holds

( IT is Ring_DOMAIN-like iff for x being Element of IT holds x is strict Ring );

registration
end;

definition

let V be Ring_DOMAIN;

:: original: Element

redefine mode Element of V -> Ring;

coherence

for b_{1} being Element of V holds b_{1} is Ring
by Def11;

end;
:: original: Element

redefine mode Element of V -> Ring;

coherence

for b

registration

let V be Ring_DOMAIN;

ex b_{1} being Element of V st b_{1} is strict

end;
cluster non empty right_complementable strict V99() V100() V101() unital associative right-distributive left-distributive right_unital well-unital V152() left_unital for Element of V;

existence ex b

proof end;

definition

let IT be set ;

end;
attr IT is RingMorphism_DOMAIN-like means :Def12: :: RINGCAT1:def 12

for x being object st x in IT holds

x is strict RingMorphism;

for x being object st x in IT holds

x is strict RingMorphism;

:: deftheorem Def12 defines RingMorphism_DOMAIN-like RINGCAT1:def 12 :

for IT being set holds

( IT is RingMorphism_DOMAIN-like iff for x being object st x in IT holds

x is strict RingMorphism );

for IT being set holds

( IT is RingMorphism_DOMAIN-like iff for x being object st x in IT holds

x is strict RingMorphism );

registration
end;

definition

let M be RingMorphism_DOMAIN;

:: original: Element

redefine mode Element of M -> RingMorphism;

coherence

for b_{1} being Element of M holds b_{1} is RingMorphism
by Def12;

end;
:: original: Element

redefine mode Element of M -> RingMorphism;

coherence

for b

registration
end;

definition

let G, H be Ring;

ex b_{1} being RingMorphism_DOMAIN st

for x being Element of b_{1} holds x is Morphism of G,H

end;
mode RingMorphism_DOMAIN of G,H -> RingMorphism_DOMAIN means :Def13: :: RINGCAT1:def 13

for x being Element of it holds x is Morphism of G,H;

existence for x being Element of it holds x is Morphism of G,H;

ex b

for x being Element of b

proof end;

:: deftheorem Def13 defines RingMorphism_DOMAIN RINGCAT1:def 13 :

for G, H being Ring

for b_{3} being RingMorphism_DOMAIN holds

( b_{3} is RingMorphism_DOMAIN of G,H iff for x being Element of b_{3} holds x is Morphism of G,H );

for G, H being Ring

for b

( b

theorem Th13: :: RINGCAT1:13

for D being non empty set

for G, H being Ring holds

( D is RingMorphism_DOMAIN of G,H iff for x being Element of D holds x is Morphism of G,H )

for G, H being Ring holds

( D is RingMorphism_DOMAIN of G,H iff for x being Element of D holds x is Morphism of G,H )

proof end;

definition

let G, H be Ring;

assume A1: G <= H ;

ex b_{1} being RingMorphism_DOMAIN of G,H st

for x being object holds

( x in b_{1} iff x is Morphism of G,H )

for b_{1}, b_{2} being RingMorphism_DOMAIN of G,H st ( for x being object holds

( x in b_{1} iff x is Morphism of G,H ) ) & ( for x being object holds

( x in b_{2} iff x is Morphism of G,H ) ) holds

b_{1} = b_{2}

end;
assume A1: G <= H ;

func Morphs (G,H) -> RingMorphism_DOMAIN of G,H means :Def14: :: RINGCAT1:def 14

for x being object holds

( x in it iff x is Morphism of G,H );

existence for x being object holds

( x in it iff x is Morphism of G,H );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def14 defines Morphs RINGCAT1:def 14 :

for G, H being Ring st G <= H holds

for b_{3} being RingMorphism_DOMAIN of G,H holds

( b_{3} = Morphs (G,H) iff for x being object holds

( x in b_{3} iff x is Morphism of G,H ) );

for G, H being Ring st G <= H holds

for b

( b

( x in b

definition

let G, H be Ring;

let M be RingMorphism_DOMAIN of G,H;

:: original: Element

redefine mode Element of M -> Morphism of G,H;

coherence

for b_{1} being Element of M holds b_{1} is Morphism of G,H
by Def13;

end;
let M be RingMorphism_DOMAIN of G,H;

:: original: Element

redefine mode Element of M -> Morphism of G,H;

coherence

for b

registration

let G, H be Ring;

let M be RingMorphism_DOMAIN of G,H;

existence

ex b_{1} being Element of M st b_{1} is strict

end;
let M be RingMorphism_DOMAIN of G,H;

existence

ex b

proof end;

::

:: 4a. Category of rings - objects

::

:: 4a. Category of rings - objects

::

:: deftheorem defines GO RINGCAT1:def 15 :

for x, y being object holds

( GO x,y iff ex x1, x2, x3, x4, x5, x6 being set st

( x = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st

( y = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) ) );

for x, y being object holds

( GO x,y iff ex x1, x2, x3, x4, x5, x6 being set st

( x = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st

( y = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) ) );

definition

let UN be Universe;

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ex x being set st

( x in UN & GO x,y ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ex x being set st

( x in UN & GO x,y ) ) ) & ( for y being object holds

( y in b_{2} iff ex x being set st

( x in UN & GO x,y ) ) ) holds

b_{1} = b_{2}

end;
func RingObjects UN -> set means :Def16: :: RINGCAT1:def 16

for y being object holds

( y in it iff ex x being set st

( x in UN & GO x,y ) );

existence for y being object holds

( y in it iff ex x being set st

( x in UN & GO x,y ) );

ex b

for y being object holds

( y in b

( x in UN & GO x,y ) )

proof end;

uniqueness for b

( y in b

( x in UN & GO x,y ) ) ) & ( for y being object holds

( y in b

( x in UN & GO x,y ) ) ) holds

b

proof end;

:: deftheorem Def16 defines RingObjects RINGCAT1:def 16 :

for UN being Universe

for b_{2} being set holds

( b_{2} = RingObjects UN iff for y being object holds

( y in b_{2} iff ex x being set st

( x in UN & GO x,y ) ) );

for UN being Universe

for b

( b

( y in b

( x in UN & GO x,y ) ) );

::

:: 4b. Category of rings - morphisms

::

:: 4b. Category of rings - morphisms

::

definition

let V be Ring_DOMAIN;

ex b_{1} being RingMorphism_DOMAIN st

for x being object holds

( x in b_{1} iff ex G, H being Element of V st

( G <= H & x is Morphism of G,H ) )

for b_{1}, b_{2} being RingMorphism_DOMAIN st ( for x being object holds

( x in b_{1} iff ex G, H being Element of V st

( G <= H & x is Morphism of G,H ) ) ) & ( for x being object holds

( x in b_{2} iff ex G, H being Element of V st

( G <= H & x is Morphism of G,H ) ) ) holds

b_{1} = b_{2}

end;
func Morphs V -> RingMorphism_DOMAIN means :Def17: :: RINGCAT1:def 17

for x being object holds

( x in it iff ex G, H being Element of V st

( G <= H & x is Morphism of G,H ) );

existence for x being object holds

( x in it iff ex G, H being Element of V st

( G <= H & x is Morphism of G,H ) );

ex b

for x being object holds

( x in b

( G <= H & x is Morphism of G,H ) )

proof end;

uniqueness for b

( x in b

( G <= H & x is Morphism of G,H ) ) ) & ( for x being object holds

( x in b

( G <= H & x is Morphism of G,H ) ) ) holds

b

proof end;

:: deftheorem Def17 defines Morphs RINGCAT1:def 17 :

for V being Ring_DOMAIN

for b_{2} being RingMorphism_DOMAIN holds

( b_{2} = Morphs V iff for x being object holds

( x in b_{2} iff ex G, H being Element of V st

( G <= H & x is Morphism of G,H ) ) );

for V being Ring_DOMAIN

for b

( b

( x in b

( G <= H & x is Morphism of G,H ) ) );

::

:: 4c. Category of rings - dom,cod,id

::

:: 4c. Category of rings - dom,cod,id

::

definition

let V be Ring_DOMAIN;

let F be Element of Morphs V;

:: original: dom

redefine func dom F -> Element of V;

coherence

dom F is Element of V

redefine func cod F -> Element of V;

coherence

cod F is Element of V

end;
let F be Element of Morphs V;

:: original: dom

redefine func dom F -> Element of V;

coherence

dom F is Element of V

proof end;

:: original: codredefine func cod F -> Element of V;

coherence

cod F is Element of V

proof end;

definition
end;

:: deftheorem defines ID RINGCAT1:def 18 :

for V being Ring_DOMAIN

for G being Element of V holds ID G = ID G;

for V being Ring_DOMAIN

for G being Element of V holds ID G = ID G;

definition

let V be Ring_DOMAIN;

ex b_{1} being Function of (Morphs V),V st

for f being Element of Morphs V holds b_{1} . f = dom f

for b_{1}, b_{2} being Function of (Morphs V),V st ( for f being Element of Morphs V holds b_{1} . f = dom f ) & ( for f being Element of Morphs V holds b_{2} . f = dom f ) holds

b_{1} = b_{2}

ex b_{1} being Function of (Morphs V),V st

for f being Element of Morphs V holds b_{1} . f = cod f

for b_{1}, b_{2} being Function of (Morphs V),V st ( for f being Element of Morphs V holds b_{1} . f = cod f ) & ( for f being Element of Morphs V holds b_{2} . f = cod f ) holds

b_{1} = b_{2}

end;
func dom V -> Function of (Morphs V),V means :Def19: :: RINGCAT1:def 20

for f being Element of Morphs V holds it . f = dom f;

existence for f being Element of Morphs V holds it . f = dom f;

ex b

for f being Element of Morphs V holds b

proof end;

uniqueness for b

b

proof end;

func cod V -> Function of (Morphs V),V means :Def20: :: RINGCAT1:def 21

for f being Element of Morphs V holds it . f = cod f;

existence for f being Element of Morphs V holds it . f = cod f;

ex b

for f being Element of Morphs V holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def19 defines dom RINGCAT1:def 20 :

for V being Ring_DOMAIN

for b_{2} being Function of (Morphs V),V holds

( b_{2} = dom V iff for f being Element of Morphs V holds b_{2} . f = dom f );

for V being Ring_DOMAIN

for b

( b

:: deftheorem Def20 defines cod RINGCAT1:def 21 :

for V being Ring_DOMAIN

for b_{2} being Function of (Morphs V),V holds

( b_{2} = cod V iff for f being Element of Morphs V holds b_{2} . f = cod f );

for V being Ring_DOMAIN

for b

( b

::

:: 4d. Category of rings - superposition

::

:: 4d. Category of rings - superposition

::

theorem Th19: :: RINGCAT1:19

for V being Ring_DOMAIN

for g, f being Element of Morphs V st dom g = cod f holds

ex G1, G2, G3 being Element of V st

( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 )

for g, f being Element of Morphs V st dom g = cod f holds

ex G1, G2, G3 being Element of V st

( G1 <= G2 & G2 <= G3 & g is Morphism of G2,G3 & f is Morphism of G1,G2 )

proof end;

definition

let V be Ring_DOMAIN;

ex b_{1} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st

( ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{1} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{1} holds

b_{1} . (g,f) = g * f ) )

for b_{1}, b_{2} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{1} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{1} holds

b_{1} . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{2} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{2} holds

b_{2} . (g,f) = g * f ) holds

b_{1} = b_{2}

end;
func comp V -> PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def21: :: RINGCAT1:def 23

( ( for g, f being Element of Morphs V holds

( [g,f] in dom it iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom it holds

it . (g,f) = g * f ) );

existence ( ( for g, f being Element of Morphs V holds

( [g,f] in dom it iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom it holds

it . (g,f) = g * f ) );

ex b

( ( for g, f being Element of Morphs V holds

( [g,f] in dom b

b

proof end;

uniqueness for b

( [g,f] in dom b

b

( [g,f] in dom b

b

b

proof end;

:: deftheorem Def21 defines comp RINGCAT1:def 23 :

for V being Ring_DOMAIN

for b_{2} being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds

( b_{2} = comp V iff ( ( for g, f being Element of Morphs V holds

( [g,f] in dom b_{2} iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b_{2} holds

b_{2} . (g,f) = g * f ) ) );

for V being Ring_DOMAIN

for b

( b

( [g,f] in dom b

b

::

:: 4e. Definition of Category of rings

::

:: 4e. Definition of Category of rings

::

definition

let UN be Universe;

CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #) is CatStr ;

end;
func RingCat UN -> CatStr equals :: RINGCAT1:def 24

CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #);

coherence CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #);

CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #) is CatStr ;

:: deftheorem defines RingCat RINGCAT1:def 24 :

for UN being Universe holds RingCat UN = CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #);

for UN being Universe holds RingCat UN = CatStr(# (RingObjects UN),(Morphs (RingObjects UN)),(dom (RingObjects UN)),(cod (RingObjects UN)),(comp (RingObjects UN)) #);

registration

let UN be Universe;

coherence

( RingCat UN is strict & not RingCat UN is void & not RingCat UN is empty ) ;

end;
coherence

( RingCat UN is strict & not RingCat UN is void & not RingCat UN is empty ) ;

theorem Th21: :: RINGCAT1:21

for UN being Universe

for f, g being Morphism of (RingCat UN) holds

( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )

for f, g being Morphism of (RingCat UN) holds

( [g,f] in dom the Comp of (RingCat UN) iff dom g = cod f )

proof end;

theorem Th22: :: RINGCAT1:22

for UN being Universe

for f being Morphism of (RingCat UN)

for f9 being Element of Morphs (RingObjects UN)

for b being Object of (RingCat UN)

for b9 being Element of RingObjects UN holds

( f is strict Element of Morphs (RingObjects UN) & f9 is Morphism of (RingCat UN) & b is strict Element of RingObjects UN & b9 is Object of (RingCat UN) )

for f being Morphism of (RingCat UN)

for f9 being Element of Morphs (RingObjects UN)

for b being Object of (RingCat UN)

for b9 being Element of RingObjects UN holds

( f is strict Element of Morphs (RingObjects UN) & f9 is Morphism of (RingCat UN) & b is strict Element of RingObjects UN & b9 is Object of (RingCat UN) )

proof end;

::$CT

theorem Th23: :: RINGCAT1:24

for UN being Universe

for f, g being Morphism of (RingCat UN)

for f9, g9 being Element of Morphs (RingObjects UN) st f = f9 & g = g9 holds

( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )

for f, g being Morphism of (RingCat UN)

for f9, g9 being Element of Morphs (RingObjects UN) st f = f9 & g = g9 holds

( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (RingObjects UN)) ) & ( [g9,f9] in dom (comp (RingObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )

proof end;

Lm9: for UN being Universe

for f, g being Morphism of (RingCat UN) st dom g = cod f holds

( dom (g (*) f) = dom f & cod (g (*) f) = cod g )

proof end;

Lm10: for UN being Universe

for f, g, h being Morphism of (RingCat UN) st dom h = cod g & dom g = cod f holds

h (*) (g (*) f) = (h (*) g) (*) f

proof end;

registration

let UN be Universe;

coherence

( RingCat UN is Category-like & RingCat UN is transitive & RingCat UN is associative & RingCat UN is reflexive )

end;
coherence

( RingCat UN is Category-like & RingCat UN is transitive & RingCat UN is associative & RingCat UN is reflexive )

proof end;

Lm11: for UN being Universe

for a being Element of (RingCat UN)

for aa being Element of RingObjects UN st a = aa holds

for i being Morphism of a,a st i = ID aa holds

for b being Element of (RingCat UN) holds

( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

proof end;

theorem :: RINGCAT1:25

for UN being Universe

for a being Object of (RingCat UN)

for aa being Element of RingObjects UN st a = aa holds

id a = ID aa

for a being Object of (RingCat UN)

for aa being Element of RingObjects UN st a = aa holds

id a = ID aa

proof end;

:: 1a. Maps of the carriers of rings

::