:: On the Categories Without Uniqueness of { \bf cod } and { \bf dom } . Some Properties of the Morphisms and the Functors
:: by Artur Korni{\l}owicz
::
:: Received October 3, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

registration
let C be non empty with_units AltCatStr ;
let o be object of C;
cluster<^o,o^> ->  non empty ;
coherence
 not <^o,o^> is empty by ALTCAT_1:19;
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 &amp; (f ") * f = idm o2 &amp; <^o1,o2^> <> {} &amp; <^o2,o3^> <> {} &amp; <^o3,o2^> <> {} holds
v = (f ") * u
proofend;

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 &amp; f * (f ") = idm o2 &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; <^o2,o3^> <> {} holds
v = u * (f ")
proofend;

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^> <> {} &amp; <^o2,o1^> <> {} &amp; m is iso holds
m " is iso
proofend;

theorem Th4: :: ALTCAT_4:4
for C being non empty with_units AltCatStr
for o being object of C holds
( idm o is epi &amp; idm o is mono )
proofend;

registration
let C be non empty with_units AltCatStr ;
let o be object of C;
cluster idm o ->  retraction coretraction mono epi ;
coherence
 ( idm o is epi &amp; idm o is mono &amp; idm o is retraction &amp; idm o is coretraction ) by Th4, ALTCAT_3:1;
end;

registration
let C be category;
let o be object of C;
cluster idm o ->  iso ;
coherence
 idm o is iso 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 &amp; f * g = idm o2 &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} holds
g = h
proofend;

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^> <> {} &amp; <^b,a^> <> {} holds
g is iso
proofend;

begin

theorem :: ALTCAT_4:7
for C being category
for o1, o2 being object of C
for m, m9 being Morphism of o1,o2 st m is _zero &amp; m9 is _zero &amp; ex O being object of C st O is _zero holds
m = m9
proofend;

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

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

theorem :: ALTCAT_4:10
for C being category
for o2, o1 being object of C st o2 is terminal &amp; o1,o2 are_iso holds
o1 is terminal
proofend;

theorem :: ALTCAT_4:11
for C being category
for o1, o2 being object of C st o1 is initial &amp; o1,o2 are_iso holds
o2 is initial
proofend;

theorem :: ALTCAT_4:12
for C being category
for o1, o2 being object of C st o1 is initial &amp; o2 is terminal &amp; <^o2,o1^> <> {} holds
( o2 is initial &amp; o1 is terminal )
proofend;

begin

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

theorem Th14: :: ALTCAT_4:14
for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr over C1,C2 holds
( F is full iff for o1, o2 being object of C1 holds Morph-Map (F,o2,o1) is onto )
proofend;

theorem Th15: :: ALTCAT_4:15
for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr over C1,C2 holds
( F is faithful iff for o1, o2 being object of C1 holds Morph-Map (F,o2,o1) is one-to-one )
proofend;

theorem Th16: :: ALTCAT_4:16
for C1, C2 being non empty AltCatStr
for F being Covariant FunctorStr over C1,C2
for o1, o2 being object of C1
for Fm being Morphism of (F . o1),(F . o2) st <^o1,o2^> <> {} &amp; F is full &amp; F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m
proofend;

theorem Th17: :: ALTCAT_4:17
for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr over C1,C2
for o1, o2 being object of C1
for Fm being Morphism of (F . o2),(F . o1) st <^o1,o2^> <> {} &amp; F is full &amp; F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m
proofend;

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^> <> {} &amp; <^o2,o1^> <> {} &amp; a is retraction holds
F . a is retraction
proofend;

theorem Th19: :: ALTCAT_4:19
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^> <> {} &amp; <^o2,o1^> <> {} &amp; a is coretraction holds
F . a is coretraction
proofend;

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^> <> {} &amp; <^o2,o1^> <> {} &amp; a is iso holds
F . a is iso
proofend;

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

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^> <> {} &amp; <^o2,o1^> <> {} &amp; a is retraction holds
F . a is coretraction
proofend;

theorem Th23: :: ALTCAT_4:23
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^> <> {} &amp; <^o2,o1^> <> {} &amp; a is coretraction holds
F . a is retraction
proofend;

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^> <> {} &amp; <^o2,o1^> <> {} &amp; a is iso holds
F . a is iso
proofend;

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

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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . a is retraction holds
a is retraction
proofend;

theorem Th27: :: ALTCAT_4:27
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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . a is coretraction holds
a is coretraction
proofend;

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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . a is iso holds
a is iso
proofend;

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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . o1,F . o2 are_iso holds
o1,o2 are_iso
proofend;

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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . a is retraction holds
a is coretraction
proofend;

theorem Th31: :: ALTCAT_4:31
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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . a is coretraction holds
a is retraction
proofend;

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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . a is iso holds
a is iso
proofend;

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 &amp; F is faithful &amp; <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; F . o2,F . o1 are_iso holds
o1,o2 are_iso
proofend;

Lm1: now__::_thesis:_for_C_being_non_empty_transitive_AltCatStr_
for_p1,_p2,_p3_being_object_of_C_st_the_Arrows_of_C_._(p1,p3)_=_{}_holds_
[:(_the_Arrows_of_C_._(p2,p3)),(_the_Arrows_of_C_._(p1,p2)):]_=_{}
let C be non empty transitive AltCatStr ; ::_thesis: for p1, p2, p3 being object of C st the Arrows of C . (p1,p3) = {} holds
[:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {}
let p1, p2, p3 be object of C; ::_thesis: ( the Arrows of C . (p1,p3) = {} implies [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} )
assume A1: the Arrows of C . (p1,p3) = {} ; ::_thesis: [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {}
thus  [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] = {} ::_thesis: verum
proof
assume  [:( the Arrows of C . (p2,p3)),( the Arrows of C . (p1,p2)):] <> {} ; ::_thesis: contradiction
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) &amp; u2 in the Arrows of C . (p1,p2) ) and
 k = [u1,u2] by A2, ZFMISC_1:def_2;
 ( u1 in <^p2,p3^> &amp; u2 in <^p1,p2^> ) by A3;
then  <^p1,p3^> <> {} by ALTCAT_1:def_2;
hence  contradiction by A1; ::_thesis: verum
end;
end;

begin

theorem Th34: :: ALTCAT_4:34
for C being AltCatStr
for D being SubCatStr of C st the carrier of C = the carrier of D &amp; the Arrows of C = the Arrows of D holds
D is full
proofend;

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 &amp; the Arrows of C = the Arrows of D holds
D is id-inheriting
proofend;

registration
let C be category;
cluster non empty transitive strict full id-inheriting for SubCatStr of C;
existence
 ex b1 being subcategory of C st
( b1 is full &amp; not b1 is empty &amp; b1 is strict )
proofend;
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
proofend;

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 &amp; p2 = o2 &amp; m = n &amp; <^p1,p2^> <> {} holds
( ( m is mono implies n is mono ) &amp; ( m is epi implies n is epi ) )
proofend;

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 &amp; p2 = o2 &amp; m = n &amp; m1 = n1 &amp; <^p1,p2^> <> {} &amp; <^p2,p1^> <> {} holds
( ( m is_left_inverse_of m1 implies n is_left_inverse_of n1 ) &amp; ( n is_left_inverse_of n1 implies m is_left_inverse_of m1 ) &amp; ( m is_right_inverse_of m1 implies n is_right_inverse_of n1 ) &amp; ( n is_right_inverse_of n1 implies m is_right_inverse_of m1 ) )
proofend;

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 &amp; p2 = o2 &amp; m = n &amp; <^p1,p2^> <> {} &amp; <^p2,p1^> <> {} holds
( ( m is retraction implies n is retraction ) &amp; ( m is coretraction implies n is coretraction ) &amp; ( m is iso implies n is iso ) )
proofend;

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 &amp; p2 = o2 &amp; m = n &amp; <^p1,p2^> <> {} &amp; <^p2,p1^> <> {} holds
( ( n is retraction implies m is retraction ) &amp; ( n is coretraction implies m is coretraction ) &amp; ( n is iso implies m is iso ) )
proofend;

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 &amp; the Arrows of it cc= the Arrows of C &amp; ( 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^> <> {} &amp; m is mono ) ) ) );
existence
 ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is mono ) ) ) )
