:: by Czes{\l}aw Byli\'nski

::

:: Received May 11, 1992

:: Copyright (c) 1992-2012 Association of Mizar Users

begin

theorem Th1: :: CAT_3:1

for I being set

for A being non empty set

for F1, F2 being Function of I,A st ( for x being set st x in I holds

F1 /. x = F2 /. x ) holds

F1 = F2

for A being non empty set

for F1, F2 being Function of I,A st ( for x being set st x in I holds

F1 /. x = F2 /. x ) holds

F1 = F2

proof end;

scheme :: CAT_3:sch 2

FuncIdxcorrectness{ F_{1}() -> set , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}() } :

FuncIdxcorrectness{ F

( ex F being Function of F_{1}(),F_{2}() st

for x being set st x in F_{1}() holds

F /. x = F_{3}(x) & ( for F1, F2 being Function of F_{1}(),F_{2}() st ( for x being set st x in F_{1}() holds

F1 /. x = F_{3}(x) ) & ( for x being set st x in F_{1}() holds

F2 /. x = F_{3}(x) ) holds

F1 = F2 ) )

for x being set st x in F

F /. x = F

F1 /. x = F

F2 /. x = F

F1 = F2 ) )

proof end;

definition

let A be non empty set ;

let x be set ;

let a be Element of A;

:: original: .-->

redefine func x .--> a -> Function of {x},A;

coherence

x .--> a is Function of {x},A by FUNCOP_1:46;

end;
let x be set ;

let a be Element of A;

:: original: .-->

redefine func x .--> a -> Function of {x},A;

coherence

x .--> a is Function of {x},A by FUNCOP_1:46;

theorem Th2: :: CAT_3:2

for I, x being set

for A being non empty set

for a being Element of A st x in I holds

(I --> a) /. x = a

for A being non empty set

for a being Element of A st x in I holds

(I --> a) /. x = a

proof end;

theorem Th3: :: CAT_3:3

for x1, x2 being set

for A being non empty set st x1 <> x2 holds

for y1, y2 being Element of A holds

( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 )

for A being non empty set st x1 <> x2 holds

for y1, y2 being Element of A holds

( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 )

proof end;

begin

definition

let C be Category;

let I be set ;

let F be Function of I, the carrier' of C;

existence

ex b_{1} being Function of I, the carrier of C st

for x being set st x in I holds

b_{1} /. x = dom (F /. x);

uniqueness

for b_{1}, b_{2} being Function of I, the carrier of C st ( for x being set st x in I holds

b_{1} /. x = dom (F /. x) ) & ( for x being set st x in I holds

b_{2} /. x = dom (F /. x) ) holds

b_{1} = b_{2};

existence

ex b_{1} being Function of I, the carrier of C st

for x being set st x in I holds

b_{1} /. x = cod (F /. x);

uniqueness

for b_{1}, b_{2} being Function of I, the carrier of C st ( for x being set st x in I holds

b_{1} /. x = cod (F /. x) ) & ( for x being set st x in I holds

b_{2} /. x = cod (F /. x) ) holds

b_{1} = b_{2};

end;
let I be set ;

let F be Function of I, the carrier' of C;

func doms F -> Function of I, the carrier of C means :Def1: :: CAT_3:def 1

for x being set st x in I holds

it /. x = dom (F /. x);

correctness for x being set st x in I holds

it /. x = dom (F /. x);

existence

ex b

for x being set st x in I holds

b

uniqueness

for b

b

b

b

proof end;

func cods F -> Function of I, the carrier of C means :Def2: :: CAT_3:def 2

for x being set st x in I holds

it /. x = cod (F /. x);

correctness for x being set st x in I holds

it /. x = cod (F /. x);

existence

ex b

for x being set st x in I holds

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def1 defines doms CAT_3:def 1 :

for C being Category

for I being set

for F being Function of I, the carrier' of C

for b_{4} being Function of I, the carrier of C holds

( b_{4} = doms F iff for x being set st x in I holds

b_{4} /. x = dom (F /. x) );

for C being Category

for I being set

for F being Function of I, the carrier' of C

for b

( b

b

:: deftheorem Def2 defines cods CAT_3:def 2 :

for C being Category

for I being set

for F being Function of I, the carrier' of C

for b_{4} being Function of I, the carrier of C holds

( b_{4} = cods F iff for x being set st x in I holds

b_{4} /. x = cod (F /. x) );

for C being Category

for I being set

for F being Function of I, the carrier' of C

for b

( b

b

theorem Th6: :: CAT_3:6

for x1, x2 being set

for C being Category

for p1, p2 being Morphism of C holds doms ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((dom p1),(dom p2))

for C being Category

for p1, p2 being Morphism of C holds doms ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((dom p1),(dom p2))

proof end;

theorem Th7: :: CAT_3:7

for x1, x2 being set

for C being Category

for p1, p2 being Morphism of C holds cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))

for C being Category

for p1, p2 being Morphism of C holds cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))

proof end;

definition

let C be Category;

let I be set ;

let F be Function of I, the carrier' of C;

existence

ex b_{1} being Function of I, the carrier' of (C opp) st

for x being set st x in I holds

b_{1} /. x = (F /. x) opp ;

uniqueness

