:: RINGCAT1 semantic presentation

definition

let c₁, c₂ be non empty doubleLoopStr ;
let c₃ be Function of c₁,c₂;
canceled;
attr a₃ is linear means :Def2: :: RINGCAT1:def 2
( ( for b₁, b₂ being Scalar of a₁ holds a₃ . (b₁ + b₂) = (a₃ . b₁) + (a₃ . b₂) ) & ( for b₁, b₂ being Scalar of a₁ holds a₃ . (b₁ * b₂) = (a₃ . b₁) * (a₃ . b₂) ) & a₃ . (1. a₁) = 1. a₂ );

end;

:: deftheorem Def1 RINGCAT1:def 1 :

:: deftheorem Def2 defines linear RINGCAT1:def 2 :

theorem Th1: :: RINGCAT1:1

canceled;

theorem Th2: :: RINGCAT1:2

canceled;

theorem Th3: :: RINGCAT1:3

for b₁, b₂, b₃ being non empty doubleLoopStr
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is linear & b₅ is linear holds
b₅ * b₄ is linear

proof end;

definition

attr a₁ is strict;
struct RingMorphismStr -> ;
aggr RingMorphismStr(# Dom, Cod, Fun #) -> RingMorphismStr ;
sel Dom c₁ -> Ring;
sel Cod c₁ -> Ring;
sel Fun c₁ -> Function of the Dom of a₁,the Cod of a₁;

end;

definition

let c₁ be RingMorphismStr ;
func dom c₁ -> Ring equals :: RINGCAT1:def 3
the Dom of a₁;
coherence ;
func cod c₁ -> Ring equals :: RINGCAT1:def 4
the Cod of a₁;
coherence ;
func fun c₁ -> Function of the Dom of a₁,the Cod of a₁ equals :: RINGCAT1:def 5
the Fun of a₁;
coherence ;

end;

:: deftheorem Def3 defines dom RINGCAT1:def 3 :

:: deftheorem Def4 defines cod RINGCAT1:def 4 :

:: deftheorem Def5 defines fun RINGCAT1:def 5 :

Lemma3: for b₁ being non empty doubleLoopStr holds id b₁ is linear

proof end;

registration

let c₁ be non empty doubleLoopStr ;
cluster id a₁ -> linear ;
coherence by Lemma3;

end;

definition

let c₁ be RingMorphismStr ;
attr a₁ is RingMorphism-like means :Def6: :: RINGCAT1:def 6
fun a₁ is linear;

end;

:: deftheorem Def6 defines RingMorphism-like RINGCAT1:def 6 :

registration

cluster strict RingMorphism-like RingMorphismStr ;
existence

proof end;

end;

definition

mode RingMorphism is RingMorphism-like RingMorphismStr ;

end;

definition

let c₁ be Ring;
func ID c₁ -> RingMorphism equals :: RINGCAT1:def 7
RingMorphismStr(# a₁,a₁,(id a₁) #);
coherence

proof end;

end;

:: deftheorem Def7 defines ID RINGCAT1:def 7 :

registration

let c₁ be Ring;
cluster ID a₁ -> strict ;
coherence ;

end;

definition

let c₁, c₂ be Ring;
pred c₁ <= c₂ means :Def8: :: RINGCAT1:def 8
ex b₁ being RingMorphism st
( dom b₁ = a₁ & cod b₁ = a₂ );
reflexivity

proof end;

end;

:: deftheorem Def8 defines <= RINGCAT1:def 8 :

Lemma6: for b₁ being RingMorphism holds RingMorphismStr(# the Dom of b₁,the Cod of b₁,the Fun of b₁ #) is RingMorphism-like

proof end;

definition

let c₁, c₂ be Ring;
assume E7: c₁ <= c₂ ;
mode Morphism of c₁,c₂ -> strict RingMorphism means :Def9: :: RINGCAT1:def 9
( dom a₃ = a₁ & cod a₃ = a₂ );
existence

proof end;

end;

:: deftheorem Def9 defines Morphism RINGCAT1:def 9 :

registration

let c₁, c₂ be Ring;
cluster strict Morphism of a₁,a₂;
existence

proof end;

end;

definition

let c₁ be Ring;
redefine func ID as ID c₁ -> strict Morphism of a₁,a₁;
coherence

proof end;

end;

Lemma8: for b₁ being RingMorphism holds the Fun of b₁ is linear

proof end;

Lemma9: for b₁, b₂ being Ring
for b₃ being strict RingMorphismStr st dom b₃ = b₁ & cod b₃ = b₂ & fun b₃ is linear holds
b₃ is Morphism of b₁,b₂

proof end;

Lemma10: for b₁, b₂ being Ring
for b₃ being Function of b₁,b₂ st b₃ is linear holds
RingMorphismStr(# b₁,b₂,b₃ #) is Morphism of b₁,b₂

proof end;

Lemma11: for b₁ being RingMorphism ex b₂, b₃ being Ring st
( b₂ <= b₃ & dom b₁ = b₂ & cod b₁ = b₃ & RingMorphismStr(# the Dom of b₁,the Cod of b₁,the Fun of b₁ #) is Morphism of b₂,b₃ )

proof end;

theorem Th4: :: RINGCAT1:4

canceled;

theorem Th5: :: RINGCAT1:5

for b₁, b₂ being RingMorphism st dom b₁ = cod b₂ holds
ex b₃, b₄, b₅ being Ring st
( b₃ <= b₄ & b₄ <= b₅ & RingMorphismStr(# the Dom of b₁,the Cod of b₁,the Fun of b₁ #) is Morphism of b₄,b₅ & RingMorphismStr(# the Dom of b₂,the Cod of b₂,the Fun of b₂ #) is Morphism of b₃,b₄ )

proof end;

theorem Th6: :: RINGCAT1:6

for b₁ being strict RingMorphism holds
( b₁ is Morphism of dom b₁, cod b₁ & dom b₁ <= cod b₁ )

proof end;

Lemma14: for b₁, b₂ being Ring
for b₃ being Morphism of b₁,b₂ st b₁ <= b₂ holds
ex b₄ being Function of b₁,b₂ st
( b₃ = RingMorphismStr(# b₁,b₂,b₄ #) & b₄ is linear )

proof end;

Lemma15: for b₁, b₂ being Ring
for b₃ being Morphism of b₁,b₂ st b₁ <= b₂ holds
ex b₄ being Function of b₁,b₂ st b₃ = RingMorphismStr(# b₁,b₂,b₄ #)

proof end;

theorem Th7: :: RINGCAT1:7

for b₁ being strict RingMorphism ex b₂, b₃ being Ringex b₄ being Function of b₂,b₃ st
( b₁ is Morphism of b₂,b₃ & b₁ = RingMorphismStr(# b₂,b₃,b₄ #) & b₄ is linear )

proof end;

definition

let c₁, c₂ be RingMorphism;
assume E16: dom c₁ = cod c₂ ;
func c₁ * c₂ -> strict RingMorphism means :Def10: :: RINGCAT1:def 10
for b₁, b₂, b₃ being Ring
for b₄ being Function of b₂,b₃
for b₅ being Function of b₁,b₂ st RingMorphismStr(# the Dom of a₁,the Cod of a₁,the Fun of a₁ #) = RingMorphismStr(# b₂,b₃,b₄ #) & RingMorphismStr(# the Dom of a₂,the Cod of a₂,the Fun of a₂ #) = RingMorphismStr(# b₁,b₂,b₅ #) holds
a₃ = RingMorphismStr(# b₁,b₃,(b₄ * b₅) #);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines * RINGCAT1:def 10 :

theorem Th8: :: RINGCAT1:8

for b₁, b₂, b₃ being Ring st b₁ <= b₂ & b₂ <= b₃ holds
b₁ <= b₃

proof end;

theorem Th9: :: RINGCAT1:9

for b₁, b₂, b₃ being Ring
for b₄ being Morphism of b₁,b₂
for b₅ being Morphism of b₃,b₁ st b₃ <= b₁ & b₁ <= b₂ holds
b₄ * b₅ is Morphism of b₃,b₂

proof end;

definition

let c₁, c₂, c₃ be Ring;
let c₄ be Morphism of c₂,c₃;
let c₅ be Morphism of c₁,c₂;
assume E19: ( c₁ <= c₂ & c₂ <= c₃ ) ;
func c₄ *' c₅ -> strict Morphism of a₁,a₃ equals :Def11: :: RINGCAT1:def 11
a₄ * a₅;
coherence by E19, Th9;

end;

:: deftheorem Def11 defines *' RINGCAT1:def 11 :

theorem Th10: :: RINGCAT1:10

for b₁, b₂ being strict RingMorphism st dom b₂ = cod b₁ holds
ex b₃, b₄, b₅ being Ringex b₆ being Function of b₃,b₄ex b₇ being Function of b₄,b₅ st
( b₁ = RingMorphismStr(# b₃,b₄,b₆ #) & b₂ = RingMorphismStr(# b₄,b₅,b₇ #) & b₂ * b₁ = RingMorphismStr(# b₃,b₅,(b₇ * b₆) #) )

proof end;

theorem Th11: :: RINGCAT1:11

for b₁, b₂ being strict RingMorphism st dom b₂ = cod b₁ holds
( dom (b₂ * b₁) = dom b₁ & cod (b₂ * b₁) = cod b₂ )

proof end;

theorem Th12: :: RINGCAT1:12

for b₁, b₂, b₃, b₄ being Ring
for b₅ being Morphism of b₁,b₂
for b₆ being Morphism of b₂,b₃
for b₇ being Morphism of b₃,b₄ st b₁ <= b₂ & b₂ <= b₃ & b₃ <= b₄ holds
b₇ * (b₆ * b₅) = (b₇ * b₆) * b₅

proof end;

theorem Th13: :: RINGCAT1:13

for b₁, b₂, b₃ being strict RingMorphism st dom b₃ = cod b₂ & dom b₂ = cod b₁ holds
b₃ * (b₂ * b₁) = (b₃ * b₂) * b₁

proof end;

theorem Th14: :: RINGCAT1:14

for b₁ being Ring holds
( dom (ID b₁) = b₁ & cod (ID b₁) = b₁ & ( for b₂ being strict RingMorphism st cod b₂ = b₁ holds
(ID b₁) * b₂ = b₂ ) & ( for b₂ being strict RingMorphism st dom b₂ = b₁ holds
b₂ * (ID b₁) = b₂ ) )

proof end;

definition

let c₁ be set ;
attr a₁ is Ring_DOMAIN-like means :Def12: :: RINGCAT1:def 12
for b₁ being Element of a₁ holds b₁ is strict Ring;

end;

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

registration

cluster non empty Ring_DOMAIN-like set ;
existence

proof end;

end;

definition

mode Ring_DOMAIN is non empty Ring_DOMAIN-like set ;

end;

definition

let c₁ be Ring_DOMAIN;
redefine mode Element as Element of c₁ -> Ring;
coherence by Def12;

end;

registration

let c₁ be Ring_DOMAIN;
cluster strict Element of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
attr a₁ is RingMorphism_DOMAIN-like means :Def13: :: RINGCAT1:def 13
for b₁ being set st b₁ in a₁ holds
b₁ is strict RingMorphism;

end;

:: deftheorem Def13 defines RingMorphism_DOMAIN-like RINGCAT1:def 13 :

registration

cluster non empty RingMorphism_DOMAIN-like set ;
existence

proof end;

end;

definition

mode RingMorphism_DOMAIN is non empty RingMorphism_DOMAIN-like set ;

end;

definition

let c₁ be RingMorphism_DOMAIN;
redefine mode Element as Element of c₁ -> RingMorphism;
coherence by Def13;

end;

registration

let c₁ be RingMorphism_DOMAIN;
cluster strict Element of a₁;
existence

proof end;

end;

theorem Th15: :: RINGCAT1:15

canceled;

theorem Th16: :: RINGCAT1:16

canceled;

theorem Th17: :: RINGCAT1:17

for b₁ being strict RingMorphism holds {b₁} is RingMorphism_DOMAIN

proof end;

definition

let c₁, c₂ be Ring;
mode RingMorphism_DOMAIN of c₁,c₂ -> RingMorphism_DOMAIN means :Def14: :: RINGCAT1:def 14
for b₁ being Element of a₃ holds b₁ is Morphism of a₁,a₂;
existence

proof end;

end;

:: deftheorem Def14 defines RingMorphism_DOMAIN RINGCAT1:def 14 :

theorem Th18: :: RINGCAT1:18

for b₁ being non empty set
for b₂, b₃ being Ring holds
( b₁ is RingMorphism_DOMAIN of b₂,b₃ iff for b₄ being Element of b₁ holds b₄ is Morphism of b₂,b₃ )

proof end;

theorem Th19: :: RINGCAT1:19

for b₁, b₂ being Ring
for b₃ being Morphism of b₁,b₂ holds {b₃} is RingMorphism_DOMAIN of b₁,b₂

proof end;

definition

let c₁, c₂ be Ring;
assume E30: c₁ <= c₂ ;
func Morphs c₁,c₂ -> RingMorphism_DOMAIN of a₁,a₂ means :Def15: :: RINGCAT1:def 15
for b₁ being set holds
( b₁ in a₃ iff b₁ is Morphism of a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Morphs RINGCAT1:def 15 :

definition

let c₁, c₂ be Ring;
let c₃ be RingMorphism_DOMAIN of c₁,c₂;
redefine mode Element as Element of c₃ -> Morphism of a₁,a₂;
coherence by Def14;

end;

registration

let c₁, c₂ be Ring;
let c₃ be RingMorphism_DOMAIN of c₁,c₂;
cluster strict Element of a₃;
existence

proof end;

end;

definition

let c₁, c₂ be set ;
pred GO c₁,c₂ means :Def16: :: RINGCAT1:def 16
ex b₁, b₂, b₃, b₄, b₅, b₆ being set st
( a₁ = [[b₁,b₂,b₃,b₄],b₅,b₆] & ex b₇ being strict Ring st
( a₂ = b₇ & b₁ = the carrier of b₇ & b₂ = the add of b₇ & b₃ = comp b₇ & b₄ = the Zero of b₇ & b₅ = the mult of b₇ & b₆ = the unity of b₇ ) );

end;

:: deftheorem Def16 defines GO RINGCAT1:def 16 :

theorem Th20: :: RINGCAT1:20

for b₁, b₂, b₃ being set st GO b₁,b₂ & GO b₁,b₃ holds
b₂ = b₃

proof end;

theorem Th21: :: RINGCAT1:21

for b₁ being Universe ex b₂ being set st
( b₂ in b₁ & GO b₂, Z3 )

proof end;

definition

let c₁ be Universe;
func RingObjects c₁ -> set means :Def17: :: RINGCAT1:def 17
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being set st
( b₂ in a₁ & GO b₂,b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines RingObjects RINGCAT1:def 17 :

theorem Th22: :: RINGCAT1:22

for b₁ being Universe holds Z3 in RingObjects b₁

proof end;

registration

let c₁ be Universe;
cluster RingObjects a₁ -> non empty ;
coherence by Th22;

end;

theorem Th23: :: RINGCAT1:23

for b₁ being Universe
for b₂ being Element of RingObjects b₁ holds b₂ is strict Ring

proof end;

registration

let c₁ be Universe;
cluster RingObjects a₁ -> non empty Ring_DOMAIN-like ;
coherence

proof end;

end;

definition

let c₁ be Ring_DOMAIN;
func Morphs c₁ -> RingMorphism_DOMAIN means :Def18: :: RINGCAT1:def 18
for b₁ being set holds
( b₁ in a₂ iff ex b₂, b₃ being Element of a₁ st
( b₂ <= b₃ & b₁ is Morphism of b₂,b₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Morphs RINGCAT1:def 18 :

definition

let c₁ be Ring_DOMAIN;
let c₂ be Element of Morphs c₁;
redefine func dom as dom c₂ -> Element of a₁;
coherence

proof end;

redefine func cod as cod c₂ -> Element of a₁;
coherence

proof end;

end;

definition

let c₁ be Ring_DOMAIN;
let c₂ be Element of c₁;
func ID c₂ -> strict Element of Morphs a₁ equals :: RINGCAT1:def 19
ID a₂;
coherence by Def18;

end;

:: deftheorem Def19 defines ID RINGCAT1:def 19 :

definition

let c₁ be Ring_DOMAIN;
func dom c₁ -> Function of Morphs a₁,a₁ means :Def20: :: RINGCAT1:def 20
for b₁ being Element of Morphs a₁ holds a₂ . b₁ = dom b₁;
existence

proof end;

uniqueness

proof end;

func cod c₁ -> Function of Morphs a₁,a₁ means :Def21: :: RINGCAT1:def 21
for b₁ being Element of Morphs a₁ holds a₂ . b₁ = cod b₁;
existence

proof end;

uniqueness

proof end;

func ID c₁ -> Function of a₁, Morphs a₁ means :Def22: :: RINGCAT1:def 22
for b₁ being Element of a₁ holds a₂ . b₁ = ID b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines dom RINGCAT1:def 20 :

:: deftheorem Def21 defines cod RINGCAT1:def 21 :

:: deftheorem Def22 defines ID RINGCAT1:def 22 :

theorem Th24: :: RINGCAT1:24

for b₁ being Ring_DOMAIN
for b₂, b₃ being Element of Morphs b₁ st dom b₂ = cod b₃ holds
ex b₄, b₅, b₆ being Element of b₁ st
( b₄ <= b₅ & b₅ <= b₆ & b₂ is Morphism of b₅,b₆ & b₃ is Morphism of b₄,b₅ )

proof end;

theorem Th25: :: RINGCAT1:25

for b₁ being Ring_DOMAIN
for b₂, b₃ being Element of Morphs b₁ st dom b₂ = cod b₃ holds
b₂ * b₃ in Morphs b₁

proof end;

definition

let c₁ be Ring_DOMAIN;
func comp c₁ -> PartFunc of [:(Morphs a₁),(Morphs a₁):], Morphs a₁ means :Def23: :: RINGCAT1:def 23
( ( for b₁, b₂ being Element of Morphs a₁ holds
( [b₁,b₂] in dom a₂ iff dom b₁ = cod b₂ ) ) & ( for b₁, b₂ being Element of Morphs a₁ st [b₁,b₂] in dom a₂ holds
a₂ . [b₁,b₂] = b₁ * b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines comp RINGCAT1:def 23 :

definition

let c₁ be Universe;
func RingCat c₁ -> CatStr equals :: RINGCAT1:def 24
CatStr(# (RingObjects a₁),(Morphs (RingObjects a₁)),(dom (RingObjects a₁)),(cod (RingObjects a₁)),(comp (RingObjects a₁)),(ID (RingObjects a₁)) #);
coherence ;

end;

:: deftheorem Def24 defines RingCat RINGCAT1:def 24 :

registration

let c₁ be Universe;
cluster RingCat a₁ -> strict ;
coherence ;

end;

theorem Th26: :: RINGCAT1:26

for b₁ being Universe
for b₂, b₃ being Morphism of (RingCat b₁) holds
( [b₃,b₂] in dom the Comp of (RingCat b₁) iff dom b₃ = cod b₂ )

proof end;

theorem Th27: :: RINGCAT1:27

for b₁ being Universe
for b₂ being Morphism of (RingCat b₁)
for b₃ being Element of Morphs (RingObjects b₁)
for b₄ being Object of (RingCat b₁)
for b₅ being Element of RingObjects b₁ holds
( b₂ is strict Element of Morphs (RingObjects b₁) & b₃ is Morphism of (RingCat b₁) & b₄ is strict Element of RingObjects b₁ & b₅ is Object of (RingCat b₁) )

proof end;

theorem Th28: :: RINGCAT1:28

for b₁ being Universe
for b₂ being Object of (RingCat b₁)
for b₃ being Element of RingObjects b₁ st b₂ = b₃ holds
id b₂ = ID b₃

proof end;

theorem Th29: :: RINGCAT1:29

for b₁ being Universe
for b₂ being Morphism of (RingCat b₁)
for b₃ being Element of Morphs (RingObjects b₁) st b₂ = b₃ holds
( dom b₂ = dom b₃ & cod b₂ = cod b₃ )

proof end;

theorem Th30: :: RINGCAT1:30

for b₁ being Universe
for b₂, b₃ being Morphism of (RingCat b₁)
for b₄, b₅ being Element of Morphs (RingObjects b₁) st b₂ = b₄ & b₃ = b₅ holds
( ( dom b₃ = cod b₂ implies dom b₅ = cod b₄ ) & ( dom b₅ = cod b₄ implies dom b₃ = cod b₂ ) & ( dom b₃ = cod b₂ implies [b₅,b₄] in dom (comp (RingObjects b₁)) ) & ( [b₅,b₄] in dom (comp (RingObjects b₁)) implies dom b₃ = cod b₂ ) & ( dom b₃ = cod b₂ implies b₃ * b₂ = b₅ * b₄ ) & ( dom b₂ = dom b₃ implies dom b₄ = dom b₅ ) & ( dom b₄ = dom b₅ implies dom b₂ = dom b₃ ) & ( cod b₂ = cod b₃ implies cod b₄ = cod b₅ ) & ( cod b₄ = cod b₅ implies cod b₂ = cod b₃ ) )

proof end;

Lemma49: for b₁ being Universe
for b₂, b₃ being Morphism of (RingCat b₁) st dom b₃ = cod b₂ holds
( dom (b₃ * b₂) = dom b₂ & cod (b₃ * b₂) = cod b₃ )

proof end;

Lemma50: for b₁ being Universe
for b₂, b₃, b₄ being Morphism of (RingCat b₁) st dom b₄ = cod b₃ & dom b₃ = cod b₂ holds
b₄ * (b₃ * b₂) = (b₄ * b₃) * b₂

proof end;

Lemma51: for b₁ being Universe
for b₂ being Object of (RingCat b₁) holds
( dom (id b₂) = b₂ & cod (id b₂) = b₂ & ( for b₃ being Morphism of (RingCat b₁) st cod b₃ = b₂ holds
(id b₂) * b₃ = b₃ ) & ( for b₃ being Morphism of (RingCat b₁) st dom b₃ = b₂ holds
b₃ * (id b₂) = b₃ ) )

proof end;

registration

let c₁ be Universe;
cluster RingCat a₁ -> strict Category-like ;
coherence

proof end;

end;