:: Categorical Pullbacks
:: by Marco Riccardi
::
:: Received December 31, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

registration

cluster ordinal -> non pair for set ;

correctness
coherence
for b₁ being set st b₁ is ordinal holds
not b₁ is pair ;

proof end;

end;

registration

let C be empty CategoryStr ;

cluster Mor C -> empty ;

correctness
coherence
Mor C is empty ;

proof end;

end;

registration

let C be non empty CategoryStr ;

cluster Mor C -> non empty ;

correctness
coherence
not Mor C is empty ;

proof end;

end;

registration

let C be empty with_identities CategoryStr ;

cluster Ob C -> empty ;

correctness
coherence
Ob C is empty ;
;

end;

registration

let C be non empty with_identities CategoryStr ;

cluster Ob C -> non empty ;

correctness
coherence
not Ob C is empty ;
;

end;

registration

let C be with_identities CategoryStr ;
let a be Object of C;

cluster id- a -> identity ;

correctness
coherence
id- a is identity ;

proof end;

end;

theorem Th1: :: CAT_7:1

for C being CategoryStr
for f being morphism of C st not C is empty holds
f in the carrier of C

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

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

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 )

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 )

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 )

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

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 )

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 )

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

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 )

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

proof end;

theorem Th13: :: CAT_7:13

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

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

proof end;

theorem Th15: :: CAT_7:15

for C, D being with_identities CategoryStr st C ~= D & C is empty holds
D is empty

proof end;

definition

let C be CategoryStr ;
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
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;

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

definition

let C be non empty composable with_identities CategoryStr ;
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
coherence
Hom (a,b) is Subset of (Mor C);
compatibility
for b₁ being Subset of (Mor C) holds
( b₁ = Hom (a,b) iff b₁ = { f where f is morphism of C : ( dom f = a & cod f = b ) } );

proof end;

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

definition

let C be CategoryStr ;
let a, b be Object of C;
assume A1: Hom (a,b) <> {} ;

mode Morphism of a,b -> morphism of C means :Def3: :: CAT_7:def 3
it in Hom (a,b);

correctness
existence
ex b₁ being morphism of C st b₁ in Hom (a,b);
by A1, SUBSET_1:4;

end;

:: 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₄ being morphism of C holds
( b₄ is Morphism of a,b iff b₄ in Hom (a,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

proof end;

end;

registration

let C be non empty with_identities CategoryStr ;
let a be Object of C;

cluster Hom (a,a) -> non empty ;

correctness
coherence
not Hom (a,a) is empty ;

proof end;

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) <> {} ) ;

func g * f -> Morphism of a,c equals :Def4: :: CAT_7:def 4
g (*) f;

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

proof end;

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;

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 )

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

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 )

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

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

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)

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

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

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

proof end;

definition

let C be composable with_identities CategoryStr ;
let a, b be Object of C;
let f be Morphism of a,b;

attr f is monomorphism means :: CAT_7:def 5
( 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 ) );

attr f is epimorphism means :: CAT_7:def 6
( 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 ) );

end;

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

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

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

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

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

proof end;

definition

let C be composable with_identities CategoryStr ;
let a, b be Object of C;
let f be Morphism of a,b;

attr f is section_ means :: CAT_7:def 7
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st g * f = id- a );

attr f is retraction means :: CAT_7:def 8
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st f * g = id- b );

end;

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

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

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

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

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

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

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

proof end;

definition

let C be composable with_identities CategoryStr ;
let a, b be Object of C;
let f be Morphism of a,b;

attr f is isomorphism means :: CAT_7:def 9
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st
( g * f = id- a & f * g = id- b ) );

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

definition

let C be composable with_identities CategoryStr ;
let a, b be Object of C;

pred a,b are_isomorphic means :: CAT_7:def 10
ex f being Morphism of a,b st f is isomorphism ;

end;

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

definition

let C be composable with_identities CategoryStr ;
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
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;

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

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 )

proof end;

definition

let C be CategoryStr ;

attr C is preorder means :Def12: :: CAT_7:def 12
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;

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

registration

cluster empty -> preorder for CategoryStr ;

correctness
coherence
for b₁ being CategoryStr st b₁ is empty holds
b₁ is preorder ;
;

