:: by Artur Korni{\l}owicz

::

:: Received October 3, 1997

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

registration

let C be non empty with_units AltCatStr ;

let o be Object of C;

coherence

not <^o,o^> is empty by ALTCAT_1:19;

end;
let o be Object of C;

coherence

not <^o,o^> is empty by ALTCAT_1:19;

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

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 o1, o2, o3 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 ")

for o1, o2, o3 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

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 )

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;

coherence

( idm o is epi & idm o is mono & idm o is retraction & idm o is coretraction ) by Th4, ALTCAT_3:1;

end;
let o be Object of C;

coherence

( idm o is epi & idm o is mono & idm o is retraction & idm o is coretraction ) by Th4, ALTCAT_3:1;

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

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

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, m9 being Morphism of o1,o2 st m is _zero & m9 is _zero & ex O being Object of C st O is _zero holds

m = m9

for o1, o2 being Object of C

for m, m9 being Morphism of o1,o2 st m is _zero & m9 is _zero & ex O being Object of C st O is _zero holds

m = m9

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

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

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 o1, o2 being Object of C st o2 is terminal & o1,o2 are_iso holds

o1 is terminal

for o1, o2 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

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 )

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)

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 over C1,C2 holds

( F is full iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is onto )

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 )

proof end;

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 )

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 )

proof end;

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^> <> {} & F is full & F is feasible holds

ex m being Morphism of o1,o2 st Fm = F . m

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^> <> {} & 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 over 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

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^> <> {} & 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

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

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 coretraction holds

F . a is coretraction

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 coretraction holds

F . a is coretraction

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

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

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

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

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 coretraction holds

F . a is retraction

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 coretraction holds

F . a is retraction

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

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

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

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

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 coretraction holds

a is coretraction

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 coretraction holds

a is coretraction

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

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

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

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

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 coretraction holds

a is retraction

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 coretraction holds

a is retraction

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

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

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 :: 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)):] = {}

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

end;
[:( 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 object 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 object such that

A3: ( u1 in the Arrows of C . (p2,p3) & u2 in the Arrows of C . (p1,p2) ) and

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

hence contradiction by A1; :: thesis: verum

end;
then consider k being object 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 object such that

A3: ( u1 in the Arrows of C . (p2,p3) & u2 in the Arrows of C . (p1,p2) ) and

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

hence contradiction by A1; :: thesis: verum

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 id-inheriting

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 id-inheriting

proof end;

registration

let C be category;

existence

ex b_{1} being subcategory of C st

( b_{1} is full & not b_{1} is empty & b_{1} is strict )

end;
existence

ex b

( b

proof 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

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

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

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

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

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;

ex b_{1} being non empty transitive strict SubCatStr of C st

( the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) )

for b_{1}, b_{2} being non empty transitive strict SubCatStr of C st the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) & the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

proof end;

uniqueness for b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

b

proof end;

:: deftheorem Def1 defines AllMono ALTCAT_4:def 1 :

for C being category

for b_{2} being non empty transitive strict SubCatStr of C holds

( b_{2} = AllMono C iff ( the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & m is mono ) ) ) ) );

for C being category

for b

( b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

definition

let C be category;

ex b_{1} being non empty transitive strict SubCatStr of C st

( the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) )

for b_{1}, b_{2} being non empty transitive strict SubCatStr of C st the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) & the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

proof end;

uniqueness for b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

b

proof end;

:: deftheorem Def2 defines AllEpi ALTCAT_4:def 2 :

for C being category

for b_{2} being non empty transitive strict SubCatStr of C holds

( b_{2} = AllEpi C iff ( the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & m is epi ) ) ) ) );

for C being category

for b

( b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

definition

let C be category;

ex b_{1} being non empty transitive strict SubCatStr of C st

( the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) )

for b_{1}, b_{2} being non empty transitive strict SubCatStr of C st the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) & the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

proof end;

uniqueness for b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

b

proof end;

:: deftheorem Def3 defines AllRetr ALTCAT_4:def 3 :

for C being category

for b_{2} being non empty transitive strict SubCatStr of C holds

( b_{2} = AllRetr C iff ( the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) ) );

for C being category

for b

( b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

definition

let C be category;

ex b_{1} being non empty transitive strict SubCatStr of C st

( the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) )

for b_{1}, b_{2} being non empty transitive strict SubCatStr of C st the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) & the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

proof end;

uniqueness for b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

b

proof end;

:: deftheorem Def4 defines AllCoretr ALTCAT_4:def 4 :

for C being category

for b_{2} being non empty transitive strict SubCatStr of C holds

( b_{2} = AllCoretr C iff ( the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) ) );

for C being category

for b

( b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

definition

let C be category;

ex b_{1} being non empty transitive strict SubCatStr of C st

( the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) )

for b_{1}, b_{2} being non empty transitive strict SubCatStr of C st the carrier of b_{1} = the carrier of C & the Arrows of b_{1} 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 b_{1} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) & the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

proof end;

uniqueness for b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

b

proof end;

:: deftheorem Def5 defines AllIso ALTCAT_4:def 5 :

for C being category

for b_{2} being non empty transitive strict SubCatStr of C holds

( b_{2} = AllIso C iff ( the carrier of b_{2} = the carrier of C & the Arrows of b_{2} 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 b_{2} . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) ) );

for C being category

for b

( b

for m being Morphism of o1,o2 holds

( m in the Arrows of b

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

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

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

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

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

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

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

for o1, o2 being Object of (AllMono C)

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

m is mono

proof end;

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

for o1, o2 being Object of (AllEpi C)

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

m is epi

proof end;

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 & m " in <^o2,o1^> )

for o1, o2 being Object of (AllIso C)

for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds

( m is iso & m " in <^o2,o1^> )

proof end;