:: ALTCAT_3 semantic presentation

definition
let c1 be non empty with_units AltCatStr ;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
let c5 be Morphism of c3,c2;
pred c4 is_left_inverse_of c5 means :Def1: :: ALTCAT_3:def 1
a4 * a5 = idm a3;
end;

:: deftheorem Def1 defines is_left_inverse_of ALTCAT_3:def 1 :
for b1 being non empty with_units AltCatStr
for b2, b3 being object of b1
for b4 being Morphism of b2,b3
for b5 being Morphism of b3,b2 holds
( b4 is_left_inverse_of b5 iff b4 * b5 = idm b3 );

notation
let c1 be non empty with_units AltCatStr ;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
let c5 be Morphism of c3,c2;
synonym c5 is_right_inverse_of c4 for c4 is_left_inverse_of c5;
end;

definition
let c1 be non empty with_units AltCatStr ;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
attr a4 is retraction means :Def2: :: ALTCAT_3:def 2
ex b1 being Morphism of a3,a2 st b1 is_right_inverse_of a4;
end;

:: deftheorem Def2 defines retraction ALTCAT_3:def 2 :
for b1 being non empty with_units AltCatStr
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 holds
( b4 is retraction iff ex b5 being Morphism of b3,b2 st b5 is_right_inverse_of b4 );

definition
let c1 be non empty with_units AltCatStr ;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
attr a4 is coretraction means :Def3: :: ALTCAT_3:def 3
ex b1 being Morphism of a3,a2 st b1 is_left_inverse_of a4;
end;

:: deftheorem Def3 defines coretraction ALTCAT_3:def 3 :
for b1 being non empty with_units AltCatStr
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 holds
( b4 is coretraction iff ex b5 being Morphism of b3,b2 st b5 is_left_inverse_of b4 );

theorem Th1: :: ALTCAT_3:1
for b1 being non empty with_units AltCatStr
for b2 being object of b1 holds
( idm b2 is retraction & idm b2 is coretraction )
proof end;

