:: by Marco Riccardi

::

:: Received December 31, 2014

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

registration
end;

registration
end;

registration
end;

registration
end;

registration

let C be with_identities CategoryStr ;

let a be Object of C;

correctness

coherence

id- a is identity ;

end;
let a be Object of C;

correctness

coherence

id- a is identity ;

proof end;

theorem Th2: :: CAT_7:2

for C being with_identities CategoryStr

for a being Object of C st not C is empty holds

a in the carrier of C

for a being Object of C st not C is empty holds

a in the carrier of C

proof end;

theorem Th3: :: CAT_7:3

for C being composable CategoryStr

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

f1 |> f3

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

f1 |> f3

proof end;

theorem Th4: :: CAT_7:4

for C being composable with_identities CategoryStr

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

( dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1 )

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

( dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1 )

proof end;

theorem Th5: :: CAT_7:5

for C being non empty composable with_identities CategoryStr

for f1, f2 being morphism of C holds

( f1 |> f2 iff dom f1 = cod f2 )

for f1, f2 being morphism of C holds

( f1 |> f2 iff dom f1 = cod f2 )

proof end;

theorem Th6: :: CAT_7:6

for C being composable with_identities CategoryStr

for f being morphism of C st f is identity holds

( dom f = f & cod f = f )

for f being morphism of C st f is identity holds

( dom f = f & cod f = f )

proof end;

theorem Th7: :: CAT_7:7

for C being composable with_identities CategoryStr

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

f1 = f2

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

f1 = f2

proof end;

theorem Th8: :: CAT_7:8

for C being non empty composable with_identities CategoryStr

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

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

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

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

proof end;

theorem Th9: :: CAT_7:9

for C being non empty composable with_identities CategoryStr

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

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

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

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

proof end;

theorem Th10: :: CAT_7:10

for C1, C2, C3, C4 being category

for F being Functor of C1,C2

for G being Functor of C2,C3

for H being Functor of C3,C4 st F is covariant & G is covariant & H is covariant holds

H (*) (G (*) F) = (H (*) G) (*) F

for F being Functor of C1,C2

for G being Functor of C2,C3

for H being Functor of C3,C4 st F is covariant & G is covariant & H is covariant holds

H (*) (G (*) F) = (H (*) G) (*) F

proof end;

theorem Th11: :: CAT_7:11

for C, D being category

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

( F (*) (id C) = F & (id D) (*) F = F )

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

( F (*) (id C) = F & (id D) (*) F = F )

proof end;

theorem Th12: :: CAT_7:12

for C, D being composable with_identities CategoryStr holds

( C ~= D iff ex F being Functor of C,D st

( F is covariant & F is bijective ) )

( C ~= D iff ex F being Functor of C,D st

( F is covariant & F is bijective ) )

proof end;

theorem Th14: :: CAT_7:14

for C, D being with_identities CategoryStr st C ~= D holds

( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )

( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )

proof end;

definition

let C be CategoryStr ;

let a, b be Object of C;

coherence

{ f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C);

end;
let a, b be Object of C;

func Hom (a,b) -> Subset of (Mor C) equals :: CAT_7:def 1