for b_{1}, b_{2} being Function of I, the carrier' of (C opp) st ( for x being set st x in I holds

b_{1} /. x = (F /. x) opp ) & ( for x being set st x in I holds

b_{2} /. x = (F /. x) opp ) holds

b_{1} = b_{2};

end;
let I be set ;

let F be Function of I, the carrier' of C;

func F opp -> Function of I, the carrier' of (C opp) means :Def3: :: CAT_3:def 3

for x being set st x in I holds

it /. x = (F /. x) opp ;

correctness for x being set st x in I holds

it /. x = (F /. x) opp ;

existence

ex b

for x being set st x in I holds

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def3 defines opp CAT_3:def 3 :

for C being Category

for I being set

for F being Function of I, the carrier' of C

for b_{4} being Function of I, the carrier' of (C opp) holds

( b_{4} = F opp iff for x being set st x in I holds

b_{4} /. x = (F /. x) opp );

for C being Category

for I being set

for F being Function of I, the carrier' of C

for b

( b

b

theorem :: CAT_3:9

for x1, x2 being set

for C being Category

for p1, p2 being Morphism of C st x1 <> x2 holds

((x1,x2) --> (p1,p2)) opp = (x1,x2) --> ((p1 opp),(p2 opp))

for C being Category

for p1, p2 being Morphism of C st x1 <> x2 holds

((x1,x2) --> (p1,p2)) opp = (x1,x2) --> ((p1 opp),(p2 opp))

proof end;

theorem :: CAT_3:10

for I being set

for C being Category

for F being Function of I, the carrier' of C holds (F opp) opp = F

for C being Category

for F being Function of I, the carrier' of C holds (F opp) opp = F

proof end;

definition

let C be Category;

let I be set ;

let F be Function of I, the carrier' of (C opp);

existence

ex b_{1} being Function of I, the carrier' of C st

for x being set st x in I holds

b_{1} /. x = opp (F /. x);

uniqueness

for b_{1}, b_{2} being Function of I, the carrier' of C st ( for x being set st x in I holds

b_{1} /. x = opp (F /. x) ) & ( for x being set st x in I holds

b_{2} /. x = opp (F /. x) ) holds

b_{1} = b_{2};

end;
let I be set ;

let F be Function of I, the carrier' of (C opp);

func opp F -> Function of I, the carrier' of C means :Def4: :: CAT_3:def 4

for x being set st x in I holds

it /. x = opp (F /. x);

correctness for x being set st x in I holds

it /. x = opp (F /. x);

existence

ex b

for x being set st x in I holds

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def4 defines opp CAT_3:def 4 :

for C being Category

for I being set

for F being Function of I, the carrier' of (C opp)

for b_{4} being Function of I, the carrier' of C holds

( b_{4} = opp F iff for x being set st x in I holds

b_{4} /. x = opp (F /. x) );

for C being Category

for I being set

for F being Function of I, the carrier' of (C opp)

for b

( b

b

theorem :: CAT_3:11

for I being set

for C being Category

for f being Morphism of (C opp) holds opp (I --> f) = I --> (opp f)

for C being Category

for f being Morphism of (C opp) holds opp (I --> f) = I --> (opp f)

proof end;

theorem :: CAT_3:12

for x1, x2 being set

for C being Category st x1 <> x2 holds

for p1, p2 being Morphism of (C opp) holds opp ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((opp p1),(opp p2))

for C being Category st x1 <> x2 holds

for p1, p2 being Morphism of (C opp) holds opp ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((opp p1),(opp p2))

proof end;

theorem :: CAT_3:13

for I being set

for C being Category

for F being Function of I, the carrier' of C holds opp (F opp) = F

for C being Category

for F being Function of I, the carrier' of C holds opp (F opp) = F

proof end;

definition

let C be Category;

let I be set ;

let F be Function of I, the carrier' of C;

let f be Morphism of C;

existence

ex b_{1} being Function of I, the carrier' of C st

for x being set st x in I holds

b_{1} /. x = (F /. x) (*) f;

uniqueness

for b_{1}, b_{2} being Function of I, the carrier' of C st ( for x being set st x in I holds

b_{1} /. x = (F /. x) (*) f ) & ( for x being set st x in I holds

b_{2} /. x = (F /. x) (*) f ) holds

b_{1} = b_{2};

existence

ex b_{1} being Function of I, the carrier' of C st

for x being set st x in I holds

b_{1} /. x = f (*) (F /. x);

uniqueness

for b_{1}, b_{2} being Function of I, the carrier' of C st ( for x being set st x in I holds

b_{1} /. x = f (*) (F /. x) ) & ( for x being set st x in I holds

b_{2} /. x = f (*) (F /. x) ) holds

b_{1} = b_{2};

end;
let I be set ;

let F be Function of I, the carrier' of C;

let f be Morphism of C;

func F * f -> Function of I, the carrier' of C means :Def5: :: CAT_3:def 5

for x being set st x in I holds

it /. x = (F /. x) (*) f;

correctness for x being set st x in I holds

it /. x = (F /. x) (*) f;

existence

ex b

for x being set st x in I holds

b

uniqueness

for b

b

b

b

proof end;

func f * F -> Function of I, the carrier' of C means :Def6: :: CAT_3:def 6

for x being set st x in I holds

