:: Categorical Pullbacks
:: by Marco Riccardi
::
:: Received December 31, 2014
:: Copyright (c) 2014-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, SUBSET_1, WELLORD1,
CAT_1, ALTCAT_1, GRAPH_1, BINOP_1, STRUCT_0, PARTFUN1, MONOID_0,
NATTRA_1, MSSUBFAM, NUMBERS, ORDINAL1, CARD_1, FUNCTOR0, MOD_4, CAT_6,
XTUPLE_0, RECDEF_2, MCART_1, CAT_3, PBOOLE, WELLORD2, FACIRC_1, FUNCT_2,
ALTCAT_2, CAT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_3, FUNCT_4, RELAT_1,
FUNCT_1, FUNCT_2, ORDINAL1, PARTFUN1, FINSEQ_1, STRUCT_0, FUNCOP_1,
RELSET_1, BINOP_1, GRAPH_1, CAT_1, CAT_2, NUMBERS, NAT_1, XXREAL_0,
XTUPLE_0, ALG_1, XCMPLX_0, WELLORD2, CARD_1, CAT_6, ENUMSET1, WELLORD1;
constructors NUMBERS, FUNCT_2, CLASSES2, FINSEQ_1, FUNCOP_1, RELAT_2,
PARTFUN1, RELSET_1, BINOP_1, FUNCT_4, CAT_1, CAT_2, NAT_1, XXREAL_0,
WELLORD2, XREAL_0, CARD_1, XCMPLX_0, INT_1, VALUED_0, ISOCAT_1, STRUCT_0,
CAT_6, REALSET1, WELLORD1, ORDERS_2;
registrations XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1,
XTUPLE_0, CARD_1, CLASSES2, STRUCT_0, RELSET_1, FUNCT_2, PARTFUN1,
GRFUNC_1, BINOP_1, CAT_1, CARD_2, NAT_LAT, FINSET_1, XXREAL_0, XREAL_0,
NAT_1, NUMBERS, VALUED_0, FINSEQ_1, WELLORD2, CAT_6, ORDERS_2, EQREL_1;
requirements SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
begin :: Preliminaries
registration
cluster ordinal -> non pair for set;
end;
registration
let C be empty CategoryStr;
cluster Mor(C) -> empty;
end;
registration
let C be non empty CategoryStr;
cluster Mor(C) -> non empty;
end;
registration
let C be empty with_identities CategoryStr;
cluster Ob(C) -> empty;
end;
registration
let C be non empty with_identities CategoryStr;
cluster Ob(C) -> non empty;
end;
registration
let C be with_identities CategoryStr;
let a be Object of C;
cluster id- a -> identity;
end;
theorem :: CAT_7:1
for C being CategoryStr, f being morphism of C
st C is non empty holds f in the carrier of C;
theorem :: CAT_7:2
for C being with_identities CategoryStr, a being Object of C
st C is non empty holds a in the carrier of C;
theorem :: CAT_7:3
for C being composable CategoryStr, f1,f2,f3 being morphism of C st
f1 |> f2 & f2 |> f3 & f2 is identity holds f1 |> f3;
theorem :: CAT_7:4
for C being with_identities composable CategoryStr,
f1,f2 being morphism of C st f1 |> f2 holds
dom (f1 (*) f2) = dom f2 & cod (f1 (*) f2) = cod f1;
theorem :: CAT_7:5
for C being non empty composable with_identities CategoryStr,
f1,f2 being morphism of C holds f1 |> f2 iff dom f1 = cod f2;
theorem :: CAT_7:6
for C being with_identities composable CategoryStr,
f being morphism of C st f is identity holds dom f = f & cod f = f;
theorem :: CAT_7:7
for C being composable with_identities CategoryStr,
f1,f2 being morphism of C st f1 |> f2 & f1 is identity & f2 is identity
holds f1 = f2;
theorem :: CAT_7:8
for C being non empty composable with_identities CategoryStr,
f1,f2 being morphism of C st dom f1 = f2 holds f1 |> f2 & f1 (*) f2 = f1;
theorem :: CAT_7:9
for C being non empty composable with_identities CategoryStr,
f1,f2 being morphism of C st f1 = cod f2 holds f1 |> f2 & f1 (*) f2 = f2;
theorem :: CAT_7:10
for C1,C2,C3,C4 being category, F being Functor of C1,C2,
G being Functor of C2,C3, H being Functor of C3,C4 st
F is covariant & G is covariant & H is covariant
holds H (*) (G (*) F) = (H (*) G) (*) F;
theorem :: CAT_7:11
for C,D being category, F being Functor of C,D st
F is covariant holds F (*) id C = F & id D (*) F = F;
theorem :: 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;
theorem :: CAT_7:13
for C,D being empty with_identities CategoryStr holds C ~= D;
theorem :: 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;
theorem :: CAT_7:15
for C,D being with_identities CategoryStr st C ~= D & C is empty
holds D is empty;
begin :: Hom-sets
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};
end;
definition
let C be non empty composable with_identities CategoryStr;
let a,b be Object of C;
redefine func Hom(a,b) -> Subset of Mor(C) equals
:: CAT_7:def 2
{f where f is morphism of C : dom f = a & cod f = b};
end;
definition
let C be CategoryStr;
let a,b be Object of C;
assume
Hom(a,b) <> {};
mode Morphism of a,b -> morphism of C means
:: CAT_7:def 3
it in Hom(a,b);
end;
definition
let C be non empty with_identities CategoryStr;
let a be Object of C;
redefine func id- a -> Morphism of a, a;
end;
registration
let C be non empty with_identities CategoryStr;
let a be Object of C;
cluster Hom(a,a) -> non empty;
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
Hom(a,b) <> {} & Hom(b,c) <> {};
func g * f -> Morphism of a,c equals
:: CAT_7:def 4
g (*) f;
end;
theorem :: CAT_7:16
for C being CategoryStr, a,b being Object of C,
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;
theorem :: CAT_7:17
for C being composable with_identities CategoryStr,
a,b,c being Object of C,
f1 being Morphism of a,b, f2 being Morphism of b,c
st Hom(a,b) <> {} & Hom(b,c) <> {} holds f2 |> f1;
theorem :: CAT_7:18
for C being composable non empty with_identities CategoryStr,
a,b being Object of C, f being Morphism of a,b
st Hom(a,b) <> {} holds f * (id- a) = f & (id- b) * f = f;
theorem :: CAT_7:19
for C being non empty with_identities composable CategoryStr,
f being morphism of C holds f in Hom(dom f,cod f);
theorem :: CAT_7:20
for C being non empty with_identities composable CategoryStr,
a,b being Object of C, f being morphism of C holds
f in Hom(a,b) iff dom f = a & cod f = b;
theorem :: CAT_7:21
for C being non empty with_identities composable CategoryStr,
a being Object of C holds a in Hom(a,a);
theorem :: CAT_7:22
for C being composable with_identities CategoryStr,
a,b,c being Object of C
st Hom(a,b) <> {} & Hom(b,c) <> {} holds Hom(a,c) <> {};
theorem :: CAT_7:23
for C being category, a,b,c,d being Object of C,
f1 being Morphism of a,b, f2 being Morphism of b,c,
f3 being Morphism of c,d
st Hom(a,b) <> {} & Hom(b,c) <> {} & Hom(c,d) <> {}
holds f3 * (f2 * f1) = (f3 * f2) * f1;
theorem :: CAT_7:24
for C being composable with_identities CategoryStr,
a,b,c being Object of C, f1 being Morphism of a,b,
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);
begin :: Monomorphisms, Epimorphisms and Isomorphisms
definition
let C be composable with_identities CategoryStr,
a,b be Object of C, 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) <> {}
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) <> {}
for g1,g2 being Morphism of b,c st g1 * f = g2 * f holds g1 = g2;
end;
theorem :: CAT_7:25
for C being composable with_identities CategoryStr,
a,b being Object of C, f1 being Morphism of a,b
st Hom(a,b) <> {} & f1 is identity holds f1 is monomorphism;
theorem :: CAT_7:26
for C being category, a,b,c being Object of C,
f1 being Morphism of a,b, f2 being Morphism of b,c
st f1 is monomorphism & f2 is monomorphism
holds f2 * f1 is monomorphism;
theorem :: CAT_7:27
for C being category, a,b,c being Object of C,
f1 being Morphism of a,b, f2 being Morphism of b,c
st f2 * f1 is monomorphism & Hom(a,b) <> {} & Hom(b,c) <> {}
holds f1 is monomorphism;
definition
let C be composable with_identities CategoryStr,
a,b be Object of C, 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;
theorem :: CAT_7:28
for C being non empty category,
a,b being Object of C, f being Morphism of a,b
st f is section_ holds f is monomorphism;
theorem :: CAT_7:29
for C being composable with_identities CategoryStr,
a,b being Object of C, f1 being Morphism of a,b
st Hom(a,b) <> {} & f1 is identity holds f1 is epimorphism;
theorem :: CAT_7:30
for C being category, a,b,c being Object of C,
f1 being Morphism of a,b, f2 being Morphism of b,c
st f1 is epimorphism & f2 is epimorphism
holds f2 * f1 is epimorphism;
theorem :: CAT_7:31
for C being category, a,b,c being Object of C,
f1 being Morphism of a,b, f2 being Morphism of b,c
st f2 * f1 is epimorphism & Hom(a,b) <> {} & Hom(b,c) <> {}
holds f2 is epimorphism;
theorem :: CAT_7:32
for C being non empty category,
a,b being Object of C, f being Morphism of a,b
st f is retraction holds f is epimorphism;
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;
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;
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, g being Morphism of b,a st
g * f = id- a & f * g = id- b;
end;
theorem :: CAT_7:33
for C being non empty category,
a,b be Object of C, f being Morphism of a,b
st f is isomorphism holds f is monomorphism & f is epimorphism;
begin :: Ordinal Numbers as Categories
definition
let C be CategoryStr;
attr C is preorder means
:: CAT_7:def 12
for a,b being Object of C, f1,f2 being morphism of C holds
f1 in Hom(a,b) & f2 in Hom(a,b) implies f1 = f2;
end;
registration
cluster empty -> preorder for CategoryStr;
end;
registration
cluster strict preorder for CategoryStr;
end;
registration
cluster preorder -> associative
for composable with_identities CategoryStr;
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)};
end;
registration
let C be empty with_identities CategoryStr;
cluster RelOb(C) -> empty;
end;
theorem :: CAT_7:34
for C being composable with_identities CategoryStr holds
dom RelOb C = Ob C & rng RelOb C = Ob C;
theorem :: CAT_7:35
for C1,C2 being composable with_identities CategoryStr st C1 ~= C2
holds RelOb(C1), RelOb(C2) are_isomorphic;
registration
let C be non empty composable with_identities CategoryStr;
cluster RelOb C -> non empty;
end;
theorem :: CAT_7:36
for C being preorder composable with_identities CategoryStr st C is non 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]);
theorem :: 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};
definition
let O be ordinal number;
let C be composable with_identities CategoryStr;
attr C is O -ordered means
:: CAT_7:def 14
RelOb(C), RelIncl(O) are_isomorphic;
end;
registration
let O be non empty ordinal number;
cluster O -ordered -> non empty for composable with_identities CategoryStr;
end;
registration
let O be ordinal number;
cluster strict O -ordered preorder
for composable with_identities CategoryStr;
end;
registration
let O be empty ordinal number;
cluster O -ordered -> empty for composable with_identities CategoryStr;
end;
theorem :: CAT_7:38
for O1,O2 being ordinal number, C1 being O1 -ordered preorder category,
C2 being O2 -ordered preorder category holds O1 = O2 iff C1 ~= C2;
definition
let O be ordinal number;
func OrdC(O) -> strict O -ordered preorder category equals
:: CAT_7:def 15
the strict O -ordered preorder category;
end;
theorem :: CAT_7:39
ex f being morphism of OrdC(2) st f is not identity &
Ob OrdC 2 = {dom f, cod f} & Mor OrdC 2 = {dom f, cod f, f} &
dom f, cod f, f are_mutually_distinct;
definition
let C be non empty category;
let f be morphism of C;
func MORPHISM(f) -> covariant Functor of OrdC 2, C means
:: CAT_7:def 16
for g being morphism of OrdC 2 st g is not identity holds it.g = f;
end;
theorem :: CAT_7:40
for C being non empty category, f being morphism of C st f is identity holds
for g being morphism of OrdC 2 holds (MORPHISM f).g = f;
begin :: Pullbacks
definition
let C be category;
let c,c1,c2,d be Object of C;
let f1 be Morphism of c1,c such that Hom(c1,c) <> {};
let f2 be Morphism of c2,c such that Hom(c2,c) <> {};
let p1 be Morphism of d,c1 such that Hom(d,c1) <> {};
let p2 be Morphism of d,c2 such that Hom(d,c2) <> {};
pred d,p1,p2 is_pullback_of f1,f2 means
:: CAT_7:def 17
f1 * p1 = f2 * p2 & for d1 being Object of C,
g1 being Morphism of d1,c1, 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;
theorem :: CAT_7:41
for C being non empty category, c,c1,c2,d,e being Object of C,
f1 being Morphism of c1,c, f2 being Morphism of c2,c,
p1 being Morphism of d,c1, p2 being Morphism of d,c2,
q1 being Morphism of e,c1, 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;
theorem :: CAT_7:42
for C being category, c,c1,c2,d being Object of C,
f1 being Morphism of c1,c, f2 being Morphism of c2,c,
p1 being Morphism of d,c1, 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;
theorem :: CAT_7:43
for C being category, c,c1,c2,d being Object of C,
f1 being Morphism of c1,c, f2 being Morphism of c2,c,
p1 being Morphism of d,c1, 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;
theorem :: CAT_7:44
for C being non empty category, c,c1,c2,d being Object of C,
f1 being Morphism of c1,c, f2 being Morphism of c2,c,
p1 being Morphism of d,c1, 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;
:: Pullback Lemma
theorem :: CAT_7:45
for C being category, c1,c2,c3,c4,c5,c6 being Object of C,
f1 being Morphism of c1,c2, f2 being Morphism of c2,c3,
f3 being Morphism of c1,c4, f4 being Morphism of c2,c5,
f5 being Morphism of c3,c6, f6 being Morphism of c4,c5,
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;
begin :: Pullbacks of Functors
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, 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;
definition
let C,C1,C2,D be category;
let F1 be Functor of C1,C such that F1 is covariant;
let F2 be Functor of C2,C such that F2 is covariant;
let P1 be Functor of D,C1 such that P1 is covariant;
let P2 be Functor of D,C2 such that P2 is covariant;
pred D,P1,P2 is_pullback_of F1,F2 means
:: CAT_7:def 20
F1 (*) P1 = F2 (*) P2 &
for D1 being category, G1 being Functor of D1,C1, 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;
theorem :: CAT_7:46
for C,C1,C2,D,E being category, F1 being Functor of C1,C,
F2 being Functor of C2,C,
P1 be Functor of D,C1, P2 be Functor of D,C2,
Q1 be Functor of E,C1, Q2 be 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;
theorem :: CAT_7:47
for C,C1,C2,D being category,
F1 being Functor of C1,C, F2 being Functor of C2,C,
P1 being Functor of D,C1, 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;
theorem :: CAT_7:48
for C,C1,C2,D being category,
F1 being Functor of C1,C, F2 being Functor of C2,C,
P1 being Functor of D,C1, 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;
theorem :: CAT_7:49
for C,C1,C2,D being category,
F1 being Functor of C1,C, F2 being Functor of C2,C,
P1 being Functor of D,C1, 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;
theorem :: CAT_7:50
for C1,C2,C3,C4,C5,C6 being category,
F1 being Functor of C1,C2, F2 being Functor of C2,C3,
F3 being Functor of C1,C4, F4 being Functor of C2,C5,
F5 being Functor of C3,C6, F6 being Functor of C4,C5,
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;
theorem :: CAT_7:51
for C,C1,C2 being category, F1 being Functor of C1,C,
F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds
ex D being strict category,
P1 being Functor of D,C1, 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,
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;
definition
let C,C1,C2 be category;
let F1 be Functor of C1,C such that
F1 is covariant;
let F2 be Functor of C2,C such that
F2 is covariant;
mode pullback of F1,F2 -> triple object means
:: CAT_7:def 21
ex D being strict category, P1 being Functor of D,C1,
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;
end;
definition
let C,C1,C2 be category;
let F1 be Functor of C1,C such that
F1 is covariant;
let F2 be Functor of C2,C such that
F2 is covariant;
func [| F1, F2 |] -> strict category equals
:: CAT_7:def 22
(the pullback of F1,F2)`1_3;
end;
definition
let C,C1,C2 be category;
let F1 be Functor of C1,C such that
F1 is covariant;
let F2 be Functor of C2,C such that
F2 is covariant;
func pr1(F1,F2) -> Functor of [|F1,F2|], C1 equals
:: CAT_7:def 23
(the pullback of F1,F2)`2_3;
func pr2(F1,F2) -> Functor of [|F1,F2|], C2 equals
:: CAT_7:def 24
(the pullback of F1,F2)`3_3;
end;
theorem :: CAT_7:52
for C,C1,C2 being category, F1 being Functor of C1,C,
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;
theorem :: CAT_7:53
for C,C1,C2 being category, F1 being Functor of C1,C,
F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds
[|F1,F2|] ~= [|F2,F1|];
theorem :: CAT_7:54
ex C,C1,C2 being Category,
F1 being Functor of C1,C, F2 being Functor of C2,C st
not ex D being Category, P1 being Functor of D,C1,
P2 being Functor of D,C2 st F1 * P1 = F2 * P2 &
for D1 being Category, G1 being Functor of D1,C1,
G2 being Functor of D1,C2 st F1 * G1 = F2 * G2 holds
ex H being Functor of D1,D st P1 * H = G1 & P2 * H = G2
& for H1 being Functor of D1,D st P1 * H1 = G1 & P2 * H1 = G2
holds H = H1;