{ f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ;

correctness { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ;

coherence

{ f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } is Subset of (Mor C);

proof end;

:: deftheorem defines Hom CAT_7:def 1 :

for C being CategoryStr

for a, b being Object of C holds Hom (a,b) = { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ;

for C being CategoryStr

for a, b being Object of C holds Hom (a,b) = { f where f is morphism of C : ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f ) } ;

definition

let C be non empty composable with_identities CategoryStr ;

let a, b be Object of C;

coherence

Hom (a,b) is Subset of (Mor C);

compatibility

for b_{1} being Subset of (Mor C) holds

( b_{1} = Hom (a,b) iff b_{1} = { f where f is morphism of C : ( dom f = a & cod f = b ) } );

end;
let a, b be Object of C;

:: original: Hom

redefine func Hom (a,b) -> Subset of (Mor C) equals :Def2: :: CAT_7:def 2

{ f where f is morphism of C : ( dom f = a & cod f = b ) } ;

correctness redefine func Hom (a,b) -> Subset of (Mor C) equals :Def2: :: CAT_7:def 2

{ f where f is morphism of C : ( dom f = a & cod f = b ) } ;

coherence

Hom (a,b) is Subset of (Mor C);

compatibility

for b

( b

proof end;

:: deftheorem Def2 defines Hom CAT_7:def 2 :

for C being non empty composable with_identities CategoryStr

for a, b being Object of C holds Hom (a,b) = { f where f is morphism of C : ( dom f = a & cod f = b ) } ;

for C being non empty composable with_identities CategoryStr

for a, b being Object of C holds Hom (a,b) = { f where f is morphism of C : ( dom f = a & cod f = b ) } ;

definition

let C be CategoryStr ;

let a, b be Object of C;

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

correctness

existence

ex b_{1} being morphism of C st b_{1} in Hom (a,b);

by A1, SUBSET_1:4;

end;
let a, b be Object of C;

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

correctness

existence

ex b

by A1, SUBSET_1:4;

:: deftheorem Def3 defines Morphism CAT_7:def 3 :

for C being CategoryStr

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

for b_{4} being morphism of C holds

( b_{4} is Morphism of a,b iff b_{4} in Hom (a,b) );

for C being CategoryStr

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

for b

( b

definition

let C be non empty with_identities CategoryStr ;

let a be Object of C;

:: original: id-

redefine func id- a -> Morphism of a,a;

coherence

id- a is Morphism of a,a

end;
let a be Object of C;

:: original: id-

redefine func id- a -> Morphism of a,a;

coherence

id- a is Morphism of a,a

proof end;

registration

let C be non empty with_identities CategoryStr ;

let a be Object of C;

correctness

coherence

not Hom (a,a) is empty ;

end;
let a be Object of C;

correctness

coherence

not Hom (a,a) is empty ;

proof end;

:: like CAT_1

definition

let C be composable with_identities CategoryStr ;

let a, b, c be Object of C;

let f be Morphism of a,b;

let g be Morphism of b,c;

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

correctness

coherence

g (*) f is Morphism of a,c;

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

let f be Morphism of a,b;

let g be Morphism of b,c;

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

correctness

coherence

g (*) f is Morphism of a,c;

proof end;

:: deftheorem Def4 defines * CAT_7:def 4 :

for C being composable with_identities CategoryStr

for a, b, c being Object of C

for f being Morphism of a,b

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

g * f = g (*) f;

for C being composable with_identities CategoryStr

for a, b, c being Object of C

for f being Morphism of a,b

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

g * f = g (*) f;

theorem Th16: :: CAT_7:16

for C being CategoryStr

for a, b being Object of C

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

ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f )

for a, b being Object of C

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

ex f1, f2 being morphism of C st

( a = f1 & b = f2 & f |> f1 & f2 |> f )

proof end;

theorem Th17: :: CAT_7:17

for C being composable with_identities CategoryStr

for a, b, c being Object of C

for f1 being Morphism of a,b

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

f2 |> f1

for a, b, c being Object of C

for f1 being Morphism of a,b

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

f2 |> f1

proof end;

theorem Th18: :: CAT_7:18

for C being non empty composable with_identities CategoryStr

for a, b being Object of C

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

( f * (id- a) = f & (id- b) * f = f )

for a, b being Object of C

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

( f * (id- a) = f & (id- b) * f = f )

proof end;

theorem Th19: :: CAT_7:19

for C being non empty composable with_identities CategoryStr

for f being morphism of C holds f in Hom ((dom f),(cod f)) ;

for f being morphism of C holds f in Hom ((dom f),(cod f)) ;

theorem Th20: :: CAT_7:20

for C being non empty composable with_identities CategoryStr

for a, b being Object of C

for f being morphism of C holds

( f in Hom (a,b) iff ( dom f = a & cod f = b ) )

for a, b being Object of C

for f being morphism of C holds

( f in Hom (a,b) iff ( dom f = a & cod f = b ) )

proof end;

theorem Th21: :: CAT_7:21

for C being non empty composable with_identities CategoryStr

for a being Object of C holds a in Hom (a,a)

for a being Object of C holds a in Hom (a,a)

proof end;

theorem Th22: :: CAT_7:22

for C being composable with_identities CategoryStr

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

Hom (a,c) <> {}

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

Hom (a,c) <> {}

proof end;

theorem Th23: :: CAT_7:23

for C being category

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

for f1 being Morphism of a,b

for f2 being Morphism of b,c

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

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

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

for f1 being Morphism of a,b

for f2 being Morphism of b,c

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

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

proof end;

theorem Th24: :: CAT_7:24

for C being composable with_identities CategoryStr

for a, b, c being Object of C

for f1 being Morphism of a,b

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

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

for a, b, c being Object of C

for f1 being Morphism of a,b

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

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

proof end;

definition

let C be composable with_identities CategoryStr ;

let a, b be Object of C;

let f be Morphism of a,b;

end;
let a, b be Object of C;

let f be Morphism of a,b;

:: deftheorem defines monomorphism CAT_7:def 5 :

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

for g1, g2 being Morphism of c,a st f * g1 = f * g2 holds

g1 = g2 ) ) );

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