it /. x = f (*) (F /. x);

correctness for x being set st x in I holds

it /. x = f (*) (F /. x);

existence

ex b

for x being set st x in I holds

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def5 defines * CAT_3:def 5 :

for C being Category

for I being set

for F being Function of I, the carrier' of C

for f being Morphism of C

for b_{5} being Function of I, the carrier' of C holds

( b_{5} = F * f iff for x being set st x in I holds

b_{5} /. x = (F /. x) (*) f );

for C being Category

for I being set

for F being Function of I, the carrier' of C

for f being Morphism of C

for b

( b

b

:: deftheorem Def6 defines * CAT_3:def 6 :

for C being Category

for I being set

for F being Function of I, the carrier' of C

for f being Morphism of C

for b_{5} being Function of I, the carrier' of C holds

( b_{5} = f * F iff for x being set st x in I holds

b_{5} /. x = f (*) (F /. x) );

for C being Category

for I being set

for F being Function of I, the carrier' of C

for f being Morphism of C

for b

( b

b

theorem Th14: :: CAT_3:14

for x1, x2 being set

for C being Category

for p1, p2, f being Morphism of C st x1 <> x2 holds

((x1,x2) --> (p1,p2)) * f = (x1,x2) --> ((p1 (*) f),(p2 (*) f))

for C being Category

for p1, p2, f being Morphism of C st x1 <> x2 holds

((x1,x2) --> (p1,p2)) * f = (x1,x2) --> ((p1 (*) f),(p2 (*) f))

proof end;

theorem Th15: :: CAT_3:15

for x1, x2 being set

for C being Category

for f, p1, p2 being Morphism of C st x1 <> x2 holds

f * ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((f (*) p1),(f (*) p2))

for C being Category

for f, p1, p2 being Morphism of C st x1 <> x2 holds

f * ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((f (*) p1),(f (*) p2))

proof end;

theorem Th16: :: CAT_3:16

for I being set

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C st doms F = I --> (cod f) holds

( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C st doms F = I --> (cod f) holds

( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )

proof end;

theorem Th17: :: CAT_3:17

for I being set

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds

( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )

proof end;

definition

let C be Category;

let I be set ;

let F, G be Function of I, the carrier' of C;

existence

ex b_{1} being Function of I, the carrier' of C st

for x being set st x in I holds

b_{1} /. x = (F /. x) (*) (G /. x);

uniqueness

for b_{1}, b_{2} being Function of I, the carrier' of C st ( for x being set st x in I holds

b_{1} /. x = (F /. x) (*) (G /. x) ) & ( for x being set st x in I holds

b_{2} /. x = (F /. x) (*) (G /. x) ) holds

b_{1} = b_{2};

end;
let I be set ;

let F, G be Function of I, the carrier' of C;

func F "*" G -> Function of I, the carrier' of C means :Def7: :: CAT_3:def 7

for x being set st x in I holds

it /. x = (F /. x) (*) (G /. x);

correctness for x being set st x in I holds

it /. x = (F /. x) (*) (G /. x);

existence

ex b

for x being set st x in I holds

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def7 defines "*" CAT_3:def 7 :

for C being Category

for I being set

for F, G, b_{5} being Function of I, the carrier' of C holds

( b_{5} = F "*" G iff for x being set st x in I holds

b_{5} /. x = (F /. x) (*) (G /. x) );

for C being Category

for I being set

for F, G, b

( b

b

theorem Th18: :: CAT_3:18

for I being set

for C being Category

for F, G being Function of I, the carrier' of C st doms F = cods G holds

( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

for C being Category

for F, G being Function of I, the carrier' of C st doms F = cods G holds

( doms (F "*" G) = doms G & cods (F "*" G) = cods F )

proof end;

theorem :: CAT_3:19

for x1, x2 being set

for C being Category

for p1, p2, q1, q2 being Morphism of C st x1 <> x2 holds

((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 (*) q1),(p2 (*) q2))

for C being Category

for p1, p2, q1, q2 being Morphism of C st x1 <> x2 holds

((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 (*) q1),(p2 (*) q2))

proof end;

theorem :: CAT_3:20

for I being set

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C holds F * f = F "*" (I --> f)

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C holds F * f = F "*" (I --> f)

proof end;

theorem :: CAT_3:21

for I being set

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C holds f * F = (I --> f) "*" F

for C being Category

for f being Morphism of C

for F being Function of I, the carrier' of C holds f * F = (I --> f) "*" F

proof end;

begin

definition

let C be Category;

let a, b be Object of C;

let IT be Morphism of a,b;

end;
let a, b be Object of C;

let IT be Morphism of a,b;

attr IT is retraction means :Def8: :: CAT_3:def 8

( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st IT * g = id b );

( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st IT * g = id b );

:: deftheorem Def8 defines retraction CAT_3:def 8 :

for C being Category

for a, b being Object of C

for IT being Morphism of a,b holds

( IT is retraction iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st IT * g = id b ) );

for C being Category

for a, b being Object of C

for IT being Morphism of a,b holds

( IT is retraction iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st IT * g = id b ) );

:: deftheorem Def9 defines coretraction CAT_3:def 9 :

for C being Category

for a, b being Object of C

for IT being Morphism of a,b holds

( IT is coretraction iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st g * IT = id a ) );

for C being Category

for a, b being Object of C

for IT being Morphism of a,b holds

( IT is coretraction iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st g * IT = id a ) );

