:: by Beata Madras

::

:: Received February 14, 1997

:: Copyright (c) 1997-2018 Association of Mizar Users

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;

end;
let o1, o2 be Object of C;

let A be Morphism of o1,o2;

let B be Morphism of o2,o1;

:: deftheorem 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 );

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;
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;

definition

let C be non empty with_units AltCatStr ;

let o1, o2 be Object of C;

let A be Morphism of o1,o2;

end;
let o1, o2 be Object of C;

let A be Morphism of o1,o2;

attr A is retraction means :: ALTCAT_3:def 2

ex B being Morphism of o2,o1 st B is_right_inverse_of A;

ex B being Morphism of o2,o1 st B is_right_inverse_of A;

:: deftheorem 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 );

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;

end;
let o1, o2 be Object of C;

let A be Morphism of o1,o2;

attr A is coretraction means :: ALTCAT_3:def 3

ex B being Morphism of o2,o1 st B is_left_inverse_of A;

ex B being Morphism of o2,o1 st B is_left_inverse_of A;

:: deftheorem 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 );

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

for C being non empty with_units AltCatStr

for o being Object of C holds

( idm o is retraction & idm o is coretraction )

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 that

A1: <^o1,o2^> <> {} and

A2: <^o2,o1^> <> {} ;

let A be Morphism of o1,o2;

assume A3: ( A is retraction & A is coretraction ) ;

ex b_{1} being Morphism of o2,o1 st

( b_{1} is_left_inverse_of A & b_{1} is_right_inverse_of A )

for b_{1}, b_{2} being Morphism of o2,o1 st b_{1} is_left_inverse_of A & b_{1} is_right_inverse_of A & b_{2} is_left_inverse_of A & b_{2} is_right_inverse_of A holds

b_{1} = b_{2}

end;
let o1, o2 be Object of C;

assume that

A1: <^o1,o2^> <> {} and

A2: <^o2,o1^> <> {} ;

let A be Morphism of o1,o2;

assume A3: ( 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 ( it is_left_inverse_of A & it is_right_inverse_of A );

ex b

( b

proof end;

uniqueness for b

b

proof 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 b_{5} being Morphism of o2,o1 holds

( b_{5} = A " iff ( b_{5} is_left_inverse_of A & b_{5} is_right_inverse_of A ) );

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 b

( b

theorem Th2: :: ALTCAT_3:2

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 )

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

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

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;

:: deftheorem 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 ) );

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

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 )

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

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 ) )

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

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 ") )

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;

for o1 being Object of C holds

( <^o1,o1^> <> {} & <^o1,o1^> <> {} & ex A being Morphism of o1,o1 st A is iso )

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 )

end;
let o1, o2 be Object of C;

pred o1,o2 are_iso means :: ALTCAT_3:def 6

( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso );

reflexivity ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso );

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;

:: deftheorem 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 ) );

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

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

for o1, o2, o3 being Object of C st o1,o2 are_iso & o2,o3 are_iso holds

o1,o3 are_iso

proof end;

:: deftheorem 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 );

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 );

:: deftheorem 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 );

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

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

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

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

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

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

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

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

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 :: thesis: for C being non empty with_units AltCatStr

for a being Object of C holds

( idm a is epi & idm a is mono )

for a being Object of C holds

( idm a is epi & idm a is mono )

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

end;
( 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

thus
idm a is mono
:: thesis: verum
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 17

.= C by A1, A2, ALTCAT_1:def 17 ; :: thesis: verum

end;
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 17

.= C by A1, A2, ALTCAT_1:def 17 ; :: 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:20

.= C by A3, A4, ALTCAT_1:20 ; :: thesis: verum

end;
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:20

.= C by A3, A4, ALTCAT_1:20 ; :: thesis: verum

theorem :: ALTCAT_3:13

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 )

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

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 )

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

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

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

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

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

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 )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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;

existence

ex b_{1} being Morphism of o,o st

( b_{1} is mono & b_{1} is epi & b_{1} is retraction & b_{1} is coretraction )

end;
let o be Object of C;

existence

ex b

( b

proof end;

registration

let C be category;

let o be Object of C;

existence

ex b_{1} being Morphism of o,o st

( b_{1} is mono & b_{1} is epi & b_{1} is iso & b_{1} is retraction & b_{1} is coretraction )

end;
let o be Object of C;

existence

ex b

( b

proof end;

registration

let C be category;

let o be Object of C;

let A, B be mono Morphism of o,o;

coherence

A * B is mono

end;
let o be Object of C;

let A, B be mono Morphism of o,o;

coherence

A * B is mono

proof end;

registration

let C be category;

let o be Object of C;

let A, B be epi Morphism of o,o;

coherence

A * B is epi

end;
let o be Object of C;

let A, B be epi Morphism of o,o;

coherence

A * B is epi

proof end;

registration

let C be category;

let o be Object of C;

let A, B be iso Morphism of o,o;

coherence

A * B is iso

end;
let o be Object of C;

let A, B be iso Morphism of o,o;

coherence

A * B is iso

proof end;

registration

let C be category;

let o be Object of C;

let A, B be retraction Morphism of o,o;

coherence

A * B is retraction

end;
let o be Object of C;

let A, B be retraction Morphism of o,o;

coherence

A * B is retraction

proof end;

registration

let C be category;

let o be Object of C;

let A, B be coretraction Morphism of o,o;

coherence

A * B is coretraction

end;
let o be Object of C;

let A, B be coretraction Morphism of o,o;

coherence

A * B is coretraction

proof end;

:: deftheorem 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 ) );

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

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 ) ) )

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

for C being category

for o1, o2 being Object of C st o1 is initial & o2 is initial holds

o1,o2 are_iso

for o1, o2 being Object of C st o1 is initial & o2 is initial holds

o1,o2 are_iso

proof end;

:: deftheorem 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 ) );

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

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 ) ) )

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

for C being category

for o1, o2 being Object of C st o1 is terminal & o2 is terminal holds

o1,o2 are_iso

for o1, o2 being Object of C st o1 is terminal & o2 is terminal holds

o1,o2 are_iso

proof end;

:: deftheorem 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 ) );

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

:: deftheorem 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 );

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

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

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;