:: by Marco Riccardi

::

:: Received August 15, 2015

:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Th1: :: CAT_8:1

for C being associative composable CategoryStr

for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 holds

(f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3)

for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 holds

(f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3)

proof end;

theorem Th2: :: CAT_8:2

for C being associative composable CategoryStr

for f1, f2, f3, f4 being morphism of C st f1 |> f2 & f2 |> f3 & f3 |> f4 holds

( ((f1 (*) f2) (*) f3) (*) f4 = (f1 (*) f2) (*) (f3 (*) f4) & ((f1 (*) f2) (*) f3) (*) f4 = (f1 (*) (f2 (*) f3)) (*) f4 & ((f1 (*) f2) (*) f3) (*) f4 = f1 (*) ((f2 (*) f3) (*) f4) & ((f1 (*) f2) (*) f3) (*) f4 = f1 (*) (f2 (*) (f3 (*) f4)) )

for f1, f2, f3, f4 being morphism of C st f1 |> f2 & f2 |> f3 & f3 |> f4 holds

( ((f1 (*) f2) (*) f3) (*) f4 = (f1 (*) f2) (*) (f3 (*) f4) & ((f1 (*) f2) (*) f3) (*) f4 = (f1 (*) (f2 (*) f3)) (*) f4 & ((f1 (*) f2) (*) f3) (*) f4 = f1 (*) ((f2 (*) f3) (*) f4) & ((f1 (*) f2) (*) f3) (*) f4 = f1 (*) (f2 (*) (f3 (*) f4)) )

proof end;

theorem Th3: :: CAT_8:3

for C being composable CategoryStr

for f, f1, f2 being morphism of C st f1 |> f2 holds

( ( f1 (*) f2 |> f implies f2 |> f ) & ( f2 |> f implies f1 (*) f2 |> f ) & ( f |> f1 (*) f2 implies f |> f1 ) & ( f |> f1 implies f |> f1 (*) f2 ) )

for f, f1, f2 being morphism of C st f1 |> f2 holds

( ( f1 (*) f2 |> f implies f2 |> f ) & ( f2 |> f implies f1 (*) f2 |> f ) & ( f |> f1 (*) f2 implies f |> f1 ) & ( f |> f1 implies f |> f1 (*) f2 ) )

proof end;

theorem Th4: :: CAT_8:4

for C being composable with_identities CategoryStr

for f1, f2 being morphism of C st f1 |> f2 holds

( ( f1 is identity implies f1 (*) f2 = f2 ) & ( f2 is identity implies f1 (*) f2 = f1 ) )

for f1, f2 being morphism of C st f1 |> f2 holds

( ( f1 is identity implies f1 (*) f2 = f2 ) & ( f2 is identity implies f1 (*) f2 = f1 ) )

proof end;

theorem Th5: :: CAT_8:5

for C being non empty with_identities CategoryStr

for f being morphism of C ex f1, f2 being morphism of C st

( f1 is identity & f2 is identity & f1 |> f & f |> f2 )

for f being morphism of C ex f1, f2 being morphism of C st

( f1 is identity & f2 is identity & f1 |> f & f |> f2 )

proof end;

theorem Th6: :: CAT_8:6

for C being CategoryStr

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) = {f} holds

for g being Morphism of a,b holds f = g

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) = {f} holds

for g being Morphism of a,b holds f = g

proof end;

theorem Th7: :: CAT_8:7

for C being CategoryStr

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds

Hom (a,b) = {f}

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds

Hom (a,b) = {f}

proof end;

theorem Th8: :: CAT_8:8

for x being object

for C being CategoryStr st the carrier of C = {x} & the composition of C = {[[x,x],x]} holds

C is non empty category

for C being CategoryStr st the carrier of C = {x} & the composition of C = {[[x,x],x]} holds

C is non empty category

proof end;

registration

let C1 be empty with_identities CategoryStr ;

let C2 be with_identities CategoryStr ;

coherence

for b_{1} being Functor of C1,C2 holds b_{1} is covariant ;

end;
let C2 be with_identities CategoryStr ;

cluster Function-like quasi_total -> covariant for Element of bool [: the carrier of C1, the carrier of C2:];

correctness coherence

for b

proof end;

theorem :: CAT_8:12

for C1, C2 being with_identities CategoryStr

for f being morphism of C1

for F being Functor of C1,C2 st F is covariant & f is identity holds

F . f is identity by CAT_6:def 22, CAT_6:def 25;

for f being morphism of C1

for F being Functor of C1,C2 st F is covariant & f is identity holds

F . f is identity by CAT_6:def 22, CAT_6:def 25;

theorem Th13: :: CAT_8:13

for C1, C2 being with_identities CategoryStr

for f1, f2 being morphism of C1

for F being Functor of C1,C2 st F is covariant & f1 |> f2 holds

( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

for f1, f2 being morphism of C1

for F being Functor of C1,C2 st F is covariant & f1 |> f2 holds

( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

proof end;

theorem Th14: :: CAT_8:14

for C being Category

for f being Morphism of C

for g being morphism of (alter C) st f = g holds

( dom g = id (dom f) & cod g = id (cod f) )

for f being Morphism of C

for g being morphism of (alter C) st f = g holds

( dom g = id (dom f) & cod g = id (cod f) )

proof end;

theorem Th16: :: CAT_8:16

for C being non empty category

for f1, f2 being morphism of C st MORPHISM f1 = MORPHISM f2 holds

f1 = f2

for f1, f2 being morphism of C st MORPHISM f1 = MORPHISM f2 holds

f1 = f2

proof end;

theorem Th17: :: CAT_8:17

for C being non empty category

for F1, F2 being covariant Functor of (OrdC 2),C

for f being morphism of (OrdC 2) st not f is identity & F1 . f = F2 . f holds

F1 = F2

for F1, F2 being covariant Functor of (OrdC 2),C

for f being morphism of (OrdC 2) st not f is identity & F1 . f = F2 . f holds

F1 = F2

proof end;

theorem Th18: :: CAT_8:18

ex f1, f2 being morphism of (OrdC 3) st

( not f1 is identity & not f2 is identity & cod f1 = dom f2 & Ob (OrdC 3) = {(dom f1),(cod f1),(cod f2)} & Mor (OrdC 3) = {(dom f1),(cod f1),(cod f2),f1,f2,(f2 (*) f1)} & dom f1, cod f1, cod f2,f1,f2,f2 (*) f1 are_mutually_distinct )

( not f1 is identity & not f2 is identity & cod f1 = dom f2 & Ob (OrdC 3) = {(dom f1),(cod f1),(cod f2)} & Mor (OrdC 3) = {(dom f1),(cod f1),(cod f2),f1,f2,(f2 (*) f1)} & dom f1, cod f1, cod f2,f1,f2,f2 (*) f1 are_mutually_distinct )

proof end;

definition

let C be non empty category;

let f1, f2 be morphism of C;

assume A1: f1 |> f2 ;

existence

ex b_{1} being covariant Functor of (OrdC 3),C st

for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds

( b_{1} . g1 = f1 & b_{1} . g2 = f2 );

uniqueness

for b_{1}, b_{2} being covariant Functor of (OrdC 3),C st ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds

( b_{1} . g1 = f1 & b_{1} . g2 = f2 ) ) & ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds

( b_{2} . g1 = f1 & b_{2} . g2 = f2 ) ) holds

b_{1} = b_{2};

end;
let f1, f2 be morphism of C;

assume A1: f1 |> f2 ;