theorem Th22: :: CAT_3:22

for C being Category

for a, b being Object of C

for f being Morphism of a,b st f is retraction holds

f is epi

for a, b being Object of C

for f being Morphism of a,b st f is retraction holds

f is epi

proof end;

theorem :: CAT_3:23

for C being Category

for a, b being Object of C

for f being Morphism of a,b st f is coretraction holds

f is monic

for a, b being Object of C

for f being Morphism of a,b st f is coretraction holds

f is monic

proof end;

theorem :: CAT_3:24

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is retraction & g is retraction holds

g * f is retraction

proof end;

theorem :: CAT_3:25

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is coretraction & g is coretraction holds

g * f is coretraction

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st f is coretraction & g is coretraction holds

g * f is coretraction

proof end;

theorem :: CAT_3:26

for C being Category

for c, a, b being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,a) <> {} & g * f is retraction holds

g is retraction

for c, a, b being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,a) <> {} & g * f is retraction holds

g is retraction

proof end;

theorem :: CAT_3:27

for C being Category

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

f is coretraction

for a, b, c being Object of C

for f being Morphism of a,b

for g being Morphism of b,c st Hom (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds

f is coretraction

proof end;

theorem :: CAT_3:28

for C being Category

for a, b being Object of C

for f being Morphism of a,b st f is retraction & f is monic holds

f is invertible

for a, b being Object of C

for f being Morphism of a,b st f is retraction & f is monic holds

f is invertible

proof end;

theorem Th29: :: CAT_3:29

for C being Category

for a, b being Object of C

for f being Morphism of a,b st f is coretraction & f is epi holds

f is invertible

for a, b being Object of C

for f being Morphism of a,b st f is coretraction & f is epi holds

f is invertible

proof end;

theorem :: CAT_3:30

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f is invertible iff ( f is retraction & f is coretraction ) )

for a, b being Object of C

for f being Morphism of a,b holds

( f is invertible iff ( f is retraction & f is coretraction ) )

proof end;

definition

let C be Category;

let a, b be Object of C;

assume Z: Hom (a,b) <> {} ;

let D be Category;

let T be Functor of C,D;

let f be Morphism of a,b;

coherence

T . f is Morphism of T . a,T . b

end;
let a, b be Object of C;

assume Z: Hom (a,b) <> {} ;

let D be Category;

let T be Functor of C,D;

let f be Morphism of a,b;

coherence

T . f is Morphism of T . a,T . b

proof end;

:: deftheorem Def10 defines /. CAT_3:def 10 :

for C being Category

for a, b being Object of C st Hom (a,b) <> {} holds

for D being Category

for T being Functor of C,D

for f being Morphism of a,b holds T /. f = T . f;

for C being Category

for a, b being Object of C st Hom (a,b) <> {} holds

for D being Category

for T being Functor of C,D

for f being Morphism of a,b holds T /. f = T . f;

Lm1: for C, D being Category

for T being Functor of C,D

for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds

for f being Morphism of a,b

for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)

proof end;

Lm2: for C, D being Category

for T being Functor of C,D

for c being Object of C holds T /. (id c) = id (T . c)

proof end;

theorem :: CAT_3:31

for C, D being Category

for a, b being Object of C

for f being Morphism of a,b

for T being Functor of C,D st f is retraction holds

T /. f is retraction

for a, b being Object of C

for f being Morphism of a,b

for T being Functor of C,D st f is retraction holds

T /. f is retraction

proof end;

theorem :: CAT_3:32

for C, D being Category

for a, b being Object of C

for f being Morphism of a,b

for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

for a, b being Object of C

for f being Morphism of a,b

for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

proof end;

theorem :: CAT_3:33

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f is retraction iff f opp is coretraction )

for a, b being Object of C

for f being Morphism of a,b holds

( f is retraction iff f opp is coretraction )

proof end;

theorem :: CAT_3:34

for C being Category

for a, b being Object of C

for f being Morphism of a,b holds

( f is coretraction iff f opp is retraction )

for a, b being Object of C

for f being Morphism of a,b holds

( f is coretraction iff f opp is retraction )

proof end;

begin

definition

let C be Category;

let a, b be Object of C;

assume A1: b is terminal ;

existence

ex b_{1} being Morphism of a,b st verum
;

uniqueness

for b_{1}, b_{2} being Morphism of a,b holds b_{1} = b_{2}

end;
let a, b be Object of C;

assume A1: b is terminal ;

existence

ex b

uniqueness

for b

proof end;

:: deftheorem defines term CAT_3:def 11 :

for C being Category

for a, b being Object of C st b is terminal holds

for b_{4} being Morphism of a,b holds

( b_{4} = term (a,b) iff verum );

for C being Category

for a, b being Object of C st b is terminal holds

for b

