:: ALTCAT_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
let B be Morphism of o2,o1;
pred A is_left_inverse_of B means :Def1: :: ALTCAT_3:def 1
A * B = idm o2;
end;

:: deftheorem Def1 defines is_left_inverse_of ALTCAT_3:def 1 :
for C being non empty with_units AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o1 holds
( A is_left_inverse_of B iff A * B = idm o2 );

notation
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
let B be Morphism of o2,o1;
synonym B is_right_inverse_of A for A is_left_inverse_of B;
end;

definition
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attr A is retraction means :Def2: :: ALTCAT_3:def 2
 ex B being Morphism of o2,o1 st B is_right_inverse_of A;
end;

:: deftheorem Def2 defines retraction ALTCAT_3:def 2 :
for C being non empty with_units AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is retraction iff ex B being Morphism of o2,o1 st B is_right_inverse_of A );

definition
let C be non empty with_units AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attr A is coretraction means :Def3: :: ALTCAT_3:def 3
 ex B being Morphism of o2,o1 st B is_left_inverse_of A;
end;

:: deftheorem Def3 defines coretraction ALTCAT_3:def 3 :
for C being non empty with_units AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is coretraction iff ex B being Morphism of o2,o1 st B is_left_inverse_of A );

theorem Th1: :: ALTCAT_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty with_units AltCatStr
for o being object of C holds
( idm o is retraction & idm o is coretraction )
proof end;

definition
let C be category;
let o1, o2 be object of C;
assume A1: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) ;
let A be Morphism of o1,o2;
assume A2: ( A is retraction & A is coretraction ) ;
func A " -> Morphism of o2,o1 means :Def4: :: ALTCAT_3:def 4
( it is_left_inverse_of A & it is_right_inverse_of A );
existence
ex b1 being Morphism of o2,o1 st
( b1 is_left_inverse_of A & b1 is_right_inverse_of A )
proof end;
uniqueness
for b1, b2 being Morphism of o2,o1 st b1 is_left_inverse_of A & b1 is_right_inverse_of A & b2 is_left_inverse_of A & b2 is_right_inverse_of A holds
b1 = b2
proof end;
end;

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

theorem Th2: :: ALTCAT_3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
( (A " ) * A = idm o1 & A * (A " ) = idm o2 )
proof end;

theorem Th3: :: ALTCAT_3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction & A is coretraction holds
(A " ) " = A
proof end;

theorem Th4: :: ALTCAT_3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o being object of C holds (idm o) " = idm o
proof end;

definition
let C be category;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attr A is iso means :Def5: :: ALTCAT_3:def 5
( A * (A " ) = idm o2 & (A " ) * A = idm o1 );
end;

:: deftheorem Def5 defines iso ALTCAT_3:def 5 :
for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is iso iff ( A * (A " ) = idm o2 & (A " ) * A = idm o1 ) );

theorem Th5: :: ALTCAT_3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 st A is iso holds
( A is retraction & A is coretraction )
proof end;

theorem Th6: :: ALTCAT_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 holds
( A is iso iff ( A is retraction & A is coretraction ) )
proof end;

theorem Th7: :: ALTCAT_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A " ) * (B " ) )
proof end;

definition
let C be category;
let o1, o2 be object of C;
pred o1,o2 are_iso means :Def6: :: ALTCAT_3:def 6
( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso );
reflexivity
for o1 being object of C holds
( <^o1,o1^> <> {} & <^o1,o1^> <> {} & ex A being Morphism of o1,o1 st A is iso )
proof end;
symmetry
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso holds
( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso )
proof end;
end;

:: deftheorem Def6 defines are_iso ALTCAT_3:def 6 :
for C being category
for o1, o2 being object of C holds
( o1,o2 are_iso iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso ) );

theorem :: ALTCAT_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2, o3 being object of C st o1,o2 are_iso & o2,o3 are_iso holds
o1,o3 are_iso
proof end;

definition
let C be non empty AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attr A is mono means :Def7: :: ALTCAT_3:def 7
for o being object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C;
end;

:: deftheorem Def7 defines mono ALTCAT_3:def 7 :
for C being non empty AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is mono iff for o being object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C );

definition
let C be non empty AltCatStr ;
let o1, o2 be object of C;
let A be Morphism of o1,o2;
attr A is epi means :Def8: :: ALTCAT_3:def 8
for o being object of C st <^o2,o^> <> {} holds
for B, C being Morphism of o2,o st B * A = C * A holds
B = C;
end;

:: deftheorem Def8 defines epi ALTCAT_3:def 8 :
for C being non empty AltCatStr
for o1, o2 being object of C
for A being Morphism of o1,o2 holds
( A is epi iff for o being object of C st <^o2,o^> <> {} holds
for B, C being Morphism of o2,o st B * A = C * A holds
B = C );

theorem Th9: :: ALTCAT_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is mono & B is mono holds
B * A is mono
proof end;

theorem Th10: :: ALTCAT_3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is epi & B is epi holds
B * A is epi
proof end;

theorem :: ALTCAT_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is mono holds
A is mono
proof end;

theorem :: ALTCAT_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty transitive associative AltCatStr
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st B * A is epi holds
B is epi
proof end;