proofend;
uniqueness
 for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is mono ) ) ) &amp; the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is mono ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines AllMono ALTCAT_4:def_1_:_
 for C being category
for b2 being non empty transitive strict SubCatStr of C holds
( b2 = AllMono C iff ( the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is mono ) ) ) ) );

registration
let C be category;
cluster AllMono C ->  non empty transitive strict id-inheriting ;
coherence
 AllMono C is id-inheriting
proofend;
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 &amp; the Arrows of it cc= the Arrows of C &amp; ( 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^> <> {} &amp; m is epi ) ) ) );
existence
 ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is epi ) ) ) )
proofend;
uniqueness
 for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is epi ) ) ) &amp; the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is epi ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines AllEpi ALTCAT_4:def_2_:_
 for C being category
for b2 being non empty transitive strict SubCatStr of C holds
( b2 = AllEpi C iff ( the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; m is epi ) ) ) ) );

registration
let C be category;
cluster AllEpi C ->  non empty transitive strict id-inheriting ;
coherence
 AllEpi C is id-inheriting
proofend;
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 &amp; the Arrows of it cc= the Arrows of C &amp; ( 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^> <> {} &amp; <^o2,o1^> <> {} &amp; m is retraction ) ) ) );
existence
 ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is retraction ) ) ) )