end;

registration

cluster strict preorder for CategoryStr ;

correctness
existence
ex b₁ being CategoryStr st
( b₁ is strict & b₁ is preorder );

proof end;

end;

registration

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

correctness
coherence
for b₁ being composable with_identities CategoryStr st b₁ is preorder holds
b₁ is associative ;

proof end;

end;

definition

let C be with_identities CategoryStr ;

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) } is Relation of (Ob C)

proof end;

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

registration

let C be empty with_identities CategoryStr ;

cluster RelOb C -> empty ;

correctness
coherence
RelOb C is empty ;
;

end;

theorem Th34: :: CAT_7:34

for C being composable with_identities CategoryStr holds
( 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

proof end;

registration

let C be non empty composable with_identities CategoryStr ;

cluster RelOb C -> non empty ;

correctness
coherence
not RelOb C is empty ;

proof end;

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

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

proof end;

definition

let O be ordinal number ;
let C be composable with_identities CategoryStr ;

attr C is O -ordered means :Def14: :: CAT_7:def 14
RelOb C, RelIncl O are_isomorphic ;

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

registration

let O be non empty ordinal number ;

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

correctness
coherence
for b₁ being composable with_identities CategoryStr st b₁ is O -ordered holds
not b₁ is empty ;

proof end;

end;

registration

let O be ordinal number ;

cluster strict composable with_identities preorder O -ordered for CategoryStr ;

correctness
existence
ex b₁ being composable with_identities CategoryStr st
( b₁ is strict & b₁ is O -ordered & b₁ is preorder );

proof end;

end;

registration

let O be empty ordinal number ;

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

correctness
coherence
for b₁ being composable with_identities CategoryStr st b₁ is O -ordered holds
b₁ is empty ;

proof end;

end;

theorem Th38: :: CAT_7:38

for O1, O2 being ordinal number
for C1 being preorder b₁ -ordered category
for C2 being preorder b₂ -ordered category holds
( O1 = O2 iff C1 ~= C2 )

proof end;

definition

let O be ordinal number ;

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

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

end;

:: deftheorem defines OrdC CAT_7:def 15 :
for O being ordinal number holds OrdC O = the strict preorder b₁ -ordered category;

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 )

proof end;

definition

let C be non empty category;
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
ex b₁ being covariant Functor of (OrdC 2),C st
for g being morphism of (OrdC 2) st not g is identity holds
b₁ . g = f

proof end;

uniqueness
for b₁, b₂ being covariant Functor of (OrdC 2),C st ( for g being morphism of (OrdC 2) st not g is identity holds
b₁ . g = f ) & ( for g being morphism of (OrdC 2) st not g is identity holds
b₂ . g = f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines MORPHISM CAT_7:def 16 :
for C being non empty category
for f being morphism of C
for b₃ being covariant Functor of (OrdC 2),C holds
( b₃ = MORPHISM f iff for g being morphism of (OrdC 2) st not g is identity holds
b₃ . g = f );

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

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) <> {} ;

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

end;

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

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

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

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

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

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

proof end;

definition

let C, D be category;
let F be Functor of C,D;

attr F is monomorphism means :: CAT_7:def 18
( 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 ) );

attr F is isomorphism means :: CAT_7:def 19
( F is covariant & ex G being Functor of D,C st
( G is covariant & G (*) F = id C & F (*) G = id D ) );

end;

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

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

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 ;

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

end;

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

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

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

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

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

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

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 )

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 ;

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
existence
ex b₁ being triple object ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( b₁ = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 );

proof end;

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₆ being triple object holds
( b₆ 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₆ = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 ) );

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 ;

func [|F1,F2|] -> strict category equals :Def22: :: CAT_7:def 22
the pullback of F1,F2 `1_3 ;

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

proof end;

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 ;

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 ;

func pr1 (F1,F2) -> Functor of [|F1,F2|],C1 equals :Def23: :: CAT_7:def 23
the pullback of F1,F2 `2_3 ;

correctness
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
coherence
the pullback of F1,F2 `3_3 is Functor of [|F1,F2|],C2;

proof end;

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 ;

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

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 )

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

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

proof end;