:: MODCAT_1 semantic presentation

definition

let c₁ be Ring;
mode LeftMod_DOMAIN of c₁ -> non empty set means :Def1: :: MODCAT_1:def 1
for b₁ being Element of a₂ holds b₁ is strict LeftMod of a₁;
existence

proof end;

end;

:: deftheorem Def1 defines LeftMod_DOMAIN MODCAT_1:def 1 :

definition

let c₁ be Ring;
let c₂ be LeftMod_DOMAIN of c₁;
redefine mode Element as Element of c₂ -> LeftMod of a₁;
coherence by Def1;

end;

registration

let c₁ be Ring;
let c₂ be LeftMod_DOMAIN of c₁;
cluster strict Element of a₂;
existence

proof end;

end;

definition

let c₁ be Ring;
mode LModMorphism_DOMAIN of c₁ -> non empty set means :Def2: :: MODCAT_1:def 2
for b₁ being Element of a₂ holds b₁ is strict LModMorphism of a₁;
existence

proof end;

end;

:: deftheorem Def2 defines LModMorphism_DOMAIN MODCAT_1:def 2 :

definition

let c₁ be Ring;
let c₂ be LModMorphism_DOMAIN of c₁;
redefine mode Element as Element of c₂ -> LModMorphism of a₁;
coherence by Def2;

end;

registration

let c₁ be Ring;
let c₂ be LModMorphism_DOMAIN of c₁;
cluster strict Element of a₂;
existence

proof end;

end;

theorem Th1: :: MODCAT_1:1

canceled;

theorem Th2: :: MODCAT_1:2

canceled;

theorem Th3: :: MODCAT_1:3

for b₁ being Ring
for b₂ being strict LModMorphism of b₁ holds {b₂} is LModMorphism_DOMAIN of b₁

proof end;

definition

let c₁ be Ring;
let c₂, c₃ be LeftMod of c₁;
mode LModMorphism_DOMAIN of c₂,c₃ -> LModMorphism_DOMAIN of a₁ means :Def3: :: MODCAT_1:def 3
for b₁ being Element of a₄ holds b₁ is strict Morphism of a₂,a₃;
existence

proof end;

end;

:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def 3 :

theorem Th4: :: MODCAT_1:4

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

proof end;

theorem Th5: :: MODCAT_1:5

for b₁ being Ring
for b₂, b₃ being LeftMod of b₁
for b₄ being strict Morphism of b₂,b₃ holds {b₄} is LModMorphism_DOMAIN of b₂,b₃

proof end;

definition