proofend;
uniqueness
 for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is retraction ) ) ) &amp; the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is retraction ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines AllRetr ALTCAT_4:def_3_:_
 for C being category
for b2 being non empty transitive strict SubCatStr of C holds
( b2 = AllRetr C iff ( the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is retraction ) ) ) ) );

registration
let C be category;
cluster AllRetr C ->  non empty transitive strict id-inheriting ;
coherence
 AllRetr C is id-inheriting
proofend;
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 &amp; the Arrows of it cc= the Arrows of C &amp; ( 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^> <> {} &amp; <^o2,o1^> <> {} &amp; m is coretraction ) ) ) );
existence
 ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is coretraction ) ) ) )
proofend;
uniqueness
 for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is coretraction ) ) ) &amp; the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is coretraction ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines AllCoretr ALTCAT_4:def_4_:_
 for C being category
for b2 being non empty transitive strict SubCatStr of C holds
( b2 = AllCoretr C iff ( the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is coretraction ) ) ) ) );

registration
let C be category;
cluster AllCoretr C ->  non empty transitive strict id-inheriting ;
coherence
 AllCoretr C is id-inheriting
proofend;
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 &amp; the Arrows of it cc= the Arrows of C &amp; ( 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^> <> {} &amp; <^o2,o1^> <> {} &amp; m is iso ) ) ) );
existence
 ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is iso ) ) ) )
proofend;
uniqueness
 for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C &amp; the Arrows of b1 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b1 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is iso ) ) ) &amp; the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is iso ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines AllIso ALTCAT_4:def_5_:_
 for C being category
for b2 being non empty transitive strict SubCatStr of C holds
( b2 = AllIso C iff ( the carrier of b2 = the carrier of C &amp; the Arrows of b2 cc= the Arrows of C &amp; ( for o1, o2 being object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b2 . (o1,o2) iff ( <^o1,o2^> <> {} &amp; <^o2,o1^> <> {} &amp; m is iso ) ) ) ) );

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

theorem Th41: :: ALTCAT_4:41
for C being category holds AllIso C is non empty subcategory of AllRetr C
proofend;

theorem Th42: :: ALTCAT_4:42
for C being category holds AllIso C is non empty subcategory of AllCoretr C
proofend;

theorem Th43: :: ALTCAT_4:43
for C being category holds AllCoretr C is non empty subcategory of AllMono C
proofend;

theorem Th44: :: ALTCAT_4:44
for C being category holds AllRetr C is non empty subcategory of AllEpi C
proofend;

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

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

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 &amp; <^o2,o1^> <> {} ) ) holds
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllRetr C
proofend;

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 &amp; <^o2,o1^> <> {} ) ) holds
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllCoretr C
proofend;

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 &amp; <^o2,o1^> <> {} ) ) holds
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllIso C
proofend;

theorem Th50: :: ALTCAT_4:50
for C being category
for o1, o2 being object of (AllMono C)
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
m is mono
proofend;

theorem Th51: :: ALTCAT_4:51
for C being category
for o1, o2 being object of (AllEpi C)
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
m is epi
proofend;

theorem Th52: :: ALTCAT_4:52
for C being category
for o1, o2 being object of (AllIso C)
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
( m is iso &amp; m " in <^o2,o1^> )
proofend;

theorem :: ALTCAT_4:53
for C being category holds AllMono (AllMono C) = AllMono C
proofend;

theorem :: ALTCAT_4:54
for C being category holds AllEpi (AllEpi C) = AllEpi C
proofend;

theorem :: ALTCAT_4:55
for C being category holds AllIso (AllIso C) = AllIso C
proofend;

theorem :: ALTCAT_4:56
for C being category holds AllIso (AllMono C) = AllIso C
proofend;

theorem :: ALTCAT_4:57
for C being category holds AllIso (AllEpi C) = AllIso C
proofend;

theorem :: ALTCAT_4:58
for C being category holds AllIso (AllRetr C) = AllIso C
proofend;

theorem :: ALTCAT_4:59
for C being category holds AllIso (AllCoretr C) = AllIso C
proofend;