Lm1: now
let C be non empty with_units AltCatStr ; :: thesis: for a being object of C holds
( idm a is epi & idm a is mono )
let a be object of C; :: thesis: ( idm a is epi & idm a is mono )
thus idm a is epi :: thesis: idm a is mono
proof
let o be object of C; :: according to ALTCAT_3:def 8 :: thesis: ( <^a,o^> <> {} implies for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds
B = C )
assume A1: <^a,o^> <> {} ; :: thesis: for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds
B = C
let B, C be Morphism of a,o; :: thesis: ( B * (idm a) = C * (idm a) implies B = C )
assume A2: B * (idm a) = C * (idm a) ; :: thesis: B = C
thus B = B * (idm a) by A1, ALTCAT_1:def 19
.= C by A1, A2, ALTCAT_1:def 19 ; :: thesis: verum
end;
thus idm a is mono :: thesis: verum
proof
let o be object of C; :: according to ALTCAT_3:def 7 :: thesis: ( <^o,a^> <> {} implies for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds
B = C )
assume A3: <^o,a^> <> {} ; :: thesis: for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds
B = C
let B, C be Morphism of o,a; :: thesis: ( (idm a) * B = (idm a) * C implies B = C )
assume A4: (idm a) * B = (idm a) * C ; :: thesis: B = C
thus B = (idm a) * B by A3, ALTCAT_1:24
.= C by A3, A4, ALTCAT_1:24 ; :: thesis: verum
end;
end;

theorem :: ALTCAT_3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is mono iff F is one-to-one )
proof end;

theorem :: ALTCAT_3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty with_non-empty_elements set
for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
proof end;

theorem Th15: :: ALTCAT_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is retraction holds
A is epi
proof end;

theorem Th16: :: ALTCAT_3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is coretraction holds
A is mono
proof end;

theorem :: ALTCAT_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
proof end;

theorem Th18: :: ALTCAT_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is retraction & B is retraction holds
B * A is retraction
proof end;

theorem Th19: :: ALTCAT_3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2, o3 being object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} holds
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st A is coretraction & B is coretraction holds
B * A is coretraction
proof end;

theorem Th20: :: ALTCAT_3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 st A is retraction & A is mono & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
proof end;

theorem :: ALTCAT_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C
for A being Morphism of o1,o2 st A is coretraction & A is epi & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
A is iso
proof end;

theorem :: ALTCAT_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is retraction holds
B is retraction
proof end;

theorem :: ALTCAT_3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2, o3 being object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & B * A is coretraction holds
A is coretraction
proof end;

theorem :: ALTCAT_3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category st ( for o1, o2 being object of C
for A1 being Morphism of o1,o2 holds A1 is retraction ) holds
for a, b being object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
proof end;

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

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

registration
let C be category;
let o be object of C;
let A, B be mono Morphism of o,o;
cluster A * B -> mono ;
coherence
A * B is mono
proof end;
end;

registration
let C be category;
let o be object of C;
let A, B be epi Morphism of o,o;
cluster A * B -> epi ;
coherence
A * B is epi
proof end;
end;

registration
let C be category;
let o be object of C;
let A, B be iso Morphism of o,o;
cluster A * B -> iso ;
coherence
A * B is iso
proof end;
end;

registration
let C be category;
let o be object of C;
let A, B be retraction Morphism of o,o;
cluster A * B -> retraction ;
coherence
A * B is retraction
proof end;
end;

registration
let C be category;
let o be object of C;
let A, B be coretraction Morphism of o,o;
cluster A * B -> coretraction ;
coherence
A * B is coretraction
proof end;
end;

definition
let C be AltGraph ;
let o be object of C;
attr o is initial means :Def9: :: ALTCAT_3:def 9
for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial );
end;

:: deftheorem Def9 defines initial ALTCAT_3:def 9 :
for C being AltGraph
for o being object of C holds
( o is initial iff for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial ) );

theorem :: ALTCAT_3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being AltGraph
for o being object of C holds
( o is initial iff for o1 being object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )
proof end;

theorem Th26: :: ALTCAT_3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st o1 is initial & o2 is initial holds
o1,o2 are_iso
proof end;

definition
let C be AltGraph ;
let o be object of C;
attr o is terminal means :Def10: :: ALTCAT_3:def 10
for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial );
end;

:: deftheorem Def10 defines terminal ALTCAT_3:def 10 :
for C being AltGraph
for o being object of C holds
( o is terminal iff for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & <^o1,o^> is trivial ) );

theorem :: ALTCAT_3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being AltGraph
for o being object of C holds
( o is terminal iff for o1 being object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) )
proof end;

theorem :: ALTCAT_3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st o1 is terminal & o2 is terminal holds
o1,o2 are_iso
proof end;

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

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

theorem :: ALTCAT_3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2 being object of C st o1 is _zero & o2 is _zero holds
o1,o2 are_iso
proof end;

definition
let C be non empty AltCatStr ;
let o1, o2 be object of C;
let M be Morphism of o1,o2;
attr M is _zero means :Def12: :: ALTCAT_3:def 12
for o being object of C st o is _zero holds
for A being Morphism of o1,o
for B being Morphism of o,o2 holds M = B * A;
end;

:: deftheorem Def12 defines _zero ALTCAT_3:def 12 :
for C being non empty AltCatStr
for o1, o2 being object of C
for M being Morphism of o1,o2 holds
( M is _zero iff for o being object of C st o is _zero holds
for A being Morphism of o1,o
for B being Morphism of o,o2 holds M = B * A );

theorem :: ALTCAT_3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being category
for o1, o2, o3 being object of C
for M1 being Morphism of o1,o2
for M2 being Morphism of o2,o3 st M1 is _zero & M2 is _zero holds
M2 * M1 is _zero
proof end;