( b

theorem Th35: :: CAT_3:35

for C being Category

for b, a being Object of C st b is terminal holds

( dom (term (a,b)) = a & cod (term (a,b)) = b )

for b, a being Object of C st b is terminal holds

( dom (term (a,b)) = a & cod (term (a,b)) = b )

proof end;

theorem Th36: :: CAT_3:36

for C being Category

for b, a being Object of C

for f being Morphism of C st b is terminal & dom f = a & cod f = b holds

term (a,b) = f

for b, a being Object of C

for f being Morphism of C st b is terminal & dom f = a & cod f = b holds

term (a,b) = f

proof end;

theorem :: CAT_3:37

for C being Category

for a, b being Object of C

for f being Morphism of a,b st b is terminal holds

term (a,b) = f

for a, b being Object of C

for f being Morphism of a,b st b is terminal holds

term (a,b) = f

proof end;

begin

definition

let C be Category;

let a, b be Object of C;

assume A1: a is initial ;

existence

ex b_{1} being Morphism of a,b st verum
;

uniqueness

for b_{1}, b_{2} being Morphism of a,b holds b_{1} = b_{2}

end;
let a, b be Object of C;

assume A1: a is initial ;

existence

ex b

uniqueness

for b

proof end;

:: deftheorem defines init CAT_3:def 12 :

for C being Category

for a, b being Object of C st a is initial holds

for b_{4} being Morphism of a,b holds

( b_{4} = init (a,b) iff verum );

for C being Category

for a, b being Object of C st a is initial holds

for b

( b

theorem Th38: :: CAT_3:38

for C being Category

for a, b being Object of C st a is initial holds

( dom (init (a,b)) = a & cod (init (a,b)) = b )

for a, b being Object of C st a is initial holds

( dom (init (a,b)) = a & cod (init (a,b)) = b )

proof end;

theorem Th39: :: CAT_3:39

for C being Category

for a, b being Object of C

for f being Morphism of C st a is initial & dom f = a & cod f = b holds

init (a,b) = f

for a, b being Object of C

for f being Morphism of C st a is initial & dom f = a & cod f = b holds

init (a,b) = f

proof end;

theorem :: CAT_3:40

for C being Category

for a, b being Object of C

for f being Morphism of a,b st a is initial holds

init (a,b) = f

for a, b being Object of C

for f being Morphism of a,b st a is initial holds

init (a,b) = f

proof end;

begin

definition

let C be Category;

let a be Object of C;

let I be set ;

ex b_{1} being Function of I, the carrier' of C st doms b_{1} = I --> a

end;
let a be Object of C;

let I be set ;

mode Projections_family of a,I -> Function of I, the carrier' of C means :Def13: :: CAT_3:def 13

doms it = I --> a;

existence doms it = I --> a;

ex b

proof end;

:: deftheorem Def13 defines Projections_family CAT_3:def 13 :

for C being Category

for a being Object of C

for I being set

for b_{4} being Function of I, the carrier' of C holds

( b_{4} is Projections_family of a,I iff doms b_{4} = I --> a );

for C being Category

for a being Object of C

for I being set

for b

( b

theorem Th41: :: CAT_3:41

for I, x being set

for C being Category

for a being Object of C

for F being Projections_family of a,I st x in I holds

dom (F /. x) = a

for C being Category

for a being Object of C

for F being Projections_family of a,I st x in I holds

dom (F /. x) = a

proof end;

theorem Th42: :: CAT_3:42

for C being Category

for a being Object of C

for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}

for a being Object of C

for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}

proof end;

theorem Th43: :: CAT_3:43

for y being set

for C being Category

for a being Object of C

for f being Morphism of C st dom f = a holds

y .--> f is Projections_family of a,{y}

for C being Category

for a being Object of C

for f being Morphism of C st dom f = a holds

y .--> f is Projections_family of a,{y}

proof end;

theorem Th44: :: CAT_3:44

for x1, x2 being set

for C being Category

for a being Object of C

for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds

(x1,x2) --> (p1,p2) is Projections_family of a,{x1,x2}

for C being Category

for a being Object of C

for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds

(x1,x2) --> (p1,p2) is Projections_family of a,{x1,x2}

proof end;

theorem Th45: :: CAT_3:45

for I being set

for C being Category

for a being Object of C

for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

for C being Category

for a being Object of C

for f being Morphism of C

for F being Projections_family of a,I st cod f = a holds

F * f is Projections_family of dom f,I

proof end;

theorem :: CAT_3:46

for I being set

for C being Category

for a being Object of C

for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

for C being Category

for a being Object of C

for F being Function of I, the carrier' of C

for G being Projections_family of a,I st doms F = cods G holds

F "*" G is Projections_family of a,I

proof end;

theorem :: CAT_3:47

for I being set

for C being Category

for f being Morphism of C

for F being Projections_family of cod f,I holds (f opp) * (F opp) = (F * f) opp

for C being Category

for f being Morphism of C

for F being Projections_family of cod f,I holds (f opp) * (F opp) = (F * f) opp

proof end;

definition

let C be Category;

let a be Object of C;

let I be set ;

let F be Function of I, the carrier' of C;

end;
let a be Object of C;

let I be set ;

let F be Function of I, the carrier' of C;

pred a is_a_product_wrt F means :Def14: :: CAT_3:def 14

( F is Projections_family of a,I & ( for b being Object of C

for F9 being Projections_family of b,I st cods F = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) );

( F is Projections_family of a,I & ( for b being Object of C

for F9 being Projections_family of b,I st cods F = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) );

:: deftheorem Def14 defines is_a_product_wrt CAT_3:def 14 :

for C being Category

for a being Object of C

for I being set

for F being Function of I, the carrier' of C holds

( a is_a_product_wrt F iff ( F is Projections_family of a,I & ( for b being Object of C

for F9 being Projections_family of b,I st cods F = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) ) );

for C being Category

for a being Object of C

for I being set

for F being Function of I, the carrier' of C holds

( a is_a_product_wrt F iff ( F is Projections_family of a,I & ( for b being Object of C

for F9 being Projections_family of b,I st cods F = cods F9 holds

ex h being Morphism of C st

( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds

( ( for x being set st x in I holds

(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) ) );

theorem Th48: :: CAT_3:48

for I being set

for C being Category

for c, d being Object of C

for F being Projections_family of c,I

for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds

c,d are_isomorphic

for C being Category

for c, d being Object of C

for F being Projections_family of c,I

for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds

c,d are_isomorphic

proof end;

theorem Th49: :: CAT_3:49

for I being set

for C being Category

for c being Object of C

for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds

Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) holds

for x being set st x in I holds

for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds

for f being Morphism of c,d st f = F /. x holds

f is retraction

for C being Category

for c being Object of C

for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds

Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) holds

for x being set st x in I holds

for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds

for f being Morphism of c,d st f = F /. x holds

f is retraction

proof end;

theorem Th50: :: CAT_3:50

for C being Category

for a being Object of C

for F being Function of {}, the carrier' of C holds

( a is_a_product_wrt F iff a is terminal )

for a being Object of C

for F being Function of {}, the carrier' of C holds

( a is_a_product_wrt F iff a is terminal )

proof end;

theorem Th51: :: CAT_3:51

for I being set

for C being Category

for a, b being Object of C

for F being Projections_family of a,I st a is_a_product_wrt F holds

for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds

b is_a_product_wrt F * f

for C being Category

for a, b being Object of C

for F being Projections_family of a,I st a is_a_product_wrt F holds

for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds

b is_a_product_wrt F * f

proof end;

theorem :: CAT_3:53

for I being set

for C being Category

for a being Object of C

for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds

cod (F /. x) is terminal ) holds

a is terminal

for C being Category

for a being Object of C

for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds

cod (F /. x) is terminal ) holds

a is terminal

proof end;

definition

let C be Category;

let c be Object of C;

let p1, p2 be Morphism of C;

end;
let c be Object of C;

let p1, p2 be Morphism of C;

pred c is_a_product_wrt p1,p2 means :Def15: :: CAT_3:def 15

( dom p1 = c & dom p2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds

ex h being Morphism of C st

( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds

( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) ) );

( dom p1 = c & dom p2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds

ex h being Morphism of C st

( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds

( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) ) );

:: deftheorem Def15 defines is_a_product_wrt CAT_3:def 15 :

for C being Category

for c being Object of C

for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff ( dom p1 = c & dom p2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds

ex h being Morphism of C st

( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds

( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) ) ) );