let c₁ be Ring;
let c₂, c₃ be LeftMod of c₁;
func Morphs c₂,c₃ -> LModMorphism_DOMAIN of a₂,a₃ means :Def4: :: MODCAT_1:def 4
for b₁ being set holds
( b₁ in a₄ iff b₁ is strict Morphism of a₂,a₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Morphs MODCAT_1:def 4 :

definition

let c₁ be Ring;
let c₂, c₃ be LeftMod of c₁;
let c₄ be LModMorphism_DOMAIN of c₂,c₃;
redefine mode Element as Element of c₄ -> Morphism of a₂,a₃;
coherence by Def3;

end;

definition

let c₁, c₂ be set ;
let c₃ be Ring;
pred GO c₁,c₂,c₃ means :Def5: :: MODCAT_1:def 5
ex b₁, b₂ being set st
( a₁ = [b₁,b₂] & ex b₃ being strict LeftMod of a₃ st
( a₂ = b₃ & b₁ = LoopStr(# the carrier of b₃,the add of b₃,the Zero of b₃ #) & b₂ = the lmult of b₃ ) );

end;

:: deftheorem Def5 defines GO MODCAT_1:def 5 :

theorem Th6: :: MODCAT_1:6

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

proof end;

theorem Th7: :: MODCAT_1:7

for b₁ being Ring
for b₂ being Universe ex b₃ being set st
( b₃ in { [b₄,b₅] where B is Element of GroupObjects b₂, B is Element of Funcs [:the carrier of b₁,{{} }:],{{} } : verum } & GO b₃, TrivialLMod b₁,b₁ )

proof end;

definition

let c₁ be Universe;
let c₂ be Ring;
func LModObjects c₁,c₂ -> set means :Def6: :: MODCAT_1:def 6
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being set st
( b₂ in { [b₃,b₄] where B is Element of GroupObjects a₁, B is Element of Funcs [:the carrier of a₂,{{} }:],{{} } : verum } & GO b₂,b₁,a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines LModObjects MODCAT_1:def 6 :

theorem Th8: :: MODCAT_1:8

for b₁ being Universe
for b₂ being Ring holds TrivialLMod b₂ in LModObjects b₁,b₂

proof end;

registration

let c₁ be Universe;
let c₂ be Ring;
cluster LModObjects a₁,a₂ -> non empty ;
coherence by Th8;

end;

theorem Th9: :: MODCAT_1:9

for b₁ being Universe
for b₂ being Ring
for b₃ being Element of LModObjects b₁,b₂ holds b₃ is strict LeftMod of b₂

proof end;

definition

let c₁ be Universe;
let c₂ be Ring;
redefine func LModObjects as LModObjects c₁,c₂ -> LeftMod_DOMAIN of a₂;
coherence

proof end;

end;

definition

let c₁ be Ring;
let c₂ be LeftMod_DOMAIN of c₁;
func Morphs c₂ -> LModMorphism_DOMAIN of a₁ means :Def7: :: MODCAT_1:def 7
for b₁ being set holds
( b₁ in a₃ iff ex b₂, b₃ being strict Element of a₂ st b₁ is strict Morphism of b₂,b₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Morphs MODCAT_1:def 7 :

definition

let c₁ be Ring;
let c₂ be LeftMod_DOMAIN of c₁;
let c₃ be Element of Morphs c₂;
func dom' c₃ -> Element of a₂ equals :: MODCAT_1:def 8
dom a₃;
coherence

proof end;

func cod' c₃ -> Element of a₂ equals :: MODCAT_1:def 9
cod a₃;
coherence

proof end;

end;

:: deftheorem Def8 defines dom' MODCAT_1:def 8 :

:: deftheorem Def9 defines cod' MODCAT_1:def 9 :

definition

let c₁ be Ring;
let c₂ be LeftMod_DOMAIN of c₁;
let c₃ be Element of c₂;
func ID c₃ -> strict Element of Morphs a₂ equals :: MODCAT_1:def 10
ID a₃;
coherence

proof end;

end;

:: deftheorem Def10 defines ID MODCAT_1:def 10 :

definition

let c₁ be Ring;
let c₂ be LeftMod_DOMAIN of c₁;
func dom c₂ -> Function of Morphs a₂,a₂ means :Def11: :: MODCAT_1:def 11
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 :Def12: :: MODCAT_1:def 12
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 :Def13: :: MODCAT_1:def 13
for b₁ being Element of a₂ holds a₃ . b₁ = ID b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines dom MODCAT_1:def 11 :

:: deftheorem Def12 defines cod MODCAT_1:def 12 :

:: deftheorem Def13 defines ID MODCAT_1:def 13 :

theorem Th10: :: MODCAT_1:10

for b₁ being Ring
for b₂ being LeftMod_DOMAIN of b₁
for b₃, b₄ being Element of Morphs b₂ st dom' b₃ = cod' b₄ holds
ex b₅, b₆, b₇ being strict Element of b₂ st
( b₃ is Morphism of b₆,b₇ & b₄ is Morphism of b₅,b₆ )

proof end;

theorem Th11: :: MODCAT_1:11

for b₁ being Ring
for b₂ being LeftMod_DOMAIN of b₁
for b₃, b₄ being Element of Morphs b₂ st dom' b₃ = cod' b₄ holds
b₃ * b₄ in Morphs b₂

proof end;

theorem Th12: :: MODCAT_1:12

for b₁ being Ring
for b₂ being LeftMod_DOMAIN of b₁
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;
let c₂ be LeftMod_DOMAIN of c₁;
func comp c₂ -> PartFunc of [:(Morphs a₂),(Morphs a₂):], Morphs a₂ means :Def14: :: MODCAT_1:def 14
( ( 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 Def14 defines comp MODCAT_1:def 14 :

theorem Th13: :: MODCAT_1:13

for b₁ being Ring
for b₂ being LeftMod_DOMAIN of b₁
for b₃, b₄ being Element of Morphs b₂ holds
( [b₃,b₄] in dom (comp b₂) iff dom b₃ = cod b₄ )

proof end;

definition

let c₁ be Universe;
let c₂ be Ring;
func LModCat c₁,c₂ -> strict CatStr equals :: MODCAT_1:def 15
CatStr(# (LModObjects a₁,a₂),(Morphs (LModObjects a₁,a₂)),(dom (LModObjects a₁,a₂)),(cod (LModObjects a₁,a₂)),(comp (LModObjects a₁,a₂)),(ID (LModObjects a₁,a₂)) #);
coherence ;

end;

:: deftheorem Def15 defines LModCat MODCAT_1:def 15 :

theorem Th14: :: MODCAT_1:14

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

proof end;

theorem Th15: :: MODCAT_1:15

for b₁ being Universe
for b₂ being Ring
for b₃ being Morphism of (LModCat b₁,b₂)
for b₄ being Element of Morphs (LModObjects b₁,b₂)
for b₅ being Object of (LModCat b₁,b₂)
for b₆ being Element of LModObjects b₁,b₂ holds
( b₃ is strict Element of Morphs (LModObjects b₁,b₂) & b₄ is Morphism of (LModCat b₁,b₂) & b₅ is strict Element of LModObjects b₁,b₂ & b₆ is Object of (LModCat b₁,b₂) )

proof end;

theorem Th16: :: MODCAT_1:16

for b₁ being Universe
for b₂ being Ring
for b₃ being Object of (LModCat b₁,b₂)
for b₄ being Element of LModObjects b₁,b₂ st b₃ = b₄ holds
id b₃ = ID b₄

proof end;

theorem Th17: :: MODCAT_1:17

for b₁ being Universe
for b₂ being Ring
for b₃ being Morphism of (LModCat b₁,b₂)
for b₄ being Element of Morphs (LModObjects b₁,b₂) st b₃ = b₄ holds
( dom b₃ = dom b₄ & cod b₃ = cod b₄ )

proof end;

theorem Th18: :: MODCAT_1:18

for b₁ being Universe
for b₂ being Ring
for b₃, b₄ being Morphism of (LModCat b₁,b₂)
for b₅, b₆ being Element of Morphs (LModObjects b₁,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 (LModObjects b₁,b₂)) ) & ( [b₆,b₅] in dom (comp (LModObjects b₁,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;

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

proof end;

Lemma28: for b₁ being Universe
for b₂ being Ring
for b₃, b₄, b₅ being Morphism of (LModCat b₁,b₂) st dom b₅ = cod b₄ & dom b₄ = cod b₃ holds
b₅ * (b₄ * b₃) = (b₅ * b₄) * b₃

proof end;

Lemma29: for b₁ being Universe
for b₂ being Ring
for b₃ being Object of (LModCat b₁,b₂) holds
( dom (id b₃) = b₃ & cod (id b₃) = b₃ & ( for b₄ being Morphism of (LModCat b₁,b₂) st cod b₄ = b₃ holds
(id b₃) * b₄ = b₄ ) & ( for b₄ being Morphism of (LModCat b₁,b₂) st dom b₄ = b₃ holds
b₄ * (id b₃) = b₄ ) )

proof end;

registration

let c₁ be Universe;
let c₂ be Ring;
cluster LModCat a₁,a₂ -> strict Category-like ;
coherence

proof end;

end;