:: ALTCAT_4 semantic presentation

registration

let C be non empty with_units AltCatStr ;
let o be object of C;
cluster <^o,o^> -> non empty ;
coherence by ALTCAT_1:23;

end;

theorem Th1: :: ALTCAT_4:1

for C being category
for o1, o2, o3 being object of C
for v being Morphism of o1,o2
for u being Morphism of o1,o3
for f being Morphism of o2,o3 st u = f * v & (f " ) * f = idm o2 & <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o2^> <> {} holds
v = (f " ) * u

proof end;

theorem Th2: :: ALTCAT_4:2

for C being category
for o2, o3, o1 being object of C
for v being Morphism of o2,o3
for u being Morphism of o1,o3
for f being Morphism of o1,o2 st u = v * f & f * (f " ) = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} holds
v = u * (f " )

proof end;

theorem Th3: :: ALTCAT_4:3

for C being category
for o1, o2 being object of C
for m being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso holds
m " is iso

proof end;

theorem Th4: :: ALTCAT_4:4

for C being non empty with_units AltCatStr
for o being object of C holds
( idm o is epi & idm o is mono )

proof end;

registration

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

end;

registration

let C be category;
let o be object of C;
cluster idm o -> retraction coretraction iso mono epi ;
coherence by ALTCAT_3:6;

end;

theorem :: ALTCAT_4:5

for C being category
for o1, o2 being object of C
for f being Morphism of o1,o2
for g, h being Morphism of o2,o1 st h * f = idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
g = h

proof end;

theorem :: ALTCAT_4:6

for C being category st ( for o1, o2 being object of C
for f being Morphism of o1,o2 holds f is coretraction ) holds
for a, b being object of C
for g being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
g is iso

proof end;

theorem :: ALTCAT_4:7

for C being category
for o1, o2 being object of C
for m, m' being Morphism of o1,o2 st m is _zero & m' is _zero & ex O being object of C st O is _zero holds
m = m'

proof end;

theorem :: ALTCAT_4:8

for C being non empty AltCatStr
for O, A being object of C
for M being Morphism of O,A st O is terminal holds
M is mono

proof end;

theorem :: ALTCAT_4:9

for C being non empty AltCatStr
for O, A being object of C
for M being Morphism of A,O st O is initial holds
M is epi

proof end;

theorem :: ALTCAT_4:10

for C being category
for o2, o1 being object of C st o2 is terminal & o1,o2 are_iso holds
o1 is terminal

proof end;

theorem :: ALTCAT_4:11

for C being category
for o1, o2 being object of C st o1 is initial & o1,o2 are_iso holds
o2 is initial

proof end;

theorem :: ALTCAT_4:12

for C being category
for o1, o2 being object of C st o1 is initial & o2 is terminal & <^o2,o1^> <> {} holds
( o2 is initial & o1 is terminal )

proof end;

theorem Th13: :: ALTCAT_4:13

for A, B being non empty transitive with_units AltCatStr
for F being contravariant Functor of A,B
for a being object of A holds F . (idm a) = idm (F . a)

proof end;

theorem Th14: :: ALTCAT_4:14

for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr of C1,C2 holds
( F is full iff for o1, o2 being object of C1 holds Morph-Map F,o2,o1 is onto )

proof end;

theorem Th15: :: ALTCAT_4:15

for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr of C1,C2 holds
( F is faithful iff for o1, o2 being object of C1 holds Morph-Map F,o2,o1 is one-to-one )

proof end;

theorem Th16: :: ALTCAT_4:16

for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr of C1,C2
for o1, o2 being object of C1
for Fm being Morphism of (F . o1),(F . o2) st <^o1,o2^> <> {} & F is full & F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m

proof end;

theorem Th17: :: ALTCAT_4:17

for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr of C1,C2
for o1, o2 being object of C1
for Fm being Morphism of (F . o2),(F . o1) st <^o1,o2^> <> {} & F is full & F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m

proof end;

theorem Th18: :: ALTCAT_4:18

for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds
F . a is retraction

proof end;

theorem Th19: :: ALTCAT_4:19

proof end;

theorem Th20: :: ALTCAT_4:20

for A, B being category
for F being covariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds
F . a is iso

proof end;

theorem :: ALTCAT_4:21

for A, B being category
for F being covariant Functor of A,B
for o1, o2 being object of A st o1,o2 are_iso holds
F . o1,F . o2 are_iso

proof end;

theorem Th22: :: ALTCAT_4:22

for A, B being non empty transitive with_units AltCatStr
for F being contravariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds
F . a is coretraction

proof end;

theorem Th23: :: ALTCAT_4:23

proof end;

theorem Th24: :: ALTCAT_4:24

for A, B being category
for F being contravariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is iso holds
F . a is iso

proof end;

theorem :: ALTCAT_4:25

for A, B being category
for F being contravariant Functor of A,B
for o1, o2 being object of A st o1,o2 are_iso holds
F . o2,F . o1 are_iso

proof end;

theorem Th26: :: ALTCAT_4:26

for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is retraction holds
a is retraction

proof end;

theorem Th27: :: ALTCAT_4:27

proof end;

theorem Th28: :: ALTCAT_4:28

for A, B being category
for F being covariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is iso holds
a is iso

proof end;

theorem :: ALTCAT_4:29

for A, B being category
for F being covariant Functor of A,B
for o1, o2 being object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o1,F . o2 are_iso holds
o1,o2 are_iso

proof end;

theorem Th30: :: ALTCAT_4:30

for A, B being non empty transitive with_units AltCatStr
for F being contravariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is retraction holds
a is coretraction

proof end;

theorem Th31: :: ALTCAT_4:31

proof end;

theorem Th32: :: ALTCAT_4:32

for A, B being category
for F being contravariant Functor of A,B
for o1, o2 being object of A
for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is iso holds
a is iso

proof end;

theorem :: ALTCAT_4:33

for A, B being category
for F being contravariant Functor of A,B
for o1, o2 being object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o2,F . o1 are_iso holds
o1,o2 are_iso

proof end;

Lm1: now

let C be non empty transitive AltCatStr ; :: thesis:
let p1, p2, p3 be object of C; :: thesis:
assume A1: the Arrows of C . p1,p3 = {} ; :: thesis:
thus [:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] = {} :: thesis:

proof

assume [:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] <> {} ; :: thesis:
then consider k being set such that
A2: k in [:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] by XBOOLE_0:def 1;
consider u1, u2 being set such that
A3: ( u1 in the Arrows of C . p2,p3 & u2 in the Arrows of C . p1,p2 & k = [u1,u2] ) by A2, ZFMISC_1:def 2;
( u1 in <^p2,p3^> & u2 in <^p1,p2^> ) by A3;
then <^p1,p3^> <> {} by ALTCAT_1:def 4;
hence contradiction by A1; :: thesis:

end;

theorem Th34: :: ALTCAT_4:34

for C being AltCatStr
for D being SubCatStr of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D holds
D is full

proof end;

theorem Th35: :: ALTCAT_4:35

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

proof end;

registration

let C be category;
cluster non empty strict full SubCatStr of C;
existence

proof end;

end;

theorem Th36: :: ALTCAT_4:36

for C being category
for B being non empty subcategory of C
for A being non empty subcategory of B holds A is non empty subcategory of C

proof end;

theorem Th37: :: ALTCAT_4:37

for C being non empty transitive AltCatStr
for D being non empty transitive SubCatStr of C
for o1, o2 being object of C
for p1, p2 being object of D
for m being Morphism of o1,o2
for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} holds
( ( m is mono implies n is mono ) & ( m is epi implies n is epi ) )

proof end;

theorem Th38: :: ALTCAT_4:38

for C being category
for D being non empty subcategory of C
for o1, o2 being object of C
for p1, p2 being object of D
for m being Morphism of o1,o2
for m1 being Morphism of o2,o1
for n being Morphism of p1,p2
for n1 being Morphism of p2,p1 st p1 = o1 & p2 = o2 & m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds
( ( m is_left_inverse_of m1 implies n is_left_inverse_of n1 ) & ( n is_left_inverse_of n1 implies m is_left_inverse_of m1 ) & ( m is_right_inverse_of m1 implies n is_right_inverse_of n1 ) & ( n is_right_inverse_of n1 implies m is_right_inverse_of m1 ) )

proof end;

theorem :: ALTCAT_4:39

for C being category
for D being non empty full subcategory of C
for o1, o2 being object of C
for p1, p2 being object of D
for m being Morphism of o1,o2
for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds
( ( m is retraction implies n is retraction ) & ( m is coretraction implies n is coretraction ) & ( m is iso implies n is iso ) )

proof end;

theorem Th40: :: ALTCAT_4:40

for C being category
for D being non empty subcategory of C
for o1, o2 being object of C
for p1, p2 being object of D
for m being Morphism of o1,o2
for n being Morphism of p1,p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds
( ( n is retraction implies m is retraction ) & ( n is coretraction implies m is coretraction ) & ( n is iso implies m is iso ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines AllMono ALTCAT_4:def 1 :

registration

let C be category;
cluster AllMono C -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines AllEpi ALTCAT_4:def 2 :

registration

let C be category;
cluster AllEpi C -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines AllRetr ALTCAT_4:def 3 :

registration

let C be category;
cluster AllRetr C -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines AllCoretr ALTCAT_4:def 4 :

registration

let C be category;
cluster AllCoretr C -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines AllIso ALTCAT_4:def 5 :

registration

let C be category;
cluster AllIso C -> non empty transitive strict id-inheriting ;
coherence

proof end;

end;

theorem Th41: :: ALTCAT_4:41

for C being category holds AllIso C is non empty subcategory of AllRetr C

proof end;

theorem Th42: :: ALTCAT_4:42

for C being category holds AllIso C is non empty subcategory of AllCoretr C

proof end;

theorem Th43: :: ALTCAT_4:43

for C being category holds AllCoretr C is non empty subcategory of AllMono C

proof end;

theorem Th44: :: ALTCAT_4:44

for C being category holds AllRetr C is non empty subcategory of AllEpi C

proof end;

theorem :: ALTCAT_4:45

for C being category st ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds m is mono ) holds
AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllMono C

proof end;

theorem :: ALTCAT_4:46

for C being category st ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds m is epi ) holds
AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllEpi C

proof end;

theorem :: ALTCAT_4:47

for C being category st ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m is retraction & <^o2,o1^> <> {} ) ) holds
AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllRetr C

proof end;

theorem :: ALTCAT_4:48

for C being category st ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m is coretraction & <^o2,o1^> <> {} ) ) holds
AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllCoretr C

proof end;

theorem :: ALTCAT_4:49

for C being category st ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m is iso & <^o2,o1^> <> {} ) ) holds
AltCatStr(# the carrier of C,the Arrows of C,the Comp of C #) = AllIso C

proof end;

theorem Th50: :: ALTCAT_4:50