for g1, g2 being Morphism of c,a st f * g1 = f * g2 holds

g1 = g2 ) ) );

:: deftheorem defines epimorphism CAT_7:def 6 :

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds

g1 = g2 ) ) );

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds

g1 = g2 ) ) );

theorem :: CAT_7:25

for C being composable with_identities CategoryStr

for a, b being Object of C

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

f1 is monomorphism

for a, b being Object of C

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

f1 is monomorphism

proof end;

theorem :: CAT_7:26

for C being category

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is monomorphism & f2 is monomorphism holds

f2 * f1 is monomorphism

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is monomorphism & f2 is monomorphism holds

f2 * f1 is monomorphism

proof end;

theorem :: CAT_7:27

for C being category

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f1 is monomorphism

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f2 * f1 is monomorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f1 is monomorphism

proof end;

definition

let C be composable with_identities CategoryStr ;

let a, b be Object of C;

let f be Morphism of a,b;

end;
let a, b be Object of C;

let f be Morphism of a,b;

:: deftheorem defines section_ CAT_7:def 7 :

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

:: deftheorem defines retraction CAT_7:def 8 :

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

theorem Th28: :: CAT_7:28

for C being non empty category

for a, b being Object of C

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

f is monomorphism

for a, b being Object of C

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

f is monomorphism

proof end;

theorem :: CAT_7:29

for C being composable with_identities CategoryStr

for a, b being Object of C

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

f1 is epimorphism

for a, b being Object of C

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

f1 is epimorphism

proof end;

theorem :: CAT_7:30

for C being category

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

proof end;

theorem :: CAT_7:31

for C being category

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f2 * f1 is epimorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f2 is epimorphism

for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f2 * f1 is epimorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds

f2 is epimorphism

proof end;

theorem Th32: :: CAT_7:32

for C being non empty category

for a, b being Object of C

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

f is epimorphism

for a, b being Object of C

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

f is epimorphism

proof end;

definition
end;

:: deftheorem defines isomorphism CAT_7:def 9 :

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

( g * f = id- a & f * g = id- b ) ) );

for C being composable with_identities CategoryStr

for a, b being Object of C

for f being Morphism of a,b holds

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

( g * f = id- a & f * g = id- b ) ) );

:: deftheorem defines are_isomorphic CAT_7:def 10 :

for C being composable with_identities CategoryStr

for a, b being Object of C holds

( a,b are_isomorphic iff ex f being Morphism of a,b st f is isomorphism );

for C being composable with_identities CategoryStr

for a, b being Object of C holds

( a,b are_isomorphic iff ex f being Morphism of a,b st f is isomorphism );

definition

let C be composable with_identities CategoryStr ;

let a, b be Object of C;

compatibility

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

( g * f = id- a & f * g = id- b ) ) );

end;
let a, b be Object of C;

redefine pred a,b are_isomorphic means :: CAT_7:def 11

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

( g * f = id- a & f * g = id- b ) );

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

( g * f = id- a & f * g = id- b ) );

compatibility

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

( g * f = id- a & f * g = id- b ) ) );

proof end;

:: deftheorem defines are_isomorphic CAT_7:def 11 :

for C being composable with_identities CategoryStr

for a, b being Object of C holds

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

( g * f = id- a & f * g = id- b ) ) );

for C being composable with_identities CategoryStr

for a, b being Object of C holds

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

( g * f = id- a & f * g = id- b ) ) );

theorem :: CAT_7:33

for C being non empty category

for a, b being Object of C

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

( f is monomorphism & f is epimorphism )