for C being Category

for c being Object of C

for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff ( dom p1 = c & dom p2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds

ex h being Morphism of C st

( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds

( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) ) ) );

theorem Th54: :: CAT_3:54

for x1, x2 being set

for C being Category

for c being Object of C

for p1, p2 being Morphism of C st x1 <> x2 holds

( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )

for C being Category

for c being Object of C

for p1, p2 being Morphism of C st x1 <> x2 holds

( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )

proof end;

theorem :: CAT_3:55

for C being Category

for c, a, b being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds

for p1 being Morphism of c,a

for p2 being Morphism of c,b holds

( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom (d,a) <> {} & Hom (d,b) <> {} holds

( Hom (d,c) <> {} & ( for f being Morphism of d,a

for g being Morphism of d,b ex h being Morphism of d,c st

for k being Morphism of d,c holds

( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )

for c, a, b being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds

for p1 being Morphism of c,a

for p2 being Morphism of c,b holds

( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom (d,a) <> {} & Hom (d,b) <> {} holds

( Hom (d,c) <> {} & ( for f being Morphism of d,a

for g being Morphism of d,b ex h being Morphism of d,c st

for k being Morphism of d,c holds

( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )

proof end;

theorem :: CAT_3:56

for C being Category

for c, d being Object of C

for p1, p2, q1, q2 being Morphism of C st c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 holds

c,d are_isomorphic

for c, d being Object of C

for p1, p2, q1, q2 being Morphism of C st c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 holds

c,d are_isomorphic

proof end;

theorem :: CAT_3:57

for C being Category

for c, a, b being Object of C

for p1 being Morphism of c,a

for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds

( p1 is retraction & p2 is retraction )

for c, a, b being Object of C

for p1 being Morphism of c,a

for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds

( p1 is retraction & p2 is retraction )

proof end;

theorem Th58: :: CAT_3:58

for C being Category

for c being Object of C

for p1, p2, h being Morphism of C st c is_a_product_wrt p1,p2 & h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 holds

h = id c

for c being Object of C

for p1, p2, h being Morphism of C st c is_a_product_wrt p1,p2 & h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 holds

h = id c

proof end;

theorem :: CAT_3:59

for C being Category

for d, c being Object of C

for p1, p2 being Morphism of C

for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds

d is_a_product_wrt p1 (*) f,p2 (*) f

for d, c being Object of C

for p1, p2 being Morphism of C

for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds

d is_a_product_wrt p1 (*) f,p2 (*) f

proof end;

theorem :: CAT_3:60

for C being Category

for c being Object of C

for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p2 is terminal holds

c, cod p1 are_isomorphic

for c being Object of C

for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p2 is terminal holds

c, cod p1 are_isomorphic

proof end;

theorem :: CAT_3:61

for C being Category

for c being Object of C

for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p1 is terminal holds

c, cod p2 are_isomorphic

for c being Object of C

for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p1 is terminal holds

c, cod p2 are_isomorphic

proof end;

begin

definition

let C be Category;

let c be Object of C;

let I be set ;

ex b_{1} being Function of I, the carrier' of C st cods b_{1} = I --> c

end;
let c be Object of C;

let I be set ;

mode Injections_family of c,I -> Function of I, the carrier' of C means :Def16: :: CAT_3:def 16

cods it = I --> c;

existence cods it = I --> c;

ex b

proof end;

:: deftheorem Def16 defines Injections_family CAT_3:def 16 :

for C being Category

for c being Object of C

for I being set

for b_{4} being Function of I, the carrier' of C holds

( b_{4} is Injections_family of c,I iff cods b_{4} = I --> c );

for C being Category

for c being Object of C

for I being set

for b

( b

theorem Th62: :: CAT_3:62

for I, x being set

for C being Category

for c being Object of C

for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

for C being Category

for c being Object of C

for F being Injections_family of c,I st x in I holds

cod (F /. x) = c

proof end;

theorem :: CAT_3:63

for C being Category

for a being Object of C

for F being Function of {}, the carrier' of C holds F is Injections_family of a, {}

for a being Object of C

for F being Function of {}, the carrier' of C holds F is Injections_family of a, {}

proof end;

theorem Th64: :: CAT_3:64

for y being set

for C being Category

for a being Object of C

for f being Morphism of C st cod f = a holds

y .--> f is Injections_family of a,{y}

for C being Category

for a being Object of C

for f being Morphism of C st cod f = a holds

y .--> f is Injections_family of a,{y}

proof end;

theorem Th65: :: CAT_3:65

for x1, x2 being set

for C being Category

for c being Object of C

for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

for C being Category

for c being Object of C

for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

proof end;

theorem Th66: :: CAT_3:66

for I being set

for C being Category

for b being Object of C

for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

for C being Category

for b being Object of C

for f being Morphism of C

for F being Injections_family of b,I st dom f = b holds

f * F is Injections_family of cod f,I

proof end;

theorem :: CAT_3:67

for I being set

for C being Category

for b being Object of C

for F being Injections_family of b,I

for G being Function of I, the carrier' of C st doms F = cods G holds

F "*" G is Injections_family of b,I

for C being Category

for b being Object of C

for F being Injections_family of b,I

for G being Function of I, the carrier' of C st doms F = cods G holds

F "*" G is Injections_family of b,I

proof end;

theorem Th68: :: CAT_3:68

for I being set

for C being Category

for c being Object of C

for F being Function of I, the carrier' of C holds

( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )

for C being Category

for c being Object of C

for F being Function of I, the carrier' of C holds

( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )

proof end;

theorem Th69: :: CAT_3:69

for I being set

for C being Category

for F being Function of I, the carrier' of (C opp)

for c being Object of (C opp) holds

( F is Injections_family of c,I iff opp F is Projections_family of opp c,I )

for C being Category

for F being Function of I, the carrier' of (C opp)

for c being Object of (C opp) holds

( F is Injections_family of c,I iff opp F is Projections_family of opp c,I )

proof end;

theorem :: CAT_3:70

for I being set

for C being Category

for f being Morphism of C

for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

for C being Category

for f being Morphism of C

for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp

proof end;

definition

let C be Category;

let c be Object of C;

let I be set ;

let F be Function of I, the carrier' of C;

end;
let c be Object of C;

let I be set ;

let F be Function of I, the carrier' of C;

pred c is_a_coproduct_wrt F means :Def17: :: CAT_3:def 17

( F is Injections_family of c,I & ( for d being Object of C

for F9 being Injections_family of d,I st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) ) );

( F is Injections_family of c,I & ( for d being Object of C

for F9 being Injections_family of d,I st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) ) );

:: deftheorem Def17 defines is_a_coproduct_wrt CAT_3:def 17 :

for C being Category

for c being Object of C

for I being set

for F being Function of I, the carrier' of C holds

( c is_a_coproduct_wrt F iff ( F is Injections_family of c,I & ( for d being Object of C

for F9 being Injections_family of d,I st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) ) ) );

for C being Category

for c being Object of C

for I being set

for F being Function of I, the carrier' of C holds

( c is_a_coproduct_wrt F iff ( F is Injections_family of c,I & ( for d being Object of C

for F9 being Injections_family of d,I st doms F = doms F9 holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( for x being set st x in I holds

k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) ) ) );

theorem :: CAT_3:71

for I being set

for C being Category

for c being Object of C

for F being Function of I, the carrier' of C holds

( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )

for C being Category

for c being Object of C

for F being Function of I, the carrier' of C holds

( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )

proof end;

theorem Th72: :: CAT_3:72

for I being set

for C being Category

for c, d being Object of C

for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

for C being Category

for c, d being Object of C

for F being Injections_family of c,I

for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds

c,d are_isomorphic

proof end;

theorem Th73: :: CAT_3:73

for I being set

for C being Category

for c being Object of C

for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds

Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds

for x being set st x in I holds

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction

for C being Category

for c being Object of C

for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds

Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds

for x being set st x in I holds

for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds

for f being Morphism of d,c st f = F /. x holds

f is coretraction

proof end;

theorem Th74: :: CAT_3:74

for I being set

for C being Category

for a, b being Object of C

for f being Morphism of a,b

for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds

b is_a_coproduct_wrt f * F

for C being Category

for a, b being Object of C

for f being Morphism of a,b

for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds

b is_a_coproduct_wrt f * F

proof end;

theorem Th75: :: CAT_3:75

for C being Category

for a being Object of C

for F being Injections_family of a, {} holds

( a is_a_coproduct_wrt F iff a is initial )

for a being Object of C

for F being Injections_family of a, {} holds

( a is_a_coproduct_wrt F iff a is initial )

proof end;

theorem :: CAT_3:76

for y being set

for C being Category

for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)

for C being Category

for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)

proof end;

theorem :: CAT_3:77

for I being set

for C being Category

for a being Object of C

for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds

dom (F /. x) is initial ) holds

a is initial

for C being Category

for a being Object of C

for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds

dom (F /. x) is initial ) holds