definition
let c1 be category;
let c2, c3 be object of c1;
assume E5: ( <^c2,c3^> <> {} & <^c3,c2^> <> {} ) ;
let c4 be Morphism of c2,c3;
assume E6: ( c4 is retraction & c4 is coretraction ) ;
func c4 " -> Morphism of a3,a2 means :Def4: :: ALTCAT_3:def 4
( a5 is_left_inverse_of a4 & a5 is_right_inverse_of a4 );
existence
ex b1 being Morphism of c3,c2 st
( b1 is_left_inverse_of c4 & b1 is_right_inverse_of c4 )
proof end;
uniqueness
for b1, b2 being Morphism of c3,c2 st b1 is_left_inverse_of c4 & b1 is_right_inverse_of c4 & b2 is_left_inverse_of c4 & b2 is_right_inverse_of c4 holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines " ALTCAT_3:def 4 :
for b1 being category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 st b4 is retraction & b4 is coretraction holds
for b5 being Morphism of b3,b2 holds
( b5 = b4 " iff ( b5 is_left_inverse_of b4 & b5 is_right_inverse_of b4 ) );

theorem Th2: :: ALTCAT_3:2
for b1 being category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 st b4 is retraction & b4 is coretraction holds
( (b4 " ) * b4 = idm b2 & b4 * (b4 " ) = idm b3 )
proof end;

theorem Th3: :: ALTCAT_3:3
for b1 being category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 st b4 is retraction & b4 is coretraction holds
(b4 " ) " = b4
proof end;

theorem Th4: :: ALTCAT_3:4
for b1 being category
for b2 being object of b1 holds (idm b2) " = idm b2
proof end;

definition
let c1 be category;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
attr a4 is iso means :Def5: :: ALTCAT_3:def 5
( a4 * (a4 " ) = idm a3 & (a4 " ) * a4 = idm a2 );
end;

:: deftheorem Def5 defines iso ALTCAT_3:def 5 :
for b1 being category
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 holds
( b4 is iso iff ( b4 * (b4 " ) = idm b3 & (b4 " ) * b4 = idm b2 ) );

theorem Th5: :: ALTCAT_3:5
for b1 being category
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 st b4 is iso holds
( b4 is retraction & b4 is coretraction )
proof end;

theorem Th6: :: ALTCAT_3:6
for b1 being category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 holds
( b4 is iso iff ( b4 is retraction & b4 is coretraction ) )
proof end;

theorem Th7: :: ALTCAT_3:7
for b1 being category
for b2, b3, b4 being object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st <^b2,b3^> <> {} & <^b3,b4^> <> {} & <^b4,b2^> <> {} & b5 is iso & b6 is iso holds
( b6 * b5 is iso & (b6 * b5) " = (b5 " ) * (b6 " ) )
proof end;

definition
let c1 be category;
let c2, c3 be object of c1;
pred c2,c3 are_iso means :Def6: :: ALTCAT_3:def 6
( <^a2,a3^> <> {} & <^a3,a2^> <> {} & ex b1 being Morphism of a2,a3 st b1 is iso );
reflexivity
for b1 being object of c1 holds
( <^b1,b1^> <> {} & <^b1,b1^> <> {} & ex b2 being Morphism of b1,b1 st b2 is iso )
proof end;
symmetry
for b1, b2 being object of c1 st <^b1,b2^> <> {} & <^b2,b1^> <> {} & ex b3 being Morphism of b1,b2 st b3 is iso holds
( <^b2,b1^> <> {} & <^b1,b2^> <> {} & ex b3 being Morphism of b2,b1 st b3 is iso )
proof end;
end;

:: deftheorem Def6 defines are_iso ALTCAT_3:def 6 :
for b1 being category
for b2, b3 being object of b1 holds
( b2,b3 are_iso iff ( <^b2,b3^> <> {} & <^b3,b2^> <> {} & ex b4 being Morphism of b2,b3 st b4 is iso ) );

theorem Th8: :: ALTCAT_3:8
for b1 being category
for b2, b3, b4 being object of b1 st b2,b3 are_iso & b3,b4 are_iso holds
b2,b4 are_iso
proof end;

definition
let c1 be non empty AltCatStr ;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
attr a4 is mono means :Def7: :: ALTCAT_3:def 7
for b1 being object of a1 st <^b1,a2^> <> {} holds
for b2, b3 being Morphism of b1,a2 st a4 * b2 = a4 * b3 holds
b2 = b3;
end;

:: deftheorem Def7 defines mono ALTCAT_3:def 7 :
for b1 being non empty AltCatStr
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 holds
( b4 is mono iff for b5 being object of b1 st <^b5,b2^> <> {} holds
for b6, b7 being Morphism of b5,b2 st b4 * b6 = b4 * b7 holds
b6 = b7 );

definition
let c1 be non empty AltCatStr ;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
attr a4 is epi means :Def8: :: ALTCAT_3:def 8
for b1 being object of a1 st <^a3,b1^> <> {} holds
for b2, b3 being Morphism of a3,b1 st b2 * a4 = b3 * a4 holds
b2 = b3;
end;

:: deftheorem Def8 defines epi ALTCAT_3:def 8 :
for b1 being non empty AltCatStr
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 holds
( b4 is epi iff for b5 being object of b1 st <^b3,b5^> <> {} holds
for b6, b7 being Morphism of b3,b5 st b6 * b4 = b7 * b4 holds
b6 = b7 );

theorem Th9: :: ALTCAT_3:9
for b1 being non empty transitive associative AltCatStr
for b2, b3, b4 being object of b1 st <^b2,b3^> <> {} & <^b3,b4^> <> {} holds
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st b5 is mono & b6 is mono holds
b6 * b5 is mono
proof end;

theorem Th10: :: ALTCAT_3:10
for b1 being non empty transitive associative AltCatStr
for b2, b3, b4 being object of b1 st <^b2,b3^> <> {} & <^b3,b4^> <> {} holds
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st b5 is epi & b6 is epi holds
b6 * b5 is epi
proof end;

theorem Th11: :: ALTCAT_3:11
for b1 being non empty transitive associative AltCatStr
for b2, b3, b4 being object of b1 st <^b2,b3^> <> {} & <^b3,b4^> <> {} holds
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st b6 * b5 is mono holds
b5 is mono
proof end;

theorem Th12: :: ALTCAT_3:12
for b1 being non empty transitive associative AltCatStr
for b2, b3, b4 being object of b1 st <^b2,b3^> <> {} & <^b3,b4^> <> {} holds
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st b6 * b5 is epi holds
b6 is epi
proof end;

E18: now
let c1 be non empty with_units AltCatStr ;
let c2 be object of c1;
thus idm c2 is epi
proof
let c3 be object of c1; :: according to ALTCAT_3:def 8
assume E19: <^c2,c3^> <> {} ;
let c4, c5 be Morphism of c2,c3;
assume E20: c4 * (idm c2) = c5 * (idm c2) ;
thus c4 = c4 * (idm c2) by E19, ALTCAT_1:def 19
.= c5 by E19, E20, ALTCAT_1:def 19 ;
end;
thus idm c2 is mono
proof
let c3 be object of c1; :: according to ALTCAT_3:def 7
assume E19: <^c3,c2^> <> {} ;
let c4, c5 be Morphism of c3,c2;
assume E20: (idm c2) * c4 = (idm c2) * c5 ;
thus c4 = (idm c2) * c4 by E19, ALTCAT_1:24
.= c5 by E19, E20, ALTCAT_1:24 ;
end;
end;

theorem Th13: :: ALTCAT_3:13
for b1 being non empty set
for b2, b3 being object of (EnsCat b1) st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3
for b5 being Function of b2,b3 st b5 = b4 holds
( b4 is mono iff b5 is one-to-one )
proof end;

theorem Th14: :: ALTCAT_3:14
for b1 being non empty with_non-empty_elements set
for b2, b3 being object of (EnsCat b1) st <^b2,b3^> <> {} holds
for b4 being Morphism of b2,b3
for b5 being Function of b2,b3 st b5 = b4 holds
( b4 is epi iff b5 is onto )
proof end;

theorem Th15: :: ALTCAT_3:15
for b1 being category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 st b4 is retraction holds
b4 is epi
proof end;

theorem Th16: :: ALTCAT_3:16
for b1 being category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 st b4 is coretraction holds
b4 is mono
proof end;

theorem Th17: :: ALTCAT_3:17
for b1 being category
for b2, b3 being object of b1 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
for b4 being Morphism of b2,b3 st b4 is iso holds
( b4 is mono & b4 is epi )
proof end;

theorem Th18: :: ALTCAT_3:18
for b1 being category
for b2, b3, b4 being object of b1 st <^b2,b3^> <> {} & <^b3,b4^> <> {} & <^b4,b2^> <> {} holds
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st b5 is retraction & b6 is retraction holds
b6 * b5 is retraction
proof end;

theorem Th19: :: ALTCAT_3:19
for b1 being category
for b2, b3, b4 being object of b1 st <^b2,b3^> <> {} & <^b3,b4^> <> {} & <^b4,b2^> <> {} holds
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st b5 is coretraction & b6 is coretraction holds
b6 * b5 is coretraction
proof end;

theorem Th20: :: ALTCAT_3:20
for b1 being category
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 st b4 is retraction & b4 is mono & <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
b4 is iso
proof end;

theorem Th21: :: ALTCAT_3:21
for b1 being category
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 st b4 is coretraction & b4 is epi & <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
b4 is iso
proof end;

theorem Th22: :: ALTCAT_3:22
for b1 being category
for b2, b3, b4 being object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st <^b2,b3^> <> {} & <^b3,b4^> <> {} & <^b4,b2^> <> {} & b6 * b5 is retraction holds
b6 is retraction
proof end;

theorem Th23: :: ALTCAT_3:23
for b1 being category
for b2, b3, b4 being object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st <^b2,b3^> <> {} & <^b3,b4^> <> {} & <^b4,b2^> <> {} & b6 * b5 is coretraction holds
b5 is coretraction
proof end;

theorem Th24: :: ALTCAT_3:24
for b1 being category st ( for b2, b3 being object of b1
for b4 being Morphism of b2,b3 holds b4 is retraction ) holds
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 st <^b2,b3^> <> {} & <^b3,b2^> <> {} holds
b4 is iso
proof end;

registration
let c1 be non empty with_units AltCatStr ;
let c2 be object of c1;
cluster retraction coretraction mono epi Element of <^a2,a2^>;
existence
ex b1 being Morphism of c2,c2 st
( b1 is mono & b1 is epi & b1 is retraction & b1 is coretraction )
proof end;
end;

registration
let c1 be category;
let c2 be object of c1;
cluster retraction coretraction iso mono epi Element of <^a2,a2^>;
existence
ex b1 being Morphism of c2,c2 st
( b1 is mono & b1 is epi & b1 is iso & b1 is retraction & b1 is coretraction )
proof end;
end;

registration
let c1 be category;
let c2 be object of c1;
let c3, c4 be mono Morphism of c2,c2;
cluster a3 * a4 -> mono ;
coherence
c3 * c4 is mono
proof end;
end;

registration
let c1 be category;
let c2 be object of c1;
let c3, c4 be epi Morphism of c2,c2;
cluster a3 * a4 -> epi ;
coherence
c3 * c4 is epi
proof end;
end;

registration
let c1 be category;
let c2 be object of c1;
let c3, c4 be iso Morphism of c2,c2;
cluster a3 * a4 -> iso ;
coherence
c3 * c4 is iso
proof end;
end;

registration
let c1 be category;
let c2 be object of c1;
let c3, c4 be retraction Morphism of c2,c2;
cluster a3 * a4 -> retraction ;
coherence
c3 * c4 is retraction
proof end;
end;

registration
let c1 be category;
let c2 be object of c1;
let c3, c4 be coretraction Morphism of c2,c2;
cluster a3 * a4 -> coretraction ;
coherence
c3 * c4 is coretraction
proof end;
end;

definition
let c1 be AltGraph ;
let c2 be object of c1;
attr a2 is initial means :Def9: :: ALTCAT_3:def 9
for b1 being object of a1 ex b2 being Morphism of a2,b1 st
( b2 in <^a2,b1^> & <^a2,b1^> is trivial );
end;

:: deftheorem Def9 defines initial ALTCAT_3:def 9 :
for b1 being AltGraph
for b2 being object of b1 holds
( b2 is initial iff for b3 being object of b1 ex b4 being Morphism of b2,b3 st
( b4 in <^b2,b3^> & <^b2,b3^> is trivial ) );

theorem Th25: :: ALTCAT_3:25
for b1 being AltGraph
for b2 being object of b1 holds
( b2 is initial iff for b3 being object of b1 ex b4 being Morphism of b2,b3 st
( b4 in <^b2,b3^> & ( for b5 being Morphism of b2,b3 st b5 in <^b2,b3^> holds
b4 = b5 ) ) )
proof end;

theorem Th26: :: ALTCAT_3:26
for b1 being category
for b2, b3 being object of b1 st b2 is initial & b3 is initial holds
b2,b3 are_iso
proof end;

definition
let c1 be AltGraph ;
let c2 be object of c1;
attr a2 is terminal means :Def10: :: ALTCAT_3:def 10
for b1 being object of a1 ex b2 being Morphism of b1,a2 st
( b2 in <^b1,a2^> & <^b1,a2^> is trivial );
end;

:: deftheorem Def10 defines terminal ALTCAT_3:def 10 :
for b1 being AltGraph
for b2 being object of b1 holds
( b2 is terminal iff for b3 being object of b1 ex b4 being Morphism of b3,b2 st
( b4 in <^b3,b2^> & <^b3,b2^> is trivial ) );

theorem Th27: :: ALTCAT_3:27
for b1 being AltGraph
for b2 being object of b1 holds
( b2 is terminal iff for b3 being object of b1 ex b4 being Morphism of b3,b2 st
( b4 in <^b3,b2^> & ( for b5 being Morphism of b3,b2 st b5 in <^b3,b2^> holds
b4 = b5 ) ) )
proof end;

theorem Th28: :: ALTCAT_3:28
for b1 being category
for b2, b3 being object of b1 st b2 is terminal & b3 is terminal holds
b2,b3 are_iso
proof end;

definition
let c1 be AltGraph ;
let c2 be object of c1;
attr a2 is _zero means :Def11: :: ALTCAT_3:def 11
( a2 is initial & a2 is terminal );
end;

:: deftheorem Def11 defines _zero ALTCAT_3:def 11 :
for b1 being AltGraph
for b2 being object of b1 holds
( b2 is _zero iff ( b2 is initial & b2 is terminal ) );

theorem Th29: :: ALTCAT_3:29
for b1 being category
for b2, b3 being object of b1 st b2 is _zero & b3 is _zero holds
b2,b3 are_iso
proof end;

definition
let c1 be non empty AltCatStr ;
let c2, c3 be object of c1;
let c4 be Morphism of c2,c3;
attr a4 is _zero means :Def12: :: ALTCAT_3:def 12
for b1 being object of a1 st b1 is _zero holds
for b2 being Morphism of a2,b1
for b3 being Morphism of b1,a3 holds a4 = b3 * b2;
end;

:: deftheorem Def12 defines _zero ALTCAT_3:def 12 :
for b1 being non empty AltCatStr
for b2, b3 being object of b1
for b4 being Morphism of b2,b3 holds
( b4 is _zero iff for b5 being object of b1 st b5 is _zero holds
for b6 being Morphism of b2,b5
for b7 being Morphism of b5,b3 holds b4 = b7 * b6 );

theorem Th30: :: ALTCAT_3:30
for b1 being category
for b2, b3, b4 being object of b1
for b5 being Morphism of b2,b3
for b6 being Morphism of b3,b4 st b5 is _zero & b6 is _zero holds
b6 * b5 is _zero
proof end;