for a, b being Object of C

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

( f is monomorphism & f is epimorphism )

proof end;

:: deftheorem Def12 defines preorder CAT_7:def 12 :

for C being CategoryStr holds

( C is preorder iff for a, b being Object of C

for f1, f2 being morphism of C st f1 in Hom (a,b) & f2 in Hom (a,b) holds

f1 = f2 );

for C being CategoryStr holds

( C is preorder iff for a, b being Object of C

for f1, f2 being morphism of C st f1 in Hom (a,b) & f2 in Hom (a,b) holds

f1 = f2 );

registration
end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( b_{1} is strict & b_{1} is preorder );

end;
existence

ex b

( b

proof end;

registration

coherence

for b_{1} being composable with_identities CategoryStr st b_{1} is preorder holds

b_{1} is associative ;

end;

cluster composable with_identities preorder -> associative composable with_identities for CategoryStr ;

correctness coherence

for b

b

proof end;

definition

let C be with_identities CategoryStr ;

{ [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } is Relation of (Ob C)

end;
func RelOb C -> Relation of (Ob C) equals :: CAT_7:def 13

{ [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } ;

coherence { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } ;

{ [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } is Relation of (Ob C)

proof end;

:: deftheorem defines RelOb CAT_7:def 13 :

for C being with_identities CategoryStr holds RelOb C = { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } ;

for C being with_identities CategoryStr holds RelOb C = { [a,b] where a, b is Object of C : ex f being morphism of C st f in Hom (a,b) } ;

registration
end;

theorem Th34: :: CAT_7:34

for C being composable with_identities CategoryStr holds

( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C )

( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C )

proof end;

theorem Th35: :: CAT_7:35

for C1, C2 being composable with_identities CategoryStr st C1 ~= C2 holds

RelOb C1, RelOb C2 are_isomorphic

RelOb C1, RelOb C2 are_isomorphic

proof end;

registration

let C be non empty composable with_identities CategoryStr ;

correctness

coherence

not RelOb C is empty ;

end;
correctness

coherence

not RelOb C is empty ;

proof end;

theorem Th36: :: CAT_7:36

for C being composable with_identities preorder CategoryStr st not C is empty holds

ex F being Function of C,(RelOb C) st

( F is bijective & ( for f being morphism of C holds F . f = [(dom f),(cod f)] ) )

ex F being Function of C,(RelOb C) st

( F is bijective & ( for f being morphism of C holds F . f = [(dom f),(cod f)] ) )

proof end;

theorem Th37: :: CAT_7:37

for O being ordinal number ex C being strict preorder category st

( Ob C = O & ( for o1, o2 being Object of C st o1 in o2 holds

Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )

( Ob C = O & ( for o1, o2 being Object of C st o1 in o2 holds

Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )

proof end;

:: deftheorem Def14 defines -ordered CAT_7:def 14 :

for O being ordinal number

for C being composable with_identities CategoryStr holds

( C is O -ordered iff RelOb C, RelIncl O are_isomorphic );

for O being ordinal number

for C being composable with_identities CategoryStr holds

( C is O -ordered iff RelOb C, RelIncl O are_isomorphic );

registration

let O be non empty ordinal number ;

coherence

for b_{1} being composable with_identities CategoryStr st b_{1} is O -ordered holds

not b_{1} is empty ;

end;
cluster composable with_identities O -ordered -> non empty composable with_identities for CategoryStr ;

correctness coherence

for b

not b

proof end;

registration

let O be ordinal number ;

correctness

existence

ex b_{1} being composable with_identities CategoryStr st

( b_{1} is strict & b_{1} is O -ordered & b_{1} is preorder );

end;
correctness

existence

ex b

( b

proof end;

registration

let O be empty ordinal number ;

correctness

coherence

for b_{1} being composable with_identities CategoryStr st b_{1} is O -ordered holds

b_{1} is empty ;

end;
correctness

coherence

for b

b

proof end;

theorem Th38: :: CAT_7:38

for O1, O2 being ordinal number

for C1 being preorder b_{1} -ordered category

for C2 being preorder b_{2} -ordered category holds

( O1 = O2 iff C1 ~= C2 )

for C1 being preorder b

for C2 being preorder b

( O1 = O2 iff C1 ~= C2 )

proof end;

definition

let O be ordinal number ;

coherence

the strict preorder O -ordered category is strict preorder O -ordered category;

;

end;
func OrdC O -> strict preorder O -ordered category equals :: CAT_7:def 15

the strict preorder O -ordered category;

correctness the strict preorder O -ordered category;

coherence

the strict preorder O -ordered category is strict preorder O -ordered category;

;

:: deftheorem defines OrdC CAT_7:def 15 :

for O being ordinal number holds OrdC O = the strict preorder b_{1} -ordered category;

for O being ordinal number holds OrdC O = the strict preorder b

theorem Th39: :: CAT_7:39

ex f being morphism of (OrdC 2) st

( not f is identity & Ob (OrdC 2) = {(dom f),(cod f)} & Mor (OrdC 2) = {(dom f),(cod f),f} & dom f, cod f,f are_mutually_distinct )

( not f is identity & Ob (OrdC 2) = {(dom f),(cod f)} & Mor (OrdC 2) = {(dom f),(cod f),f} & dom f, cod f,f are_mutually_distinct )

proof end;

definition

let C be non empty category;

let f be morphism of C;

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

for g being morphism of (OrdC 2) st not g is identity holds

b_{1} . g = f

for b_{1}, b_{2} being covariant Functor of (OrdC 2),C st ( for g being morphism of (OrdC 2) st not g is identity holds

b_{1} . g = f ) & ( for g being morphism of (OrdC 2) st not g is identity holds

b_{2} . g = f ) holds

b_{1} = b_{2}

end;
let f be morphism of C;

func MORPHISM f -> covariant Functor of (OrdC 2),C means :Def16: :: CAT_7:def 16

for g being morphism of (OrdC 2) st not g is identity holds

it . g = f;

existence for g being morphism of (OrdC 2) st not g is identity holds

it . g = f;

ex b

for g being morphism of (OrdC 2) st not g is identity holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def16 defines MORPHISM CAT_7:def 16 :

for C being non empty category

for f being morphism of C

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

( b_{3} = MORPHISM f iff for g being morphism of (OrdC 2) st not g is identity holds

b_{3} . g = f );

for C being non empty category

for f being morphism of C

for b

( b

b

theorem Th40: :: CAT_7:40

for C being non empty category

for f being morphism of C st f is identity holds

for g being morphism of (OrdC 2) holds (MORPHISM f) . g = f

for f being morphism of C st f is identity holds

for g being morphism of (OrdC 2) holds (MORPHISM f) . g = f

proof end;

definition

let C be category;

let c, c1, c2, d be Object of C;

let f1 be Morphism of c1,c;

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

let f2 be Morphism of c2,c;

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

let p1 be Morphism of d,c1;

assume Hom (d,c1) <> {} ;

let p2 be Morphism of d,c2;

assume Hom (d,c2) <> {} ;

end;
let c, c1, c2, d be Object of C;

let f1 be Morphism of c1,c;

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

let f2 be Morphism of c2,c;

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

let p1 be Morphism of d,c1;

assume Hom (d,c1) <> {} ;

let p2 be Morphism of d,c2;

assume Hom (d,c2) <> {} ;

pred d,p1,p2 is_pullback_of f1,f2 means :Def17: :: CAT_7:def 17

( f1 * p1 = f2 * p2 & ( for d1 being Object of C

for g1 being Morphism of d1,c1

for g2 being Morphism of d1,c2 st Hom (d1,c1) <> {} & Hom (d1,c2) <> {} & f1 * g1 = f2 * g2 holds

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

( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) ) ) );

( f1 * p1 = f2 * p2 & ( for d1 being Object of C

for g1 being Morphism of d1,c1

for g2 being Morphism of d1,c2 st Hom (d1,c1) <> {} & Hom (d1,c2) <> {} & f1 * g1 = f2 * g2 holds

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

( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) ) ) );

:: deftheorem Def17 defines is_pullback_of CAT_7:def 17 :

for C being category

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c st Hom (c1,c) <> {} holds

for f2 being Morphism of c2,c st Hom (c2,c) <> {} holds

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

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

( d,p1,p2 is_pullback_of f1,f2 iff ( f1 * p1 = f2 * p2 & ( for d1 being Object of C

for g1 being Morphism of d1,c1

for g2 being Morphism of d1,c2 st Hom (d1,c1) <> {} & Hom (d1,c2) <> {} & f1 * g1 = f2 * g2 holds

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

( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) ) ) ) );

for C being category

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c st Hom (c1,c) <> {} holds

for f2 being Morphism of c2,c st Hom (c2,c) <> {} holds

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

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

( d,p1,p2 is_pullback_of f1,f2 iff ( f1 * p1 = f2 * p2 & ( for d1 being Object of C

for g1 being Morphism of d1,c1

for g2 being Morphism of d1,c2 st Hom (d1,c1) <> {} & Hom (d1,c2) <> {} & f1 * g1 = f2 * g2 holds

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

( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds

h = h1 ) ) ) ) ) );

theorem :: CAT_7:41

for C being non empty category

for c, c1, c2, d, e being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

for c, c1, c2, d, e being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

proof end;

theorem :: CAT_7:42

for C being category

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

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

d,p2,p1 is_pullback_of f2,f1

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

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

d,p2,p1 is_pullback_of f2,f1

proof end;

theorem :: CAT_7:43

for C being category

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & f1 is monomorphism holds

p2 is monomorphism

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & f1 is monomorphism holds

p2 is monomorphism

proof end;

theorem :: CAT_7:44

for C being non empty category

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & f1 is isomorphism holds

p2 is isomorphism

for c, c1, c2, d being Object of C

for f1 being Morphism of c1,c

for f2 being Morphism of c2,c

for p1 being Morphism of d,c1

for p2 being Morphism of d,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & f1 is isomorphism holds

p2 is isomorphism

proof end;

:: Pullback Lemma

theorem :: CAT_7:45

for C being category

for c1, c2, c3, c4, c5, c6 being Object of C

for f1 being Morphism of c1,c2

for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

for c1, c2, c3, c4, c5, c6 being Object of C

for f1 being Morphism of c1,c2

for f2 being Morphism of c2,c3

for f3 being Morphism of c1,c4

for f4 being Morphism of c2,c5

for f5 being Morphism of c3,c6

for f6 being Morphism of c4,c5

for f7 being Morphism of c5,c6 st Hom (c1,c2) <> {} & Hom (c2,c3) <> {} & Hom (c1,c4) <> {} & Hom (c2,c5) <> {} & Hom (c3,c6) <> {} & Hom (c4,c5) <> {} & Hom (c5,c6) <> {} & c2,f2,f4 is_pullback_of f5,f7 holds

( c1,f1,f3 is_pullback_of f4,f6 iff ( c1,f2 * f1,f3 is_pullback_of f5,f7 * f6 & f4 * f1 = f6 * f3 ) )

proof end;

definition

let C, D be category;

let F be Functor of C,D;

end;
let F be Functor of C,D;

:: deftheorem defines monomorphism CAT_7:def 18 :

for C, D being category

for F being Functor of C,D holds

( F is monomorphism iff ( F is covariant & ( for B being category

for G1, G2 being Functor of B,C st G1 is covariant & G2 is covariant & F (*) G1 = F (*) G2 holds

G1 = G2 ) ) );

for C, D being category

for F being Functor of C,D holds

( F is monomorphism iff ( F is covariant & ( for B being category

for G1, G2 being Functor of B,C st G1 is covariant & G2 is covariant & F (*) G1 = F (*) G2 holds

G1 = G2 ) ) );

:: deftheorem defines isomorphism CAT_7:def 19 :

for C, D being category

for F being Functor of C,D holds

( F is isomorphism iff ( F is covariant & ex G being Functor of D,C st

( G is covariant & G (*) F = id C & F (*) G = id D ) ) );

for C, D being category

for F being Functor of C,D holds

( F is isomorphism iff ( F is covariant & ex G being Functor of D,C st

( G is covariant & G (*) F = id C & F (*) G = id D ) ) );

definition

let C, C1, C2, D be category;

let F1 be Functor of C1,C;

assume F1 is covariant ;

let F2 be Functor of C2,C;

assume F2 is covariant ;

let P1 be Functor of D,C1;

assume P1 is covariant ;

let P2 be Functor of D,C2;

assume P2 is covariant ;

end;
let F1 be Functor of C1,C;

assume F1 is covariant ;

let F2 be Functor of C2,C;

assume F2 is covariant ;

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_pullback_of F1,F2 means :Def20: :: CAT_7:def 20

( F1 (*) P1 = F2 (*) P2 & ( 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 & F1 (*) G1 = F2 (*) G2 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 ) ) ) );

( F1 (*) P1 = F2 (*) P2 & ( 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 & F1 (*) G1 = F2 (*) G2 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 Def20 defines is_pullback_of CAT_7:def 20 :

for C, C1, C2, D being category

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

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

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_pullback_of F1,F2 iff ( F1 (*) P1 = F2 (*) P2 & ( 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 & F1 (*) G1 = F2 (*) G2 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 C, C1, C2, D being category

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

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

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_pullback_of F1,F2 iff ( F1 (*) P1 = F2 (*) P2 & ( 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 & F1 (*) G1 = F2 (*) G2 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 Th46: :: CAT_7:46

for C, C1, C2, D, E being category

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2

for Q1 being Functor of E,C1

for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds

D ~= E

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2

for Q1 being Functor of E,C1

for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds

D ~= E

proof end;

theorem Th47: :: CAT_7:47

for C, C1, C2, D being category

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 holds

D,P2,P1 is_pullback_of F2,F1

proof end;

theorem :: CAT_7:48

for C, C1, C2, D being category

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is monomorphism holds

P2 is monomorphism

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is monomorphism holds

P2 is monomorphism

proof end;

theorem :: CAT_7:49

for C, C1, C2, D being category

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

proof end;

theorem :: CAT_7:50

for C1, C2, C3, C4, C5, C6 being category

for F1 being Functor of C1,C2

for F2 being Functor of C2,C3

for F3 being Functor of C1,C4

for F4 being Functor of C2,C5

for F5 being Functor of C3,C6

for F6 being Functor of C4,C5

for F7 being Functor of C5,C6 st F1 is covariant & F2 is covariant & F3 is covariant & F4 is covariant & F5 is covariant & F6 is covariant & F7 is covariant & C2,F2,F4 is_pullback_of F5,F7 holds

( C1,F1,F3 is_pullback_of F4,F6 iff ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 ) )

for F1 being Functor of C1,C2

for F2 being Functor of C2,C3

for F3 being Functor of C1,C4

for F4 being Functor of C2,C5

for F5 being Functor of C3,C6

for F6 being Functor of C4,C5

for F7 being Functor of C5,C6 st F1 is covariant & F2 is covariant & F3 is covariant & F4 is covariant & F5 is covariant & F6 is covariant & F7 is covariant & C2,F2,F4 is_pullback_of F5,F7 holds

( C1,F1,F3 is_pullback_of F4,F6 iff ( C1,F2 (*) F1,F3 is_pullback_of F5,F7 (*) F6 & F4 (*) F1 = F6 (*) F3 ) )

proof end;

theorem Th51: :: CAT_7:51

for C, C1, C2 being category

for F1 being Functor of C1,C

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

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

( the carrier of D = { [f1,f2] where f1 is morphism of C1, f2 is morphism of C2 : ( f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) } & the composition of D = { [[f1,f2],f3] where f1, f2, f3 is morphism of D : ( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1

for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds

( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 )

for F1 being Functor of C1,C

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

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

( the carrier of D = { [f1,f2] where f1 is morphism of C1, f2 is morphism of C2 : ( f1 in the carrier of C1 & f2 in the carrier of C2 & F1 . f1 = F2 . f2 ) } & the composition of D = { [[f1,f2],f3] where f1, f2, f3 is morphism of D : ( f1 in the carrier of D & f2 in the carrier of D & f3 in the carrier of D & ( for f11, f12, f13 being morphism of C1

for f21, f22, f23 being morphism of C2 st f1 = [f11,f21] & f2 = [f12,f22] & f3 = [f13,f23] holds

( f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 & f23 = f21 (*) f22 ) ) ) } & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 )

proof end;

definition

let C, C1, C2 be category;

let F1 be Functor of C1,C;

assume A1: F1 is covariant ;

let F2 be Functor of C2,C;

assume A2: F2 is covariant ;

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_pullback_of F1,F2 );

end;
let F1 be Functor of C1,C;

assume A1: F1 is covariant ;

let F2 be Functor of C2,C;

assume A2: F2 is covariant ;

mode pullback of F1,F2 -> triple object means :Def21: :: CAT_7:def 21

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_pullback_of F1,F2 );

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_pullback_of F1,F2 );

existence

ex b

( b

proof end;

:: deftheorem Def21 defines pullback CAT_7:def 21 :

for C, C1, C2 being category

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

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

for b_{6} being triple object holds

( b_{6} is pullback of F1,F2 iff ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st

( b_{6} = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 ) );

for C, C1, C2 being category

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

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

for b

( b

( b

definition

let C, C1, C2 be category;

let F1 be Functor of C1,C;

assume A1: F1 is covariant ;

let F2 be Functor of C2,C;

assume A2: F2 is covariant ;

correctness

coherence

the pullback of F1,F2 `1_3 is strict category;

end;
let F1 be Functor of C1,C;

assume A1: F1 is covariant ;

let F2 be Functor of C2,C;

assume A2: F2 is covariant ;

correctness

coherence

the pullback of F1,F2 `1_3 is strict category;

proof end;

:: deftheorem Def22 defines [| CAT_7:def 22 :

for C, C1, C2 being category

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

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

[|F1,F2|] = the pullback of F1,F2 `1_3 ;

for C, C1, C2 being category

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

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

[|F1,F2|] = the pullback of F1,F2 `1_3 ;

definition

let C, C1, C2 be category;

let F1 be Functor of C1,C;

assume A1: F1 is covariant ;

let F2 be Functor of C2,C;

assume A2: F2 is covariant ;

coherence

the pullback of F1,F2 `2_3 is Functor of [|F1,F2|],C1;

coherence

the pullback of F1,F2 `3_3 is Functor of [|F1,F2|],C2;

end;
let F1 be Functor of C1,C;

assume A1: F1 is covariant ;

let F2 be Functor of C2,C;

assume A2: F2 is covariant ;

func pr1 (F1,F2) -> Functor of [|F1,F2|],C1 equals :Def23: :: CAT_7:def 23

the pullback of F1,F2 `2_3 ;

correctness the pullback of F1,F2 `2_3 ;

coherence

the pullback of F1,F2 `2_3 is Functor of [|F1,F2|],C1;

proof end;

func pr2 (F1,F2) -> Functor of [|F1,F2|],C2 equals :Def24: :: CAT_7:def 24

the pullback of F1,F2 `3_3 ;

correctness the pullback of F1,F2 `3_3 ;

coherence

the pullback of F1,F2 `3_3 is Functor of [|F1,F2|],C2;

proof end;

:: deftheorem Def23 defines pr1 CAT_7:def 23 :

for C, C1, C2 being category

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

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

pr1 (F1,F2) = the pullback of F1,F2 `2_3 ;

for C, C1, C2 being category

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

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

pr1 (F1,F2) = the pullback of F1,F2 `2_3 ;

:: deftheorem Def24 defines pr2 CAT_7:def 24 :

for C, C1, C2 being category

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

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

pr2 (F1,F2) = the pullback of F1,F2 `3_3 ;

for C, C1, C2 being category

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

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

pr2 (F1,F2) = the pullback of F1,F2 `3_3 ;

theorem Th52: :: CAT_7:52

for C, C1, C2 being category

for F1 being Functor of C1,C

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

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

for F1 being Functor of C1,C

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

( pr1 (F1,F2) is covariant & pr2 (F1,F2) is covariant & [|F1,F2|], pr1 (F1,F2), pr2 (F1,F2) is_pullback_of F1,F2 )

proof end;

theorem :: CAT_7:53

for C, C1, C2 being category

for F1 being Functor of C1,C

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

[|F1,F2|] ~= [|F2,F1|]

for F1 being Functor of C1,C

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

[|F1,F2|] ~= [|F2,F1|]

proof end;

theorem :: CAT_7:54

ex C, C1, C2 being Category ex F1 being Functor of C1,C ex F2 being Functor of C2,C st

for D being Category

for P1 being Functor of D,C1

for P2 being Functor of D,C2 holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1 being Functor of D1,C1 ex G2 being Functor of D1,C2 st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

for D being Category

for P1 being Functor of D,C1

for P2 being Functor of D,C2 holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1 being Functor of D1,C1 ex G2 being Functor of D1,C2 st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

proof end;