func COMPOSITION (f1,f2) -> covariant Functor of (OrdC 3),C means :Def1: :: CAT_8:def 1

for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds

( it . g1 = f1 & it . g2 = f2 );

correctness for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds

( it . g1 = f1 & it . g2 = f2 );

existence

ex b

for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds

( b

uniqueness

for b

( b

( b

b

proof end;

:: deftheorem Def1 defines COMPOSITION CAT_8:def 1 :

for C being non empty category

for f1, f2 being morphism of C st f1 |> f2 holds

for b_{4} being covariant Functor of (OrdC 3),C holds

( b_{4} = COMPOSITION (f1,f2) iff for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds

( b_{4} . g1 = f1 & b_{4} . g2 = f2 ) );

for C being non empty category

for f1, f2 being morphism of C st f1 |> f2 holds

for b

( b

( b

:: deftheorem defines terminal CAT_8:def 2 :

for C being CategoryStr

for a being Object of C holds

( a is terminal iff for b being Object of C holds

( Hom (b,a) <> {} & ex f being Morphism of b,a st

for g being Morphism of b,a holds f = g ) );

for C being CategoryStr

for a being Object of C holds

( a is terminal iff for b being Object of C holds

( Hom (b,a) <> {} & ex f being Morphism of b,a st

for g being Morphism of b,a holds f = g ) );

theorem :: CAT_8:19

for C being CategoryStr

for b being Object of C holds

( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

for b being Object of C holds

( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

proof end;

theorem Th20: :: CAT_8:20

for C being non empty with_identities CategoryStr

for a being Object of C st a is terminal holds

for h being Morphism of a,a holds id- a = h

for a being Object of C st a is terminal holds

for h being Morphism of a,a holds id- a = h

proof end;

theorem :: CAT_8:21

for C being non empty composable with_identities CategoryStr

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

a,b are_isomorphic

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

a,b are_isomorphic

proof end;

theorem :: CAT_8:22

for C being non empty category

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

a is terminal

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

a is terminal

proof end;

theorem :: CAT_8:23

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds

f is monomorphism

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds

f is monomorphism

proof end;

:: deftheorem defines with_terminal_objects CAT_8:def 3 :

for C being category holds

( C is with_terminal_objects iff ex a being Object of C st a is terminal );

for C being category holds

( C is with_terminal_objects iff ex a being Object of C st a is terminal );

registration
end;

:: deftheorem Def4 defines terminal CAT_8:def 4 :

for C being category holds

( C is terminal iff for B being category ex F being Functor of B,C st

( F is covariant & ( for G being Functor of B,C st G is covariant holds

F = G ) ) );

for C being category holds

( C is terminal iff for B being category ex F being Functor of B,C st

( F is covariant & ( for G being Functor of B,C st G is covariant holds

F = G ) ) );

registration

correctness

existence

ex b_{1} being category st

( b_{1} is strict & not b_{1} is empty & b_{1} is terminal );

existence

ex b_{1} being category st

( b_{1} is strict & not b_{1} is terminal );

end;
existence

ex b

( b

proof end;

correctness existence

ex b

( b

proof end;

Lm1: for C being category st C is terminal holds

( not C is empty & C is trivial )

proof end;

registration

correctness

coherence

for b_{1} being category st not b_{1} is empty & b_{1} is trivial holds

b_{1} is terminal ;

coherence

for b_{1} being category st b_{1} is terminal holds

( not b_{1} is empty & b_{1} is trivial );

by Lm1;

end;
coherence

for b

b

proof end;

correctness coherence

for b

( not b

by Lm1;

definition

let C be category;

correctness

existence

ex b_{1} being covariant Functor of C,(OrdC 1) st verum;

uniqueness

for b_{1}, b_{2} being covariant Functor of C,(OrdC 1) holds b_{1} = b_{2};

end;
correctness

existence

ex b

uniqueness

for b

proof end;

:: deftheorem defines ->OrdC1 CAT_8:def 5 :

for C being category

for b_{2} being covariant Functor of C,(OrdC 1) holds

( b_{2} = C ->OrdC1 iff verum );

for C being category

for b

( b

theorem Th29: :: CAT_8:29

for C, C1, C2 being category

for F1 being Functor of C,C1

for F2 being Functor of C,C2 st F1 is covariant & F2 is covariant holds

(C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2

for F1 being Functor of C,C1

for F2 being Functor of C,C2 st F1 is covariant & F2 is covariant holds

(C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2

proof end;

:: deftheorem defines initial CAT_8:def 6 :

for C being CategoryStr

for a being Object of C holds

( a is initial iff for b being Object of C holds

( Hom (a,b) <> {} & ex f being Morphism of a,b st

for g being Morphism of a,b holds f = g ) );

for C being CategoryStr

for a being Object of C holds

( a is initial iff for b being Object of C holds

( Hom (a,b) <> {} & ex f being Morphism of a,b st

for g being Morphism of a,b holds f = g ) );

theorem :: CAT_8:30

for C being CategoryStr

for b being Object of C holds

( b is initial iff for a being Object of C ex f being Morphism of b,a st Hom (b,a) = {f} )

for b being Object of C holds

( b is initial iff for a being Object of C ex f being Morphism of b,a st Hom (b,a) = {f} )

proof end;

theorem Th31: :: CAT_8:31

for C being non empty with_identities CategoryStr

for a being Object of C st a is initial holds

for h being Morphism of a,a holds id- a = h

for a being Object of C st a is initial holds

for h being Morphism of a,a holds id- a = h

proof end;

theorem :: CAT_8:32

for C being non empty composable with_identities CategoryStr

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

a,b are_isomorphic

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

a,b are_isomorphic

proof end;

theorem :: CAT_8:33

for C being non empty category

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

a is initial

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

a is initial

proof end;

theorem :: CAT_8:34

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} & b is initial holds

f is epimorphism

for a, b being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} & b is initial holds

f is epimorphism

proof end;

:: deftheorem defines with_initial_objects CAT_8:def 7 :

for C being category holds

( C is with_initial_objects iff ex a being Object of C st a is initial );

for C being category holds

( C is with_initial_objects iff ex a being Object of C st a is initial );

registration
end;

:: deftheorem Def8 defines initial CAT_8:def 8 :

for C being category holds

( C is initial iff for C1 being category ex F being Functor of C,C1 st

( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds

F = F1 ) ) );

for C being category holds

( C is initial iff for C1 being category ex F being Functor of C,C1 st

( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds

F = F1 ) ) );

registration

correctness

existence

ex b_{1} being category st

( b_{1} is strict & b_{1} is empty & b_{1} is initial );

existence

ex b_{1} being category st

( b_{1} is strict & not b_{1} is initial );

end;
existence

ex b

( b

proof end;

correctness existence

ex b

( b

proof end;

registration

correctness

coherence

for b_{1} being category st b_{1} is empty holds

b_{1} is initial ;

end;
coherence

for b

b

proof end;

definition

let C be category;

correctness

existence

ex b_{1} being covariant Functor of (OrdC 0),C st verum;

uniqueness

for b_{1}, b_{2} being covariant Functor of (OrdC 0),C holds b_{1} = b_{2};

;

end;
correctness

existence

ex b

uniqueness

for b

;

:: deftheorem defines OrdC0-> CAT_8:def 9 :

for C being category

for b_{2} being covariant Functor of (OrdC 0),C holds

( b_{2} = OrdC0-> C iff verum );

for C being category

for b

( b

theorem :: CAT_8:38

definition

let C be category;

let a, b, c be Object of C;

let p1 be Morphism of c,a;

assume Hom (c,a) <> {} ;

let p2 be Morphism of c,b;

assume Hom (c,b) <> {} ;

end;
let a, b, c be Object of C;

let p1 be Morphism of c,a;

assume Hom (c,a) <> {} ;

let p2 be Morphism of c,b;

assume Hom (c,b) <> {} ;

pred c,p1,p2 is_product_of a,b means :Def10: :: CAT_8:def 10

for c1 being Object of C

for q1 being Morphism of c1,a

for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds

( Hom (c1,c) <> {} & ex h being Morphism of c1,c st

( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds

h = h1 ) ) );

for c1 being Object of C

for q1 being Morphism of c1,a

for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds

( Hom (c1,c) <> {} & ex h being Morphism of c1,c st

( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds

h = h1 ) ) );

:: deftheorem Def10 defines is_product_of CAT_8:def 10 :

for C being category

for a, b, c being Object of C

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

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

( c,p1,p2 is_product_of a,b iff for c1 being Object of C

for q1 being Morphism of c1,a

for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds

( Hom (c1,c) <> {} & ex h being Morphism of c1,c st

( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds

h = h1 ) ) ) );

for C being category

for a, b, c being Object of C

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

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

( c,p1,p2 is_product_of a,b iff for c1 being Object of C

for q1 being Morphism of c1,a

for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds

( Hom (c1,c) <> {} & ex h being Morphism of c1,c st

( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds

h = h1 ) ) ) );

theorem :: CAT_8:39

for C being non empty category

for c1, c2, a, b being Object of C

for p1 being Morphism of a,c1

for p2 being Morphism of a,c2

for q1 being Morphism of b,c1

for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds

a,b are_isomorphic

for c1, c2, a, b being Object of C

for p1 being Morphism of a,c1

for p2 being Morphism of a,c2

for q1 being Morphism of b,c1

for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds

a,b are_isomorphic

proof end;

theorem :: CAT_8:40

for C being category

for c1, c2, d being Object of C

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 holds

d,p2,p1 is_product_of c2,c1

for c1, c2, d being Object of C

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 holds

d,p2,p1 is_product_of c2,c1

proof end;

definition

let C be category;

end;
attr C is with_binary_products means :Def11: :: CAT_8:def 11

for a, b being Object of C ex d being Object of C ex p1 being Morphism of d,a ex p2 being Morphism of d,b st

( Hom (d,a) <> {} & Hom (d,b) <> {} & d,p1,p2 is_product_of a,b );

for a, b being Object of C ex d being Object of C ex p1 being Morphism of d,a ex p2 being Morphism of d,b st

( Hom (d,a) <> {} & Hom (d,b) <> {} & d,p1,p2 is_product_of a,b );

:: deftheorem Def11 defines with_binary_products CAT_8:def 11 :

for C being category holds

( C is with_binary_products iff for a, b being Object of C ex d being Object of C ex p1 being Morphism of d,a ex p2 being Morphism of d,b st

( Hom (d,a) <> {} & Hom (d,b) <> {} & d,p1,p2 is_product_of a,b ) );

for C being category holds

( C is with_binary_products iff for a, b being Object of C ex d being Object of C ex p1 being Morphism of d,a ex p2 being Morphism of d,b st

( Hom (d,a) <> {} & Hom (d,b) <> {} & d,p1,p2 is_product_of a,b ) );

registration

correctness

existence

ex b_{1} being category st

( b_{1} is with_binary_products & not b_{1} is empty );

by Th41;

end;
existence

ex b

( b

by Th41;

definition

let C be with_binary_products category;

let c1, c2 be Object of C;

existence

ex b_{1} being triple object ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st

( b_{1} = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 );

end;
let c1, c2 be Object of C;

mode categorical_product of c1,c2 -> triple object means :Def12: :: CAT_8:def 12

ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st

( it = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 );

correctness ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st

( it = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 );

existence

ex b

( b

proof end;

:: deftheorem Def12 defines categorical_product CAT_8:def 12 :

for C being with_binary_products category

for c1, c2 being Object of C

for b_{4} being triple object holds

( b_{4} is categorical_product of c1,c2 iff ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st

( b_{4} = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 ) );

for C being with_binary_products category

for c1, c2 being Object of C

for b

( b

( b

definition

let C be with_binary_products category;

let c1, c2 be Object of C;

correctness

coherence

the categorical_product of c1,c2 `1_3 is Object of C;

end;
let c1, c2 be Object of C;

correctness

coherence

the categorical_product of c1,c2 `1_3 is Object of C;

proof end;

:: deftheorem defines [x] CAT_8:def 13 :

for C being with_binary_products category

for c1, c2 being Object of C holds c1 [x] c2 = the categorical_product of c1,c2 `1_3 ;

for C being with_binary_products category

for c1, c2 being Object of C holds c1 [x] c2 = the categorical_product of c1,c2 `1_3 ;

definition

let C be with_binary_products category;

let c1, c2 be Object of C;

coherence

the categorical_product of c1,c2 `2_3 is Morphism of c1 [x] c2,c1;

coherence

the categorical_product of c1,c2 `3_3 is Morphism of c1 [x] c2,c2;

end;
let c1, c2 be Object of C;

func pr1 (c1,c2) -> Morphism of c1 [x] c2,c1 equals :: CAT_8:def 14

the categorical_product of c1,c2 `2_3 ;

correctness the categorical_product of c1,c2 `2_3 ;

coherence

the categorical_product of c1,c2 `2_3 is Morphism of c1 [x] c2,c1;

proof end;

func pr2 (c1,c2) -> Morphism of c1 [x] c2,c2 equals :: CAT_8:def 15

the categorical_product of c1,c2 `3_3 ;

correctness the categorical_product of c1,c2 `3_3 ;

coherence

the categorical_product of c1,c2 `3_3 is Morphism of c1 [x] c2,c2;

proof end;

:: deftheorem defines pr1 CAT_8:def 14 :

for C being with_binary_products category

for c1, c2 being Object of C holds pr1 (c1,c2) = the categorical_product of c1,c2 `2_3 ;

for C being with_binary_products category

for c1, c2 being Object of C holds pr1 (c1,c2) = the categorical_product of c1,c2 `2_3 ;

:: deftheorem defines pr2 CAT_8:def 15 :

for C being with_binary_products category

for c1, c2 being Object of C holds pr2 (c1,c2) = the categorical_product of c1,c2 `3_3 ;

for C being with_binary_products category

for c1, c2 being Object of C holds pr2 (c1,c2) = the categorical_product of c1,c2 `3_3 ;

theorem Th42: :: CAT_8:42

for C being with_binary_products category

for a, b being Object of C holds

( a [x] b, pr1 (a,b), pr2 (a,b) is_product_of a,b & Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )

for a, b being Object of C holds

( a [x] b, pr1 (a,b), pr2 (a,b) is_product_of a,b & Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )

proof end;

theorem :: CAT_8:43

for C being with_binary_products category

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

Hom (c,(a [x] b)) <> {}

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

Hom (c,(a [x] b)) <> {}

proof end;

theorem Th44: :: CAT_8:44

for C being with_binary_products category

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

Hom ((a [x] c),(b [x] d)) <> {}

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

Hom ((a [x] c),(b [x] d)) <> {}

proof end;

definition

let C be with_binary_products category;

let a, b, c, d be Object of C;

let f be Morphism of a,b;

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

let g be Morphism of c,d;

assume A2: Hom (c,d) <> {} ;

existence

ex b_{1} being Morphism of a [x] c,b [x] d st

( f * (pr1 (a,c)) = (pr1 (b,d)) * b_{1} & g * (pr2 (a,c)) = (pr2 (b,d)) * b_{1} );

uniqueness

for b_{1}, b_{2} being Morphism of a [x] c,b [x] d st f * (pr1 (a,c)) = (pr1 (b,d)) * b_{1} & g * (pr2 (a,c)) = (pr2 (b,d)) * b_{1} & f * (pr1 (a,c)) = (pr1 (b,d)) * b_{2} & g * (pr2 (a,c)) = (pr2 (b,d)) * b_{2} holds

b_{1} = b_{2};

end;
let a, b, c, d be Object of C;

let f be Morphism of a,b;

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

let g be Morphism of c,d;

assume A2: Hom (c,d) <> {} ;

func f [x] g -> Morphism of a [x] c,b [x] d means :Def16: :: CAT_8:def 16

( f * (pr1 (a,c)) = (pr1 (b,d)) * it & g * (pr2 (a,c)) = (pr2 (b,d)) * it );

correctness ( f * (pr1 (a,c)) = (pr1 (b,d)) * it & g * (pr2 (a,c)) = (pr2 (b,d)) * it );

existence

ex b

( f * (pr1 (a,c)) = (pr1 (b,d)) * b

uniqueness

for b

b

proof end;

:: deftheorem Def16 defines [x] CAT_8:def 16 :

for C being with_binary_products category

for a, b, c, d being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} holds

for g being Morphism of c,d st Hom (c,d) <> {} holds

for b_{8} being Morphism of a [x] c,b [x] d holds

( b_{8} = f [x] g iff ( f * (pr1 (a,c)) = (pr1 (b,d)) * b_{8} & g * (pr2 (a,c)) = (pr2 (b,d)) * b_{8} ) );

for C being with_binary_products category

for a, b, c, d being Object of C

for f being Morphism of a,b st Hom (a,b) <> {} holds

for g being Morphism of c,d st Hom (c,d) <> {} holds

for b

( b

definition

let C1, C2, D be category;

let P1 be Functor of D,C1;

assume P1 is covariant ;

let P2 be Functor of D,C2;

assume P2 is covariant ;

end;
let P1 be Functor of D,C1;

assume P1 is covariant ;

let P2 be Functor of D,C2;

assume P2 is covariant ;

pred D,P1,P2 is_product_of C1,C2 means :Def17: :: CAT_8:def 17

for D1 being category

for G1 being Functor of D1,C1

for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant holds

ex H being Functor of D1,D st

( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1 ) );

for D1 being category

for G1 being Functor of D1,C1

for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant holds

ex H being Functor of D1,D st

( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1 ) );

:: deftheorem Def17 defines is_product_of CAT_8:def 17 :

for C1, C2, D being category

for P1 being Functor of D,C1 st P1 is covariant holds

for P2 being Functor of D,C2 st P2 is covariant holds

( D,P1,P2 is_product_of C1,C2 iff for D1 being category

for G1 being Functor of D1,C1

for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant holds

ex H being Functor of D1,D st

( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1 ) ) );

for C1, C2, D being category

for P1 being Functor of D,C1 st P1 is covariant holds

for P2 being Functor of D,C2 st P2 is covariant holds

( D,P1,P2 is_product_of C1,C2 iff for D1 being category

for G1 being Functor of D1,C1

for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant holds

ex H being Functor of D1,D st

( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1 ) ) );

theorem :: CAT_8:45

for C1, C2, A, B being category

for P1 being Functor of A,C1

for P2 being Functor of A,C2

for Q1 being Functor of B,C1

for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds

A ~= B

for P1 being Functor of A,C1

for P2 being Functor of A,C2

for Q1 being Functor of B,C1

for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds

A ~= B

proof end;

theorem :: CAT_8:46

for C1, C2, D being category

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 holds

D,P2,P1 is_product_of C2,C1

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 holds

D,P2,P1 is_product_of C2,C1

proof end;

notation

let C, C1, C2 be category;

let F1 be Functor of C1,C;

let F2 be Functor of C2,C;

synonym F1 [|x|] F2 for [|F1,F2|];

end;
let F1 be Functor of C1,C;

let F2 be Functor of C2,C;

synonym F1 [|x|] F2 for [|F1,F2|];

theorem Th47: :: CAT_8:47

for C1, C2 being category holds (C1 ->OrdC1) [|x|] (C2 ->OrdC1), pr1 ((C1 ->OrdC1),(C2 ->OrdC1)), pr2 ((C1 ->OrdC1),(C2 ->OrdC1)) is_product_of C1,C2

proof end;

definition

let C1, C2 be category;

existence

ex b_{1} being triple object ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( b_{1} = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 );

end;
mode categorical_product of C1,C2 -> triple object means :Def18: :: CAT_8:def 18

ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( it = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 );

correctness ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( it = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 );

existence

ex b

( b

proof end;

:: deftheorem Def18 defines categorical_product CAT_8:def 18 :

for C1, C2 being category

for b_{3} being triple object holds

( b_{3} is categorical_product of C1,C2 iff ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( b_{3} = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 ) );

for C1, C2 being category

for b

( b

( b

definition

let C1, C2 be category;

correctness

coherence

the categorical_product of C1,C2 `1_3 is strict category;

end;
correctness

coherence

the categorical_product of C1,C2 `1_3 is strict category;

proof end;

:: deftheorem defines [x] CAT_8:def 19 :

for C1, C2 being category holds C1 [x] C2 = the categorical_product of C1,C2 `1_3 ;

for C1, C2 being category holds C1 [x] C2 = the categorical_product of C1,C2 `1_3 ;

definition

let C1, C2 be category;

coherence

the categorical_product of C1,C2 `2_3 is Functor of (C1 [x] C2),C1;

coherence

the categorical_product of C1,C2 `3_3 is Functor of (C1 [x] C2),C2;

end;
func pr1 (C1,C2) -> Functor of (C1 [x] C2),C1 equals :: CAT_8:def 20

the categorical_product of C1,C2 `2_3 ;

correctness the categorical_product of C1,C2 `2_3 ;

coherence

the categorical_product of C1,C2 `2_3 is Functor of (C1 [x] C2),C1;

proof end;

func pr2 (C1,C2) -> Functor of (C1 [x] C2),C2 equals :: CAT_8:def 21

the categorical_product of C1,C2 `3_3 ;

correctness the categorical_product of C1,C2 `3_3 ;

coherence

the categorical_product of C1,C2 `3_3 is Functor of (C1 [x] C2),C2;

proof end;

:: deftheorem defines pr1 CAT_8:def 20 :

for C1, C2 being category holds pr1 (C1,C2) = the categorical_product of C1,C2 `2_3 ;

for C1, C2 being category holds pr1 (C1,C2) = the categorical_product of C1,C2 `2_3 ;

:: deftheorem defines pr2 CAT_8:def 21 :

for C1, C2 being category holds pr2 (C1,C2) = the categorical_product of C1,C2 `3_3 ;

for C1, C2 being category holds pr2 (C1,C2) = the categorical_product of C1,C2 `3_3 ;

registration

let C1, C2 be category;

correctness

coherence

pr1 (C1,C2) is covariant ;

coherence

pr2 (C1,C2) is covariant ;

end;
correctness

coherence

pr1 (C1,C2) is covariant ;

proof end;

correctness coherence

pr2 (C1,C2) is covariant ;

proof end;

theorem Th49: :: CAT_8:49

for C1, C2 being category holds

( not C1 [x] C2 is empty iff ( not C1 is empty & not C2 is empty ) )

( not C1 [x] C2 is empty iff ( not C1 is empty & not C2 is empty ) )

proof end;

registration
end;

registration
end;

registration
end;

definition

let C1, C2, D1, D2 be category;

let F1 be Functor of C1,D1;

let F2 be Functor of C2,D2;

assume A1: ( F1 is covariant & F2 is covariant ) ;

existence

ex b_{1} being Functor of (C1 [x] C2),(D1 [x] D2) st

( b_{1} is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b_{1} & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b_{1} );

uniqueness

for b_{1}, b_{2} being Functor of (C1 [x] C2),(D1 [x] D2) st b_{1} is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b_{1} & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b_{1} & b_{2} is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b_{2} & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b_{2} holds

b_{1} = b_{2};

end;
let F1 be Functor of C1,D1;

let F2 be Functor of C2,D2;

assume A1: ( F1 is covariant & F2 is covariant ) ;

func F1 [x] F2 -> Functor of (C1 [x] C2),(D1 [x] D2) means :Def22: :: CAT_8:def 22

( it is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) it & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) it );

correctness ( it is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) it & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) it );

existence

ex b

( b

uniqueness

for b

b

proof end;

:: deftheorem Def22 defines [x] CAT_8:def 22 :

for C1, C2, D1, D2 being category

for F1 being Functor of C1,D1

for F2 being Functor of C2,D2 st F1 is covariant & F2 is covariant holds

for b_{7} being Functor of (C1 [x] C2),(D1 [x] D2) holds

( b_{7} = F1 [x] F2 iff ( b_{7} is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b_{7} & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b_{7} ) );

for C1, C2, D1, D2 being category

for F1 being Functor of C1,D1

for F2 being Functor of C2,D2 st F1 is covariant & F2 is covariant holds

for b

( b

theorem Th50: :: CAT_8:50

for A1, A2, B1, B2, C1, C2 being category

for F1 being Functor of A1,B1

for F2 being Functor of A2,B2

for G1 being Functor of B1,C1

for G2 being Functor of B2,C2 st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant holds

(G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)

for F1 being Functor of A1,B1

for F2 being Functor of A2,B2

for G1 being Functor of B1,C1

for G2 being Functor of B2,C2 st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant holds

(G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)

proof end;

definition

let C1, C2 be category;

let f1 be morphism of C1;

let f2 be morphism of C2;

consistency

for b_{1} being morphism of (C1 [x] C2) holds verum;

existence

( ( for b_{1} being morphism of (C1 [x] C2) holds verum ) & ( not C1 is empty & not C2 is empty implies ex b_{1} being morphism of (C1 [x] C2) st

( (pr1 (C1,C2)) . b_{1} = f1 & (pr2 (C1,C2)) . b_{1} = f2 ) ) & ( ( C1 is empty or C2 is empty ) implies ex b_{1} being morphism of (C1 [x] C2) st b_{1} = the morphism of (C1 [x] C2) ) );

uniqueness

for b_{1}, b_{2} being morphism of (C1 [x] C2) holds

( ( not C1 is empty & not C2 is empty & (pr1 (C1,C2)) . b_{1} = f1 & (pr2 (C1,C2)) . b_{1} = f2 & (pr1 (C1,C2)) . b_{2} = f1 & (pr2 (C1,C2)) . b_{2} = f2 implies b_{1} = b_{2} ) & ( ( C1 is empty or C2 is empty ) & b_{1} = the morphism of (C1 [x] C2) & b_{2} = the morphism of (C1 [x] C2) implies b_{1} = b_{2} ) );

end;
let f1 be morphism of C1;

let f2 be morphism of C2;

func [f1,f2] -> morphism of (C1 [x] C2) means :Def23: :: CAT_8:def 23

( (pr1 (C1,C2)) . it = f1 & (pr2 (C1,C2)) . it = f2 ) if ( not C1 is empty & not C2 is empty )

otherwise it = the morphism of (C1 [x] C2);

correctness ( (pr1 (C1,C2)) . it = f1 & (pr2 (C1,C2)) . it = f2 ) if ( not C1 is empty & not C2 is empty )

otherwise it = the morphism of (C1 [x] C2);

consistency

for b

existence

( ( for b

( (pr1 (C1,C2)) . b

uniqueness

for b

( ( not C1 is empty & not C2 is empty & (pr1 (C1,C2)) . b

proof end;

:: deftheorem Def23 defines [ CAT_8:def 23 :

for C1, C2 being category

for f1 being morphism of C1

for f2 being morphism of C2

for b_{5} being morphism of (C1 [x] C2) holds

( ( not C1 is empty & not C2 is empty implies ( b_{5} = [f1,f2] iff ( (pr1 (C1,C2)) . b_{5} = f1 & (pr2 (C1,C2)) . b_{5} = f2 ) ) ) & ( ( C1 is empty or C2 is empty ) implies ( b_{5} = [f1,f2] iff b_{5} = the morphism of (C1 [x] C2) ) ) );

for C1, C2 being category

for f1 being morphism of C1

for f2 being morphism of C2

for b

( ( not C1 is empty & not C2 is empty implies ( b

theorem Th52: :: CAT_8:52

for C1, C2 being category

for f being morphism of (C1 [x] C2) ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]

for f being morphism of (C1 [x] C2) ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]

proof end;

Lm2: for C1, C2 being non empty category

for f1, g1 being morphism of C1

for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds

[f1,f2] |> [g1,g2]

proof end;

theorem Th53: :: CAT_8:53

for C1, C2 being non empty category

for f1, g1 being morphism of C1

for f2, g2 being morphism of C2 st [f1,f2] = [g1,g2] holds

( f1 = g1 & f2 = g2 )

for f1, g1 being morphism of C1

for f2, g2 being morphism of C2 st [f1,f2] = [g1,g2] holds

( f1 = g1 & f2 = g2 )

proof end;

theorem Th54: :: CAT_8:54

for C1, C2 being category

for f1, g1 being morphism of C1

for f2, g2 being morphism of C2 holds

( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )

for f1, g1 being morphism of C1

for f2, g2 being morphism of C2 holds

( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )

proof end;

theorem Th55: :: CAT_8:55

for C1, C2 being category

for f1, g1 being morphism of C1

for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds

[f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)]

for f1, g1 being morphism of C1

for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds

[f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)]

proof end;

theorem Th56: :: CAT_8:56

for C1, C2 being category

for f1 being morphism of C1

for f2 being morphism of C2

for f being morphism of (C1 [x] C2) st f = [f1,f2] & not C1 is empty & not C2 is empty holds

( f is identity iff ( f1 is identity & f2 is identity ) )

for f1 being morphism of C1

for f2 being morphism of C2

for f being morphism of (C1 [x] C2) st f = [f1,f2] & not C1 is empty & not C2 is empty holds

( f is identity iff ( f1 is identity & f2 is identity ) )

proof end;

theorem Th57: :: CAT_8:57

for C1, C2 being non empty category

for D1, D2 being category

for F1 being Functor of C1,D1

for F2 being Functor of C2,D2

for c1 being morphism of C1

for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds

(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]

for D1, D2 being category

for F1 being Functor of C1,D1

for F2 being Functor of C2,D2

for c1 being morphism of C1

for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds

(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]

proof end;

:: deftheorem defines is_natural_transformation_of CAT_8:def 24 :

for C1, C2 being category

for F1, F2, T being Functor of C1,C2 holds

( T is_natural_transformation_of F1,F2 iff for f1, f2 being morphism of C1 st f1 |> f2 holds

( T . f1 |> F1 . f2 & F2 . f1 |> T . f2 & T . (f1 (*) f2) = (T . f1) (*) (F1 . f2) & T . (f1 (*) f2) = (F2 . f1) (*) (T . f2) ) );

for C1, C2 being category

for F1, F2, T being Functor of C1,C2 holds

( T is_natural_transformation_of F1,F2 iff for f1, f2 being morphism of C1 st f1 |> f2 holds

( T . f1 |> F1 . f2 & F2 . f1 |> T . f2 & T . (f1 (*) f2) = (T . f1) (*) (F1 . f2) & T . (f1 (*) f2) = (F2 . f1) (*) (T . f2) ) );

theorem Th58: :: CAT_8:58

for C1, C2 being category

for F1, F2, T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds

( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds

( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )

for F1, F2, T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds

( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds

( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )

proof end;

theorem :: CAT_8:59

for C1, C2 being non empty category

for F1, F2 being covariant Functor of C1,C2

for T being Function of (Ob C1),(Mor C2) holds

( ex T1 being Functor of C1,C2 st

( T = T1 | (Ob C1) & T1 is_natural_transformation_of F1,F2 ) iff ( ( for a being Object of C1 holds T . a in Hom ((F1 . a),(F2 . a)) ) & ( for a1, a2 being Object of C1

for f being Morphism of a1,a2 st Hom (a1,a2) <> {} holds

(T . a2) (*) (F1 . f) = (F2 . f) (*) (T . a1) ) ) )

for F1, F2 being covariant Functor of C1,C2

for T being Function of (Ob C1),(Mor C2) holds

( ex T1 being Functor of C1,C2 st

( T = T1 | (Ob C1) & T1 is_natural_transformation_of F1,F2 ) iff ( ( for a being Object of C1 holds T . a in Hom ((F1 . a),(F2 . a)) ) & ( for a1, a2 being Object of C1

for f being Morphism of a1,a2 st Hom (a1,a2) <> {} holds

(T . a2) (*) (F1 . f) = (F2 . f) (*) (T . a1) ) ) )

proof end;

theorem :: CAT_8:60

for C, D being Category

for F1, F2 being Functor of C,D

for G1, G2, T being Functor of (alter C),(alter D) st F1 = G1 & F2 = G2 & T is_natural_transformation_of G1,G2 holds

(IdMap C) * T is natural_transformation of F1,F2

for F1, F2 being Functor of C,D

for G1, G2, T being Functor of (alter C),(alter D) st F1 = G1 & F2 = G2 & T is_natural_transformation_of G1,G2 holds

(IdMap C) * T is natural_transformation of F1,F2

proof end;

definition

let C, D be category;

let F1, F2 be Functor of C,D;

end;
let F1, F2 be Functor of C,D;

pred F1 is_naturally_transformable_to F2 means :: CAT_8:def 25

ex T being Functor of C,D st T is_natural_transformation_of F1,F2;

ex T being Functor of C,D st T is_natural_transformation_of F1,F2;

:: deftheorem defines is_naturally_transformable_to CAT_8:def 25 :

for C, D being category

for F1, F2 being Functor of C,D holds

( F1 is_naturally_transformable_to F2 iff ex T being Functor of C,D st T is_natural_transformation_of F1,F2 );

for C, D being category

for F1, F2 being Functor of C,D holds

( F1 is_naturally_transformable_to F2 iff ex T being Functor of C,D st T is_natural_transformation_of F1,F2 );

definition

let C, D be category;

let F1, F2 be Functor of C,D;

assume A1: F1 is_naturally_transformable_to F2 ;

existence

ex b_{1} being Functor of C,D st b_{1} is_natural_transformation_of F1,F2;

by A1;

end;
let F1, F2 be Functor of C,D;

assume A1: F1 is_naturally_transformable_to F2 ;

mode natural_transformation of F1,F2 -> Functor of C,D means :Def26: :: CAT_8:def 26

it is_natural_transformation_of F1,F2;

correctness it is_natural_transformation_of F1,F2;

existence

ex b

by A1;

:: deftheorem Def26 defines natural_transformation CAT_8:def 26 :

for C, D being category

for F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F2 holds

for b_{5} being Functor of C,D holds

( b_{5} is natural_transformation of F1,F2 iff b_{5} is_natural_transformation_of F1,F2 );

for C, D being category

for F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F2 holds

for b

( b

theorem Th61: :: CAT_8:61

for C, D being category

for F being Functor of C,D st F is covariant holds

F is_natural_transformation_of F,F

for F being Functor of C,D st F is covariant holds

F is_natural_transformation_of F,F

proof end;

Lm3: for C, D being category

for F, F1, F2 being Functor of C,D

for T1 being natural_transformation of F1,F

for T2 being natural_transformation of F,F2 st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds

ex T being natural_transformation of F1,F2 st

( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )

proof end;

definition

let C, D be category;

let F, F1, F2 be Functor of C,D;

assume that

A1: ( F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 ) and

A2: ( F is covariant & F1 is covariant & F2 is covariant ) ;

let T1 be natural_transformation of F1,F;

let T2 be natural_transformation of F,F2;

ex b_{1} being natural_transformation of F1,F2 st

for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

b_{1} . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1)

for b_{1}, b_{2} being natural_transformation of F1,F2 st ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

b_{1} . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

b_{2} . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) holds

b_{1} = b_{2}

end;
let F, F1, F2 be Functor of C,D;

assume that

A1: ( F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 ) and

A2: ( F is covariant & F1 is covariant & F2 is covariant ) ;

let T1 be natural_transformation of F1,F;

let T2 be natural_transformation of F,F2;

func T2 `*` T1 -> natural_transformation of F1,F2 means :Def27: :: CAT_8:def 27

for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

it . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1);

existence for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

it . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1);

ex b

for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def27 defines `*` CAT_8:def 27 :

for C, D being category

for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds

for T1 being natural_transformation of F1,F

for T2 being natural_transformation of F,F2

for b_{8} being natural_transformation of F1,F2 holds

( b_{8} = T2 `*` T1 iff for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds

b_{8} . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) );

for C, D being category

for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds

for T1 being natural_transformation of F1,F

for T2 being natural_transformation of F,F2

for b

( b

b

theorem Th62: :: CAT_8:62

for C, D being category

for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds

F1 is_naturally_transformable_to F2

for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds

F1 is_naturally_transformable_to F2

proof end;

Lm4: for C1, C2 being category

for X being set st not C1 is empty & C2 is empty & X = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } holds

( X = {} & { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {} )

proof end;

Lm5: for C1, C2 being category

for X1, X2 being set st C1 is empty & X1 = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & X2 = [[{},{}],{}] holds

( X1 = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {[[X2,X2],X2]} )

proof end;

definition

let C1, C2 be category;

ex b_{1} being strict category st

( the carrier of b_{1} = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b_{1} = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b_{1} : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )

for b_{1}, b_{2} being strict category st the carrier of b_{1} = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b_{1} = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b_{1} : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } & the carrier of b_{2} = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b_{2} = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b_{2} : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } holds

b_{1} = b_{2}
;

end;
func Functors (C1,C2) -> strict category means :Def28: :: CAT_8:def 28

( the carrier of it = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of it = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of it : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } );

existence ( the carrier of it = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of it = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of it : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } );

ex b

( the carrier of b

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )

proof end;

uniqueness for b

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } & the carrier of b

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } holds

b

:: deftheorem Def28 defines Functors CAT_8:def 28 :

for C1, C2 being category

for b_{3} being strict category holds

( b_{3} = Functors (C1,C2) iff ( the carrier of b_{3} = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b_{3} = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b_{3} : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ) );

for C1, C2 being category

for b

( b

( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ) );

registration

let C1 be non empty category;

let C2 be empty category;

correctness

coherence

Functors (C1,C2) is empty ;

end;
let C2 be empty category;

correctness

coherence

Functors (C1,C2) is empty ;

proof end;

registration

let C1 be empty category;

let C2 be category;

correctness

coherence

( not Functors (C1,C2) is empty & Functors (C1,C2) is trivial );

end;
let C2 be category;

correctness

coherence

( not Functors (C1,C2) is empty & Functors (C1,C2) is trivial );

proof end;

registration
end;

theorem Th63: :: CAT_8:63

for C1, C2 being non empty category

for f1, f2 being morphism of (Functors (C1,C2)) holds

( f1 |> f2 iff ex F, F1, F2 being covariant Functor of C1,C2 ex T1 being natural_transformation of F1,F ex T2 being natural_transformation of F,F2 st

( f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1 (*) f2 = [[F1,F2],(T2 `*` T1)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds

( T2 . g2 |> T1 . g1 & (T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) ) )

for f1, f2 being morphism of (Functors (C1,C2)) holds

( f1 |> f2 iff ex F, F1, F2 being covariant Functor of C1,C2 ex T1 being natural_transformation of F1,F ex T2 being natural_transformation of F,F2 st

( f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1 (*) f2 = [[F1,F2],(T2 `*` T1)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds

( T2 . g2 |> T1 . g1 & (T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) ) )

proof end;

theorem Th64: :: CAT_8:64

for C1, C2 being non empty category

for f being morphism of (Functors (C1,C2)) holds

( f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F] )

for f being morphism of (Functors (C1,C2)) holds

( f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F] )

proof end;

theorem Th65: :: CAT_8:65

for C1, C2 being non empty category

for f being morphism of (Functors (C1,C2)) ex F1, F2 being covariant Functor of C1,C2 ex T being natural_transformation of F1,F2 st

( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )

for f being morphism of (Functors (C1,C2)) ex F1, F2 being covariant Functor of C1,C2 ex T being natural_transformation of F1,F2 st

( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )

proof end;

definition

let C be non empty with_binary_products category;

let a, b, c be Object of C;

let e be Morphism of c [x] a,b;

assume Hom ((c [x] a),b) <> {} ;

end;
let a, b, c be Object of C;

let e be Morphism of c [x] a,b;

assume Hom ((c [x] a),b) <> {} ;

pred c,e is_exponent_of a,b means :Def29: :: CAT_8:def 29

for d being Object of C

for f being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds

( Hom (d,c) <> {} & ex h being Morphism of d,c st

( f = e * (h [x] (id- a)) & ( for h1 being Morphism of d,c st f = e * (h1 [x] (id- a)) holds

h = h1 ) ) );

for d being Object of C

for f being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds

( Hom (d,c) <> {} & ex h being Morphism of d,c st

( f = e * (h [x] (id- a)) & ( for h1 being Morphism of d,c st f = e * (h1 [x] (id- a)) holds

h = h1 ) ) );

:: deftheorem Def29 defines is_exponent_of CAT_8:def 29 :

for C being non empty with_binary_products category

for a, b, c being Object of C

for e being Morphism of c [x] a,b st Hom ((c [x] a),b) <> {} holds

( c,e is_exponent_of a,b iff for d being Object of C

for f being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds

( Hom (d,c) <> {} & ex h being Morphism of d,c st

( f = e * (h [x] (id- a)) & ( for h1 being Morphism of d,c st f = e * (h1 [x] (id- a)) holds

h = h1 ) ) ) );

for C being non empty with_binary_products category

for a, b, c being Object of C

for e being Morphism of c [x] a,b st Hom ((c [x] a),b) <> {} holds

( c,e is_exponent_of a,b iff for d being Object of C

for f being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds

( Hom (d,c) <> {} & ex h being Morphism of d,c st

( f = e * (h [x] (id- a)) & ( for h1 being Morphism of d,c st f = e * (h1 [x] (id- a)) holds

h = h1 ) ) ) );

theorem Th66: :: CAT_8:66

for C being with_binary_products category

for a1, a2, b1, b2, c1, c2 being Object of C

for f1 being Morphism of a1,b1

for f2 being Morphism of a2,b2

for g1 being Morphism of b1,c1

for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds

(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)

for a1, a2, b1, b2, c1, c2 being Object of C

for f1 being Morphism of a1,b1

for f2 being Morphism of a2,b2

for g1 being Morphism of b1,c1

for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds

(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)

proof end;

theorem Th67: :: CAT_8:67

for C being non empty with_binary_products category

for a, b being Object of C holds (id- a) [x] (id- b) = id- (a [x] b)

for a, b being Object of C holds (id- a) [x] (id- b) = id- (a [x] b)

proof end;

theorem :: CAT_8:68

for C being non empty with_binary_products category

for a, b, c1, c2 being Object of C

for e1 being Morphism of c1 [x] a,b

for e2 being Morphism of c2 [x] a,b st Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b holds

c1,c2 are_isomorphic

for a, b, c1, c2 being Object of C

for e1 being Morphism of c1 [x] a,b

for e2 being Morphism of c2 [x] a,b st Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b holds

c1,c2 are_isomorphic

proof end;

definition

let C be non empty with_binary_products category;

end;
attr C is with_exponential_objects means :Def30: :: CAT_8:def 30

for a, b being Object of C ex c being Object of C ex e being Morphism of c [x] a,b st

( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

for a, b being Object of C ex c being Object of C ex e being Morphism of c [x] a,b st

( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

:: deftheorem Def30 defines with_exponential_objects CAT_8:def 30 :

for C being non empty with_binary_products category holds

( C is with_exponential_objects iff for a, b being Object of C ex c being Object of C ex e being Morphism of c [x] a,b st

( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b ) );

for C being non empty with_binary_products category holds

( C is with_exponential_objects iff for a, b being Object of C ex c being Object of C ex e being Morphism of c [x] a,b st

( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b ) );

registration

existence

ex b_{1} being non empty with_binary_products category st b_{1} is with_exponential_objects ;

by Th69;

end;

cluster non empty associative composable with_identities with_binary_products with_exponential_objects for CategoryStr ;

correctness existence

ex b

by Th69;

definition

let C be non empty with_binary_products with_exponential_objects category;

let a, b be Object of C;

existence

ex b_{1} being pair object ex c being Object of C ex e being Morphism of c [x] a,b st

( b_{1} = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

end;
let a, b be Object of C;

mode categorical_exponent of a,b -> pair object means :Def31: :: CAT_8:def 31

ex c being Object of C ex e being Morphism of c [x] a,b st

( it = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

correctness ex c being Object of C ex e being Morphism of c [x] a,b st

( it = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

existence

ex b

( b

proof end;

:: deftheorem Def31 defines categorical_exponent CAT_8:def 31 :

for C being non empty with_binary_products with_exponential_objects category

for a, b being Object of C

for b_{4} being pair object holds

( b_{4} is categorical_exponent of a,b iff ex c being Object of C ex e being Morphism of c [x] a,b st

( b_{4} = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b ) );

for C being non empty with_binary_products with_exponential_objects category

for a, b being Object of C

for b

( b

( b

definition

let C be non empty with_binary_products with_exponential_objects category;

let a, b be Object of C;

correctness

coherence

the categorical_exponent of a,b `1 is Object of C;

end;
let a, b be Object of C;

correctness

coherence

the categorical_exponent of a,b `1 is Object of C;

proof end;

:: deftheorem defines |^ CAT_8:def 32 :

for C being non empty with_binary_products with_exponential_objects category

for a, b being Object of C holds b |^ a = the categorical_exponent of a,b `1 ;

for C being non empty with_binary_products with_exponential_objects category

for a, b being Object of C holds b |^ a = the categorical_exponent of a,b `1 ;

definition

let C be non empty with_binary_products with_exponential_objects category;

let a, b be Object of C;

coherence

the categorical_exponent of a,b `2 is Morphism of (b |^ a) [x] a,b;

end;
let a, b be Object of C;

func eval (a,b) -> Morphism of (b |^ a) [x] a,b equals :: CAT_8:def 33

the categorical_exponent of a,b `2 ;

correctness the categorical_exponent of a,b `2 ;

coherence

the categorical_exponent of a,b `2 is Morphism of (b |^ a) [x] a,b;

proof end;

:: deftheorem defines eval CAT_8:def 33 :

for C being non empty with_binary_products with_exponential_objects category

for a, b being Object of C holds eval (a,b) = the categorical_exponent of a,b `2 ;

for C being non empty with_binary_products with_exponential_objects category

for a, b being Object of C holds eval (a,b) = the categorical_exponent of a,b `2 ;

theorem Th70: :: CAT_8:70

for C being non empty with_binary_products with_exponential_objects category

for a, b being Object of C holds

( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b )

for a, b being Object of C holds

( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b )

proof end;

theorem :: CAT_8:71

for C being non empty with_binary_products with_exponential_objects category

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

ex L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) st

( ( for f being Morphism of c [x] a,b

for h being Morphism of c,b |^ a st h = L . f holds

(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective )

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

ex L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) st

( ( for f being Morphism of c [x] a,b

for h being Morphism of c,b |^ a st h = L . f holds

(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective )

proof end;

definition

let A, B, C be category;

let E be Functor of (C [x] A),B;

assume E is covariant ;

end;
let E be Functor of (C [x] A),B;

assume E is covariant ;

pred C,E is_exponent_of A,B means :Def34: :: CAT_8:def 34

for D being category

for F being Functor of (D [x] A),B st F is covariant holds

ex H being Functor of D,C st

( H is covariant & F = E (*) (H [x] (id A)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id A)) holds

H = H1 ) );

for D being category

for F being Functor of (D [x] A),B st F is covariant holds

ex H being Functor of D,C st

( H is covariant & F = E (*) (H [x] (id A)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id A)) holds

H = H1 ) );

:: deftheorem Def34 defines is_exponent_of CAT_8:def 34 :

for A, B, C being category

for E being Functor of (C [x] A),B st E is covariant holds

( C,E is_exponent_of A,B iff for D being category

for F being Functor of (D [x] A),B st F is covariant holds

ex H being Functor of D,C st

( H is covariant & F = E (*) (H [x] (id A)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id A)) holds

H = H1 ) ) );

for A, B, C being category

for E being Functor of (C [x] A),B st E is covariant holds

( C,E is_exponent_of A,B iff for D being category

for F being Functor of (D [x] A),B st F is covariant holds

ex H being Functor of D,C st

( H is covariant & F = E (*) (H [x] (id A)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id A)) holds

H = H1 ) ) );

Lm6: for C, C1, C2 being non empty category st C = Functors (C1,C2) holds

ex E being Functor of (C [x] C1),C2 st

( E is covariant & ( for D being category

for F being Functor of (D [x] C1),C2 st F is covariant holds

ex H being Functor of D,C st

( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds

H = H1 ) ) ) )

proof end;

Lm7: for C1 being non empty category

for C2 being empty category

for E being Functor of ((OrdC 0) [x] C1),C2 st E = OrdC0-> C2 holds

OrdC 0,E is_exponent_of C1,C2

proof end;

Lm8: for C1 being empty category

for C2 being category

for E being Functor of ((OrdC 1) [x] C1),C2 st E = OrdC0-> C2 holds

OrdC 1,E is_exponent_of C1,C2

proof end;

definition

let C1, C2 be category;

ex b_{1} being pair object ex C being category ex E being Functor of (C [x] C1),C2 st

( b_{1} = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )

end;
mode categorical_exponent of C1,C2 -> pair object means :Def35: :: CAT_8:def 35

ex C being category ex E being Functor of (C [x] C1),C2 st

( it = [C,E] & E is covariant & C,E is_exponent_of C1,C2 );

existence ex C being category ex E being Functor of (C [x] C1),C2 st

( it = [C,E] & E is covariant & C,E is_exponent_of C1,C2 );

ex b

( b

proof end;

:: deftheorem Def35 defines categorical_exponent CAT_8:def 35 :

for C1, C2 being category

for b_{3} being pair object holds

( b_{3} is categorical_exponent of C1,C2 iff ex C being category ex E being Functor of (C [x] C1),C2 st

( b_{3} = [C,E] & E is covariant & C,E is_exponent_of C1,C2 ) );

for C1, C2 being category

for b

( b

( b

definition

let C1, C2 be category;

correctness

coherence

the categorical_exponent of C1,C2 `1 is category;

end;
correctness

coherence

the categorical_exponent of C1,C2 `1 is category;

proof end;

:: deftheorem defines |^ CAT_8:def 36 :

for C1, C2 being category holds C2 |^ C1 = the categorical_exponent of C1,C2 `1 ;

for C1, C2 being category holds C2 |^ C1 = the categorical_exponent of C1,C2 `1 ;

definition

let C1, C2 be category;

coherence

the categorical_exponent of C1,C2 `2 is Functor of ((C2 |^ C1) [x] C1),C2;

end;
func eval (C1,C2) -> Functor of ((C2 |^ C1) [x] C1),C2 equals :: CAT_8:def 37

the categorical_exponent of C1,C2 `2 ;

correctness the categorical_exponent of C1,C2 `2 ;

coherence

the categorical_exponent of C1,C2 `2 is Functor of ((C2 |^ C1) [x] C1),C2;

proof end;

:: deftheorem defines eval CAT_8:def 37 :

for C1, C2 being category holds eval (C1,C2) = the categorical_exponent of C1,C2 `2 ;

for C1, C2 being category holds eval (C1,C2) = the categorical_exponent of C1,C2 `2 ;

theorem Th73: :: CAT_8:73

for A, B, C1, C2 being category

for E1 being Functor of (C1 [x] A),B

for E2 being Functor of (C2 [x] A),B st E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds

C1 ~= C2

for E1 being Functor of (C1 [x] A),B

for E2 being Functor of (C2 [x] A),B st E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds

C1 ~= C2

proof end;

registration
end;

registration

let C1 be non empty category;

let C2 be empty category;

correctness

coherence

C2 |^ C1 is empty ;

end;
let C2 be empty category;

correctness

coherence

C2 |^ C1 is empty ;

proof end;

registration

let C1 be empty category;

let C2 be category;

correctness

coherence

( not C2 |^ C1 is empty & C2 |^ C1 is trivial );

end;
let C2 be category;

correctness

coherence

( not C2 |^ C1 is empty & C2 |^ C1 is trivial );

proof end;

registration
end;