:: ALTCAT_4 semantic presentation

registration

let c₁ be non empty with_units AltCatStr ;
let c₂ be object of c₁;
cluster <^a₂,a₂^> -> non empty ;
coherence by ALTCAT_1:23;

end;

theorem Th1: :: ALTCAT_4:1

for b₁ being category
for b₂, b₃, b₄ being object of b₁
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₇ = idm b₃ & <^b₂,b₃^> <> {} & <^b₃,b₄^> <> {} & <^b₄,b₃^> <> {} holds
b₅ = (b₇ " ) * b₆

proof end;

theorem Th2: :: ALTCAT_4:2

for b₁ being category
for b₂, b₃, b₄ being object of b₁
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₇ " ) = idm b₂ & <^b₄,b₂^> <> {} & <^b₂,b₄^> <> {} & <^b₂,b₃^> <> {} holds
b₅ = b₆ * (b₇ " )

proof end;

theorem Th3: :: ALTCAT_4:3

for b₁ being category
for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ st <^b₂,b₃^> <> {} & <^b₃,b₂^> <> {} & b₄ is iso holds
b₄ " is iso

proof end;

theorem Th4: :: ALTCAT_4:4

for b₁ being non empty with_units AltCatStr
for b₂ being object of b₁ holds
( idm b₂ is epi & idm b₂ is mono )

proof end;

registration

let c₁ be non empty with_units AltCatStr ;
let c₂ be object of c₁;
cluster idm a₂ -> retraction coretraction mono epi ;
coherence by Th4, ALTCAT_3:1;

end;

registration

let c₁ be category;
let c₂ be object of c₁;
cluster idm a₂ -> retraction coretraction iso mono epi ;
coherence by ALTCAT_3:6;

end;

theorem Th5: :: ALTCAT_4:5

for b₁ being category
for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃
for b₅, b₆ being Morphism of b₃,b₂ st b₆ * b₄ = idm b₂ & b₄ * b₅ = idm b₃ & <^b₂,b₃^> <> {} & <^b₃,b₂^> <> {} holds
b₅ = b₆

proof end;

theorem Th6: :: ALTCAT_4:6

for b₁ being category st ( for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ holds b₄ is coretraction ) holds
for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ st <^b₂,b₃^> <> {} & <^b₃,b₂^> <> {} holds
b₄ is iso

proof end;

theorem Th7: :: ALTCAT_4:7

for b₁ being category
for b₂, b₃ being object of b₁
for b₄, b₅ being Morphism of b₂,b₃ st b₄ is _zero & b₅ is _zero & ex b₆ being object of b₁ st b₆ is _zero holds
b₄ = b₅

proof end;

theorem Th8: :: ALTCAT_4:8

for b₁ being non empty AltCatStr
for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ st b₂ is terminal holds
b₄ is mono

proof end;

theorem Th9: :: ALTCAT_4:9

for b₁ being non empty AltCatStr
for b₂, b₃ being object of b₁
for b₄ being Morphism of b₃,b₂ st b₂ is initial holds
b₄ is epi

proof end;

theorem Th10: :: ALTCAT_4:10

for b₁ being category
for b₂, b₃ being object of b₁ st b₂ is terminal & b₃,b₂ are_iso holds
b₃ is terminal

proof end;

theorem Th11: :: ALTCAT_4:11

for b₁ being category
for b₂, b₃ being object of b₁ st b₂ is initial & b₂,b₃ are_iso holds
b₃ is initial

proof end;

theorem Th12: :: ALTCAT_4:12

for b₁ being category
for b₂, b₃ being object of b₁ st b₂ is initial & b₃ is terminal & <^b₃,b₂^> <> {} holds
( b₃ is initial & b₂ is terminal )

proof end;

theorem Th13: :: ALTCAT_4:13

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being contravariant Functor of b₁,b₂
for b₄ being object of b₁ holds b₃ . (idm b₄) = idm (b₃ . b₄)

proof end;

theorem Th14: :: ALTCAT_4:14

for b₁, b₂ being non empty AltCatStr
for b₃ being Contravariant FunctorStr of b₁,b₂ holds
( b₃ is full iff for b₄, b₅ being object of b₁ holds Morph-Map b₃,b₅,b₄ is onto )

proof end;

theorem Th15: :: ALTCAT_4:15

for b₁, b₂ being non empty AltCatStr
for b₃ being Contravariant FunctorStr of b₁,b₂ holds
( b₃ is faithful iff for b₄, b₅ being object of b₁ holds Morph-Map b₃,b₅,b₄ is one-to-one )

proof end;

theorem Th16: :: ALTCAT_4:16

for b₁, b₂ being non empty AltCatStr
for b₃ being Covariant FunctorStr of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of (b₃ . b₄),(b₃ . b₅) st <^b₄,b₅^> <> {} & b₃ is full & b₃ is feasible holds
ex b₇ being Morphism of b₄,b₅ st b₆ = b₃ . b₇

proof end;

theorem Th17: :: ALTCAT_4:17

for b₁, b₂ being non empty AltCatStr
for b₃ being Contravariant FunctorStr of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of (b₃ . b₅),(b₃ . b₄) st <^b₄,b₅^> <> {} & b₃ is full & b₃ is feasible holds
ex b₇ being Morphism of b₄,b₅ st b₆ = b₃ . b₇

proof end;

theorem Th18: :: ALTCAT_4:18

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being covariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₆ is retraction holds
b₃ . b₆ is retraction

proof end;

theorem Th19: :: ALTCAT_4:19

proof end;

theorem Th20: :: ALTCAT_4:20

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₆ is iso holds
b₃ . b₆ is iso

proof end;

theorem Th21: :: ALTCAT_4:21

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂
for b₄, b₅ being object of b₁ st b₄,b₅ are_iso holds
b₃ . b₄,b₃ . b₅ are_iso

proof end;

theorem Th22: :: ALTCAT_4:22

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being contravariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₆ is retraction holds
b₃ . b₆ is coretraction

proof end;

theorem Th23: :: ALTCAT_4:23

proof end;

theorem Th24: :: ALTCAT_4:24

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₆ is iso holds
b₃ . b₆ is iso

proof end;

theorem Th25: :: ALTCAT_4:25

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂
for b₄, b₅ being object of b₁ st b₄,b₅ are_iso holds
b₃ . b₅,b₃ . b₄ are_iso

proof end;

theorem Th26: :: ALTCAT_4:26

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being covariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st b₃ is full & b₃ is faithful & <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₃ . b₆ is retraction holds
b₆ is retraction

proof end;

theorem Th27: :: ALTCAT_4:27

proof end;

theorem Th28: :: ALTCAT_4:28

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st b₃ is full & b₃ is faithful & <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₃ . b₆ is iso holds
b₆ is iso

proof end;

theorem Th29: :: ALTCAT_4:29

for b₁, b₂ being category
for b₃ being covariant Functor of b₁,b₂
for b₄, b₅ being object of b₁ st b₃ is full & b₃ is faithful & <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₃ . b₄,b₃ . b₅ are_iso holds
b₄,b₅ are_iso

proof end;

theorem Th30: :: ALTCAT_4:30

for b₁, b₂ being non empty transitive with_units AltCatStr
for b₃ being contravariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st b₃ is full & b₃ is faithful & <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₃ . b₆ is retraction holds
b₆ is coretraction

proof end;

theorem Th31: :: ALTCAT_4:31

proof end;

theorem Th32: :: ALTCAT_4:32

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂
for b₄, b₅ being object of b₁
for b₆ being Morphism of b₄,b₅ st b₃ is full & b₃ is faithful & <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₃ . b₆ is iso holds
b₆ is iso

proof end;

theorem Th33: :: ALTCAT_4:33

for b₁, b₂ being category
for b₃ being contravariant Functor of b₁,b₂
for b₄, b₅ being object of b₁ st b₃ is full & b₃ is faithful & <^b₄,b₅^> <> {} & <^b₅,b₄^> <> {} & b₃ . b₅,b₃ . b₄ are_iso holds
b₄,b₅ are_iso

proof end;

E22: now

let c₁ be non empty transitive AltCatStr ;
let c₂, c₃, c₄ be object of c₁;
assume E23: the Arrows of c₁ . c₂,c₄ = {} ;
thus [:(the Arrows of c₁ . c₃,c₄),(the Arrows of c₁ . c₂,c₃):] = {}

proof

assume [:(the Arrows of c₁ . c₃,c₄),(the Arrows of c₁ . c₂,c₃):] <> {} ;
then consider c₅ being set such that
E24: c₅ in [:(the Arrows of c₁ . c₃,c₄),(the Arrows of c₁ . c₂,c₃):] by XBOOLE_0:def 1;
consider c₆, c₇ being set such that
E25: ( c₆ in the Arrows of c₁ . c₃,c₄ & c₇ in the Arrows of c₁ . c₂,c₃ & c₅ = [c₆,c₇] ) by E24, ZFMISC_1:def 2;
( c₆ in <^c₃,c₄^> & c₇ in <^c₂,c₃^> ) by E25;
then <^c₂,c₄^> <> {} by ALTCAT_1:def 4;
hence contradiction by E23;

end;

theorem Th34: :: ALTCAT_4:34

for b₁ being AltCatStr
for b₂ being SubCatStr of b₁ st the carrier of b₁ = the carrier of b₂ & the Arrows of b₁ = the Arrows of b₂ holds
b₂ is full

proof end;

theorem Th35: :: ALTCAT_4:35

for b₁ being non empty with_units AltCatStr
for b₂ being SubCatStr of b₁ st the carrier of b₁ = the carrier of b₂ & the Arrows of b₁ = the Arrows of b₂ holds
( b₂ is full & b₂ is id-inheriting )

proof end;

registration

let c₁ be category;
cluster non empty strict full SubCatStr of a₁;
existence

proof end;

end;

theorem Th36: :: ALTCAT_4:36

for b₁ being category
for b₂ being non empty subcategory of b₁
for b₃ being non empty subcategory of b₂ holds b₃ is non empty subcategory of b₁

proof end;

theorem Th37: :: ALTCAT_4:37

for b₁ being non empty transitive AltCatStr
for b₂ being non empty transitive SubCatStr of b₁
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂
for b₇ being Morphism of b₃,b₄
for b₈ being Morphism of b₅,b₆ st b₅ = b₃ & b₆ = b₄ & b₇ = b₈ & <^b₅,b₆^> <> {} holds
( ( b₇ is mono implies b₈ is mono ) & ( b₇ is epi implies b₈ is epi ) )

proof end;

theorem Th38: :: ALTCAT_4:38

for b₁ being category
for b₂ being non empty subcategory of b₁
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂
for b₇ being Morphism of b₃,b₄
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₉ & b₈ = b₁₀ & <^b₅,b₆^> <> {} & <^b₆,b₅^> <> {} holds
( ( b₇ is_left_inverse_of b₈ implies b₉ is_left_inverse_of b₁₀ ) & ( b₉ is_left_inverse_of b₁₀ implies b₇ is_left_inverse_of b₈ ) & ( b₇ is_right_inverse_of b₈ implies b₉ is_right_inverse_of b₁₀ ) & ( b₉ is_right_inverse_of b₁₀ implies b₇ is_right_inverse_of b₈ ) )

proof end;

theorem Th39: :: ALTCAT_4:39

for b₁ being category
for b₂ being non empty full subcategory of b₁
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂
for b₇ being Morphism of b₃,b₄
for b₈ being Morphism of b₅,b₆ st b₅ = b₃ & b₆ = b₄ & b₇ = b₈ & <^b₅,b₆^> <> {} & <^b₆,b₅^> <> {} holds
( ( b₇ is retraction implies b₈ is retraction ) & ( b₇ is coretraction implies b₈ is coretraction ) & ( b₇ is iso implies b₈ is iso ) )

proof end;

theorem Th40: :: ALTCAT_4:40

for b₁ being category
for b₂ being non empty subcategory of b₁
for b₃, b₄ being object of b₁
for b₅, b₆ being object of b₂
for b₇ being Morphism of b₃,b₄
for b₈ being Morphism of b₅,b₆ st b₅ = b₃ & b₆ = b₄ & b₇ = b₈ & <^b₅,b₆^> <> {} & <^b₆,b₅^> <> {} holds
( ( b₈ is retraction implies b₇ is retraction ) & ( b₈ is coretraction implies b₇ is coretraction ) & ( b₈ is iso implies b₇ is iso ) )

proof end;

definition

let c₁ be category;
func AllMono c₁ -> non empty transitive strict SubCatStr of a₁ means :Def1: :: ALTCAT_4:def 1
( the carrier of a₂ = the carrier of a₁ & the Arrows of a₂ cc= the Arrows of a₁ & ( for b₁, b₂ being object of a₁
for b₃ being Morphism of b₁,b₂ holds
( b₃ in the Arrows of a₂ . b₁,b₂ iff ( <^b₁,b₂^> <> {} & b₃ is mono ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines AllMono ALTCAT_4:def 1 :

registration

let c₁ be category;
cluster AllMono a₁ -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

let c₁ be category;
func AllEpi c₁ -> non empty transitive strict SubCatStr of a₁ means :Def2: :: ALTCAT_4:def 2
( the carrier of a₂ = the carrier of a₁ & the Arrows of a₂ cc= the Arrows of a₁ & ( for b₁, b₂ being object of a₁
for b₃ being Morphism of b₁,b₂ holds
( b₃ in the Arrows of a₂ . b₁,b₂ iff ( <^b₁,b₂^> <> {} & b₃ is epi ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines AllEpi ALTCAT_4:def 2 :

registration

let c₁ be category;
cluster AllEpi a₁ -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

let c₁ be category;
func AllRetr c₁ -> non empty transitive strict SubCatStr of a₁ means :Def3: :: ALTCAT_4:def 3
( the carrier of a₂ = the carrier of a₁ & the Arrows of a₂ cc= the Arrows of a₁ & ( for b₁, b₂ being object of a₁
for b₃ being Morphism of b₁,b₂ holds
( b₃ in the Arrows of a₂ . b₁,b₂ iff ( <^b₁,b₂^> <> {} & <^b₂,b₁^> <> {} & b₃ is retraction ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines AllRetr ALTCAT_4:def 3 :

registration

let c₁ be category;
cluster AllRetr a₁ -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

let c₁ be category;
func AllCoretr c₁ -> non empty transitive strict SubCatStr of a₁ means :Def4: :: ALTCAT_4:def 4
( the carrier of a₂ = the carrier of a₁ & the Arrows of a₂ cc= the Arrows of a₁ & ( for b₁, b₂ being object of a₁
for b₃ being Morphism of b₁,b₂ holds
( b₃ in the Arrows of a₂ . b₁,b₂ iff ( <^b₁,b₂^> <> {} & <^b₂,b₁^> <> {} & b₃ is coretraction ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines AllCoretr ALTCAT_4:def 4 :

registration

let c₁ be category;
cluster AllCoretr a₁ -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

let c₁ be category;
func AllIso c₁ -> non empty transitive strict SubCatStr of a₁ means :Def5: :: ALTCAT_4:def 5
( the carrier of a₂ = the carrier of a₁ & the Arrows of a₂ cc= the Arrows of a₁ & ( for b₁, b₂ being object of a₁
for b₃ being Morphism of b₁,b₂ holds
( b₃ in the Arrows of a₂ . b₁,b₂ iff ( <^b₁,b₂^> <> {} & <^b₂,b₁^> <> {} & b₃ is iso ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines AllIso ALTCAT_4:def 5 :

registration

let c₁ be category;
cluster AllIso a₁ -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

theorem Th41: :: ALTCAT_4:41

for b₁ being category holds AllIso b₁ is non empty subcategory of AllRetr b₁

proof end;

theorem Th42: :: ALTCAT_4:42

for b₁ being category holds AllIso b₁ is non empty subcategory of AllCoretr b₁

proof end;

theorem Th43: :: ALTCAT_4:43

for b₁ being category holds AllCoretr b₁ is non empty subcategory of AllMono b₁

proof end;

theorem Th44: :: ALTCAT_4:44

for b₁ being category holds AllRetr b₁ is non empty subcategory of AllEpi b₁

proof end;

theorem Th45: :: ALTCAT_4:45

for b₁ being category st ( for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ holds b₄ is mono ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AllMono b₁

proof end;

theorem Th46: :: ALTCAT_4:46

for b₁ being category st ( for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ holds b₄ is epi ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AllEpi b₁

proof end;

theorem Th47: :: ALTCAT_4:47

for b₁ being category st ( for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ holds
( b₄ is retraction & <^b₃,b₂^> <> {} ) ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AllRetr b₁

proof end;

theorem Th48: :: ALTCAT_4:48

for b₁ being category st ( for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ holds
( b₄ is coretraction & <^b₃,b₂^> <> {} ) ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AllCoretr b₁

proof end;

theorem Th49: :: ALTCAT_4:49

for b₁ being category st ( for b₂, b₃ being object of b₁
for b₄ being Morphism of b₂,b₃ holds
( b₄ is iso & <^b₃,b₂^> <> {} ) ) holds
AltCatStr(# the carrier of b₁,the Arrows of b₁,the Comp of b₁ #) = AllIso b₁

proof end;

theorem Th50: :: ALTCAT_4:50

for b₁ being category
for b₂, b₃ being object of (AllMono b₁)
for b₄ being Morphism of b₂,b₃ st <^b₂,b₃^> <> {} holds
b₄ is mono

proof end;

theorem Th51: :: ALTCAT_4:51

for b₁ being category
for b₂, b₃ being object of (AllEpi b₁)
for b₄ being Morphism of b₂,b₃ st <^b₂,b₃^> <> {} holds
b₄ is epi

proof end;

theorem Th52: :: ALTCAT_4:52

for b₁ being category
for b₂, b₃ being object of (AllIso b₁)
for b₄ being Morphism of b₂,b₃ st <^b₂,b₃^> <> {} holds
( b₄ is iso & b₄ " in <^b₃,b₂^> )

proof end;

theorem Th53: :: ALTCAT_4:53

for b₁ being category holds AllMono (AllMono b₁) = AllMono b₁

proof end;

theorem Th54: :: ALTCAT_4:54

for b₁ being category holds AllEpi (AllEpi b₁) = AllEpi b₁

proof end;

theorem Th55: :: ALTCAT_4:55

for b₁ being category holds AllIso (AllIso b₁) = AllIso b₁

proof end;

theorem Th56: :: ALTCAT_4:56

for b₁ being category holds AllIso (AllMono b₁) = AllIso b₁

proof end;

theorem Th57: :: ALTCAT_4:57

for b₁ being category holds AllIso (AllEpi b₁) = AllIso b₁

proof end;

theorem Th58: :: ALTCAT_4:58

for b₁ being category holds AllIso (AllRetr b₁) = AllIso b₁

proof end;

theorem Th59: :: ALTCAT_4:59

for b₁ being category holds AllIso (AllCoretr b₁) = AllIso b₁

proof end;