a is initial

proof end;

definition

let C be Category;

let c be Object of C;

let i1, i2 be Morphism of C;

end;
let c be Object of C;

let i1, i2 be Morphism of C;

pred c is_a_coproduct_wrt i1,i2 means :Def18: :: CAT_3:def 18

( cod i1 = c & cod i2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) );

( cod i1 = c & cod i2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) );

:: deftheorem Def18 defines is_a_coproduct_wrt CAT_3:def 18 :

for C being Category

for c being Object of C

for i1, i2 being Morphism of C holds

( c is_a_coproduct_wrt i1,i2 iff ( cod i1 = c & cod i2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) ) );

for C being Category

for c being Object of C

for i1, i2 being Morphism of C holds

( c is_a_coproduct_wrt i1,i2 iff ( cod i1 = c & cod i2 = c & ( for d being Object of C

for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds

ex h being Morphism of C st

( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds

( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) ) );

theorem :: CAT_3:78

for C being Category

for c being Object of C

for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

for c being Object of C

for p1, p2 being Morphism of C holds

( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )

proof end;

theorem Th79: :: CAT_3:79

for x1, x2 being set

for C being Category

for c being Object of C

for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

for C being Category

for c being Object of C

for i1, i2 being Morphism of C st x1 <> x2 holds

( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )

proof end;

theorem :: CAT_3:80

for C being Category

for c, d being Object of C

for i1, i2, j1, j2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 holds

c,d are_isomorphic

for c, d being Object of C

for i1, i2, j1, j2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 holds

c,d are_isomorphic

proof end;

theorem :: CAT_3:81

for C being Category

for a, c, b being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds

for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds

( Hom (c,d) <> {} & ( for f being Morphism of a,d

for g being Morphism of b,d ex h being Morphism of c,d st

for k being Morphism of c,d holds

( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) )

for a, c, b being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds

for i1 being Morphism of a,c

for i2 being Morphism of b,c holds

( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds

( Hom (c,d) <> {} & ( for f being Morphism of a,d

for g being Morphism of b,d ex h being Morphism of c,d st

for k being Morphism of c,d holds

( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) )

proof end;

theorem :: CAT_3:82

for C being Category

for a, c, b being Object of C

for i1 being Morphism of a,c

for i2 being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds

( i1 is coretraction & i2 is coretraction )

for a, c, b being Object of C

for i1 being Morphism of a,c

for i2 being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds

( i1 is coretraction & i2 is coretraction )

proof end;

theorem Th83: :: CAT_3:83

for C being Category

for c being Object of C

for i1, i2, h being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom (c,c) & h (*) i1 = i1 & h (*) i2 = i2 holds

h = id c

for c being Object of C

for i1, i2, h being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom (c,c) & h (*) i1 = i1 & h (*) i2 = i2 holds

h = id c

proof end;

theorem :: CAT_3:84

for C being Category

for c, d being Object of C

for i1, i2 being Morphism of C

for f being Morphism of c,d st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds

d is_a_coproduct_wrt f (*) i1,f (*) i2

for c, d being Object of C

for i1, i2 being Morphism of C

for f being Morphism of c,d st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds

d is_a_coproduct_wrt f (*) i1,f (*) i2

proof end;

theorem :: CAT_3:85

for C being Category

for c being Object of C

for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i2 is initial holds

dom i1,c are_isomorphic

for c being Object of C

for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i2 is initial holds

dom i1,c are_isomorphic

proof end;

theorem :: CAT_3:86

for C being Category

for c being Object of C

for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i1 is initial holds

dom i2,c are_isomorphic

for c being Object of C

for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i1 is initial holds

dom i2,c are_isomorphic

proof end;