:: Categorical Pullbacks
:: by Marco Riccardi
::
:: Received December 31, 2014
:: Copyright (c) 2014-2026 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, RELAT_1, FUNCT_1, ORDINAL1, XTUPLE_0,
CARD_1, STRUCT_0, RELSET_1, FUNCT_2, CARD_2, FINSET_1, NAT_1, WELLORD2,
CAT_6;
requirements SUBSET, BOOLE, NUMERALS;
theorems TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, RELAT_1, FUNCT_1, STRUCT_0,
FUNCT_2, SUBSET_1, BINOP_1, ORDINAL1, CAT_6, XBOOLE_1, WELLORD1,
WELLORD2, ENUMSET1, CARD_1, CARD_2;
schemes FUNCT_2;
begin :: Preliminaries
registration
cluster ordinal -> non pair for set;
correctness
proof
let X be set;
assume
A1: X is ordinal;
assume X is pair;
then consider x1,x2 be object such that
A2: X = [x1,x2] by XTUPLE_0:def 1;
X = {{x1,x2},{x1}} by A2,TARSKI:def 5;
hence contradiction by A2,A1;
end;
end;
registration
let C be empty CategoryStr;
cluster Mor(C) -> empty;
correctness
proof
the carrier of C = {};
hence thesis by CAT_6:def 1;
end;
end;
registration
let C be non empty CategoryStr;
cluster Mor(C) -> non empty;
correctness
proof
the carrier of C <> {};
hence thesis by CAT_6:def 1;
end;
end;
registration
let C be empty with_identities CategoryStr;
cluster Ob(C) -> empty;
correctness;
end;
registration
let C be non empty with_identities CategoryStr;
cluster Ob(C) -> non empty;
correctness;
end;
registration
let C be with_identities CategoryStr;
let a be Object of C;
cluster id- a -> identity;
correctness
proof
per cases;
suppose C is empty;
hence thesis by CAT_6:10;
end;
suppose
A1: C is non empty;
id- a = a by CAT_6:def 20;
hence thesis by A1,CAT_6:22;
end;
end;
end;
theorem Th1:
for C being CategoryStr, f being morphism of C
st C is non empty holds f in the carrier of C
proof
let C be CategoryStr;
let f be morphism of C;
assume C is non empty;
then f in Mor C by SUBSET_1:def 1;
hence f in the carrier of C by CAT_6:def 1;
end;
theorem Th2:
for C being with_identities CategoryStr, a being Object of C
st C is non empty holds a in the carrier of C
proof
let C be with_identities CategoryStr;
let a be Object of C;
assume C is non empty;
then a in Ob C by SUBSET_1:def 1;
then a in Mor C;
hence a in the carrier of C by CAT_6:def 1;
end;
theorem Th3:
for C being composable CategoryStr, f1,f2,f3 being morphism of C st
f1 |> f2 & f2 |> f3 & f2 is identity holds f1 |> f3
proof
let C be composable CategoryStr;
let f1,f2,f3 be morphism of C;
A1: C is right_composable by CAT_6:def 11;
assume
A2: f1 |> f2 & f2 |> f3;
assume f2 is identity;
then f2(*)f3 = f3 by A2,CAT_6:def 14,def 4;
hence f1 |> f3 by A2,A1,CAT_6:def 9;
end;
theorem Th4:
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
proof
let C be with_identities composable CategoryStr;
let f1,f2 be morphism of C;
assume
A1: f1 |> f2;
per cases;
suppose
A2: C is empty;
thus dom (f1 (*) f2) = the Object of C by A2,CAT_6:def 18
.= dom f2 by A2,CAT_6:def 18;
thus cod (f1 (*) f2) = the Object of C by A2,CAT_6:def 19
.= cod f1 by A2,CAT_6:def 19;
end;
suppose
A3: C is non empty;
[f1,f2] in dom the composition of C by A1,CAT_6:def 2;
then [f1,f2] in dom(CompMap C) by CAT_6:def 29;
then
A4: (SourceMap C).f1 = (TargetMap C).f2 by A3,CAT_6:36;
A5: f1 (*) f2 = (the composition of C).(f1,f2) by A1,CAT_6:def 3
.= (CompMap C).(f1,f2) by CAT_6:def 29;
thus dom (f1 (*) f2) = (SourceMap C).(f1(*)f2) by A3,CAT_6:def 30
.= (SourceMap C).f2 by A4,A5,CAT_6:37
.= dom f2 by A3,CAT_6:def 30;
thus cod (f1 (*) f2) = (TargetMap C).(f1(*)f2) by A3,CAT_6:def 31
.= (TargetMap C).f1 by A4,A5,CAT_6:37
.= cod f1 by A3,CAT_6:def 31;
end;
end;
theorem Th5:
for C being non empty composable with_identities CategoryStr,
f1,f2 being morphism of C holds f1 |> f2 iff dom f1 = cod f2
proof
let C be non empty composable with_identities CategoryStr;
let f1,f2 be morphism of C;
A1: dom f1 = (SourceMap C).f1 by CAT_6:def 30;
A2: cod f2 = (TargetMap C).f2 by CAT_6:def 31;
hereby
assume f1 |> f2;
then [f1,f2] in dom the composition of C by CAT_6:def 2;
then [f1,f2] in dom CompMap C by CAT_6:def 29;
hence dom f1 = cod f2 by A1,A2,CAT_6:36;
end;
assume dom f1 = cod f2;
then (SourceMap C).f1 = (TargetMap C).f2 by A1,CAT_6:def 31;
then [f1,f2] in dom CompMap C by CAT_6:36;
then [f1,f2] in dom the composition of C by CAT_6:def 29;
hence f1 |> f2 by CAT_6:def 2;
end;
theorem Th6:
for C being with_identities composable CategoryStr,
f being morphism of C st f is identity holds dom f = f & cod f = f
proof
let C be with_identities composable CategoryStr;
let f be morphism of C;
assume
A1: f is identity;
per cases;
suppose
A2: C is empty;
then
A3: the Object of C = {} by SUBSET_1:def 1;
dom f = the Object of C & cod f = the Object of C
by A2,CAT_6:def 18,def 19;
hence thesis by A3,A2,SUBSET_1:def 1;
end;
suppose C is non empty;
hence thesis by A1,CAT_6:24,26,27;
end;
end;
theorem Th7:
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
proof
let C be composable with_identities CategoryStr;
let f1,f2 be morphism of C;
assume
A1: f1 |> f2;
assume
A2: f1 is identity;
assume f2 is identity;
hence f1 = f1 (*) f2 by A1,CAT_6:def 5,def 14
.= f2 by A1,A2,CAT_6:def 4,def 14;
end;
theorem Th8:
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
proof
let C be non empty composable with_identities CategoryStr;
let f1,f2 be morphism of C;
assume dom f1 = f2;
then consider f be morphism of C such that
A1: f2 = f & f1 |> f & f is identity by CAT_6:def 18;
thus f1 |> f2 by A1;
thus f1 (*) f2 = f1 by A1,CAT_6:def 5,def 14;
end;
theorem Th9:
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
proof
let C be non empty composable with_identities CategoryStr;
let f1,f2 be morphism of C;
assume f1 = cod f2;
then consider f be morphism of C such that
A1: f1 = f & f |> f2 & f is identity by CAT_6:def 19;
thus f1 |> f2 by A1;
thus f1 (*) f2 = f2 by A1,CAT_6:def 4,def 14;
end;
theorem Th10:
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
proof
let C1,C2,C3,C4 be category;
let F be Functor of C1,C2;
let G be Functor of C2,C3;
let H be Functor of C3,C4;
assume
A1: F is covariant;
assume
A2: G is covariant;
assume
A3: H is covariant;
set GF = G (*) F, HG = H (*) G;
A4: GF is covariant by A1,A2,CAT_6:35;
A5: HG is covariant by A2,A3,CAT_6:35;
thus H (*) (G (*) F) = GF * H by A4,A3,CAT_6:def 27
.= (F * G) * H by A1,A2,CAT_6:def 27
.= F * (G * H) by RELAT_1:36
.= F * HG by A2,A3,CAT_6:def 27
.= (H (*) G) (*) F by A5,A1,CAT_6:def 27;
end;
theorem Th11:
for C,D being category, F being Functor of C,D st
F is covariant holds F (*) id C = F & id D (*) F = F
proof
let C,D be category;
let F be Functor of C,D;
assume
A1: F is covariant;
thus F (*) id C = (id C) * F by A1,CAT_6:def 27
.= (id the carrier of C) * F by STRUCT_0:def 4
.= F by FUNCT_2:17;
thus id D (*) F = F * (id D) by A1,CAT_6:def 27
.= F * (id the carrier of D) by STRUCT_0:def 4
.= F by FUNCT_2:17;
end;
theorem Th12:
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
let C,D be composable with_identities CategoryStr;
hereby
assume C ~= D;
then consider F be Functor of C,D, G be Functor of D,C such that
A1: F is covariant & G is covariant & G(*)F = id C & F(*)G = id D
by CAT_6:def 28;
take F;
thus F is covariant by A1;
F * G = id C by A1,CAT_6:def 27 .= id the carrier of C by STRUCT_0:def 4;
then
A2: F is one-to-one by FUNCT_2:23;
G * F = id D by A1,CAT_6:def 27 .= id the carrier of D by STRUCT_0:def 4;
then
F is onto by FUNCT_2:23;
hence F is bijective by A2;
end;
given F be Functor of C,D such that
A3: F is covariant & F is bijective;
A4: rng F = the carrier of D by A3,FUNCT_2:def 3;
then reconsider G = F" as Function of the carrier of D, the carrier of C
by A3,FUNCT_2:25;
reconsider G as Functor of D,C;
per cases;
suppose
A5: the carrier of D <> {};
then
A6: G*F = id the carrier of D & F*G = id the carrier of C
by A3,A4,FUNCT_2:29;
A7: D is non empty by A5;
A8: C is non empty by A4,A5;
A9: F is identity-preserving & F is multiplicative by A3,CAT_6:def 25;
A10: for g being morphism of D holds F.(G.g) = g
proof
let g be morphism of D;
reconsider x1 = G.g, x2 = g as object;
g in Mor D by A7,SUBSET_1:def 1;
then
A11: g in the carrier of D by CAT_6:def 1;
then
A12: x2 in dom G by A8,FUNCT_2:def 1;
thus F.(G.g) = F.x1 by A8,CAT_6:def 21
.= F.(G.x2) by A7,CAT_6:def 21
.= (id the carrier of D).x2 by A6,A12,FUNCT_1:13
.= g by A11,FUNCT_1:18;
end;
A13: for f1,f2 being morphism of C st F.f1 = F.f2 holds f1 = f2
proof
let f1,f2 be morphism of C;
assume
A14: F.f1 = F.f2;
reconsider x1 = f1, x2 = f2 as object;
f1 in Mor C & f2 in Mor C by A8,SUBSET_1:def 1;
then f1 in the carrier of C & f2 in the carrier of C by CAT_6:def 1;
then
A15: x1 in dom F & x2 in dom F by A5,FUNCT_2:def 1;
F.x1 = F.f1 by A8,CAT_6:def 21
.= F.x2 by A14,A8,CAT_6:def 21;
hence f1 = f2 by A3,A15,FUNCT_1:def 4;
end;
for g being morphism of D st g is identity holds G.g is identity
proof
let g be morphism of D;
assume g is identity;
then
A16: for g1 being morphism of D st g |> g1 holds g(*)g1=g1
by CAT_6:def 4,def 14;
A17: for f1 being morphism of C st (G.g) |> f1 holds (G.g) (*) f1 = f1
proof
let f1 be morphism of C;
assume (G.g) |> f1;
then F.(G.g) |> F.f1 & F.((G.g) (*) f1) = (F.(G.g)) (*) (F.f1)
by A9,CAT_6:def 23;
then g |> F.f1 & F.((G.g) (*) f1) = g (*) (F.f1) by A10;
hence (G.g) (*) f1 = f1 by A16,A13;
end;
then
G.g is left_identity by CAT_6:def 4;
then G.g is right_identity by CAT_6:9;
hence G.g is identity by A17,CAT_6:def 4,CAT_6:def 14;
end;
then
A18: G is identity-preserving by CAT_6:def 22;
A19: for f being morphism of C holds G.(F.f) = f
proof
let f be morphism of C;
reconsider x1 = F.f, x2 = f as object;
f in Mor C by A8,SUBSET_1:def 1;
then
A20: f in the carrier of C by CAT_6:def 1;
then
A21: x2 in dom F by A5,FUNCT_2:def 1;
thus G.(F.f) = G.x1 by A7,CAT_6:def 21
.= G.(F.x2) by A8,CAT_6:def 21
.= (id the carrier of C).x2 by A6,A21,FUNCT_1:13
.= f by A20,FUNCT_1:18;
end;
for g1,g2 being morphism of D st g1 |> g2 holds
G.g1 |> G.g2 & G.(g1 (*) g2) = (G.g1) (*) (G.g2)
proof
let g1,g2 be morphism of D;
assume
A22: g1 |> g2;
reconsider f1 = G.g1, f2 = G.g2 as morphism of C;
A23: g1 = F.(G.g1) & g2 = F.(G.g2) by A10;
A24: dom(F.f1) = cod(F.f2) by A22,A23,A7,Th5;
Ob C is non empty by A8;
then dom f1 in Ob C & cod f2 in Ob C;
then reconsider d1 = dom f1, c2 = cod f2 as morphism of C;
F.d1 = F.(dom f1) by A8,CAT_6:def 21
.= dom(F.f1) by A7,A8,A3,CAT_6:32
.= F.(cod f2) by A24,A7,A8,A3,CAT_6:32
.= F.c2 by A8,CAT_6:def 21;
hence
A25: G.g1 |> G.g2 by A13,A8,Th5;
A26: F is multiplicative by A3,CAT_6:def 25;
g1 (*) g2
= F.((G.g1) (*) (G.g2)) by A23,A26,A25,CAT_6:def 23;
hence G.(g1 (*) g2) = (G.g1) (*) (G.g2) by A19;
end;
then
A27: G is covariant by A18,CAT_6:def 23,def 25;
then G*F = F (*) G & F*G = G (*) F by A3,CAT_6:def 27;
then G(*)F = id C & F(*)G = id D by A6,STRUCT_0:def 4;
hence C ~= D by A3,A27,CAT_6:def 28;
end;
suppose
A28: the carrier of D = {};
then
A29: D is empty;
then
A30: C is empty by A3,CAT_6:31;
for g being morphism of D st g is identity holds G.g is identity
by A30,CAT_6:10;
then
A31: G is identity-preserving by CAT_6:def 22;
for g1,g2 being morphism of D st g1 |> g2 holds
G.g1 |> G.g2 & G.(g1 (*) g2) = (G.g1) (*) (G.g2) by A29,CAT_6:1;
then
A32: G is covariant by A31,CAT_6:def 23,def 25;
G(*)F = id C & F(*)G = id D by A30,A28;
hence C ~= D by A3,A32,CAT_6:def 28;
end;
end;
theorem Th13:
for C,D being empty with_identities CategoryStr holds C ~= D
proof
let C,D be empty with_identities CategoryStr;
set F = the covariant Functor of C,D;
set G = the covariant Functor of D,C;
G (*) F = id C & F (*) G = id D;
hence C ~= D by CAT_6:def 28;
end;
theorem Th14:
for C,D being with_identities CategoryStr st
C ~= D holds card Mor C = card Mor D & card Ob C = card Ob D
proof
let C,D be with_identities CategoryStr;
assume C ~= D;
then consider F be Functor of C,D, G be Functor of D,C such that
A1: F is covariant & G is covariant & G(*)F = id C & F(*)G = id D
by CAT_6:def 28;
F * G = id C by A1,CAT_6:def 27 .= id the carrier of C by STRUCT_0:def 4;
then
A2: F is one-to-one by FUNCT_2:23;
A3: G * F = id D by A1,CAT_6:def 27 .= id the carrier of D by STRUCT_0:def 4;
per cases;
suppose
A4: D is empty;
C is empty by A4,A1,CAT_6:31;
hence thesis by A4;
end;
suppose
A5: D is not empty;
F is onto by A3,FUNCT_2:23;
then rng F = the carrier of D by FUNCT_2:def 3;
then
A6: rng F = Mor D by CAT_6:def 1;
A7: dom F = the carrier of C by A5,FUNCT_2:def 1;
then
A8: dom F = Mor C by CAT_6:def 1;
hence card Mor C = card Mor D by CARD_1:5,A6,A2,WELLORD2:def 4;
set F1 = F|(Ob C);
A9: dom F1 = Ob C by A8,RELAT_1:62;
for y being object holds y in rng F1 iff y in Ob D
proof
let y be object;
hereby
assume y in rng F1;
then consider x be object such that
A10: x in dom F1 & y = F1.x by FUNCT_1:def 3;
A11: x in Ob C by A10;
A12: y = F.x by A10,FUNCT_1:49;
x in {f where f is morphism of C : f is identity & f in Mor C}
by A11,CAT_6:def 17;
then consider f be morphism of C such that
A13: x = f & f is identity & f in Mor C;
C is non empty by A10;
then
A14: y = F.f by A12,A13,CAT_6:def 21;
then reconsider g = y as morphism of D;
Mor D <> {} by A5;
then g is identity & g in Mor D
by A14,A13,CAT_6:def 22,A1,CAT_6:def 25;
then g in {f1 where f1 is morphism of D :
f1 is identity & f1 in Mor D};
hence y in Ob D by CAT_6:def 17;
end;
assume y in Ob D;
then y in {g where g is morphism of D : g is identity & g in Mor D}
by CAT_6:def 17;
then consider g be morphism of D such that
A15: y = g & g is identity & g in Mor D;
consider x be object such that
A16: x in dom F & g = F.x by A15,A6,FUNCT_1:def 3;
reconsider f = x as morphism of C by A16,CAT_6:def 1;
A17: C is non empty by A16;
then g = F.f by A16,CAT_6:def 21;
then G.g = (G (*) F).f by A1,A17,CAT_6:34
.= (id C).x by A1,A17,CAT_6:def 21
.= (id the carrier of C).x by STRUCT_0:def 4
.= x by FUNCT_1:18,A16;
then f is identity & f in Mor C
by A16,A7,A15,CAT_6:def 22,A1,CAT_6:def 25,CAT_6:def 1;
then f in {f1 where f1 is morphism of C:f1 is identity & f1 in Mor C};
then
A18: f in Ob C by CAT_6:def 17;
g = F1.f by A18,A16,FUNCT_1:49;
hence y in rng F1 by A9,A18,A15,FUNCT_1:def 3;
end;
then
A19: rng F1 = Ob D by TARSKI:2;
F1 is one-to-one by A2,FUNCT_1:52;
hence card Ob C = card Ob D by CARD_1:5,A9,A19,WELLORD2:def 4;
end;
end;
theorem Th15:
for C,D being with_identities CategoryStr st C ~= D & C is empty
holds D is empty
proof
let C,D be with_identities CategoryStr;
assume C ~= D;
then
A1: card Mor C = card Mor D by Th14;
assume C is empty;
hence D is empty by A1;
end;
begin :: Hom-sets
definition
let C be CategoryStr;
let a,b be Object of C;
func Hom(a,b) -> Subset of Mor C equals
{f where f is morphism of C : ex f1,f2 being morphism of C st
a = f1 & b = f2 & f |> f1 & f2 |> f};
correctness
proof
set IT = {f where f is morphism of C : ex f1,f2 being morphism of C st
a = f1 & b = f2 & f |> f1 & f2 |> f};
now
for x being object st x in IT holds x in Mor C
proof
let x be object;
assume x in IT;
then consider f be morphism of C such that
A1: x = f & ex f1,f2 being morphism of C st
a = f1 & b = f2 & f |> f1 & f2 |> f;
consider f1,f2 be morphism of C such that
A2: a = f1 & b = f2 & f |> f1 & f2 |> f by A1;
C is non empty by A2,CAT_6:1;
then Mor C is non empty;
hence x in Mor C by A1;
end;
hence IT is Subset of Mor C by TARSKI:def 3;
end;
hence thesis;
end;
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 :Def2: :: redefines Hom (CAT_7, definition)
{f where f is morphism of C : dom f = a & cod f = b};
correctness
proof
for x being object holds x in Hom(a,b) iff
x in {f where f is morphism of C : dom f = a & cod f = b}
proof
let x be object;
hereby
assume x in Hom(a,b);
then consider f be morphism of C such that
A1: x = f & ex f1,f2 being morphism of C st
a = f1 & b = f2 & f |> f1 & f2 |> f;
consider f1,f2 be morphism of C such that
A2: a = f1 & b = f2 & f |> f1 & f2 |> f by A1;
dom f = a & cod f = b by A2,CAT_6:26,CAT_6:27,CAT_6:22;
hence x in {f where f is morphism of C:dom f = a & cod f = b} by A1;
end;
assume x in {f where f is morphism of C : dom f = a & cod f = b};
then consider f be morphism of C such that
A3: x = f & dom f = a & cod f = b;
consider f1 be morphism of C such that
A4: dom f = f1 & f |> f1 & f1 is identity by CAT_6:def 18;
consider f2 be morphism of C such that
A5: cod f = f2 & f2 |> f & f2 is identity by CAT_6:def 19;
thus x in Hom(a,b) by A3,A4,A5;
end;
hence thesis by TARSKI:2;
end;
end;
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:
it in Hom(a,b);
correctness by A1,SUBSET_1:4;
end;
definition
let C be non empty with_identities CategoryStr;
let a be Object of C;
redefine func id- a -> Morphism of a, a; :: redefines id- (CAT_6, definition)
coherence
proof
A3: id- a = a by CAT_6:def 20;
then id- a |> id- a by CAT_6:23;
then id- a in Hom(a,a) by A3;
hence thesis by Def3;
end;
end;
registration
let C be non empty with_identities CategoryStr;
let a be Object of C;
cluster Hom(a,a) -> non empty;
correctness
proof
A1: id- a = a by CAT_6:def 20;
then id- a |> id- a by CAT_6:23;
then id- a in Hom(a,a) by A1;
hence thesis;
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:
g (*) f;
correctness
proof
f in Hom(a,b) by A1,Def3;
then consider f3 be morphism of C such that
A2: f = f3 & ex f1,f2 being morphism of C
st a = f1 & b = f2 & f3 |> f1 & f2 |> f3;
consider f1,f2 be morphism of C such that
A3: a = f1 & b = f2 & f3 |> f1 & f2 |> f3 by A2;
g in Hom(b,c) by A1,Def3;
then consider g3 be morphism of C such that
A4: g = g3 & ex g1,g2 being morphism of C
st b = g1 & c = g2 & g3 |> g1 & g2 |> g3;
consider g1,g2 be morphism of C such that
A5: b = g1 & c = g2 & g3 |> g1 & g2 |> g3 by A4;
A6: C is left_composable & C is right_composable by CAT_6:def 11;
C is non empty by A2,CAT_6:1;
then
A7: g |> f by A2,A4,Th3,CAT_6:22;
g2 |> g(*)f & g(*)f |> f1 by A2,A3,A4,A5,A7,A6,CAT_6:def 8,def 9;
then g(*)f in Hom(a,c) by A3,A5;
hence thesis by Def3;
end;
end;
theorem Th16:
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
proof
let C be CategoryStr;
let a,b be Object of C;
let f be Morphism of a,b;
assume Hom(a,b) <> {};
then f in Hom(a,b) by Def3;
then consider f11 be morphism of C such that
A1: f11 = f & ex f1,f2 being morphism of C
st a = f1 & b = f2 & f11 |> f1 & f2 |> f11;
thus thesis by A1;
end;
theorem Th17:
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
proof
let C be composable with_identities CategoryStr;
let a,b,c be Object of C;
let f1 be Morphism of a,b;
let f2 be Morphism of b,c;
assume Hom(a,b) <> {};
then consider f11,f12 be morphism of C such that
A1: a = f11 & b = f12 & f1 |> f11 & f12 |> f1 by Th16;
assume Hom(b,c) <> {};
then consider f21,f22 be morphism of C such that
A2: b = f21 & c = f22 & f2 |> f21 & f22 |> f2 by Th16;
C is non empty by A1,CAT_6:1;
hence f2 |> f1 by A1,A2,Th3,CAT_6:22;
end;
theorem Th18:
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
proof
let C be composable non empty with_identities CategoryStr;
let a,b be Object of C;
let f be Morphism of a,b;
assume
A1: Hom(a,b) <> {};
A3: id- a = a & id- b = b by CAT_6:def 20;
A4: Hom(a,a) <> {} & Hom(b,b) <> {};
A5: f |> id- a & id- b |> f by A1,A4,Th17;
thus f * (id- a) = f (*) (id- a) by A4,A1,Def4
.= f by A3,A5,CAT_6:23;
thus (id- b) * f = (id- b) (*) f by A4,A1,Def4
.= f by A3,A5,CAT_6:23;
end;
theorem Th19:
for C being non empty with_identities composable CategoryStr,
f being morphism of C holds f in Hom(dom f,cod f);
theorem Th20:
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
proof
let C be non empty with_identities composable CategoryStr;
let a,b be Object of C;
let f be morphism of C;
hereby
assume f in Hom(a,b);
then consider f1 be morphism of C such that
A1: f = f1 & a = dom f1 & b = cod f1;
thus dom f = a & cod f = b by A1;
end;
assume dom f = a & cod f = b;
hence f in Hom(a,b);
end;
theorem Th21:
for C being non empty with_identities composable CategoryStr,
a being Object of C holds a in Hom(a,a)
proof
let C be non empty with_identities composable CategoryStr;
let a be Object of C;
a in Ob C;
then reconsider f = a as morphism of C;
f is identity by CAT_6:22;
then dom f = f & cod f = f by Th6;
hence a in Hom(a,a);
end;
theorem Th22:
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) <> {}
proof
let C be composable with_identities CategoryStr;
let a,b,c be Object of C;
assume
A1: Hom(a,b) <> {};
set f1 = the Morphism of a,b;
consider f11,f12 be morphism of C such that
A2: a = f11 & b = f12 & f1 |> f11 & f12 |> f1 by A1,Th16;
assume
A3: Hom(b,c) <> {};
set f2 = the Morphism of b,c;
consider f22,f23 be morphism of C such that
A4: b = f22 & c = f23 & f2 |> f22 & f23 |> f2 by A3,Th16;
A5: C is left_composable & C is right_composable by CAT_6:def 11;
C is non empty by A2,CAT_6:1;
then
A6: f2 |> f1 by A2,A4,Th3,CAT_6:22;
f23 |> f2(*)f1 & f2(*)f1 |> f11 by A2,A4,A6,A5,CAT_6:def 8,def 9;
then f2(*)f1 in Hom(a,c) by A2,A4;
hence Hom(a,c) <> {};
end;
theorem Th23:
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
proof
let C be category;
let a,b,c,d be Object of C;
let f1 be Morphism of a,b;
let f2 be Morphism of b,c;
let f3 be Morphism of c,d;
assume
A1: Hom(a,b) <> {};
assume
A2: Hom(b,c) <> {};
assume
A3: Hom(c,d) <> {};
A4: Hom(a,c) <> {} by A1,A2,Th22;
A5: Hom(b,d) <> {} by A2,A3,Th22;
A6: f3 |> f2 & f2 |> f1 by A1,A2,A3,Th17;
f3 * f2 |> f1 by A5,A1,Th17;
then
A7: f3 (*) f2 |> f1 by A2,A3,Def4;
f3 |> f2 * f1 by A4,A3,Th17;
then
A8: f3 |> f2 (*) f1 by A1,A2,Def4;
thus f3 * (f2 * f1) = f3 (*) (f2 * f1) by A3,A4,Def4
.= f3 (*) (f2 (*) f1) by A1,A2,Def4
.= (f3 (*) f2) (*) f1 by A6,A7,A8,CAT_6:def 10
.= (f3 * f2) (*) f1 by A2,A3,Def4
.= (f3 * f2) * f1 by A1,A5,Def4;
end;
theorem Th24:
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)
proof
let C be composable with_identities CategoryStr;
let a,b,c be Object of C;
let f1 be Morphism of a,b;
let f2 be Morphism of b,c;
assume
A1: Hom(a,b) <> {} & Hom(b,c) <> {};
then
A2: C is non empty;
A3: f2 |> f1 by A1,Th17;
thus (f1 is identity implies f2 * f1 = f2)
proof
assume
f1 is identity;
then
A4: f1 is Object of C by A2,CAT_6:22;
thus f2 * f1 = f2 (*) f1 by A1,Def4
.= f2 by A2,A4,A3,CAT_6:23;
end;
assume
f2 is identity;
then
A5: f2 is Object of C by A2,CAT_6:22;
thus f2 * f1 = f2 (*) f1 by A1,Def4
.= f1 by A2,A5,A3,CAT_6:23;
end;
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
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
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
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
proof
let C be composable with_identities CategoryStr;
let a,b be Object of C;
let f1 be Morphism of a,b;
assume
A1: Hom(a,b) <> {};
assume
A2: f1 is identity;
thus Hom(a,b) <> {} by A1;
let c be Object of C;
assume
A3: Hom(c,a) <> {};
let g1,g2 be Morphism of c,a;
assume
A4: f1 * g1 = f1 * g2;
thus g1 = f1 * g1 by A3,A1,A2,Th24
.= g2 by A3,A1,A4,A2,Th24;
end;
theorem
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
proof
let C be category;
let a,b,c be Object of C;
let f1 be Morphism of a,b;
let f2 be Morphism of b,c;
assume
A1: f1 is monomorphism;
assume
A2: f2 is monomorphism;
hence Hom(a,c) <> {} by A1,Th22;
let d be Object of C;
assume
A3: Hom(d,a) <> {};
let g1,g2 be Morphism of d,a;
assume
A4: (f2 * f1) * g1 = (f2 * f1) * g2;
A5: Hom(d,b) <> {} by A3,A1,Th22;
f2 * (f1 * g1) = (f2 * f1) * g1 by A1,A2,A3,Th23
.= f2 * (f1 * g2) by A4,A1,A2,A3,Th23;
hence g1 = g2 by A1,A3,A2,A5;
end;
theorem
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
proof
let C be category;
let a,b,c be Object of C;
let f1 be Morphism of a,b;
let f2 be Morphism of b,c;
assume
A1: f2 * f1 is monomorphism;
assume
A2: Hom(a,b) <> {} & Hom(b,c) <> {};
thus Hom(a,b) <> {} by A2;
let d be Object of C;
assume
A3: Hom(d,a) <> {};
let g1,g2 be Morphism of d,a;
assume
A4: f1 * g1 = f1 * g2;
(f2 * f1) * g1 = f2 * (f1 * g1) by A2,A3,Th23
.= (f2 * f1) * g2 by A2,A4,A3,Th23;
hence g1 = g2 by A1,A3;
end;
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
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g being Morphism of b,a st g * f = id- a;
attr f is retraction means
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g being Morphism of b,a st f * g = id- b;
end;
theorem Th28:
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
proof
let C be non empty category;
let a,b be Object of C;
let f be Morphism of a,b;
assume
A1: f is section_;
then consider g be Morphism of b,a such that
A2: g * f = id- a;
thus Hom(a,b) <> {} by A1;
let c be Object of C;
assume
A3: Hom(c,a) <> {};
let g1,g2 be Morphism of c,a;
assume
A4: f * g1 = f * g2;
A5: (g * f) * g1 = g * (f * g1) by A1,A3,Th23
.= (g * f) * g2 by A1,A4,A3,Th23;
thus g1 = (g * f) * g1 by A3,A2,Th18
.= g2 by A5,A3,A2,Th18;
end;
theorem
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
proof
let C be composable with_identities CategoryStr;
let a,b be Object of C;
let f1 be Morphism of a,b;
assume
A1: Hom(a,b) <> {};
assume
A2: f1 is identity;
thus Hom(a,b) <> {} by A1;
let c be Object of C;
assume
A3: Hom(b,c) <> {};
let g1,g2 be Morphism of b,c;
assume
A4: g1 * f1 = g2 * f1;
thus g1 = g1 * f1 by A3,A1,A2,Th24
.= g2 by A3,A1,A4,A2,Th24;
end;
theorem
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
proof
let C be category;
let a,b,c be Object of C;
let f1 be Morphism of a,b;
let f2 be Morphism of b,c;
assume
A1: f1 is epimorphism;
assume
A2: f2 is epimorphism;
hence Hom(a,c) <> {} by A1,Th22;
let d be Object of C;
assume
A3: Hom(c,d) <> {};
let g1,g2 be Morphism of c,d;
assume
A4: g1 * (f2 * f1) = g2 * (f2 * f1);
A5: Hom(b,d) <> {} by A3,A2,Th22;
(g1 * f2) * f1 = g1 * (f2 * f1) by A1,A2,A3,Th23
.= (g2 * f2) * f1 by A4,A1,A2,A3,Th23;
hence g1 = g2 by A3,A2,A1,A5;
end;
theorem
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
proof
let C be category;
let a,b,c be Object of C;
let f1 be Morphism of a,b;
let f2 be Morphism of b,c;
assume
A1: f2 * f1 is epimorphism;
assume
A2: Hom(a,b) <> {} & Hom(b,c) <> {};
thus Hom(b,c) <> {} by A2;
let d be Object of C;
assume
A3: Hom(c,d) <> {};
let g1,g2 be Morphism of c,d;
assume
A4: g1 * f2 = g2 * f2;
g1 * (f2 * f1) = (g1 * f2) * f1 by A2,A3,Th23
.= g2 * (f2 * f1) by A2,A4,A3,Th23;
hence g1 = g2 by A1,A3;
end;
theorem Th32:
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
proof
let C be non empty category;
let a,b be Object of C;
let f be Morphism of a,b;
assume
A1: f is retraction;
then consider g be Morphism of b,a such that
A2: f * g = id- b;
thus Hom(a,b) <> {} by A1;
let c be Object of C;
assume
A3: Hom(b,c) <> {};
let g1,g2 be Morphism of b,c;
assume
A4: g1 * f = g2 * f;
A5: g1 * (f * g) = (g1 * f) * g by A1,A3,Th23
.= g2 * (f * g) by A1,A4,A3,Th23;
thus g1 = g1 * (f * g) by A3,A2,Th18
.= g2 by A5,A3,A2,Th18;
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
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
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 :: redefines are_isomorphic (CAT_7, definition)
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;
correctness
proof
hereby
assume a,b are_isomorphic;
then consider f be Morphism of a,b such that
A1: f is isomorphism;
thus Hom(a,b) <> {} & Hom(b,a) <> {} by A1;
consider g be Morphism of b,a such that
A2: g * f = id- a & f * g = id- b by A1;
take f,g;
thus g * f = id- a & f * g = id- b by A2;
end;
assume
A3: Hom(a,b) <> {} & Hom(b,a) <> {};
given f be Morphism of a,b, g be Morphism of b,a such that
A4: g * f = id- a & f * g = id- b;
f is isomorphism by A3,A4;
hence a,b are_isomorphic;
end;
end;
theorem
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
proof
let C be non empty category;
let a,b be Object of C;
let f be Morphism of a,b;
assume
A1: f is isomorphism;
f is section_ by A1;
hence f is monomorphism by Th28;
f is retraction by A1;
hence f is epimorphism by Th32;
end;
begin :: Ordinal Numbers as Categories
definition
let C be CategoryStr;
attr C is preorder means :Def12:
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;
correctness;
end;
registration
cluster strict preorder for CategoryStr;
correctness
proof
set C = the strict empty CategoryStr;
take C;
thus thesis;
end;
end;
registration
cluster preorder -> associative
for composable with_identities CategoryStr;
correctness
proof
let C be composable with_identities CategoryStr;
assume
A1: C is preorder;
per cases;
suppose C is empty;
hence thesis;
end;
suppose
A2: C is non empty;
for f1,f2,f3 being morphism of C
st f1 |> f2 & f2 |> f3 & (f1(*)f2) |> f3 & f1 |> (f2(*)f3)
holds f1(*)(f2(*)f3) = (f1(*)f2)(*)f3
proof
let f1,f2,f3 be morphism of C;
assume
A3: f1 |> f2 & f2 |> f3 & (f1(*)f2) |> f3 & f1 |> (f2(*)f3);
set f11 = f1(*)(f2(*)f3), f22 = (f1(*)f2)(*)f3;
A4: dom f11 = dom(f2(*)f3) by A3,Th4 .= dom f3 by A3,Th4
.= dom f22 by A3,Th4;
cod f11 = cod f1 by A3,Th4 .= cod (f1(*)f2) by A3,Th4
.= cod f22 by A3,Th4;
then f11 in Hom(dom f11,cod f11) & f22 in Hom(dom f11,cod f11)
by A4,A2,Th19;
hence f1(*)(f2(*)f3) = (f1(*)f2)(*)f3 by A1;
end;
hence thesis by CAT_6:def 10;
end;
end;
end;
definition
let C be with_identities CategoryStr;
func RelOb(C) -> Relation of Ob(C) equals
{[a,b] where a,b is Object of C :
ex f being morphism of C st f in Hom(a,b)};
coherence
proof
set IT = {[a,b] where a,b is Object of C :
ex f being morphism of C st f in Hom(a,b)};
for x being object st x in IT holds x in [:Ob C, Ob C:]
proof
let x be object;
assume x in IT;
then consider a,b be Object of C such that
A1: x = [a,b] & ex f being morphism of C st f in Hom(a,b);
C is non empty by A1;
hence x in [:Ob C, Ob C:] by A1,ZFMISC_1:def 2;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
let C be empty with_identities CategoryStr;
cluster RelOb(C) -> empty;
correctness;
end;
theorem Th34:
for C being composable with_identities CategoryStr holds
dom RelOb C = Ob C & rng RelOb C = Ob C
proof
let C be composable with_identities CategoryStr;
per cases;
suppose C is empty;
then Ob C = {} & RelOb C = {};
hence thesis;
end;
suppose
A1: C is non empty;
for x being object st x in Ob C holds x in dom RelOb C
proof
let x be object;
assume
A2: x in Ob C;
then reconsider o = x as Object of C;
reconsider f = o as morphism of C by A2;
f is identity by A1,CAT_6:22;
then
A3: dom f = o & cod f = o by Th6;
f in Hom(dom f,cod f) by A1,Th19;
then [o,o] in RelOb C by A3;
hence x in dom RelOb C by XTUPLE_0:def 12;
end;
then Ob C c= dom RelOb C by TARSKI:def 3;
hence dom RelOb C = Ob C by XBOOLE_0:def 10;
for x being object st x in Ob C holds x in rng RelOb C
proof
let x be object;
assume
A4: x in Ob C;
then reconsider o = x as Object of C;
reconsider f = o as morphism of C by A4;
f is identity by A1,CAT_6:22;
then
A5: dom f = o & cod f = o by Th6;
f in Hom(dom f,cod f) by A1,Th19;
then [o,o] in RelOb C by A5;
hence x in rng RelOb C by XTUPLE_0:def 13;
end;
then Ob C c= rng RelOb C by TARSKI:def 3;
hence rng RelOb C = Ob C by XBOOLE_0:def 10;
end;
end;
theorem Th35:
for C1,C2 being composable with_identities CategoryStr st C1 ~= C2
holds RelOb(C1), RelOb(C2) are_isomorphic
proof
let C1,C2 be composable with_identities CategoryStr;
assume
A1: C1 ~= C2;
per cases;
suppose
A2: C1 is empty;
then
A3: RelOb(C1) is empty;
C2 is empty by A2,A1,Th15;
then RelOb(C2) is empty;
hence thesis by A3,WELLORD1:38;
end;
suppose
A4: C1 is non empty;
then
A5: C2 is non empty by A1,Th15;
consider F be Functor of C1,C2, G be Functor of C2,C1 such that
A6: F is covariant & G is covariant & G (*) F = id C1 & F (*) G = id C2
by A1,CAT_6:def 28;
F * G = id C1 by A6,CAT_6:def 27
.= id the carrier of C1 by STRUCT_0:def 4;
then
A7: F is one-to-one by FUNCT_2:23;
set F1 = F | Ob(C1);
A8: dom F = the carrier of C1 by A5,FUNCT_2:def 1
.= Mor C1 by CAT_6:def 1;
then
A9: dom F1 = Ob C1 by RELAT_1:62;
A10: Ob C1 = Ob C1 \/ Ob C1
.= Ob C1 \/ rng RelOb(C1) by Th34
.= dom RelOb(C1) \/ rng RelOb(C1) by Th34
.= field RelOb(C1) by RELAT_1:def 6;
then
A11: dom F1 = field RelOb(C1) by A8,RELAT_1:62;
for y being object holds y in rng F1 implies y in Ob C2
proof
let y be object;
assume y in rng F1;
then consider x be object such that
A12: x in dom F1 & y = F1.x by FUNCT_1:def 3;
x in Ob C1 by A12;
then x in {f where f is morphism of C1:
f is identity & f in Mor C1} by CAT_6:def 17;
then consider f be morphism of C1 such that
A13: x = f & f is identity & f in Mor C1;
A14: y = F.x by A12,FUNCT_1:49
.= F.f by A13,A4,CAT_6:def 21;
F.f is identity by A13,CAT_6:def 22,A6,CAT_6:def 25;
then F.f in {g where g is morphism of C2:
g is identity & g in Mor C2} by A5;
hence y in Ob C2 by A14,CAT_6:def 17;
end;
then
A15: rng F1 c= Ob C2 by TARSKI:def 3;
for y being object holds y in Ob C2 implies y in rng F1
proof
let y be object;
assume
A16: y in Ob C2;
set x = G.y;
A17: G*F = id C2 by A6,CAT_6:def 27;
A18: y in Mor C2 by A16;
then
A19: y in the carrier of C2 by CAT_6:def 1;
y in dom id the carrier of C2 by A18,CAT_6:def 1;
then
A20: y in dom(G*F) by A17,STRUCT_0:def 4;
then
A21: x in dom F by FUNCT_1:11;
A22: F.x = (G*F).y by A20,FUNCT_1:12
.= (id C2).y by A6,CAT_6:def 27
.= (id the carrier of C2).y by STRUCT_0:def 4
.= y by A19,FUNCT_1:18;
y in {g where g is morphism of C2:
g is identity & g in Mor C2} by A16,CAT_6:def 17;
then consider g be morphism of C2 such that
A23: y = g & g is identity & g in Mor C2;
A24: x = G.g by A23,A4,A1,Th15,CAT_6:def 21;
G.g is identity by A23,CAT_6:def 22,A6,CAT_6:def 25;
then G.g in {f where f is morphism of C1:
f is identity & f in Mor C1} by A4;
then x in Ob C1 by A24,CAT_6:def 17;
hence y in rng F1 by A21,A22,FUNCT_1:50;
end;
then
A25: Ob C2 c= rng F1 by TARSKI:def 3;
then
A26: rng F1 = Ob C2 by A15,XBOOLE_0:def 10;
A27: rng F1 = Ob C2 \/ Ob C2 by A25,A15,XBOOLE_0:def 10
.= Ob C2 \/ rng RelOb(C2) by Th34
.= dom RelOb(C2) \/ rng RelOb(C2) by Th34
.= field RelOb(C2) by RELAT_1:def 6;
A28: F1 is one-to-one by A7,FUNCT_1:52;
for a,b being object holds [a,b] in RelOb(C1) iff
(a in field RelOb(C1) & b in field RelOb(C1) & [F1.a, F1.b] in RelOb(C2))
proof
let a,b be object;
hereby
assume [a,b] in RelOb(C1);
then consider a1,b1 be Object of C1 such that
A29: [a,b] = [a1,b1] & ex f being morphism of C1 st f in Hom(a1,b1);
consider f be morphism of C1 such that
A30: f in Hom(a1,b1) by A29;
A31: a = a1 & b = b1 by A29,XTUPLE_0:1;
Ob C1 is non empty by A4;
then
A32: a1 in Ob C1 & b1 in Ob C1;
hence a in field RelOb(C1) & b in field RelOb(C1)
by A10,A29,XTUPLE_0:1;
A33: F1.a = F.a1 by A31,A4,FUNCT_1:49;
A34: F1.b = F.b1 by A31,A4,FUNCT_1:49;
a in dom F1 & b in dom F1 by A9,A29,XTUPLE_0:1,A32;
then reconsider a2 = F1.a, b2 = F1.b as Object of C2
by A26,FUNCT_1:3;
dom f = a1 & cod f = b1 by A30,A4,Th20;
then dom(F.f) = F.a1 & cod(F.f) = F.b1 by A4,A5,A6,CAT_6:32;
then F.f in Hom(a2,b2) by A33,A34,A5,Th20;
hence [F1.a, F1.b] in RelOb(C2);
end;
assume
A35: a in field RelOb(C1) & b in field RelOb(C1);
assume [F1.a, F1.b] in RelOb(C2);
then consider a2,b2 be Object of C2 such that
A36: [F1.a,F1.b] = [a2,b2] & ex g being morphism of C2 st g in Hom(a2,b2);
consider g be morphism of C2 such that
A37: g in Hom(a2,b2) by A36;
reconsider a1=a, b1=b as Object of C1 by A10,A35;
A38: F*G = id C1 by A6,CAT_6:def 27;
A39: a in Mor C1 by A10,A35;
then
A40: a in the carrier of C1 by CAT_6:def 1;
a in dom id the carrier of C1 by A39,CAT_6:def 1;
then
A41: a in dom(F*G) by A38,STRUCT_0:def 4;
A42: G.a2 = G.(F1.a) by A36,XTUPLE_0:1
.= G.(F.a) by A10,A35,FUNCT_1:49
.= (F*G).a by A41,FUNCT_1:12
.= (id C1).a by A6,CAT_6:def 27
.= (id the carrier of C1).a by STRUCT_0:def 4
.= a1 by A40,FUNCT_1:18;
A43: b in Mor C1 by A10,A35; then
A44: b in the carrier of C1 by CAT_6:def 1;
b in dom id the carrier of C1 by A43,CAT_6:def 1; then
A45: b in dom(F*G) by A38,STRUCT_0:def 4;
A46: G.b2 = G.(F1.b) by A36,XTUPLE_0:1
.= G.(F.b) by A10,A35,FUNCT_1:49
.= (F*G).b by A45,FUNCT_1:12
.= (id C1).b by A6,CAT_6:def 27
.= (id the carrier of C1).b by STRUCT_0:def 4
.= b1 by A44,FUNCT_1:18;
G.(dom g) = G.a2 & G.(cod g) = G.b2 by A37,A5,Th20;
then dom(G.g) = G.a2 & cod(G.g) = G.b2 by A4,A5,A6,CAT_6:32;
then G.g in Hom(a1,b1) by A42,A46,A4,Th20;
hence [a,b] in RelOb(C1);
end;
hence thesis by A11,A27,A28,WELLORD1:def 7,def 8;
end;
end;
registration
let C be non empty composable with_identities CategoryStr;
cluster RelOb C -> non empty;
correctness
proof
assume RelOb C is empty;
then dom RelOb C = {};
hence contradiction by Th34;
end;
end;
theorem Th36:
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])
proof
let C be preorder composable with_identities CategoryStr;
assume
A1: C is non empty;
then reconsider C1 = C as non empty composable with_identities CategoryStr;
defpred P[object,object] means for f being morphism of C1 st $1 = f holds
$2 = [dom f, cod f];
A2: for x being Element of the carrier of C1
ex y being Element of RelOb(C1) st P[x,y]
proof
let x be Element of the carrier of C1;
reconsider f = x as morphism of C1 by CAT_6:def 1;
set y = [dom f, cod f];
f in Hom(dom f, cod f);
then y in RelOb(C1);
then reconsider y as Element of RelOb(C1);
take y;
thus P[x,y];
end;
consider F be Function of the carrier of C1, RelOb(C1) such that
A3: for x being Element of the carrier of C1 holds P[x,F.x]
from FUNCT_2:sch 3(A2);
reconsider F as Function of C, RelOb(C);
take F;
for y being object st y in RelOb(C) holds y in rng F
proof
let y be object;
assume y in RelOb(C);
then consider a,b be Object of C such that
A4: y = [a,b] & ex f being morphism of C st f in Hom (a,b);
consider f be morphism of C such that
A5: f in Hom(a,b) by A4;
reconsider x = f as Element of C1 by CAT_6:def 1;
x in the carrier of C1;
then
A6: x in dom F by FUNCT_2:def 1;
a = dom f & b = cod f by A1,A5,Th20;
then F.x = [a,b] by A3;
hence y in rng F by A4,A6,FUNCT_1:3;
end;
then RelOb(C1) c= rng F by TARSKI:def 3;
then
A7: F is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
for x1,x2 being object st x1 in dom F & x2 in dom F & F.x1 = F.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A8: x1 in dom F & x2 in dom F;
assume
A9: F.x1 = F.x2;
reconsider x11=x1, x22=x2 as Element of the carrier of C1 by A8;
reconsider f1=x11,f2=x22 as morphism of C1 by CAT_6:def 1;
A10: F.f1 = [dom f1, cod f1] by A3;
F.f2 = [dom f2, cod f2] by A3;
then dom f1 = dom f2 & cod f1 = cod f2 by A10,A9,XTUPLE_0:1;
then f1 in Hom(dom f1, cod f1) & f2 in Hom(dom f1, cod f1);
hence x1=x2 by Def12;
end;
then F is one-to-one by FUNCT_1:def 4;
hence F is bijective by A7;
let f be morphism of C;
reconsider x = f as Element of the carrier of C1 by CAT_6:def 1;
thus F.f = F.x .= [dom f,cod f] by A3;
end;
theorem Th37:
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
let O be ordinal number;
per cases;
suppose
A1: O is empty;
set C = the strict empty category;
take C;
thus Ob C = O by A1;
for x being object holds
not x in {[o1,o2] where o1,o2 is Element of O: o1 in o2}
proof
let x be object;
assume x in {[o1,o2] where o1,o2 is Element of O: o1 in o2};
then consider o1,o2 be Element of O such that
A2: x = [o1,o2] & o1 in o2;
thus contradiction by A2,A1,SUBSET_1:def 1;
end;
hence thesis by A1,SUBSET_1:def 1,XBOOLE_0:def 1;
end;
suppose
A3: O is non empty;
set X1 = {[o1,o2] where o1,o2 is Element of O: o1 in o2};
set X = O \/ X1;
set F1 = {[[o1,o1],o1] where o1 is Element of O: not contradiction};
set F2 = {[[o2,[o1,o2]],[o1,o2]] where o1,o2 is Element of O: o1 in o2};
set F3 = {[[[o1,o2],o1],[o1,o2]] where o1,o2 is Element of O: o1 in o2};
set F4 = {[[[o2,o3],[o1,o2]],[o1,o3]] where o1,o2,o3 is Element of O:
o1 in o2 & o2 in o3};
set F = F1 \/ F2 \/ F3 \/ F4;
A4: for x being object st x in F holds
(ex o1 being Element of O st x = [[o1,o1],o1]) or
(ex o1,o2 being Element of O st o1 in o2 &
(x=[[o2,[o1,o2]],[o1,o2]] or x=[[[o1,o2],o1],[o1,o2]])) or
(ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]])
proof
let x be object;
assume
A5: x in F;
per cases by A5,XBOOLE_0:def 3;
suppose
A6: x in F1 \/ F2 \/ F3;
per cases by A6,XBOOLE_0:def 3;
suppose
A7: x in F1 \/ F2;
per cases by A7,XBOOLE_0:def 3;
suppose x in F1;
then consider o1 be Element of O such that
A8: x = [[o1,o1],o1];
thus thesis by A8;
end;
suppose x in F2;
then consider o1,o2 be Element of O such that
A9: x=[[o2,[o1,o2]],[o1,o2]] & o1 in o2;
thus thesis by A9;
end;
end;
suppose x in F3;
then consider o1,o2 be Element of O such that
A10: x = [[[o1,o2],o1],[o1,o2]] & o1 in o2;
thus thesis by A10;
end;
end;
suppose x in F4;
then consider o1,o2,o3 be Element of O such that
A11: x = [[[o2,o3],[o1,o2]],[o1,o3]] & o1 in o2 & o2 in o3;
thus thesis by A11;
end;
end;
A12: for x,y1,y2 being object st [x,y1] in F & [x,y2] in F holds y1 = y2
proof
let x,y1,y2 be object;
assume
A13: [x,y1] in F;
per cases by A4,A13;
suppose ex o1 being Element of O st [x,y1] = [[o1,o1],o1];
then consider o1 be Element of O such that
A14: [x,y1] = [[o1,o1],o1];
A15: x = [o1,o1] & y1 = o1 by A14,XTUPLE_0:1;
assume
A16: [x,y2] in F;
per cases by A4,A16;
suppose ex o1 being Element of O st [x,y2] = [[o1,o1],o1];
then consider o11 be Element of O such that
A17: [x,y2] = [[o11,o11],o11];
x = [o11,o11] & y2 = o11 by A17,XTUPLE_0:1;
hence thesis by A15,XTUPLE_0:1;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([x,y2]=[[o2,[o1,o2]],[o1,o2]] or [x,y2]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A18: o11 in o12 & ([x,y2]=[[o12,[o11,o12]],[o11,o12]] or
[x,y2]=[[[o11,o12],o11],[o11,o12]]);
x = [o12,[o11,o12]] or x = [[o11,o12],o11] by A18,XTUPLE_0:1;
hence thesis by A15,XTUPLE_0:1;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o11,o12,o13 be Element of O such that
A19: o11 in o12 & o12 in o13 & [x,y2]=[[[o12,o13],[o11,o12]],[o11,o13]];
x = [[o12,o13],[o11,o12]] by A19,XTUPLE_0:1;
hence thesis by A15,XTUPLE_0:1;
end;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([x,y1]=[[o2,[o1,o2]],[o1,o2]] or [x,y1]=[[[o1,o2],o1],[o1,o2]]);
then consider o1,o2 be Element of O such that
A20: o1 in o2 &
([x,y1]=[[o2,[o1,o2]],[o1,o2]] or [x,y1]=[[[o1,o2],o1],[o1,o2]]);
per cases by A20;
suppose [x,y1]=[[o2,[o1,o2]],[o1,o2]];
then
A21: x = [o2,[o1,o2]] & y1 = [o1,o2] by XTUPLE_0:1;
assume
A22: [x,y2] in F;
per cases by A4,A22;
suppose ex o1 being Element of O st [x,y2] = [[o1,o1],o1];
then consider o11 be Element of O such that
A23: [x,y2] = [[o11,o11],o11];
x = [o11,o11] by A23,XTUPLE_0:1;
hence thesis by A21,XTUPLE_0:1;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([x,y2]=[[o2,[o1,o2]],[o1,o2]] or [x,y2]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A24: o11 in o12 & ([x,y2]=[[o12,[o11,o12]],[o11,o12]] or
[x,y2]=[[[o11,o12],o11],[o11,o12]]);
per cases by A24;
suppose [x,y2]=[[o12,[o11,o12]],[o11,o12]];
then x = [o12,[o11,o12]] & y2 = [o11,o12] by XTUPLE_0:1;
hence thesis by A21,XTUPLE_0:1;
end;
suppose [x,y2]=[[[o11,o12],o11],[o11,o12]];
then x = [[o11,o12],o11] by XTUPLE_0:1;
hence thesis by A21,XTUPLE_0:1;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o11,o12,o13 be Element of O such that
A25: o11 in o12 & o12 in o13 &
[x,y2]=[[[o12,o13],[o11,o12]],[o11,o13]];
x = [[o12,o13],[o11,o12]] by A25,XTUPLE_0:1;
hence thesis by A21,XTUPLE_0:1;
end;
end;
suppose [x,y1]=[[[o1,o2],o1],[o1,o2]];
then
A26: x = [[o1,o2],o1] & y1 = [o1,o2] by XTUPLE_0:1;
assume
A27: [x,y2] in F;
per cases by A4,A27;
suppose ex o1 being Element of O st [x,y2] = [[o1,o1],o1];
then consider o11 be Element of O such that
A28: [x,y2] = [[o11,o11],o11];
x = [o11,o11] by A28,XTUPLE_0:1;
hence thesis by A26,XTUPLE_0:1;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([x,y2]=[[o2,[o1,o2]],[o1,o2]] or [x,y2]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A29: o11 in o12 & ([x,y2]=[[o12,[o11,o12]],[o11,o12]] or
[x,y2]=[[[o11,o12],o11],[o11,o12]]);
per cases by A29;
suppose [x,y2]=[[o12,[o11,o12]],[o11,o12]];
then x = [o12,[o11,o12]] by XTUPLE_0:1;
hence thesis by A26,XTUPLE_0:1;
end;
suppose [x,y2]=[[[o11,o12],o11],[o11,o12]];
then
A30: x = [[o11,o12],o11] & y2 = [o11,o12] by XTUPLE_0:1;
thus thesis by A26,A30,XTUPLE_0:1;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o11,o12,o13 be Element of O such that
A31: o11 in o12 & o12 in o13 &
[x,y2]=[[[o12,o13],[o11,o12]],[o11,o13]];
x = [[o12,o13],[o11,o12]] by A31,XTUPLE_0:1;
hence thesis by A26,XTUPLE_0:1;
end;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[x,y1] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o1,o2,o3 be Element of O such that
A32: o1 in o2 & o2 in o3 & [x,y1] = [[[o2,o3],[o1,o2]],[o1,o3]];
A33: x = [[o2,o3],[o1,o2]] & y1 = [o1,o3] by A32,XTUPLE_0:1;
assume
A34: [x,y2] in F;
per cases by A4,A34;
suppose ex o1 being Element of O st [x,y2] = [[o1,o1],o1];
then consider o11 be Element of O such that
A35: [x,y2] = [[o11,o11],o11];
x = [o11,o11] by A35,XTUPLE_0:1;
hence thesis by A33,XTUPLE_0:1;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([x,y2]=[[o2,[o1,o2]],[o1,o2]] or [x,y2]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A36: o11 in o12 & ([x,y2]=[[o12,[o11,o12]],[o11,o12]] or
[x,y2]=[[[o11,o12],o11],[o11,o12]]);
x = [o12,[o11,o12]] or x = [[o11,o12],o11] by A36,XTUPLE_0:1;
hence thesis by A33,XTUPLE_0:1;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[x,y2] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o11,o12,o13 be Element of O such that
A37: o11 in o12 & o12 in o13 & [x,y2]=[[[o12,o13],[o11,o12]],[o11,o13]];
x = [[o12,o13],[o11,o12]] & y2 = [o11,o13] by A37,XTUPLE_0:1;
then [o1,o2] = [o11,o12] & [o2,o3] = [o12,o13] by A33,XTUPLE_0:1;
then o1 = o11 & o2 = o12 & o3 = o13 by XTUPLE_0:1;
hence thesis by A32,XTUPLE_0:1,A37;
end;
end;
end;
A38: for o1,o2 being Element of O st o1 in o2 holds [o1,o2] in X
proof
let o1,o2 be Element of O;
assume o1 in o2;
then [o1,o2] in X1;
hence [o1,o2] in X by XBOOLE_0:def 3;
end;
for x being object st x in F holds x in [:[:X,X:],X:]
proof
let x be object;
assume
A39: x in F;
per cases by A39,A4;
suppose ex o1 being Element of O st x = [[o1,o1],o1];
then consider o1 be Element of O such that
A40: x = [[o1,o1],o1];
A41: o1 in X by A3,XBOOLE_0:def 3;
then [o1,o1] in [:X,X:] by ZFMISC_1:def 2;
hence thesis by A40,A41,ZFMISC_1:def 2;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
(x=[[o2,[o1,o2]],[o1,o2]] or x=[[[o1,o2],o1],[o1,o2]]);
then consider o1,o2 be Element of O such that
A42: o1 in o2 & (x=[[o2,[o1,o2]],[o1,o2]] or x=[[[o1,o2],o1],[o1,o2]]);
per cases by A42;
suppose
A43: x=[[o2,[o1,o2]],[o1,o2]];
A44: o2 in X & [o1,o2] in X by A42,A38,A3,XBOOLE_0:def 3;
then [o2,[o1,o2]] in [:X,X:] by ZFMISC_1:def 2;
hence thesis by A43,A44,ZFMISC_1:def 2;
end;
suppose
A45: x=[[[o1,o2],o1],[o1,o2]];
A46: o1 in X & [o1,o2] in X by A42,A38,A3,XBOOLE_0:def 3;
then [[o1,o2],o1] in [:X,X:] by ZFMISC_1:def 2;
hence thesis by A45,A46,ZFMISC_1:def 2;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o1,o2,o3 be Element of O such that
A47: o1 in o2 & o2 in o3 & x = [[[o2,o3],[o1,o2]],[o1,o3]];
A48: [o1,o2] in X & [o2,o3] in X & [o1,o3] in X by A47,A38,ORDINAL1:10;
then [[o2,o3],[o1,o2]] in [:X,X:] by ZFMISC_1:def 2;
hence thesis by A47,A48,ZFMISC_1:def 2;
end;
end;
then reconsider F as PartFunc of [:X,X:],X
by A12,TARSKI:def 3,FUNCT_1:def 1;
set C = CategoryStr(# X, F #);
reconsider C as strict non empty CategoryStr by A3;
A49: for f being morphism of C holds
(f is Element of O) or
(ex o1,o2 being Element of O st f = [o1,o2] & o1 in o2)
proof
let f be morphism of C;
f in Mor(C);
then
A50: f in the carrier of C by CAT_6:def 1;
per cases by A50,XBOOLE_0:def 3;
suppose f in O;
hence thesis;
end;
suppose f in X1;
then consider o1,o2 be Element of O such that
A51: f = [o1,o2] & o1 in o2;
thus thesis by A51;
end;
end;
A52: for o being Element of O holds o is morphism of C
proof
let o be Element of O;
o in X by A3,XBOOLE_0:def 3;
hence thesis by CAT_6:def 1;
end;
A53: for o1,o2 being Element of O st o1 in o2 holds
ex f being morphism of C st f = [o1,o2]
proof
let o1,o2 be Element of O;
assume o1 in o2;
then [o1,o2] in X by A38;
then reconsider f = [o1,o2] as morphism of C by CAT_6:def 1;
take f;
thus thesis;
end;
A54: for x being object st
(ex o1 being Element of O st x = [[o1,o1],o1]) or
(ex o1,o2 being Element of O st o1 in o2 &
(x=[[o2,[o1,o2]],[o1,o2]] or x=[[[o1,o2],o1],[o1,o2]])) or
(ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]]) holds x in F
proof
let x be object;
assume
A55: (ex o1 being Element of O st x = [[o1,o1],o1]) or
(ex o1,o2 being Element of O st o1 in o2 & (x=[[o2,[o1,o2]],[o1,o2]]
or x=[[[o1,o2],o1],[o1,o2]])) or
(ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]]);
per cases by A55;
suppose ex o1 being Element of O st x = [[o1,o1],o1];
then x in F1;
then x in F1 \/ F2 by XBOOLE_0:def 3;
then x in F1 \/ F2 \/ F3 by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
(x=[[o2,[o1,o2]],[o1,o2]] or x=[[[o1,o2],o1],[o1,o2]]);
then x in F2 or x in F3;
then x in F2 \/ F3 by XBOOLE_0:def 3;
then x in F1 \/ (F2 \/ F3) by XBOOLE_0:def 3;
then x in F1 \/ F2 \/ F3 by XBOOLE_1:4;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
x = [[[o2,o3],[o1,o2]],[o1,o3]];
then x in F4;
hence thesis by XBOOLE_0:def 3;
end;
end;
A56: for o1 being Element of O, f1,f2 being morphism of C
st f1 = o1 & f2 = o1 holds f1 |> f2 & f1(*)f2 = o1
proof
let o1 be Element of O;
let f1,f2 be morphism of C;
assume
A57: f1 = o1 & f2 = o1;
A58: [[f1,f2],f2] in F by A57,A54;
then
A59: [f1,f2] in dom the composition of C by XTUPLE_0:def 12;
hence f1 |> f2 by CAT_6:def 2;
thus f1(*)f2 = (the composition of C).(f1,f2) by A59,CAT_6:def 2,def 3
.= F.[f1,f2] by BINOP_1:def 1
.= o1 by A57,A58,FUNCT_1:1;
end;
A60: for o1,o2 being Element of O, f1,f2 being morphism of C
st f1 = o2 & f2 = [o1,o2] & o1 in o2
holds f1 |> f2 & f1(*)f2 = [o1,o2]
proof
let o1,o2 be Element of O;
let f1,f2 be morphism of C;
assume
A61: f1 = o2 & f2 = [o1,o2];
assume
A62: o1 in o2;
A63: [[f1,f2],f2] in F by A61,A62,A54;
then
A64: [f1,f2] in dom the composition of C by XTUPLE_0:def 12;
hence f1 |> f2 by CAT_6:def 2;
thus f1(*)f2 = (the composition of C).(f1,f2) by A64,CAT_6:def 2,def 3
.= F.[f1,f2] by BINOP_1:def 1
.= [o1,o2] by A61,A63,FUNCT_1:1;
end;
A65: for o1,o2 being Element of O, f1,f2 being morphism of C
st f1 = [o1,o2] & f2 = o1 & o1 in o2
holds f1 |> f2 & f1(*)f2 = [o1,o2]
proof
let o1,o2 be Element of O;
let f1,f2 be morphism of C;
assume
A66: f1 = [o1,o2] & f2 = o1;
assume
A67: o1 in o2;
A68: [[f1,f2],f1] in F by A66,A67,A54;
then
A69: [f1,f2] in dom the composition of C by XTUPLE_0:def 12;
hence f1 |> f2 by CAT_6:def 2;
thus f1(*)f2 = (the composition of C).(f1,f2) by A69,CAT_6:def 2,def 3
.= F.[f1,f2] by BINOP_1:def 1
.= [o1,o2] by A66,A68,FUNCT_1:1;
end;
A70: for o1,o2,o3 being Element of O, f1,f2 being morphism of C
st f1 = [o2,o3] & f2 = [o1,o2] & o1 in o2 & o2 in o3
holds f1 |> f2 & f1(*)f2 = [o1,o3]
proof
let o1,o2,o3 be Element of O;
let f1,f2 be morphism of C;
assume
A71: f1 = [o2,o3] & f2 = [o1,o2];
assume
A72: o1 in o2 & o2 in o3;
then consider f3 be morphism of C such that
A73: f3 = [o1,o3] by A53,ORDINAL1:10;
A74: [[f1,f2],f3] in F by A71,A72,A73,A54;
then
A75: [f1,f2] in dom the composition of C by XTUPLE_0:def 12;
hence f1 |> f2 by CAT_6:def 2;
thus f1(*)f2 = (the composition of C).(f1,f2) by A75,CAT_6:def 2,def 3
.= F.[f1,f2] by BINOP_1:def 1
.= [o1,o3] by A73,A74,FUNCT_1:1;
end;
A76: for o1,o2 being Element of O, f1,f2 being morphism of C
st f1 = o1 & f2 = o2 & f1 |> f2 holds o1 = o2
proof
let o1,o2 be Element of O;
let f1,f2 be morphism of C;
assume
A77: f1 = o1 & f2 = o2;
assume f1 |> f2;
then [f1,f2] in dom the composition of C by CAT_6:def 2;
then consider y be object such that
A78: [[f1,f2],y] in F by XTUPLE_0:def 12;
per cases by A78,A4;
suppose ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1];
then consider o11 be Element of O such that
A79: [[f1,f2],y] = [[o11,o11],o11];
[f1,f2] = [o11,o11] by A79,XTUPLE_0:1;
then f1 = o11 & f2 = o11 by XTUPLE_0:1;
hence thesis by A77;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([[f1,f2],y]=[[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A80: o11 in o12 & ([[f1,f2],y]=[[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y]=[[[o11,o12],o11],[o11,o12]]);
[f1,f2] = [o12,[o11,o12]] or [f1,f2] = [[o11,o12],o11]
by A80,XTUPLE_0:1;
hence thesis by A77,XTUPLE_0:1;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o1,o2,o3 be Element of O such that
A81: o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
[f1,f2] = [[o2,o3],[o1,o2]] by A81,XTUPLE_0:1;
hence thesis by A77,XTUPLE_0:1;
end;
end;
A82: for o1,o2,o3 being Element of O, f1,f2 being morphism of C
st f1 = o1 & f2 = [o2,o3] & f1 |> f2 holds o1 = o3
proof
let o1,o2,o3 be Element of O;
let f1,f2 be morphism of C;
assume
A83: f1 = o1 & f2 = [o2,o3];
assume f1 |> f2;
then [f1,f2] in dom the composition of C by CAT_6:def 2;
then consider y be object such that
A84: [[f1,f2],y] in F by XTUPLE_0:def 12;
per cases by A84,A4;
suppose ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1];
then consider o11 be Element of O such that
A85: [[f1,f2],y] = [[o11,o11],o11];
[f1,f2] = [o11,o11] by A85,XTUPLE_0:1;
hence thesis by A83,XTUPLE_0:1;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([[f1,f2],y]=[[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A86: o11 in o12 & ([[f1,f2],y]=[[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y]=[[[o11,o12],o11],[o11,o12]]);
per cases by A86,XTUPLE_0:1;
suppose [f1,f2] = [o12,[o11,o12]];
then f1 = o12 & f2 = [o11,o12] by XTUPLE_0:1;
hence thesis by A83,XTUPLE_0:1;
end;
suppose [f1,f2] = [[o11,o12],o11];
hence thesis by A83,XTUPLE_0:1;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o1,o2,o3 be Element of O such that
A87: o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
[f1,f2] = [[o2,o3],[o1,o2]] by A87,XTUPLE_0:1;
hence thesis by A83,XTUPLE_0:1;
end;
end;
A88: for o1,o2,o3 being Element of O, f1,f2 being morphism of C
st f1 = [o1,o2] & f2 = o3 & f1 |> f2 holds o1 = o3
proof
let o1,o2,o3 be Element of O;
let f1,f2 be morphism of C;
assume
A89: f1 = [o1,o2] & f2 = o3;
assume f1 |> f2;
then [f1,f2] in dom the composition of C by CAT_6:def 2;
then consider y be object such that
A90: [[f1,f2],y] in F by XTUPLE_0:def 12;
per cases by A90,A4;
suppose ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1];
then consider o11 be Element of O such that
A91: [[f1,f2],y] = [[o11,o11],o11];
[f1,f2] = [o11,o11] by A91,XTUPLE_0:1;
hence thesis by A89,XTUPLE_0:1;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([[f1,f2],y]=[[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A92: o11 in o12 & ([[f1,f2],y]=[[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y]=[[[o11,o12],o11],[o11,o12]]);
per cases by A92,XTUPLE_0:1;
suppose [f1,f2] = [o12,[o11,o12]];
hence thesis by A89,XTUPLE_0:1;
end;
suppose [f1,f2] = [[o11,o12],o11];
then f1 = [o11,o12] & f2 = o11 by XTUPLE_0:1;
hence thesis by A89,XTUPLE_0:1;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o1,o2,o3 be Element of O such that
A93: o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
[f1,f2] = [[o2,o3],[o1,o2]] by A93,XTUPLE_0:1;
hence thesis by A89,XTUPLE_0:1;
end;
end;
A94: for o being Element of O, f being morphism of C
st f = o holds f is identity
proof
let o be Element of O;
let f be morphism of C;
assume
A95: f = o;
for f1 being morphism of C st f |> f1 holds f (*) f1 = f1
proof
let f1 be morphism of C;
per cases by A49;
suppose
A96: f1 is Element of O;
assume f |> f1;
then f = f1 by A95,A96,A76;
hence thesis by A96,A56;
end;
suppose ex o1,o2 being Element of O st f1 = [o1,o2] & o1 in o2;
then consider o1,o2 be Element of O such that
A97: f1 = [o1,o2] & o1 in o2;
assume f |> f1;
then o2 = o by A95,A97,A82;
hence thesis by A95,A97,A60;
end;
end;
then
A98: f is left_identity by CAT_6:def 4;
for f1 being morphism of C st f1 |> f holds f1 (*) f = f1
proof
let f1 be morphism of C;
per cases by A49;
suppose
A99: f1 is Element of O;
assume f1 |> f;
then f = f1 by A95,A99,A76;
hence thesis by A99,A56;
end;
suppose ex o1,o2 being Element of O st f1 = [o1,o2] & o1 in o2;
then consider o1,o2 be Element of O such that
A100: f1 = [o1,o2] & o1 in o2;
assume f1 |> f;
then o1 = o by A95,A100,A88;
hence thesis by A95,A100,A65;
end;
end;
hence f is identity by A98,CAT_6:def 5,def 14;
end;
for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st f |> f1 & f is left_identity
proof
let f1 be morphism of C;
assume f1 in the carrier of C;
per cases by A49;
suppose
A101: f1 is Element of O;
take f1;
thus f1 |> f1 by A56,A101;
f1 is identity by A101,A94;
hence f1 is left_identity by CAT_6:def 14;
thus thesis;
end;
suppose ex o1,o2 being Element of O st f1 = [o1,o2] & o1 in o2;
then consider o11,o12 be Element of O such that
A102: f1 = [o11,o12] & o11 in o12;
reconsider f = o12 as morphism of C by A52;
take f;
thus f |> f1 by A60,A102;
f is identity by A94;
hence f is left_identity by CAT_6:def 14;
end;
end;
then
A103: C is with_left_identities by CAT_6:def 6;
A104: for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st f1 |> f & f is right_identity
proof
let f1 be morphism of C;
assume f1 in the carrier of C;
per cases by A49;
suppose
A105: f1 is Element of O;
take f1;
thus f1 |> f1 by A56,A105;
f1 is identity by A105,A94;
hence f1 is right_identity by CAT_6:def 14;
thus thesis;
end;
suppose ex o1,o2 being Element of O st f1 = [o1,o2] & o1 in o2;
then consider o11,o12 be Element of O such that
A106: f1 = [o11,o12] & o11 in o12;
reconsider f = o11 as morphism of C by A52;
take f;
thus f1 |> f by A65,A106;
f is identity by A94;
hence f is right_identity by CAT_6:def 14;
end;
end;
A107: for f1,f2 being morphism of C st f1 |> f2 holds
(ex o1 being Element of O st f1 = o1 & f2 = o1) or
(ex o1,o2 being Element of O st o1 in o2 & ((f1 = [o1,o2] & f2 = o1) or
(f1 = o2 & f2 = [o1,o2]))) or
(ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 & f1 = [o2,o3] &
f2 = [o1,o2])
proof
let f1,f2 be morphism of C;
assume f1 |> f2;
then [f1,f2] in dom the composition of C by CAT_6:def 2;
then consider y be object such that
A108: [[f1,f2],y] in F by XTUPLE_0:def 12;
per cases by A108,A4;
suppose ex o1 being Element of O st [[f1,f2],y] = [[o1,o1],o1];
then consider o11 be Element of O such that
A109: [[f1,f2],y] = [[o11,o11],o11];
[f1,f2] = [o11,o11] by A109,XTUPLE_0:1;
then f1 = o11 & f2 = o11 by XTUPLE_0:1;
hence thesis;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
([[f1,f2],y]=[[o2,[o1,o2]],[o1,o2]] or
[[f1,f2],y]=[[[o1,o2],o1],[o1,o2]]);
then consider o11,o12 be Element of O such that
A110: o11 in o12 & ([[f1,f2],y]=[[o12,[o11,o12]],[o11,o12]] or
[[f1,f2],y]=[[[o11,o12],o11],[o11,o12]]);
per cases by A110,XTUPLE_0:1;
suppose [f1,f2] = [o12,[o11,o12]];
then f1 = o12 & f2 = [o11,o12] by XTUPLE_0:1;
hence thesis by A110;
end;
suppose [f1,f2] = [[o11,o12],o11];
then f1 = [o11,o12] & f2 = o11 by XTUPLE_0:1;
hence thesis by A110;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
[[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
then consider o1,o2,o3 be Element of O such that
A111: o1 in o2 & o2 in o3 & [[f1,f2],y] = [[[o2,o3],[o1,o2]],[o1,o3]];
[f1,f2] = [[o2,o3],[o1,o2]] by A111,XTUPLE_0:1;
then f1 = [o2,o3] & f2 = [o1,o2] by XTUPLE_0:1;
hence thesis by A111;
end;
end;
for f,f1,f2 being morphism of C st f1 |> f2 holds
f1(*)f2 |> f iff f2 |> f
proof
let f,f1,f2 be morphism of C;
assume
A112: f1 |> f2;
per cases by A112,A107;
suppose ex o1 being Element of O st f1 = o1 & f2 = o1;
then consider o1 be Element of O such that
A113: f1 = o1 & f2 = o1;
A114: f1(*)f2 = o1 by A113,A56;
hereby
assume
A115: f1(*)f2 |> f;
per cases by A115,A107;
suppose ex o1 being Element of O st f1(*)f2 = o1 & f = o1;
then consider o11 be Element of O such that
A116: f1(*)f2 = o11 & f = o11;
thus f2 |> f by A113,A116,A114,A56;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f1(*)f2 = [o1,o2] & f = o1) or (f1(*)f2 = o2 & f = [o1,o2]));
then consider o11,o12 be Element of O such that
A117: o11 in o12 & ((f1(*)f2 = [o11,o12] & f = o11) or
(f1(*)f2 = o12 & f = [o11,o12]));
thus f2 |> f by A113,A114,A117,A60;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f1(*)f2 = [o2,o3] & f = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A118: o11 in o12 & o12 in o13 & f1(*)f2 = [o12,o13] & f = [o11,o12];
thus f2 |> f by A118,A113,A56;
end;
end;
assume
A119: f2 |> f;
per cases by A119,A107;
suppose ex o1 being Element of O st f2 = o1 & f = o1;
then consider o11 be Element of O such that
A120: f2 = o11 & f = o11;
thus f1(*)f2 |> f by A113,A120,A114,A56;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f2 = [o1,o2] & f = o1) or (f2 = o2 & f = [o1,o2]));
then consider o11,o12 be Element of O such that
A121: o11 in o12 & ((f2 = [o11,o12] & f = o11) or
(f2 = o12 & f = [o11,o12]));
f1(*)f2 = o12 by A113,A121,A56;
hence f1(*)f2 |> f by A121,A113,A60;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f2 = [o2,o3] & f = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A122: o11 in o12 & o12 in o13 & f2 = [o12,o13] & f = [o11,o12];
thus f1(*)f2 |> f by A113,A122;
end;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f1 = [o1,o2] & f2 = o1) or (f1 = o2 & f2 = [o1,o2]));
then consider o1,o2 being Element of O such that
A123: o1 in o2 &
((f1 = [o1,o2] & f2 = o1) or (f1 = o2 & f2 = [o1,o2]));
A124: f1(*)f2 = [o1,o2] by A123,A60,A65;
hereby
assume
A125: f1(*)f2 |> f;
per cases by A125,A107;
suppose ex o1 being Element of O st f1(*)f2 = o1 & f = o1;
then consider o11 be Element of O such that
A126: f1(*)f2 = o11 & f = o11;
thus f2 |> f by A126,A123,A60,A65;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f1(*)f2 = [o1,o2] & f = o1) or (f1(*)f2 = o2 & f = [o1,o2]));
then consider o11,o12 be Element of O such that
A127: o11 in o12 & ((f1(*)f2 = [o11,o12] & f = o11) or
(f1(*)f2 = o12 & f = [o11,o12]));
o1 = o11 & o2 = o12 by A124,XTUPLE_0:1,A127;
hence f2 |> f by A127,A123,A60,A65,A56;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f1(*)f2 = [o2,o3] & f = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A128: o11 in o12 & o12 in o13 & f1(*)f2 = [o12,o13] & f = [o11,o12];
A129: o1 = o12 & o2 = o13 by A124,A128,XTUPLE_0:1;
per cases by A123;
suppose f1 = [o1,o2] & f2 = o1;
hence f2 |> f by A129,A128,A60;
end;
suppose f1 = o2 & f2 = [o1,o2];
hence f2 |> f by A128,A124,A70;
end;
end;
end;
assume
A130: f2 |> f;
per cases by A130,A107;
suppose ex o1 being Element of O st f2 = o1 & f = o1;
then consider o11 be Element of O such that
A131: f2 = o11 & f = o11;
thus f1(*)f2 |> f by A123,A131,A124,A65;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f2 = [o1,o2] & f = o1) or (f2 = o2 & f = [o1,o2]));
then consider o11,o12 be Element of O such that
A132: o11 in o12 & ((f2 = [o11,o12] & f = o11) or
(f2 = o12 & f = [o11,o12]));
per cases by A132;
suppose f2 = [o11,o12] & f = o11;
hence f1(*)f2 |> f by A124,A132,A123,A65;
end;
suppose
A133: f2 = o12 & f = [o11,o12];
thus f1(*)f2 |> f by A133,A124,A132,A123,A70;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f2 = [o2,o3] & f = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A134: o11 in o12 & o12 in o13 & f2 = [o12,o13] & f = [o11,o12];
thus f1(*)f2 |> f by A123,A134,A124,A70;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f1 = [o2,o3] & f2 = [o1,o2];
then consider o1,o2,o3 be Element of O such that
A135: o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2];
A136: f1(*)f2 = [o1,o3] by A135,A70;
hereby
assume
A137: f1(*)f2 |> f;
per cases by A137,A107;
suppose ex o1 being Element of O st f1(*)f2 = o1 & f = o1;
then consider o11 be Element of O such that
A138: f1(*)f2 = o11 & f = o11;
thus f2 |> f by A138,A136;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f1(*)f2 = [o1,o2] & f = o1) or (f1(*)f2 = o2 & f = [o1,o2]));
then consider o11,o12 be Element of O such that
A139: o11 in o12 & ((f1(*)f2 = [o11,o12] & f = o11) or
(f1(*)f2 = o12 & f = [o11,o12]));
o1 = o11 & o3 = o12 by A139,A136,XTUPLE_0:1;
hence f2 |> f by A139,A70,A135,A65;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f1(*)f2 = [o2,o3] & f = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A140: o11 in o12 & o12 in o13 & f1(*)f2 = [o12,o13] & f = [o11,o12];
o1 = o12 & o3 = o13 by A136,A140,XTUPLE_0:1;
hence f2 |> f by A140,A135,A70;
end;
end;
assume
A141: f2 |> f;
per cases by A141,A107;
suppose ex o1 being Element of O st f2 = o1 & f = o1;
then consider o11 be Element of O such that
A142: f2 = o11 & f = o11;
thus f1(*)f2 |> f by A135,A142;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f2 = [o1,o2] & f = o1) or (f2 = o2 & f = [o1,o2]));
then consider o11,o12 be Element of O such that
A143: o11 in o12 & ((f2 = [o11,o12] & f = o11) or
(f2 = o12 & f = [o11,o12]));
per cases by A143;
suppose f2 = [o11,o12] & f = o11;
then
A144: o1 = o11 & o12 = o2 by A135,XTUPLE_0:1;
o1 in o3 by A135,ORDINAL1:10;
hence f1(*)f2 |> f by A144,A136,A143,A135,A65;
end;
suppose
A145: f2 = o12 & f = [o11,o12];
thus f1(*)f2 |> f by A145,A135;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f2 = [o2,o3] & f = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A146: o11 in o12 & o12 in o13 & f2 = [o12,o13] & f = [o11,o12];
A147: o1 = o12 & o2 = o13 by A135,A146,XTUPLE_0:1;
o1 in o3 by A135,ORDINAL1:10;
hence f1(*)f2 |> f by A146,A147,A136,A70;
end;
end;
end;
then
A148: C is left_composable by CAT_6:def 8;
A149: for f,f1,f2 being morphism of C st f1 |> f2 holds
f |> f1(*)f2 iff f |> f1
proof
let f,f1,f2 be morphism of C;
assume
A150: f1 |> f2;
per cases by A150,A107;
suppose ex o1 being Element of O st f1 = o1 & f2 = o1;
then consider o1 be Element of O such that
A151: f1 = o1 & f2 = o1;
A152: f1(*)f2 = o1 by A151,A56;
hereby
assume
A153: f |> f1(*)f2;
per cases by A153,A107;
suppose ex o1 being Element of O st f = o1 & f1(*)f2 = o1;
then consider o11 be Element of O such that
A154: f = o11 & f1(*)f2 = o11;
thus f |> f1 by A151,A154,A152,A56;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f = [o1,o2] & f1(*)f2 = o1) or (f = o2 & f1(*)f2 = [o1,o2]));
then consider o11,o12 be Element of O such that
A155: o11 in o12 & ((f = [o11,o12] & f1(*)f2 = o11) or
(f = o12 & f1(*)f2 = [o11,o12]));
thus f |> f1 by A152,A155,A151,A65;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f = [o2,o3] & f1(*)f2 = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A156: o11 in o12 & o12 in o13 & f = [o12,o13] & f1(*)f2 = [o11,o12];
thus f |> f1 by A156,A151,A56;
end;
end;
assume
A157: f |> f1;
per cases by A157,A107;
suppose ex o1 being Element of O st f = o1 & f1 = o1;
then consider o11 be Element of O such that
A158: f = o11 & f1 = o11;
thus f |> f1(*)f2 by A151,A158,A152,A56;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f = [o1,o2] & f1 = o1) or (f = o2 & f1 = [o1,o2]));
then consider o11,o12 be Element of O such that
A159: o11 in o12 & ((f = [o11,o12] & f1 = o11) or
(f = o12 & f1 = [o11,o12]));
thus f |> f1(*)f2 by A159,A151,A152,A65;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f = [o2,o3] & f1 = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A160: o11 in o12 & o12 in o13 & f = [o12,o13] & f1 = [o11,o12];
thus f |> f1(*)f2 by A151,A160;
end;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f1 = [o1,o2] & f2 = o1) or (f1 = o2 & f2 = [o1,o2]));
then consider o1,o2 being Element of O such that
A161: o1 in o2 &
((f1 = [o1,o2] & f2 = o1) or (f1 = o2 & f2 = [o1,o2]));
A162: f1(*)f2 = [o1,o2] by A161,A60,A65;
hereby
assume
A163: f |> f1(*)f2;
per cases by A163,A107;
suppose ex o1 being Element of O st f = o1 & f1(*)f2 = o1;
then consider o11 be Element of O such that
A164: f = o11 & f1(*)f2 = o11;
thus f |> f1 by A164,A161,A60,A65;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f = [o1,o2] & f1(*)f2 = o1) or (f = o2 & f1(*)f2 = [o1,o2]));
then consider o11,o12 be Element of O such that
A165: o11 in o12 & ((f = [o11,o12] & f1(*)f2 = o11) or
(f = o12 & f1(*)f2 = [o11,o12]));
o1 = o11 & o2 = o12 by A162,XTUPLE_0:1,A165;
hence f |> f1 by A165,A161,A60,A56,A65;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f = [o2,o3] & f1(*)f2 = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A166: o11 in o12 & o12 in o13 & f = [o12,o13] & f1(*)f2 = [o11,o12];
A167: o1 = o11 & o2 = o12 by A162,A166,XTUPLE_0:1;
per cases by A161;
suppose f1 = [o1,o2] & f2 = o1;
hence f |> f1 by A166,A162,A70;
end;
suppose f1 = o2 & f2 = [o1,o2];
hence f |> f1 by A167,A166,A65;
end;
end;
end;
assume
A168: f |> f1;
per cases by A168,A107;
suppose ex o1 being Element of O st f = o1 & f1 = o1;
then consider o11 be Element of O such that
A169: f = o11 & f1 = o11;
thus f |> f1(*)f2 by A161,A169,A162,A60;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f = [o1,o2] & f1 = o1) or (f = o2 & f1 = [o1,o2]));
then consider o11,o12 be Element of O such that
A170: o11 in o12 & ((f = [o11,o12] & f1 = o11) or
(f = o12 & f1 = [o11,o12]));
per cases by A170;
suppose
A171: f = [o11,o12] & f1 = o11;
thus f |> f1(*)f2 by A171,A162,A170,A161,A70;
end;
suppose
A172: f = o12 & f1 = [o11,o12];
thus f |> f1(*)f2 by A162,A172,A170,A161,A60;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f = [o2,o3] & f1 = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A173: o11 in o12 & o12 in o13 & f = [o12,o13] & f1 = [o11,o12];
thus f |> f1(*)f2 by A161,A173,A162,A70;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f1 = [o2,o3] & f2 = [o1,o2];
then consider o1,o2,o3 be Element of O such that
A174: o1 in o2 & o2 in o3 & f1 = [o2,o3] & f2 = [o1,o2];
A175: f1(*)f2 = [o1,o3] by A174,A70;
hereby
assume
A176: f |> f1(*)f2;
per cases by A176,A107;
suppose ex o1 being Element of O st f = o1 & f1(*)f2 = o1;
then consider o11 be Element of O such that
A177: f = o11 & f1(*)f2 = o11;
thus f |> f1 by A177,A175;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f = [o1,o2] & f1(*)f2 = o1) or (f = o2 & f1(*)f2 = [o1,o2]));
then consider o11,o12 be Element of O such that
A178: o11 in o12 & ((f = [o11,o12] & f1(*)f2 = o11) or
(f = o12 & f1(*)f2 = [o11,o12]));
o1 = o11 & o3 = o12 by A178,A175,XTUPLE_0:1;
hence f |> f1 by A178,A174,A70,A60;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f = [o2,o3] & f1(*)f2 = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A179: o11 in o12 & o12 in o13 & f = [o12,o13] & f1(*)f2 = [o11,o12];
o1 = o11 & o3 = o12 by A175,A179,XTUPLE_0:1;
hence f |> f1 by A179,A174,A70;
end;
end;
assume
A180: f |> f1;
per cases by A180,A107;
suppose ex o1 being Element of O st f = o1 & f1 = o1;
then consider o11 be Element of O such that
A181: f = o11 & f1 = o11;
thus f |> f1(*)f2 by A174,A181;
end;
suppose ex o1,o2 being Element of O st o1 in o2 &
((f = [o1,o2] & f1 = o1) or (f = o2 & f1 = [o1,o2]));
then consider o11,o12 be Element of O such that
A182: o11 in o12 & ((f = [o11,o12] & f1 = o11) or
(f = o12 & f1 = [o11,o12]));
per cases by A182;
suppose
A183: f = [o11,o12] & f1 = o11;
thus f |> f1(*)f2 by A183,A174;
end;
suppose f = o12 & f1 = [o11,o12];
then
A184: o2 = o11 & o12 = o3 by A174,XTUPLE_0:1;
o1 in o3 by A174,ORDINAL1:10;
hence f |> f1(*)f2 by A184,A175,A182,A174,A60;
end;
end;
suppose ex o1,o2,o3 being Element of O st o1 in o2 & o2 in o3 &
f = [o2,o3] & f1 = [o1,o2];
then consider o11,o12,o13 be Element of O such that
A185: o11 in o12 & o12 in o13 & f = [o12,o13] & f1 = [o11,o12];
A186: o2 = o11 & o3 = o12 by A174,A185,XTUPLE_0:1;
o1 in o3 by A174,ORDINAL1:10;
hence f |> f1(*)f2 by A185,A186,A175,A70;
end;
end;
end;
reconsider C as strict non empty composable with_identities
CategoryStr by A104,A103,CAT_6:def 7,def 12,
A149,A148,CAT_6:def 9,def 11;
A187: for x being object holds x in Ob C iff x in O
proof
let x be object;
hereby
assume
A188: x in Ob C;
reconsider f = x as morphism of C by A188;
x in Mor C by A188;
then
A189: f in X by CAT_6:def 1;
per cases by A189,XBOOLE_0:def 3;
suppose f in O;
hence x in O;
end;
suppose f in X1;
then consider o1,o2 be Element of O such that
A190: f = [o1,o2] & o1 in o2;
reconsider f1 = o1, f2 = o2 as morphism of C by A52;
A191: f2 is identity by A94;
A192: cod f = o2 by A190,A60,A191,CAT_6:27;
f is identity by A188,CAT_6:22;
hence x in O by A192,A190,Th6;
end;
end;
assume
A193: x in O;
then reconsider o = x as Element of O;
o in X by A193,XBOOLE_0:def 3;
then reconsider f = o as morphism of C by CAT_6:def 1;
f is Object of C by A94,CAT_6:22;
hence x in Ob C;
end;
then
A194: Ob C = O by TARSKI:2;
A195: for o1,o2 being Object of C, f being morphism of C st
f in Hom(o1,o2) holds (f = o1 & o1 = o2) or (f = [o1,o2] & o1 in o2)
proof
let o1,o2 be Object of C;
let f be morphism of C;
assume f in Hom(o1,o2);
then
A196: dom f = o1 & cod f = o2 by Th20;
assume
A197: not (f = o1 & o1 = o2);
per cases by A49;
suppose f is Element of O;
then f is identity by A194,CAT_6:22;
then o1 = f & o2 = f by A196,Th6;
hence thesis by A197;
end;
suppose ex o1,o2 being Element of O st f = [o1,o2] & o1 in o2;
then consider o11,o22 be Element of O such that
A198: f = [o11,o22] & o11 in o22;
A199: o11 in Ob C & o22 in Ob C by A194;
reconsider f1 = o11, f2 = o22 as morphism of C by A199;
f1 is identity by A94;
then
A200: dom f = o11 by A198,A65,CAT_6:26;
f2 is identity by A94;
hence thesis by A198,A200,A196,A60,CAT_6:27;
end;
end;
A201: for o1,o2 being Object of C, f1,f2 being morphism of C st
f1 in Hom(o1,o2) & f2 in Hom(o1,o2) holds f1 = f2
proof
let o1,o2 be Object of C;
let f1,f2 be morphism of C;
assume A202: f1 in Hom(o1,o2);
assume A203: f2 in Hom(o1,o2);
per cases by A202,A195;
suppose
A204: f1 = o1 & o1 = o2;
per cases by A203,A195;
suppose f2 = o1 & o1 = o2;
hence thesis by A204;
end;
suppose f2 = [o1,o2] & o1 in o2;
hence thesis by A204;
end;
end;
suppose
A205: f1 = [o1,o2] & o1 in o2;
per cases by A203,A195;
suppose f2 = o1 & o1 = o2;
hence thesis by A205;
end;
suppose f2 = [o1,o2] & o1 in o2;
hence thesis by A205;
end;
end;
end;
then C is preorder;
then reconsider C as strict preorder category;
take C;
thus
A206: Ob C = O by A187,TARSKI:2;
thus
A207: for o1,o2 being Object of C st o1 in o2 holds Hom(o1,o2) = {[o1,o2]}
proof
let o1,o2 be Object of C;
A208: o1 in Ob C & o2 in Ob C by SUBSET_1:def 1;
assume
A209: o1 in o2;
reconsider o11=o1, o22=o2 as Element of O by A187;
consider f be morphism of C such that
A210: f = [o11,o22] by A209,A53;
reconsider f1 = o1, f2 = o2 as morphism of C by A208;
A211: f1 is identity by A94,A206;
A212: dom f = o1 by A210,A209,A65,A211,CAT_6:26;
A213: f2 is identity by A94,A206;
cod f = o2 by A210,A209,A60,A213,CAT_6:27;
then f in {ff where ff is morphism of C: dom ff = o1 & cod ff = o2}
by A212;
then
A214: f in Hom(o1,o2) by Def2;
for x being object holds x in Hom(o1,o2) iff x = [o1,o2]
by A210,A214,A201;
hence Hom(o1,o2) = {[o1,o2]} by TARSKI:def 1;
end;
for a,b being object holds [a,b] in RelOb C iff [a,b] in RelIncl O
proof
let a,b be object;
hereby
assume [a,b] in RelOb C;
then consider o1,o2 be Object of C such that
A215: [a,b] = [o1,o2] & ex f being morphism of C st f in Hom(o1,o2);
consider f be morphism of C such that
A216: f in Hom(o1,o2) by A215;
A217: dom f = o1 & cod f = o2 by A216,Th20;
A218: o1 c= o2
proof
per cases by A49;
suppose f is Element of O;
then f is identity by A94;
then dom f = f & cod f = f by Th6;
hence thesis by A217;
end;
suppose ex o1,o2 being Element of O st f = [o1,o2] & o1 in o2;
then consider o11,o22 be Element of O such that
A219: f = [o11,o22] & o11 in o22;
o11 in O & o22 in O by A3;
then reconsider f1 = o11, f2 = o22 as morphism of C by A206;
A220: f1 is identity by A94;
A221: f2 is identity by A94;
o1 = o11 & o2 = o22
by A219,A65,A220,CAT_6:26,A217,A60,A221,CAT_6:27;
hence thesis by A219,ORDINAL1:def 2;
end;
end;
thus [a,b] in RelIncl O by A206,A215,A218,WELLORD2:def 1;
end;
assume
A222: [a,b] in RelIncl O;
then
A223: a in field RelIncl O & b in field RelIncl O by RELAT_1:15;
then
A224: a in O & b in O by WELLORD2:def 1;
reconsider o1 = a, o2 = b as Object of C by A223,A206,WELLORD2:def 1;
A225: o1 c= o2 by A222,A224,WELLORD2:def 1;
ex f being morphism of C st f in Hom(o1,o2)
proof
per cases by A224,ORDINAL1:def 3;
suppose
A226: o1 in o2;
reconsider o11=o1, o22=o2 as Element of O by A223,WELLORD2:def 1;
consider f be morphism of C such that
A227: f = [o11,o22] by A226,A53;
f in {[o1,o2]} by A227,TARSKI:def 1;
then f in Hom(o1,o2) by A226,A207;
hence thesis;
end;
suppose o1 = o2 or o2 in o1;
then o1 = o2 or o2 c= o1 by A224,ORDINAL1:def 2;
then
A228: o1 = o2 by A225,XBOOLE_0:def 10;
o1 in Hom(o1,o1) by Th21;
hence thesis by A228;
end;
end;
hence [a,b] in RelOb C;
end;
hence RelOb C = RelIncl O by RELAT_1:def 2;
thus thesis by CAT_6:def 1;
end;
end;
definition
let O be ordinal number;
let C be composable with_identities CategoryStr;
attr C is O -ordered means :Def14:
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;
correctness
proof
let C be composable with_identities CategoryStr;
assume
A1: C is O -ordered;
assume
A2: C is empty;
consider F be Function such that
A3: F is_isomorphism_of RelOb C, RelIncl O by A1,WELLORD1:def 8;
dom F = field RelOb C by A3,WELLORD1:def 7
.= dom RelOb C \/ rng RelOb C by RELAT_1:def 6
.= {} by A2;
then
A4: F = {};
field RelIncl O = rng F by A3,WELLORD1:def 7;
then dom RelIncl O \/ rng RelIncl O = {} by A4,RELAT_1:def 6;
hence contradiction;
end;
end;
registration
let O be ordinal number;
cluster strict O -ordered preorder
for composable with_identities CategoryStr;
correctness
proof
consider C be strict preorder category such that
A1: 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} by Th37;
take C;
thus thesis by A1,WELLORD1:38;
end;
end;
registration
let O be empty ordinal number;
cluster O -ordered -> empty for composable with_identities CategoryStr;
correctness
proof
let C be composable with_identities CategoryStr;
assume C is O -ordered;
then consider F be Function such that
A1: F is_isomorphism_of RelOb C, RelIncl O by WELLORD1:def 8;
rng F = field RelIncl O by A1,WELLORD1:def 7
.= dom RelIncl O \/ rng RelIncl O by RELAT_1:def 6
.= {} \/ rng RelIncl O
.= {};
then
A2: F = {};
field RelOb C = dom F by A1,WELLORD1:def 7;
then dom RelOb C \/ rng RelOb C = {} by A2,RELAT_1:def 6;
hence thesis;
end;
end;
theorem Th38:
for O1,O2 being ordinal number, C1 being O1 -ordered preorder category,
C2 being O2 -ordered preorder category holds O1 = O2 iff C1 ~= C2
proof
let O1,O2 be ordinal number;
let C1 be O1 -ordered preorder category;
let C2 be O2 -ordered preorder category;
thus O1 = O2 implies C1 ~= C2
proof
assume
A1: O1 = O2;
per cases;
suppose O1 is empty;
hence thesis by A1,Th13;
end;
suppose
A2: O1 is non empty;
then reconsider D1 = C1, D2 = C2 as non empty category by A1;
consider F1 be Function such that
A3: F1 is_isomorphism_of RelOb(C1), RelIncl(O1) by Def14,WELLORD1:def 8;
consider F2 be Function such that
A4: F2 is_isomorphism_of RelOb(C2), RelIncl(O2) by Def14,WELLORD1:def 8;
A5: F2" is_isomorphism_of RelIncl(O2), RelOb(C2) by A4,WELLORD1:39;
set F3 = (F2") * F1;
A6: F3 is_isomorphism_of RelOb(C1), RelOb(C2) by A1,A3,A5,WELLORD1:41;
consider F4 be Function of C1, RelOb(C1) such that
A7: F4 is bijective &
for f being morphism of C1 holds F4.f = [dom f,cod f] by A2,Th36;
consider F5 be Function of C2, RelOb(C2) such that
A8: F5 is bijective &
for f being morphism of C2 holds F5.f = [dom f,cod f] by A1,A2,Th36;
A9: dom F3 = field RelOb(C1) & rng F3 = field RelOb(C2) &
F3 is one-to-one &
for a,b being set holds [a,b] in RelOb(C1) iff (a in field RelOb(C1) &
b in field RelOb(C1) & [F3.a, F3.b] in RelOb(C2)) by A6,WELLORD1:def 7;
A10: field RelOb(C1) = dom RelOb(C1) \/ rng RelOb(C1) by RELAT_1:def 6
.= dom RelOb(C1) \/ Ob C1 by Th34
.= Ob(C1) \/ Ob C1 by Th34
.= Ob C1;
defpred P[object,object] means for a,b being set st $1 = [a,b] holds
$2 = [F3.a, F3.b];
A11: for x being Element of RelOb(D1)
ex y being Element of RelOb(D2) st P[x,y]
proof
let x be Element of RelOb(D1);
x in RelOb(D1);
then consider o1,o2 be Object of D1 such that
A12: x = [o1,o2] & ex f being morphism of D1 st f in Hom(o1,o2);
reconsider y = [F3.o1,F3.o2] as Element of RelOb(D2)
by A12,A6,WELLORD1:def 7;
take y;
for a,b being set st x = [a,b] holds y = [F3.a, F3.b]
proof
let a,b be set;
assume x = [a,b];
then a = o1 & b = o2 by A12,XTUPLE_0:1;
hence y = [F3.a, F3.b];
end;
hence P[x,y];
end;
consider F33 be Function of RelOb(D1), RelOb(D2) such that
A13: for x being Element of RelOb(D1) holds P[x,F33.x]
from FUNCT_2:sch 3(A11);
A14: rng F5 = dom(F5") & dom F5 = rng(F5") by A8,FUNCT_1:33;
set F = F5" * F33 * F4;
rng F33 c= RelOb(C2);
then rng F33 c= rng F5 by A8,FUNCT_2:def 3;
then
A15: dom (F5" * F33) = dom F33 by A14,RELAT_1:27;
RelOb(C1) c= dom F33 by FUNCT_2:def 1;
then rng F4 c= dom F33 by XBOOLE_1:1;
then
A16: dom F = dom F4 by A15,RELAT_1:27;
then
A17: dom F = the carrier of C1 by FUNCT_2:def 1;
for y being object st y in RelOb(C2) holds y in rng F33
proof
let y be object;
assume y in RelOb(C2);
then consider o1,o2 be Object of C2 such that
A18: y = [o1,o2] & ex g being morphism of C2 st g in Hom(o1,o2);
A19: rng F3 = dom RelOb(C2) \/ rng RelOb(C2) by A9,RELAT_1:def 6
.= dom RelOb(C2) \/ Ob C2 by Th34
.= Ob(C2) \/ Ob C2 by Th34
.= Ob D2;
consider x1 be object such that
A20: x1 in dom F3 & o1 = F3.x1 by A19,FUNCT_1:def 3;
consider x2 be object such that
A21: x2 in dom F3 & o2 = F3.x2 by A19,FUNCT_1:def 3;
reconsider x1,x2 as set by A20,A21;
set x = [x1,x2];
A22: x1 in field RelOb(C1) & x2 in field RelOb(C1)
by A20,A21,A6,WELLORD1:def 7;
[F3.x1, F3.x2] in RelOb(C2) by A18,A20,A21;
then reconsider x as Element of RelOb(D1)
by A22,A6,WELLORD1:def 7;
A23: dom F33 = RelOb(D1) by FUNCT_2:def 1;
F33.x = [F3.x1,F3.x2] by A13;
hence y in rng F33 by A23,A18,A20,A21,FUNCT_1:def 3;
end;
then RelOb(C2) c= rng F33 by TARSKI:def 3;
then rng F5 c= rng F33 by A8,FUNCT_2:def 3;
then rng(F5" * F33) = rng(F5") by A14,RELAT_1:28;
then
A24: rng(F5" * F33) = the carrier of C2 by A14,FUNCT_2:def 1;
dom F33 c= RelOb(C1);
then dom F33 c= rng F4 by A7,FUNCT_2:def 3;
then
A25: rng F = the carrier of C2 by A24,A15,RELAT_1:28;
then reconsider F as Functor of C1,C2 by A17,FUNCT_2:1;
for x1,x2 being object st x1 in dom F33 & x2 in dom F33 &
F33.x1 = F33.x2 holds x1 = x2
proof
let x1,x2 be object;
assume x1 in dom F33;
then x1 in RelOb(D1);
then consider o11,o12 be Object of D1 such that
A26: x1 = [o11,o12] & ex f1 being morphism of D1 st f1 in Hom(o11,o12);
A27: [o11,o12] in RelOb(C1) by A26;
reconsider x11=x1 as Element of RelOb(D1) by A26,A27;
assume x2 in dom F33;
then x2 in RelOb(D1);
then consider o21,o22 be Object of D1 such that
A28: x2 = [o21,o22] & ex f1 being morphism of D1 st f1 in Hom(o21,o22);
A29: [o21,o22] in RelOb(C1) by A28;
reconsider x22=x2 as Element of RelOb(D1) by A28,A29;
assume
A30: F33.x1 = F33.x2;
F33.x11 = [F3.o11,F3.o12] & F33.x22 = [F3.o21,F3.o22] by A13,A26,A28;
then F3.o11 = F3.o21 & F3.o12 = F3.o22 by A30,XTUPLE_0:1;
then o11 = o21 & o12 = o22 by A10,A9,FUNCT_1:def 4;
hence x1 = x2 by A26,A28;
end;
then
A31: F33 is one-to-one by FUNCT_1:def 4;
A32: F is onto by A25,FUNCT_2:def 3;
A33: for f being morphism of C1 holds dom(F.f) = F3.(dom f) &
cod(F.f) = F3.(cod f)
proof
let f be morphism of C1;
reconsider x = f as object;
x in Mor C1 by A2,SUBSET_1:def 1;
then
A34: x in dom F4 by A17,A16,CAT_6:def 1;
f in Hom(dom f, cod f) by A2,Th20;
then
A35: [dom f, cod f] in RelOb(D1);
then
A36: [dom f, cod f] in dom F33 by FUNCT_2:def 1;
reconsider x1 = [dom f, cod f] as Element of RelOb(D1) by A35;
A37: for a,b being set st x1 = [a,b] holds F33.x1 = [F3.a, F3.b] by A13;
[F3.(dom f), F3.(cod f)] in RelOb(C2) by A35,A6,WELLORD1:def 7;
then
A38: [F3.(dom f), F3.(cod f)] in rng F5 by A8,FUNCT_2:def 3;
A39: F.f = ((F5" * F33) * F4).x by CAT_6:def 21
.= (F5" * F33).(F4.x) by A34,FUNCT_1:13
.= (F5" * F33).[dom f, cod f] by A7
.= (F5").(F33.[dom f, cod f]) by A36,FUNCT_1:13
.= (F5").[F3.(dom f), F3.(cod f)] by A37;
[dom(F.f), cod(F.f)]
= F5.((F5").[F3.(dom f), F3.(cod f)]) by A8,A39
.= [F3.(dom f), F3.(cod f)] by A8,A38,FUNCT_1:35;
hence thesis by XTUPLE_0:1;
end;
for f1,f2 being morphism of C1 st f1 |> f2 holds F.f1 |> F.f2 &
F.(f1(*)f2) = (F.f1) (*) (F.f2)
proof
let f1,f2 be morphism of C1;
assume
A40: f1 |> f2;
dom(F.f1) = F3.(dom f1) by A33
.= F3.(cod f2) by A2,A40,Th5
.= cod(F.f2) by A33;
hence
A41: F.f1 |> F.f2 by Th5;
set g1 = F.(f1(*)f2);
set g2 = (F.f1) (*) (F.f2);
A42: dom g1 = F3.(dom(f1(*)f2)) by A33
.= F3.(dom f2) by A40,Th4
.= dom(F.f2) by A33
.= dom g2 by A41,Th4;
A43: cod g1 = F3.(cod(f1(*)f2)) by A33
.= F3.(cod f1) by A40,Th4
.= cod(F.f1) by A33
.= cod g2 by A41,Th4;
A44: g1 in Hom(dom g1, cod g1) by Th20;
g2 in Hom(dom g1, cod g1) by A42,A43,Th20;
hence F.(f1(*)f2) = (F.f1) (*) (F.f2) by A44,Def12;
end;
then
A45: F is multiplicative by CAT_6:def 23;
for f being morphism of C1 st f is identity holds F.f is identity
proof
let f be morphism of C1;
assume
A46: f is identity;
then
A47: dom f = f by Th6 .= cod f by A46,Th6;
A48: for g1 being morphism of C2 st (F.f) |> g1 holds (F.f) (*) g1 = g1
proof
let g1 be morphism of C2;
assume
A49: (F.f) |> g1;
set g2 = (F.f) (*) g1;
A50: dom g2 = dom g1 by A49,Th4;
A51: cod g2 = cod(F.f) by A49,Th4
.= F3.(dom f) by A33,A47
.= dom(F.f) by A33
.= cod g1 by A49,Th5;
A52: g1 in Hom(dom g1, cod g1) by A1,A2,Th20;
g2 in Hom(dom g1, cod g1) by A50,A51,Th20;
hence (F.f) (*) g1 = g1 by A52,Def12;
end;
then F.f is left_identity by CAT_6:def 4;
then F.f is right_identity by CAT_6:9;
hence F.f is identity by A48,CAT_6:def 4,def 14;
end;
then F is identity-preserving by CAT_6:def 22;
hence C1 ~= C2 by A32,Th12,A45,CAT_6:def 25,A8,A7,A31;
end;
end;
thus C1 ~= C2 implies O1 = O2
proof
assume C1 ~= C2;
then
A53: RelOb(C1), RelOb(C2) are_isomorphic by Th35;
A54: RelOb(C1), RelIncl(O1) are_isomorphic by Def14;
RelOb(C2), RelIncl(O2) are_isomorphic by Def14;
then RelOb(C1), RelIncl(O2) are_isomorphic by A53,WELLORD1:42;
then RelIncl(O2), RelOb(C1) are_isomorphic by WELLORD1:40;
hence O1 = O2 by A54,WELLORD1:42,WELLORD2:10;
end;
end;
definition
let O be ordinal number;
func OrdC(O) -> strict O -ordered preorder category equals
the strict O -ordered preorder category;
correctness;
end;
theorem Th39:
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
proof
consider C be strict preorder category such that
A1: Ob C = 2 and
for o1,o2 being Object of C st o1 in o2 holds Hom(o1,o2) = {[o1,o2]} and
A2: RelOb C = RelIncl 2 and
A3: Mor C = 2 \/ {[o1,o2] where o1,o2 is Element of 2: o1 in o2} by Th37;
A4: C is 2-ordered by A2,WELLORD1:38;
then
A5: C ~= OrdC 2 by Th38;
consider F be Functor of C, OrdC 2,
G be Functor of OrdC 2,C such that
A6: F is covariant & G is covariant and
A7: G (*) F = id C & F (*) G = id OrdC 2 by A4,Th38,CAT_6:def 28;
0 in 1 & 0 is Element of 2 & 1 is Element of 2
by CARD_1:49,50,TARSKI:def 1,def 2;
then
A8: [0,1] in {[o1,o2] where o1,o2 is Element of 2: o1 in o2};
then
A9: [0,1] in Mor C by A3,XBOOLE_0:def 3;
reconsider g = [0,1] as morphism of C by A8,A3,XBOOLE_0:def 3;
A10: C is non empty by A1;
A11: g is not identity
proof
assume g is identity;
then g is Object of C by A10,CAT_6:22;
hence contradiction by A1;
end;
set f = F.g;
take f;
thus
A12: f is not identity
proof
assume
A13: f is identity;
[0,1] in the carrier of C by A9,CAT_6:def 1;
then (id the carrier of C).[0,1] = [0,1] by FUNCT_1:18;
then
A14: (id C).[0,1] = g by STRUCT_0:def 4;
G.(F.g) is identity by A13,CAT_6:def 22,A6,CAT_6:def 25;
then (G(*)F).g is identity by A6,A10,CAT_6:34;
hence contradiction by A11,A7,A10,A14,CAT_6:def 21;
end;
card Ob OrdC 2 = card 2 by A1,A5,Th14;
then consider x,y be object such that
A15: x <> y & Ob OrdC 2 = {x,y} by CARD_2:60;
A16: dom f = x or dom f = y by A15,TARSKI:def 2;
A17: dom f <> cod f
proof
assume dom f = cod f;
then
A18: f in Hom(dom f, dom f);
id- (dom f) in Hom(dom f, dom f) by Def3;
hence contradiction by A12,A18,Def12;
end;
hence
A19: Ob OrdC 2 = {dom f, cod f} by A15,A16,TARSKI:def 2;
for x being object holds x in Mor OrdC 2 iff x in {dom f, cod f, f}
proof
let x be object;
hereby
assume
A20: x in Mor OrdC 2;
then
A21: x in the carrier of OrdC 2 by CAT_6:def 1;
reconsider f1 = x as morphism of OrdC 2 by A20;
per cases;
suppose f1 is identity;
then f1 is Object of OrdC 2 by CAT_6:22;
then x = dom f or x = cod f by A19,TARSKI:def 2;
hence x in {dom f, cod f, f} by ENUMSET1:def 1;
end;
suppose
A22: f1 is not identity;
A23: (id (the carrier of OrdC 2)).x = x by A21,FUNCT_1:18;
A24: F.(G.f1) = (F(*)G).f1 by A6,CAT_6:34
.= (id the carrier of OrdC 2).f1 by A7,STRUCT_0:def 4
.= f1 by A23,CAT_6:def 21;
G.f1 is not identity by A24,A22,CAT_6:def 22,A6,CAT_6:def 25;
then not G.f1 in 2 by A1,A10,CAT_6:22;
then G.f1 in {[o1,o2] where o1,o2 is Element of 2: o1 in o2}
by A3,XBOOLE_0:def 3;
then consider o1,o2 be Element of 2 such that
A25: G.f1 = [o1,o2] & o1 in o2;
A26: o1 = 0 or o1 = 1 by CARD_1:50,TARSKI:def 2;
o2 = 0 or o2 = 1 by CARD_1:50,TARSKI:def 2;
hence x in {dom f, cod f, f} by A25,A26,A24,ENUMSET1:def 1,CARD_1:49;
end;
end;
assume x in {dom f, cod f, f};
then
A27: x in {dom f, cod f} \/ {f} by ENUMSET1:3;
per cases by A27,A19,XBOOLE_0:def 3;
suppose x in Ob OrdC 2;
hence x in Mor OrdC 2;
end;
suppose x in {f};
then x = f by TARSKI:def 1;
hence x in Mor OrdC 2;
end;
end;
hence Mor OrdC 2 = {dom f, cod f, f} by TARSKI:2;
dom f <> cod f & dom f <> f & cod f <> f by A12,A17,CAT_6:22;
hence dom f, cod f, f are_mutually_distinct by ZFMISC_1:def 5;
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:
for g being morphism of OrdC 2 st g is not identity holds it.g = f;
existence
proof
consider f1 be morphism of OrdC 2 such that
A1: f1 is not identity and
Ob OrdC 2 = {dom f1, cod f1} and
A2: Mor OrdC 2 = {dom f1, cod f1, f1} and
A3: dom f1, cod f1, f1 are_mutually_distinct by Th39;
defpred P[object,object] means
($1 = dom f1 implies $2 = dom f) &
($1 = cod f1 implies $2 = cod f) &
($1 = f1 implies $2 = f);
A4: for x being object st x in the carrier of OrdC 2
ex y being object st y in the carrier of C & P[x,y]
proof
let x be object;
assume x in the carrier of OrdC 2;
then
A5: x in {dom f1, cod f1, f1} by CAT_6:def 1,A2;
per cases by A5,ENUMSET1:def 1;
suppose
A6: x = dom f1;
reconsider y = dom f as object;
take y;
y in Ob C;
then y in Mor C;
hence y in the carrier of C by CAT_6:def 1;
thus P[x,y] by A6,A3,ZFMISC_1:def 5;
end;
suppose
A7: x = cod f1;
reconsider y = cod f as object;
take y;
y in Ob C;
then y in Mor C;
hence y in the carrier of C by CAT_6:def 1;
thus P[x,y] by A7,A3,ZFMISC_1:def 5;
end;
suppose
A8: x = f1;
reconsider y = f as object;
take y;
y in Mor C;
hence y in the carrier of C by CAT_6:def 1;
thus P[x,y] by A8,A3,ZFMISC_1:def 5;
end;
end;
consider F be Function of the carrier of OrdC 2, the carrier of C
such that
A9: for x being object st x in the carrier of OrdC 2
holds P[x,F.x] from FUNCT_2:sch 1(A4);
reconsider F as Functor of OrdC 2, C;
for g being morphism of OrdC 2 st g is identity
holds F.g is identity
proof
let g be morphism of OrdC 2;
assume
A10: g is identity;
reconsider x = g as object;
A11: F.x = F.g by CAT_6:def 21;
g in Mor OrdC 2;
then x in the carrier of OrdC 2 by CAT_6:def 1;
then P[x,F.x] by A9;
hence F.g is identity by A11,CAT_6:22,A2,A1,A10,ENUMSET1:def 1;
end;
then
A12: F is identity-preserving by CAT_6:def 22;
for g1,g2 being morphism of OrdC 2 st g1 |> g2 holds
F.g1 |> F.g2 & F.(g1 (*) g2) = (F.g1) (*) (F.g2)
proof
let g1,g2 be morphism of OrdC 2;
assume
A13: g1 |> g2;
A14: for g being morphism of OrdC 2 st g = dom f1 holds F.g = dom f
proof
let g be morphism of OrdC 2;
assume
A15: g = dom f1;
reconsider x = g as object;
A16: F.x = F.g by CAT_6:def 21;
g in Mor OrdC 2;
then x in the carrier of OrdC 2 by CAT_6:def 1;
hence thesis by A9,A15,A16;
end;
A17: for g being morphism of OrdC 2 st g = cod f1 holds F.g = cod f
proof
let g be morphism of OrdC 2;
assume
A18: g = cod f1;
reconsider x = g as object;
A19: F.x = F.g by CAT_6:def 21;
g in Mor OrdC 2;
then x in the carrier of OrdC 2 by CAT_6:def 1;
hence thesis by A9,A18,A19;
end;
A20: for g being morphism of OrdC 2 st g = f1 holds F.g = f
proof
let g be morphism of OrdC 2;
assume
A21: g = f1;
reconsider x = g as object;
A22: F.x = F.g by CAT_6:def 21;
g in Mor OrdC 2;
then x in the carrier of OrdC 2 by CAT_6:def 1;
hence thesis by A9,A21,A22;
end;
per cases by A2,ENUMSET1:def 1;
suppose
A23: g1 = dom f1 & g2 = dom f1;
then
A24: F.g1 = dom f & F.g2 = dom f by A14;
hence
A25: F.g1 |> F.g2 by CAT_6:23;
thus F.(g1 (*) g2) = F.g1 by A23,A13,CAT_6:23
.= (F.g1) (*) (F.g2) by A25,A24,CAT_6:23;
end;
suppose
A26: g1 = dom f1 & g2 = cod f1;
then g1 is identity & g2 is identity by CAT_6:22;
then g1 = g2 by A13,Th7;
hence thesis by A26,A3,ZFMISC_1:def 5;
end;
suppose
A27: g1 = dom f1 & g2 = f1;
then cod f1 = g1 by A13,CAT_6:22,27;
hence thesis by A27,A3,ZFMISC_1:def 5;
end;
suppose
A28: g1 = cod f1 & g2 = dom f1;
then g1 is identity & g2 is identity by CAT_6:22;
then g1 = g2 by A13,Th7;
hence thesis by A28,A3,ZFMISC_1:def 5;
end;
suppose
A29: g1 = cod f1 & g2 = cod f1;
then
A30: F.g1 = cod f & F.g2 = cod f by A17;
hence
A31: F.g1 |> F.g2 by CAT_6:23;
thus F.(g1 (*) g2) = F.g1 by A29,A13,CAT_6:23
.= (F.g1) (*) (F.g2) by A31,A30,CAT_6:23;
end;
suppose
A32: g1 = cod f1 & g2 = f1;
then
A33: F.g1 = cod f & F.g2 = f by A17,A20;
hence F.g1 |> F.g2 by Th9;
thus F.(g1 (*) g2) = F.g2 by A32,Th9
.= (F.g1) (*) (F.g2) by A33,Th9;
end;
suppose
A34: g1 = f1 & g2 = dom f1;
then
A35: F.g1 = f & F.g2 = dom f by A14,A20;
hence F.g1 |> F.g2 by Th8;
thus F.(g1 (*) g2) = F.g1 by A34,Th8
.= (F.g1) (*) (F.g2) by A35,Th8;
end;
suppose
A36: g1 = f1 & g2 = cod f1;
then dom f1 = g2 by A13,CAT_6:22,26;
hence thesis by A36,A3,ZFMISC_1:def 5;
end;
suppose g1 = f1 & g2 = f1;
then dom f1 = cod f1 by A13,Th5;
hence thesis by A3,ZFMISC_1:def 5;
end;
end;
then reconsider F as covariant Functor of OrdC 2, C
by A12,CAT_6:def 23,def 25;
take F;
let g be morphism of OrdC 2;
assume
A37: g is not identity;
A38: g = dom f1 or g = cod f1 or g = f1 by A2,ENUMSET1:def 1;
reconsider x = g as object;
A39: F.x = F.g by CAT_6:def 21;
g in Mor OrdC 2;
then x in the carrier of OrdC 2 by CAT_6:def 1;
hence F.g = f by A9,A38,A39,A37,CAT_6:22;
end;
uniqueness
proof
let F1,F2 be covariant Functor of OrdC 2,C;
assume
A40: for g being morphism of OrdC 2 st not g is identity holds F1.g=f;
assume
A41: for g being morphism of OrdC 2 st not g is identity holds F2.g=f;
consider f1 be morphism of OrdC 2 such that
A42: f1 is not identity and
Ob OrdC 2 = {dom f1, cod f1} and
A43: Mor OrdC 2 = {dom f1, cod f1, f1} by Th39;
for x being object st x in the carrier of OrdC 2 holds F1.x = F2.x
proof
let x be object;
assume x in the carrier of OrdC 2;
then
A44: x in {dom f1, cod f1, f1} by A43,CAT_6:def 1;
A45: F1.f1 = f by A40,A42 .= F2.f1 by A41,A42;
per cases by A44,ENUMSET1:def 1;
suppose
A46: x = dom f1;
hence F1.x = dom(F1.f1) by CAT_6:32
.= F2.x by A46,A45,CAT_6:32;
end;
suppose
A47: x = cod f1;
hence F1.x = cod(F1.f1) by CAT_6:32
.= F2.x by A47,A45,CAT_6:32;
end;
suppose
A48: x = f1;
hence F1.x = F1.f1 by CAT_6:def 21
.= F2.x by A45,A48,CAT_6:def 21;
end;
end;
hence F1 = F2 by FUNCT_2:12;
end;
end;
theorem Th40:
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
proof
let C be non empty category;
let f be morphism of C;
assume
A1: f is identity;
let g be morphism of OrdC 2;
consider f1 be morphism of OrdC(2) such that
A2: f1 is not identity & Ob OrdC 2 = {dom f1, cod f1} &
Mor OrdC 2 = {dom f1, cod f1, f1} &
dom f1, cod f1, f1 are_mutually_distinct by Th39;
per cases by A2,ENUMSET1:def 1;
suppose g = dom f1;
hence (MORPHISM f).g = (MORPHISM f).(dom f1) by CAT_6:def 21
.= dom ((MORPHISM f).f1) by CAT_6:32
.= dom f by A2,Def16
.= f by A1,Th6;
end;
suppose g = cod f1;
hence (MORPHISM f).g = (MORPHISM f).(cod f1) by CAT_6:def 21
.= cod ((MORPHISM f).f1) by CAT_6:32
.= cod f by A2,Def16
.= f by A1,Th6;
end;
suppose g = f1; hence thesis by A2,Def16; end;
end;
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 :Def17:
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
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
proof
let C be non empty category;
let c,c1,c2,d,e be Object of C;
let f1 be Morphism of c1,c;
let f2 be Morphism of c2,c;
let p1 be Morphism of d,c1;
let p2 be Morphism of d,c2;
let q1 be Morphism of e,c1;
let q2 be Morphism of e,c2;
assume
A1: Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {} &
Hom(e,c1) <> {} & Hom(e,c2) <> {};
assume
A2: d,p1,p2 is_pullback_of f1,f2;
assume
A3: e,q1,q2 is_pullback_of f1,f2;
A4: 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 by A1,A2,Def17;
A5: f1 * q1 = f2 * q2 & for e1 being Object of C,
g1 being Morphism of e1,c1, g2 being Morphism of e1,c2
st Hom(e1,c1) <> {} & Hom(e1,c2) <> {} & f1 * g1 = f2 * g2
holds Hom(e1,e) <> {} & ex h being Morphism of e1,e st
q1 * h = g1 & q2 * h = g2
& for h1 being Morphism of e1,e st q1 * h1 = g1 & q2 * h1 = g2
holds h = h1 by A1,A3,Def17;
ex ff being Morphism of d,e, gg being Morphism of e,d st
Hom(d,e)<>{} & Hom(e,d)<>{} & gg * ff = id- d & ff * gg = id- e
proof
consider f be Morphism of d,e such that
A6: q1 * f = p1 & q2 * f = p2 &
for h1 being Morphism of d,e st q1 * h1 = p1 & q2 * h1 = p2
holds f = h1 by A4,A1,A3,Def17;
consider g be Morphism of e,d such that
A7: p1 * g = q1 & p2 * g = q2 &
for h1 being Morphism of e,d st p1 * h1 = q1 & p2 * h1 = q2
holds g = h1 by A5,A1,A2,Def17;
take f,g;
thus
A8: Hom(d,e)<>{} by A4,A1,A3,Def17;
thus
A9: Hom(e,d)<>{} by A5,A1,A2,Def17;
set g11 = q1 * f;
set g12 = q2 * f;
consider h1 be Morphism of d,d such that
A10: p1 * h1 = g11 & p2 * h1 = g12 & for h being Morphism of d,d
st p1 * h = g11 & p2 * h = g12 holds h1 = h by A1,A4,A6;
A11: p1 * (g * f) = g11 by A1,A7,A9,A8,Th23;
A12: p2 * (g * f) = g12 by A1,A7,A9,A8,Th23;
A13: p1 * id- d = g11 by A1,A6,Th18;
A14: p2 * id- d = g12 by A1,A6,Th18;
thus g * f = h1 by A10,A11,A12 .= id- d by A10,A13,A14;
set g21 = p1 * g;
set g22 = p2 * g;
consider h2 be Morphism of e,e such that
A15: q1 * h2 = g21 & q2 * h2 = g22 & for h being Morphism of e,e
st q1 * h = g21 & q2 * h = g22 holds h2 = h by A1,A5,A7;
A16: q1 * (f * g) = g21 by A1,A6,A9,A8,Th23;
A17: q2 * (f * g) = g22 by A1,A6,A9,A8,Th23;
A18: q1 * id- e = g21 by A1,A7,Th18;
A19: q2 * id- e = g22 by A1,A7,Th18;
thus f * g = h2 by A15,A16,A17 .= id- e by A15,A18,A19;
end;
hence d,e are_isomorphic;
end;
theorem
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
proof
let C be category;
let c,c1,c2,d be Object of C;
let f1 be Morphism of c1,c;
let f2 be Morphism of c2,c;
let p1 be Morphism of d,c1;
let p2 be Morphism of d,c2;
assume
A1: Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {};
assume
A2: d,p1,p2 is_pullback_of f1,f2;
then
A3: 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
by A1,Def17;
for d1 being Object of C,
g2 being Morphism of d1,c2, g1 being Morphism of d1,c1
st Hom(d1,c2) <> {} & Hom(d1,c1) <> {} & f2 * g2 = f1 * g1
holds Hom(d1,d) <> {} & ex h being Morphism of d1,d st
p2 * h = g2 & p1 * h = g1
& for h1 being Morphism of d1,d st p2 * h1 = g2 & p1 * h1 = g1
holds h = h1
proof
let d1 be Object of C;
let g2 be Morphism of d1,c2;
let g1 be Morphism of d1,c1;
assume
A4: Hom(d1,c2) <> {} & Hom(d1,c1) <> {} & f2 * g2 = f1 * g1;
hence Hom(d1,d) <> {} by A2,A1,Def17;
consider h be Morphism of d1,d such that
A5: p1 * h = g1 & p2 * h = g2
& for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2
holds h = h1 by A4,A2,A1,Def17;
take h;
thus thesis by A5;
end;
hence d,p2,p1 is_pullback_of f2,f1 by A3,A1,Def17;
end;
theorem
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
proof
let C be category;
let c,c1,c2,d be Object of C;
let f1 be Morphism of c1,c;
let f2 be Morphism of c2,c;
let p1 be Morphism of d,c1;
let p2 be Morphism of d,c2;
assume
A1: Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {};
assume
A2: d,p1,p2 is_pullback_of f1,f2;
then
A3: 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
by A1,Def17;
assume
A4: f1 is monomorphism;
thus Hom(d,c2)<>{} by A1;
let d1 be Object of C;
assume
A5: Hom(d1,d) <> {};
let q1,q2 be Morphism of d1,d;
assume
A6: p2 * q1 = p2 * q2;
set p11 = p1 * q1;
set p12 = p2 * q1;
A7: Hom(d1,c1) <> {} & Hom(d1,c2) <> {} by A1,A5,Th22;
f1 * p11 = (f1 * p1) * q1 by A5,A1,Th23
.= f2 * p12 by A5,A3,A1,Th23;
then consider h be Morphism of d1,d such that
A8: p1 * h = p11 & p2 * h = p12
& for h1 being Morphism of d1,d st p1 * h1 = p11 & p2 * h1 = p12
holds h = h1 by A1,A2,Def17,A7;
A9: q1 = h by A8;
f1 * (p1 * q2) = (f1 * p1) * q2 by A5,A1,Th23
.= f2 * (p2 * q2) by A5,A3,A1,Th23
.= (f2 * p2) * q1 by A6,A5,A1,Th23
.= f1 * p11 by A5,A3,A1,Th23;
hence q1 = q2 by A9,A8,A6,A7,A4;
end;
theorem
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
proof
let C be non empty category;
let c,c1,c2,d be Object of C;
let f1 be Morphism of c1,c;
let f2 be Morphism of c2,c;
let p1 be Morphism of d,c1;
let p2 be Morphism of d,c2;
assume
A1: Hom(c1,c) <> {} & Hom(c2,c) <> {} & Hom(d,c1) <> {} & Hom(d,c2) <> {};
assume
A2: d,p1,p2 is_pullback_of f1,f2;
then
A3: 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
by A1,Def17;
assume
A4: f1 is isomorphism;
consider g1 be Morphism of c,c1 such that
A5: g1 * f1 = id- c1 & f1 * g1 = id- c by A4;
set g11 = g1 * f2;
set g22 = id- c2;
A6: Hom(c2,c1) <> {} & Hom(c2,c2) <> {} & Hom(c1,c1) <> {} by A1,A4,Th22;
A7: f1 * g11 = (f1 * g1) * f2 by A4,A1,Th23
.= f2 by A5,A1,Th18
.= f2 * g22 by A1,Th18;
then
A8: Hom(c2,d) <> {} & ex h being Morphism of c2,d st
p1 * h = g11 & p2 * h = g22
& for h1 being Morphism of c2,d st p1 * h1 = g11 & p2 * h1 = g22
holds h = h1 by A2,A1,Def17,A6;
consider q2 be Morphism of c2,d such that
A9: p1 * q2 = g11 & p2 * q2 = g22
& for h1 being Morphism of c2,d st p1 * h1 = g11 & p2 * h1 = g22
holds q2 = h1 by A6,A2,A1,Def17,A7;
set g33 = p1 * q2 * p2;
A10: Hom(d,c) <> {} by A1,Th22;
f1 * g33 = f1 * (g1 * (f2 * p2)) by A9,A4,A1,Th23
.= (f1 * g1) * (f2 * p2) by A10,A4,Th23
.= f2 * p2 by A10,Th18,A5;
then consider h be Morphism of d,d such that
p1 * h = g33 & p2 * h = p2 and
A11: for h1 being Morphism of d,d st p1 * h1 = g33 & p2 * h1 = p2 holds h = h1
by A1,A2,Def17;
A12: p1 * id- d = p1 by A1,Th18
.= g1 * f1 * p1 by A1,A5,Th18
.= g1 * (f1 * p1) by A1,A4,Th23
.= g33 by A9,A3,A4,A1,Th23;
A13: p2 * id- d = p2 by A1,Th18;
A14: p1 * (q2 * p2) = g33 by A1,A8,Th23;
p2 * (q2 * p2) = p2 * q2 * p2 by A1,A8,Th23
.= p2 by A1,A9,Th18;
then h = q2 * p2 by A11,A14;
hence p2 is isomorphism by A7,A9,A13,A11,A12,A2,A1,Def17,A6;
end;
:: Pullback Lemma
theorem
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
proof
let C be category;
let c1,c2,c3,c4,c5,c6 be Object of C;
let f1 be Morphism of c1,c2;
let f2 be Morphism of c2,c3;
let f3 be Morphism of c1,c4;
let f4 be Morphism of c2,c5;
let f5 be Morphism of c3,c6;
let f6 be Morphism of c4,c5;
let f7 be Morphism of c5,c6;
assume
A1: Hom(c1,c2) <> {} & Hom(c2,c3) <> {} & Hom(c1,c4) <> {} &
Hom(c2,c5) <> {} & Hom(c3,c6) <> {} & Hom(c4,c5) <> {} &
Hom(c5,c6) <> {};
assume
A2: c2,f2,f4 is_pullback_of f5,f7;
then
A3: f5 * f2 = f7 * f4 & for d1 being Object of C,
g1 being Morphism of d1,c3, g2 being Morphism of d1,c5
st Hom(d1,c3) <> {} & Hom(d1,c5) <> {} & f5 * g1 = f7 * g2
holds Hom(d1,c2) <> {} & ex h being Morphism of d1,c2 st
f2 * h = g1 & f4 * h = g2
& for h1 being Morphism of d1,c2 st f2 * h1 = g1 & f4 * h1 = g2
holds h = h1 by A1,Def17;
hereby
assume
A4: c1,f1,f3 is_pullback_of f4,f6;
then
A5: f4 * f1 = f6 * f3 & for d1 being Object of C,
g1 being Morphism of d1,c2, g2 being Morphism of d1,c4
st Hom(d1,c2) <> {} & Hom(d1,c4) <> {} & f4 * g1 = f6 * g2
holds Hom(d1,c1) <> {} & ex h being Morphism of d1,c1 st
f1 * h = g1 & f3 * h = g2
& for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2
holds h = h1 by A1,Def17;
A6: Hom(c4,c6) <> {} & Hom(c1,c3) <> {} & Hom(c1,c4) <> {} by A1,Th22;
A7: f5 * (f2*f1) = f5 * f2 * f1 by A1,Th23
.= f7 * (f6 * f3) by A3,A5,Th23,A1
.= (f7*f6) * f3 by A1,Th23;
for d1 being Object of C,
g1 being Morphism of d1,c3, g2 being Morphism of d1,c4
st Hom(d1,c3) <> {} & Hom(d1,c4) <> {} & f5 * g1 = (f7*f6) * g2
holds Hom(d1,c1) <> {} & ex h being Morphism of d1,c1 st
(f2*f1) * h = g1 & f3 * h = g2
& for h1 being Morphism of d1,c1 st (f2*f1) * h1 = g1 & f3 * h1 = g2
holds h = h1
proof
let d1 be Object of C;
let g1 be Morphism of d1,c3;
let g2 be Morphism of d1,c4;
assume
A8: Hom(d1,c3) <> {};
assume
A9: Hom(d1,c4) <> {};
assume
A10: f5 * g1 = (f7*f6) * g2;
A11: Hom(d1,c5) <> {} by A9,A1,Th22;
A12: f5 * g1 = f7 * (f6*g2) by A10,A9,A1,Th23;
then
A13: Hom(d1,c2) <> {} & ex h being Morphism of d1,c2 st
f2 * h = g1 & f4 * h = f6*g2
& for h1 being Morphism of d1,c2 st f2 * h1 = g1 & f4 * h1 = f6*g2
holds h = h1 by A1,A2,A11,A8,Def17;
consider g3 be Morphism of d1,c2 such that
A14: f2 * g3 = g1 & f4 * g3 = f6*g2
& for h1 being Morphism of d1,c2 st f2 * h1 = g1 & f4 * h1 = f6*g2
holds g3 = h1 by A1,A12,A2,A11,A8,Def17;
thus
A15: Hom(d1,c1) <> {} by A1,A13,A9,A4,Def17;
consider h be Morphism of d1,c1 such that
A16: f1 * h = g3 & f3 * h = g2
& for h1 being Morphism of d1,c1 st f1 * h1 = g3 & f3 * h1 = g2
holds h = h1 by A1,A14,A13,A9,A4,Def17;
take h;
thus (f2*f1) * h = g1 by A1,A14,A16,A15,Th23;
thus f3 * h = g2 by A16;
let h1 be Morphism of d1,c1;
assume
A17: (f2*f1) * h1 = g1;
assume
A18: f3 * h1 = g2;
A19: f2 * (f1*h1) = g1 by A1,A17,A15,Th23;
f4 * (f1*h1) = f4*f1 * h1 by A1,A15,Th23
.= f6*g2 by A18,A5,A15,Th23,A1;
then g3 = f1*h1 by A19,A14;
hence h = h1 by A18,A16;
end;
hence c1,f2*f1,f3 is_pullback_of f5,f7*f6 by A1,A6,A7,Def17;
thus f4 * f1 = f6 * f3 by A1,A4,Def17;
end;
A20: Hom(c1,c3) <> {} & Hom(c3,c6) <> {} & Hom(c4,c6) <> {} by A1,Th22;
assume
A21: c1,f2*f1,f3 is_pullback_of f5,f7*f6;
assume
A22: f4 * f1 = f6 * f3;
for d1 being Object of C,
g1 being Morphism of d1,c2, g2 being Morphism of d1,c4
st Hom(d1,c2) <> {} & Hom(d1,c4) <> {} & f4 * g1 = f6 * g2
holds Hom(d1,c1) <> {} & ex h being Morphism of d1,c1 st
f1 * h = g1 & f3 * h = g2
& for h1 being Morphism of d1,c1 st f1 * h1 = g1 & f3 * h1 = g2
holds h = h1
proof
let d1 be Object of C;
let g1 be Morphism of d1,c2;
let g2 be Morphism of d1,c4;
assume
A23: Hom(d1,c2) <> {};
assume
A24: Hom(d1,c4) <> {};
assume
A25: f4 * g1 = f6 * g2;
set g11 = f2 * g1;
A26: Hom(d1,c3) <> {} by A1,A23,Th22;
A27: f5 * g11 = (f5*f2) * g1 by A23,A1,Th23
.= f7* (f6 * g2) by A25,A23,A3,Th23,A1
.= (f7*f6) * g2 by A24,A1,Th23;
then
A28: Hom(d1,c1) <> {} & ex h being Morphism of d1,c1 st
(f2*f1) * h = g11 & f3 * h = g2
& for h1 being Morphism of d1,c1 st (f2*f1) * h1 = g11 & f3 * h1 = g2
holds h = h1 by A1,A24,A26,A21,A20,Def17;
thus
A29: Hom(d1,c1) <> {} by A1,A27,A24,A26,A21,A20,Def17;
consider h be Morphism of d1,c1 such that
A30: (f2*f1) * h = g11 & f3 * h = g2
& for h1 being Morphism of d1,c1 st (f2*f1) * h1 = g11 & f3 * h1 = g2
holds h = h1 by A1,A27,A24,A26,A21,A20,Def17;
take h;
set g22 = f4 * g1;
A31: Hom(d1,c3) <> {} & Hom(d1,c5) <> {} by A1,A23,Th22;
A32: f5 * g11 = (f5*f2) * g1 by A23,A1,Th23
.= f7 * g22 by A23,A3,Th23,A1;
consider h2 be Morphism of d1,c2 such that
A33: f2 * h2 = g11 & f4 * h2 = g22
& for h1 being Morphism of d1,c2 st f2 * h1 = g11 & f4 * h1 = g22
holds h2 = h1 by A1,A32,A31,A2,Def17;
A34: h2 = g1 by A33;
A35: f2 * (f1 * h) = f2 * g1 by A1,A30,A28,Th23;
f4 * (f1 * h) = (f4 * f1) * h by A1,A28,Th23
.= f4 * g1 by A30,A25,A22,A28,A1,Th23;
hence f1 * h = g1 by A33,A35,A34;
thus f3 * h = g2 by A30;
let h1 be Morphism of d1,c1;
assume
A36: f1 * h1 = g1;
A37: (f2*f1) * h1 = g11 by A1,A36,A29,Th23;
assume f3 * h1 = g2;
hence h = h1 by A30,A37;
end;
hence c1,f1,f3 is_pullback_of f4,f6 by A22,A1,Def17;
end;
begin :: Pullbacks of Functors
definition
let C,D be category;
let F be Functor of C,D;
attr F is monomorphism means
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
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 :Def20:
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 Th46:
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
proof
let C,C1,C2,D,E be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
let P1 be Functor of D,C1;
let P2 be Functor of D,C2;
let Q1 be Functor of E,C1;
let Q2 be Functor of E,C2;
assume
A1: F1 is covariant & F2 is covariant;
assume
A2: P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant;
assume
A3: D,P1,P2 is_pullback_of F1,F2;
assume
A4: E,Q1,Q2 is_pullback_of F1,F2;
ex FF being Functor of D,E, GG being Functor of E,D st
FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E
proof
A5: F1 (*) P1 = F2 (*) P2 &
for D0 being category, G1 being Functor of D0,C1,
G2 being Functor of D0,C2
st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D0,D st H is covariant & P1 (*) H = G1 &
P2 (*) H = G2 & for H1 being Functor of D0,D
st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds H=H1
by A2,A1,A3,Def20;
A6: F1 (*) Q1 = F2 (*) Q2 &
for D0 being category, G1 being Functor of D0,C1,
G2 being Functor of D0,C2
st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D0,E st H is covariant & Q1 (*) H = G1 &
Q2 (*) H = G2 & for H1 being Functor of D0,E
st H1 is covariant & Q1 (*) H1 = G1 & Q2 (*) H1 = G2 holds H=H1
by A2,A1,A4,Def20;
consider FF be Functor of D,E such that
A7: FF is covariant & Q1 (*) FF = P1 & Q2 (*) FF = P2 &
for H1 being Functor of D,E st H1 is covariant &
Q1 (*) H1 = P1 & Q2 (*) H1 = P2 holds FF = H1 by A2,A5,A1,A4,Def20;
consider GG be Functor of E,D such that
A8: GG is covariant & P1 (*) GG = Q1 & P2 (*) GG = Q2 &
for H1 being Functor of E,D st H1 is covariant &
P1 (*) H1 = Q1 & P2 (*) H1 = Q2 holds GG = H1 by A2,A6,A1,A3,Def20;
take FF,GG;
thus FF is covariant & GG is covariant by A7,A8;
set G11 = Q1 (*) FF;
set G12 = Q2 (*) FF;
consider H1 be Functor of D,D such that
A9: H1 is covariant & P1 (*) H1 = G11 & P2 (*) H1 = G12 &
for H being Functor of D,D st H is covariant & P1 (*) H = G11 &
P2 (*) H = G12 holds H1 = H by A2,A5,A7;
A10: P1 (*) (GG (*) FF) = G11 by A2,A7,A8,Th10;
A11: P2 (*) (GG (*) FF) = G12 by A2,A7,A8,Th10;
A12: P1 (*) id D = G11 by A2,A7,Th11;
A13: P2 (*) id D = G12 by A2,A7,Th11;
thus GG (*) FF = H1 by A9,A10,A11,A7,A8,CAT_6:35 .= id D by A9,A12,A13;
set G21 = P1 (*) GG;
set G22 = P2 (*) GG;
consider H2 be Functor of E,E such that
A14: H2 is covariant & Q1 (*) H2 = G21 & Q2 (*) H2 = G22 &
for H being Functor of E,E st H is covariant & Q1 (*) H = G21 &
Q2 (*) H = G22 holds H2 = H by A2,A6,A8;
A15: Q1 (*) (FF (*) GG) = G21 by A2,A7,A8,Th10;
A16: Q2 (*) (FF (*) GG) = G22 by A2,A7,A8,Th10;
A17: Q1 (*) id E = G21 by A2,A8,Th11;
A18: Q2 (*) id E = G22 by A2,A8,Th11;
thus FF (*) GG = H2 by A14,A15,A16,A7,A8,CAT_6:35
.= id E by A14,A17,A18;
end;
hence D ~= E by CAT_6:def 28;
end;
theorem Th47:
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
proof
let C,C1,C2,D be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
let P1 be Functor of D,C1;
let P2 be Functor of D,C2;
assume
A1: F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant;
assume
A2: D,P1,P2 is_pullback_of F1,F2;
then
A3: 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
by A1,Def20;
for D1 being category, G1 being Functor of D1,C2, G2 being Functor of D1,C1
st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds
ex H being Functor of D1,D st H is covariant &
P2 (*) H = G1 & P1 (*) H = G2 & for H1 being Functor of D1,D
st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds H = H1
proof
let D1 be category;
let G1 be Functor of D1,C2;
let G2 be Functor of D1,C1;
assume
A4: G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2;
consider H be Functor of D1,D such that
A5: H is covariant & P1 (*) H = G2 & P2 (*) H = G1
& for H1 being Functor of D1,D
st H1 is covariant & P1 (*) H1 = G2 & P2 (*) H1 = G1 holds H = H1
by A4,A2,A1,Def20;
take H;
thus H is covariant & P2 (*) H = G1 & P1 (*) H = G2 by A5;
let H1 be Functor of D1,D;
assume H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2;
hence H = H1 by A5;
end;
hence D,P2,P1 is_pullback_of F2,F1 by A3,A1,Def20;
end;
theorem
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
proof
let C,C1,C2,D be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
let P1 be Functor of D,C1;
let P2 be Functor of D,C2;
assume
A1: F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant;
assume
A2: D,P1,P2 is_pullback_of F1,F2;
then
A3: 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 by A1,Def20;
assume
A4: F1 is monomorphism;
for D1 being category
for Q1,Q2 being Functor of D1,D st Q1 is covariant & Q2 is covariant &
P2 (*) Q1 = P2 (*) Q2 holds Q1 = Q2
proof
let D1 be category;
let Q1,Q2 be Functor of D1,D;
assume
A5: Q1 is covariant & Q2 is covariant;
assume
A6: P2 (*) Q1 = P2 (*) Q2;
set P11 = P1 (*) Q1;
set P12 = P2 (*) Q1;
A7: P11 is covariant & P12 is covariant by A1,A5,CAT_6:35;
F1 (*) P11 = (F1 (*) P1) (*) Q1 by A5,A1,Th10
.= F2 (*) P12 by A5,A3,A1,Th10;
then consider H be Functor of D1,D such that
A8: H is covariant & P1 (*) H = P11 & P2 (*) H = P12
& for H1 being Functor of D1,D st H1 is covariant &
P1 (*) H1 = P11 & P2 (*) H1 = P12 holds H = H1 by A1,A2,Def20,A7;
A9: Q1 = H by A5,A8;
A10: P1 (*) Q2 is covariant by A5,A1,CAT_6:35;
F1 (*) (P1 (*) Q2) = (F1 (*) P1) (*) Q2 by A5,A1,Th10
.= F2 (*) (P2 (*) Q2) by A5,A3,A1,Th10
.= (F2 (*) P2) (*) Q1 by A6,A5,A1,Th10
.= F1 (*) P11 by A5,A3,A1,Th10;
hence Q1 = Q2 by A5,A9,A8,A6,A7,A10,A4;
end;
hence thesis by A1;
end;
theorem
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
proof
let C,C1,C2,D be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
let P1 be Functor of D,C1;
let P2 be Functor of D,C2;
assume
A1: F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant;
assume
A2: D,P1,P2 is_pullback_of F1,F2;
then
A3: 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 by A1,Def20;
assume
A4: F1 is isomorphism;
consider G1 be Functor of C,C1 such that
A5: G1 is covariant & G1 (*) F1 = id C1 & F1 (*) G1 = id C by A4;
set G11 = G1 (*) F2;
set G22 = id C2;
A6: G11 is covariant by A5,A1,CAT_6:35;
A7: F1 (*) G11 = (F1 (*) G1) (*) F2 by A5,A1,Th10
.= F2 by A5,A1,Th11
.= F2 (*) G22 by A1,Th11;
consider Q2 be Functor of C2,D such that
A8: Q2 is covariant & P1 (*) Q2 = G11 & P2 (*) Q2 = G22
& for H1 being Functor of C2,D st H1 is covariant & P1 (*) H1 = G11 &
P2 (*) H1 = G22
holds Q2 = H1 by A6,A2,A1,Def20,A7;
set G33 = P1 (*) Q2 (*) P2;
A9: F2 (*) P2 is covariant by A1,CAT_6:35;
A10: G33 is covariant by A8,A6,A1,CAT_6:35;
F1 (*) G33 = F1 (*) (G1 (*) (F2 (*) P2)) by A5,A8,A1,Th10
.= (F1 (*) G1) (*) (F2 (*) P2) by A9,A5,A4,Th10
.= F2 (*) P2 by A9,Th11,A5;
then consider H be Functor of D,D such that
H is covariant & P1 (*) H = G33 & P2 (*) H = P2 and
A11: for H1 being Functor of D,D st H1 is covariant & P1 (*) H1 = G33 &
P2 (*) H1 = P2 holds H = H1
by A1,A2,A10,Def20;
A12: P1 (*) id D = P1 by A1,Th11
.= G1 (*) F1 (*) P1 by A1,A5,Th11
.= G1 (*) (F1 (*) P1) by A1,A5,Th10
.= G33 by A8,A3,A1,A5,Th10;
A13: P2 (*) id D = P2 by A1,Th11;
A14: P1 (*) (Q2 (*) P2) = G33 by A1,A8,Th10;
P2 (*) (Q2 (*) P2) = P2 (*) Q2 (*) P2 by A1,A8,Th10
.= P2 by A1,A8,Th11;
then H = Q2 (*) P2 by A11,A14,A1,A8,CAT_6:35;
hence P2 is isomorphism by A8,A13,A11,A12,A1;
end;
theorem
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
proof
let C1,C2,C3,C4,C5,C6 be category;
let F1 be Functor of C1,C2;
let F2 be Functor of C2,C3;
let F3 be Functor of C1,C4;
let F4 be Functor of C2,C5;
let F5 be Functor of C3,C6;
let F6 be Functor of C4,C5;
let F7 be Functor of C5,C6;
assume
A1: F1 is covariant & F2 is covariant & F3 is covariant & F4 is covariant &
F5 is covariant & F6 is covariant & F7 is covariant;
assume
A2: C2,F2,F4 is_pullback_of F5,F7;
then
A3: F5 (*) F2 = F7 (*) F4 &
for D1 being category, G1 being Functor of D1,C3, G2 being Functor of D1,C5
st G1 is covariant & G2 is covariant & F5 (*) G1 = F7 (*) G2
holds ex H being Functor of D1,C2 st H is covariant &
F2 (*) H = G1 & F4 (*) H = G2
& for H1 being Functor of D1,C2 st H1 is covariant &
F2 (*) H1 = G1 & F4 (*) H1 = G2 holds H = H1 by A1,Def20;
hereby
assume
A4: C1,F1,F3 is_pullback_of F4,F6;
then
A5: F4 (*) F1 = F6 (*) F3 & for D1 being category,
G1 being Functor of D1,C2, G2 being Functor of D1,C4
st G1 is covariant & G2 is covariant & F4 (*) G1 = F6 (*) G2
holds ex H being Functor of D1,C1 st H is covariant &
F1 (*) H = G1 & F3 (*) H = G2
& for H1 being Functor of D1,C1 st H1 is covariant &
F1 (*) H1 = G1 & F3 (*) H1 = G2 holds H = H1 by A1,Def20;
A6: F7(*)F6 is covariant & F2(*)F1 is covariant &
F3 is covariant by A1,CAT_6:35;
A7: F5 (*) (F2(*)F1) = F5 (*) F2 (*) F1 by A1,Th10
.= F7 (*) (F6 (*) F3) by A3,A5,Th10,A1
.= (F7(*)F6) (*) F3 by A1,Th10;
for D1 being category,
G1 being Functor of D1,C3, G2 being Functor of D1,C4
st G1 is covariant & G2 is covariant & F5 (*) G1 = (F7(*)F6) (*) G2
holds ex H being Functor of D1,C1 st H is covariant &
(F2(*)F1) (*) H = G1 & F3 (*) H = G2
& for H1 being Functor of D1,C1 st H1 is covariant &
(F2(*)F1) (*) H1 = G1 & F3 (*) H1 = G2 holds H = H1
proof
let D1 be category;
let G1 be Functor of D1,C3;
let G2 be Functor of D1,C4;
assume
A8: G1 is covariant;
assume
A9: G2 is covariant;
assume
A10: F5 (*) G1 = (F7(*)F6) (*) G2;
A11: F6(*)G2 is covariant by A1,A9,CAT_6:35;
A12: F5 (*) G1 = F7 (*) (F6(*)G2) by A10,A9,A1,Th10;
consider G3 be Functor of D1,C2 such that
A13: G3 is covariant & F2 (*) G3 = G1 & F4 (*) G3 = F6(*)G2
& for H1 being Functor of D1,C2 st H1 is covariant &
F2 (*) H1 = G1 & F4 (*) H1 = F6(*)G2
holds G3 = H1 by A11,A12,A2,A8,A1,Def20;
consider H be Functor of D1,C1 such that
A14: H is covariant & F1 (*) H = G3 & F3 (*) H = G2
& for H1 being Functor of D1,C1 st H1 is covariant &
F1 (*) H1 = G3 & F3 (*) H1 = G2
holds H = H1 by A13,A9,A4,A1,Def20;
take H;
thus H is covariant by A14;
thus (F2(*)F1) (*) H = G1 by A1,A13,A14,Th10;
thus F3 (*) H = G2 by A14;
let H1 be Functor of D1,C1;
assume
A15: H1 is covariant;
assume
A16: (F2(*)F1) (*) H1 = G1;
assume
A17: F3 (*) H1 = G2;
A18: F2 (*) (F1(*)H1) = G1 by A1,A15,A16,Th10;
F4 (*) (F1(*)H1) = F4(*)F1 (*) H1 by A1,A15,Th10
.= F6(*)G2 by A15,A17,A5,Th10,A1;
then G3 = F1(*)H1 by A18,A13,A1,A15,CAT_6:35;
hence H = H1 by A15,A17,A14;
end;
hence C1,F2(*)F1,F3 is_pullback_of F5,F7(*)F6 by A6,A1,A7,Def20;
thus F4 (*) F1 = F6 (*) F3 by A4,A1,Def20;
end;
A19: F7(*)F6 is covariant & F2(*)F1 is covariant by A1,CAT_6:35;
assume
A20: C1,F2(*)F1,F3 is_pullback_of F5,F7(*)F6;
assume
A21: F4 (*) F1 = F6 (*) F3;
for D1 being category,
G1 being Functor of D1,C2, G2 being Functor of D1,C4
st G1 is covariant & G2 is covariant & F4 (*) G1 = F6 (*) G2
holds ex H being Functor of D1,C1 st H is covariant &
F1 (*) H = G1 & F3 (*) H = G2
& for H1 being Functor of D1,C1 st H1 is covariant &
F1 (*) H1 = G1 & F3 (*) H1 = G2 holds H = H1
proof
let D1 be category;
let G1 be Functor of D1,C2;
let G2 be Functor of D1,C4;
assume
A22: G1 is covariant;
assume
A23: G2 is covariant;
assume
A24: F4 (*) G1 = F6 (*) G2;
set G11 = F2 (*) G1;
A25: G11 is covariant by A1,A22,CAT_6:35;
A26: F5 (*) G11 = (F5(*)F2) (*) G1 by A22,A1,Th10
.= F7 (*) (F6 (*) G2) by A24,A22,A3,Th10,A1
.= (F7(*)F6) (*) G2 by A23,A1,Th10;
consider H be Functor of D1,C1 such that
A27: H is covariant & (F2(*)F1) (*) H = G11 & F3 (*) H = G2
& for H1 being Functor of D1,C1 st H1 is covariant &
(F2(*)F1) (*) H1 = G11 & F3 (*) H1 = G2
holds H = H1 by A1,A26,A23,A25,A20,A19,Def20;
take H;
thus H is covariant by A27;
set G22 = F4 (*) G1;
A28: G11 is covariant & G22 is covariant by A1,A22,CAT_6:35;
A29: F5 (*) G11 = (F5(*)F2) (*) G1 by A22,A1,Th10
.= F7 (*) G22 by A22,A3,Th10,A1;
consider H2 be Functor of D1,C2 such that
A30: H2 is covariant & F2 (*) H2 = G11 & F4 (*) H2 = G22
& for H1 being Functor of D1,C2 st H1 is covariant &
F2 (*) H1 = G11 & F4 (*) H1 = G22
holds H2 = H1 by A29,A28,A2,A1,Def20;
A31: H2 = G1 by A22,A30;
A32: F2 (*) (F1 (*) H) = F2 (*) G1 by A1,A27,Th10;
F4 (*) (F1 (*) H) = (F4 (*) F1) (*) H by A1,A27,Th10
.= F4 (*) G1 by A27,A24,A21,A1,Th10;
hence F1 (*) H = G1 by A30,A32,A31,A1,A27,CAT_6:35;
thus F3 (*) H = G2 by A27;
let H1 be Functor of D1,C1;
assume
A33: H1 is covariant;
assume
A34: F1 (*) H1 = G1;
A35: (F2(*)F1) (*) H1 = G11 by A1,A33,A34,Th10;
assume F3 (*) H1 = G2;
hence H = H1 by A33,A27,A35;
end;
hence C1,F1,F3 is_pullback_of F4,F6 by A21,A1,Def20;
end;
theorem Th51:
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
proof
let C,C1,C2 be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
assume
A1: F1 is covariant & F2 is covariant;
reconsider car = {[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} as set;
set comp = {[[x1,x2],x3] where x1,x2,x3 is Element of car:
x1 in car & x2 in car & x3 in car & for f11,f12,f13 being morphism of C1,
f21,f22,f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] &
x3 = [f13,f23] holds f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 &
f23 = f21 (*) f22};
for x being object st x in comp holds x in [:[:car,car:],car:]
proof
let x be object;
assume x in comp;
then consider x1,x2,x3 be Element of car such that
A2: x = [[x1,x2],x3] &
x1 in car & x2 in car & x3 in car & for f11,f12,f13 being morphism of C1,
f21,f22,f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] &
x3 = [f13,f23] holds f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 &
f23 = f21 (*) f22;
[x1,x2] in [:car,car:] by A2,ZFMISC_1:def 2;
hence thesis by A2,ZFMISC_1:def 2;
end;
then reconsider comp as Relation of [:car,car:],car by TARSKI:def 3;
for x,y1,y2 being object st [x,y1] in comp & [x,y2] in comp
holds y1 = y2
proof
let x,y1,y2 be object;
assume [x,y1] in comp;
then consider x11,x12,x13 be Element of car such that
A3: [x,y1] = [[x11,x12],x13] & x11 in car & x12 in car & x13 in car &
for f11,f12,f13 being morphism of C1,
f21,f22,f23 being morphism of C2 st x11 = [f11,f21] & x12 = [f12,f22] &
x13 = [f13,f23] holds f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 &
f23 = f21 (*) f22;
assume [x,y2] in comp;
then consider x21,x22,x23 be Element of car such that
A4: [x,y2] = [[x21,x22],x23] & x21 in car & x22 in car & x23 in car &
for f11,f12,f13 being morphism of C1,
f21,f22,f23 being morphism of C2 st x21 = [f11,f21] & x22 = [f12,f22] &
x23 = [f13,f23] holds f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 &
f23 = f21 (*) f22;
A5: x = [x11,x12] & y1 = x13 by A3,XTUPLE_0:1;
A6: x = [x21,x22] & y2 = x23 by A4,XTUPLE_0:1;
A7: x11 = x21 & x12 = x22 by A5,A6,XTUPLE_0:1;
consider f11 be morphism of C1, f21 be morphism of C2 such that
A8: x11 = [f11,f21] & f11 in the carrier of C1 & f21 in the carrier of C2 &
F1.f11 = F2.f21 by A3;
consider f12 be morphism of C1, f22 be morphism of C2 such that
A9: x12 = [f12,f22] & f12 in the carrier of C1 & f22 in the carrier of C2 &
F1.f12 = F2.f22 by A3;
consider f13 be morphism of C1, f23 be morphism of C2 such that
A10: x13 = [f13,f23] & f13 in the carrier of C1 & f23 in the carrier of C2 &
F1.f13 = F2.f23 by A3;
consider f213 be morphism of C1, f223 be morphism of C2 such that
A11: x23 = [f213,f223] & f213 in the carrier of C1 &
f223 in the carrier of C2 & F1.f213 = F2.f223 by A4;
A12: f13 = f11 (*) f12 & f23 = f21 (*) f22 by A3,A8,A9,A10;
f213 = f11 (*) f12 & f223 = f21 (*) f22 by A8,A9,A11,A4,A7;
hence thesis by A6,A12,A10,A11,A3,XTUPLE_0:1;
end;
then reconsider comp as PartFunc of [:car,car:],car by FUNCT_1:def 1;
set D = CategoryStr(# car, comp #);
A13: for g1,g2 being morphism of D st g1 |> g2 holds
ex f11,f12,f13 being morphism of C1, f21,f22,f23 being morphism of C2 st
g1 = [f11,f21] & g2 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22 &
g1(*)g2 = [f13,f23]
proof
let g1,g2 be morphism of D;
assume
A14: g1 |> g2;
g1 in the carrier of D by A14,Th1,CAT_6:1;
then consider f11 be morphism of C1, f21 be morphism of C2 such that
A15: g1 = [f11,f21] & f11 in the carrier of C1 & f21 in the carrier of C2 &
F1.f11 = F2.f21;
g2 in the carrier of D by A14,Th1,CAT_6:1;
then consider f12 be morphism of C1, f22 be morphism of C2 such that
A16: g2 = [f12,f22] & f12 in the carrier of C1 & f22 in the carrier of C2 &
F1.f12 = F2.f22;
[g1,g2] in dom the composition of D by A14,CAT_6:def 2;
then consider y be object such that
A17: [[g1,g2],y] in comp by XTUPLE_0:def 12;
consider x1,x2,x3 be Element of car such that
A18: [[g1,g2],y] = [[x1,x2],x3] & x1 in car & x2 in car & x3 in car &
for f11,f12,f13 being morphism of C1,
f21,f22,f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] &
x3 = [f13,f23] holds f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 &
f23 = f21 (*) f22 by A17;
consider f13 be morphism of C1, f23 be morphism of C2 such that
A19: x3 = [f13,f23] & f13 in the carrier of C1 & f23 in the carrier of C2 &
F1.f13 = F2.f23 by A18;
[x1,x2] = [g1,g2] & y = x3 by A18,XTUPLE_0:1;
then
A20: x1 = g1 & x2 = g2 by XTUPLE_0:1;
take f11,f12,f13, f21,f22,f23;
thus g1 = [f11,f21] & g2 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22
by A15,A16;
thus f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22
by A20,A18,A19,A15,A16;
thus g1(*)g2 = (the composition of D).(g1,g2) by A14,CAT_6:def 3
.= (the composition of D).[g1,g2] by BINOP_1:def 1
.= y by A17,FUNCT_1:1
.= [f13,f23] by A19,A18,XTUPLE_0:1;
end;
A21: F1 is multiplicative & F2 is multiplicative by A1,CAT_6:def 25;
A22: for g1,g2 being morphism of D st
ex f11,f12 being morphism of C1, f21,f22 being morphism of C2 st
g1 = [f11,f21] & g2 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 holds g1 |> g2
proof
let g1,g2 be morphism of D;
given f11,f12 be morphism of C1, f21,f22 be morphism of C2 such that
A23: g1 = [f11,f21] & g2 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22;
set x3 = [f11(*)f12,f21(*)f22];
A24: f11 in the carrier of C1 & f12 in the carrier of C1 &
f21 in the carrier of C2 & f22 in the carrier of C2 by A23,Th1,CAT_6:1;
A25: f11(*)f12 in the carrier of C1 &
f21(*)f22 in the carrier of C2 by A23,Th1,CAT_6:1;
F1.(f11(*)f12) = (F1.f11)(*)(F1.f12) by A21,A23,CAT_6:def 23
.= F2.(f21(*)f22) by A21,A23,CAT_6:def 23;
then x3 in car by A25;
then reconsider g3 = x3 as morphism of D by CAT_6:def 1;
reconsider x1 = g1, x2= g2, x3 = g3 as Element of car by CAT_6:def 1;
A26: x1 in car & x2 in car by A23,A24;
for f011,f012,f013 being morphism of C1,
f021,f022,f023 being morphism of C2 st x1 = [f011,f021] &
x2 = [f012,f022] & x3 = [f013,f023] holds f011 |> f012 & f021 |> f022 &
f013 = f011 (*) f012 & f023 = f021 (*) f022
proof
let f011,f012,f013 be morphism of C1;
let f021,f022,f023 be morphism of C2;
assume x1 = [f011,f021] & x2 = [f012,f022] & x3 = [f013,f023];
then f11 = f011 & f21 = f021 & f12 = f012 & f22 = f022
& f11(*)f12 = f013 & f21(*)f22 = f023 by A23,XTUPLE_0:1;
hence thesis by A23;
end;
then [[x1,x2],x3] in the composition of D by A26;
then [g1,g2] in dom the composition of D by XTUPLE_0:def 12;
hence g1 |> g2 by CAT_6:def 2;
end;
for g,g1,g2 being morphism of D st g1|>g2 holds g1(*)g2 |> g iff g2 |> g
proof
let g,g1,g2 be morphism of D;
assume g1 |> g2;
then consider f11,f12,f13 be morphism of C1,
f21,f22,f23 be morphism of C2 such that
A27: g1 = [f11,f21] & g2 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22 &
g1(*)g2 = [f13,f23] by A13;
hereby
assume g1 (*) g2 |> g;
then consider f011,f012,f013 be morphism of C1,
f021,f022,f023 be morphism of C2 such that
A28: g1 (*) g2 = [f011,f021] & g = [f012,f022] & F1.f011 = F2.f021 &
F1.f012 = F2.f022 & f011 |> f012 & f021 |> f022 & f013 = f011(*)f012 &
f023 = f021(*)f022 & (g1(*)g2) (*) g = [f013,f023] by A13;
A29: f13 = f011 & f23 = f021 by A27,A28,XTUPLE_0:1;
C1 is left_composable & C2 is left_composable by CAT_6:def 11;
then f12 |> f012 & f22 |> f022 by A27,A28,A29,CAT_6:def 8;
hence g2 |> g by A22,A27,A28;
end;
assume g2 |> g;
then consider f011,f012,f013 be morphism of C1,
f021,f022,f023 be morphism of C2 such that
A30: g2 = [f011,f021] & g = [f012,f022] & F1.f011 = F2.f021 &
F1.f012 = F2.f022 & f011 |> f012 & f021 |> f022 & f013 = f011(*)f012 &
f023 = f021(*)f022 & g2 (*) g = [f013,f023] by A13;
A31: f12 = f011 & f22 = f021 by A27,A30,XTUPLE_0:1;
C1 is left_composable & C2 is left_composable by CAT_6:def 11;
then
A32: f13 |> f012 & f23 |> f022 by A27,A30,A31,CAT_6:def 8;
F1.f13 = (F1.f11) (*) (F1.f12) by A21,A27,CAT_6:def 23
.= F2.f23 by A21,A27,CAT_6:def 23;
hence g1 (*) g2 |> g by A22,A27,A30,A32;
end;
then
A33: D is left_composable by CAT_6:def 8;
A34: for g,g1,g2 being morphism of D st g1|>g2 holds g |> g1(*)g2 iff g |> g1
proof
let g,g1,g2 be morphism of D;
assume g1 |> g2;
then consider f11,f12,f13 be morphism of C1,
f21,f22,f23 be morphism of C2 such that
A35: g1 = [f11,f21] & g2 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22 &
g1(*)g2 = [f13,f23] by A13;
hereby
assume g |> g1 (*) g2;
then consider f011,f012,f013 be morphism of C1,
f021,f022,f023 be morphism of C2 such that
A36: g = [f011,f021] & g1 (*) g2 = [f012,f022] & F1.f011 = F2.f021 &
F1.f012 = F2.f022 & f011 |> f012 & f021 |> f022 & f013 = f011(*)f012 &
f023 = f021(*)f022 & g (*) (g1(*)g2) = [f013,f023] by A13;
A37: f13 = f012 & f23 = f022 by A35,A36,XTUPLE_0:1;
C1 is right_composable & C2 is right_composable by CAT_6:def 11;
then f011 |> f11 & f021 |> f21 by A35,A36,A37,CAT_6:def 9;
hence g |> g1 by A22,A35,A36;
end;
assume g |> g1;
then consider f011,f012,f013 be morphism of C1,
f021,f022,f023 be morphism of C2 such that
A38: g = [f011,f021] & g1 = [f012,f022] & F1.f011 = F2.f021 &
F1.f012 = F2.f022 & f011 |> f012 & f021 |> f022 & f013 = f011(*)f012 &
f023 = f021(*)f022 & g (*) g1 = [f013,f023] by A13;
A39: f11 = f012 & f21 = f022 by A35,A38,XTUPLE_0:1;
C1 is right_composable & C2 is right_composable by CAT_6:def 11;
then
A40: f011 |> f13 & f021 |> f23 by A35,A38,A39,CAT_6:def 9;
F1.f13 = (F1.f11) (*) (F1.f12) by A21,A35,CAT_6:def 23
.= F2.f23 by A21,A35,CAT_6:def 23;
hence g |> g1 (*) g2 by A22,A35,A38,A40;
end;
for g1 being morphism of D st g1 in the carrier of D holds
ex g being morphism of D st g |> g1 & g is left_identity
proof
let g1 be morphism of D;
assume g1 in the carrier of D;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A41: g1 = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 &
F1.f1 = F2.f2;
A42: C1 is non empty by A41;
A43: cod f1 in the carrier of C1 by A42,Th2;
then reconsider c1 = cod f1 as morphism of C1 by CAT_6:def 1;
A44: C2 is non empty by A41;
A45: cod f2 in the carrier of C2 by A44,Th2;
then reconsider c2 = cod f2 as morphism of C2 by CAT_6:def 1;
A46: C is non empty by A1,A42,CAT_6:31;
set g = [c1,c2];
A47: F1.c1 = F1.(cod f1) by A42,CAT_6:def 21
.= cod(F1.f1) by A42,A46,A1,CAT_6:32
.= F2.(cod f2) by A41,A44,A46,A1,CAT_6:32
.= F2.c2 by A44,CAT_6:def 21;
then g in car by A43,A45;
then reconsider g = [c1,c2] as morphism of D by CAT_6:def 1;
take g;
consider c11 be morphism of C1 such that
A48: c1 = c11 & c11 |> f1 & c11 is identity by A42,CAT_6:def 19;
consider c22 be morphism of C2 such that
A49: c2 = c22 & c22 |> f2 & c22 is identity by A44,CAT_6:def 19;
thus g |> g1 by A22,A47,A41,A48,A49;
for g1 being morphism of D st g |> g1 holds g (*) g1 = g1
proof
let g1 be morphism of D;
assume g |> g1;
then consider f11,f12,f13 be morphism of C1,
f21,f22,f23 be morphism of C2 such that
A50: g = [f11,f21] & g1 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22 &
g (*) g1 = [f13,f23] by A13;
A51: c11 = f11 & c22 = f21 by A48,A49,A50,XTUPLE_0:1;
f13 = f12 & f23 = f22
by A51,A50,CAT_6:def 4,A48,A49,CAT_6:def 14;
hence g (*) g1 = g1 by A50;
end;
hence g is left_identity by CAT_6:def 4;
end;
then
A52: D is with_left_identities by CAT_6:def 6;
A53: for g1 being morphism of D st g1 in the carrier of D holds
ex g being morphism of D st g1 |> g & g is right_identity
proof
let g1 be morphism of D;
assume g1 in the carrier of D;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A54: g1 = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 &
F1.f1 = F2.f2;
A55: C1 is non empty by A54;
A56: dom f1 in the carrier of C1 by A55,Th2;
then reconsider d1 = dom f1 as morphism of C1 by CAT_6:def 1;
A57: C2 is non empty by A54;
A58: dom f2 in the carrier of C2 by A57,Th2;
then reconsider d2 = dom f2 as morphism of C2 by CAT_6:def 1;
A59: C is non empty by A1,A55,CAT_6:31;
set g = [d1,d2];
A60: F1.d1 = F1.(dom f1) by A55,CAT_6:def 21
.= dom(F1.f1) by A55,A59,A1,CAT_6:32
.= F2.(dom f2) by A54,A57,A59,A1,CAT_6:32
.= F2.d2 by A57,CAT_6:def 21;
then g in car by A56,A58;
then reconsider g = [d1,d2] as morphism of D by CAT_6:def 1;
take g;
consider d11 be morphism of C1 such that
A61: d1 = d11 & f1 |> d11 & d11 is identity by A55,CAT_6:def 18;
consider d22 be morphism of C2 such that
A62: d2 = d22 & f2 |> d22 & d22 is identity by A57,CAT_6:def 18;
thus g1 |> g by A22,A60,A54,A61,A62;
for g1 being morphism of D st g1 |> g holds g1 (*) g = g1
proof
let g1 be morphism of D;
assume g1 |> g;
then consider f11,f12,f13 be morphism of C1,
f21,f22,f23 be morphism of C2 such that
A63: g1 = [f11,f21] & g = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22 &
g1 (*) g = [f13,f23] by A13;
A64: d11 = f12 & d22 = f22 by A61,A62,A63,XTUPLE_0:1;
f13 = f11 & f23 = f21
by A64,A63,CAT_6:def 5,A61,A62,CAT_6:def 14;
hence g1 (*) g = g1 by A63;
end;
hence g is right_identity by CAT_6:def 5;
end;
for g1,g2,g3 being morphism of D st
g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3
holds g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3
proof
let g1,g2,g3 be morphism of D;
assume g1 |> g2;
then consider f011,f012,f013 be morphism of C1,
f021,f022,f023 be morphism of C2 such that
A65: g1 = [f011,f021] & g2 = [f012,f022] & F1.f011 = F2.f021 &
F1.f012 = F2.f022 & f011 |> f012 & f021 |> f022 & f013 = f011(*)f012 &
f023 = f021(*)f022 & g1(*)g2 = [f013,f023] by A13;
assume g2 |> g3;
then consider f111,f112,f113 be morphism of C1,
f121,f122,f123 be morphism of C2 such that
A66: g2 = [f111,f121] & g3 = [f112,f122] & F1.f111 = F2.f121 &
F1.f112 = F2.f122 & f111 |> f112 & f121 |> f122 & f113 = f111(*)f112 &
f123 = f121(*)f122 & g2(*)g3 = [f113,f123] by A13;
assume g1 (*) g2 |> g3;
then consider f211,f212,f213 be morphism of C1,
f221,f222,f223 be morphism of C2 such that
A67: g1 (*) g2 = [f211,f221] & g3 = [f212,f222] & F1.f211 = F2.f221 &
F1.f212 = F2.f222 & f211 |> f212 & f221 |> f222 & f213 = f211(*)f212 &
f223 = f221(*)f222 & (g1(*)g2)(*)g3 = [f213,f223] by A13;
assume g1 |> g2 (*) g3;
then consider f311,f312,f313 be morphism of C1,
f321,f322,f323 be morphism of C2 such that
A68: g1 = [f311,f321] & g2(*)g3 = [f312,f322] & F1.f311 = F2.f321 &
F1.f312 = F2.f322 & f311 |> f312 & f321 |> f322 & f313 = f311(*)f312 &
f323 = f321(*)f322 & g1(*)(g2(*)g3) = [f313,f323] by A13;
A69: f113 = f312 & f123 = f322 by A66,A68,XTUPLE_0:1;
A70: f013 = f211 & f023 = f221 by A65,A67,XTUPLE_0:1;
A71: f011 = f311 & f021 = f321 by A65,A68,XTUPLE_0:1;
A72: f012 = f111 & f022 = f121 by A65,A66,XTUPLE_0:1;
A73: f112 = f212 & f122 = f222 by A66,A67,XTUPLE_0:1;
A74: f313 = f213 by A67,A65,A66,A68,A69,A70,A71,A72,A73,CAT_6:def 10;
thus g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3
by A68,A67,A74,A65,A66,A69,A70,A71,A72,A73,CAT_6:def 10;
end;
then reconsider D as strict category
by A53,A52,A34,A33,CAT_6:def 10,def 11,def 12,def 7,def 9;
A75: for x being object holds x in comp iff
x in {[[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}
proof
let x be object;
hereby
assume x in comp;
then consider x1,x2,x3 be Element of car such that
A76: x = [[x1,x2],x3] & x1 in car & x2 in car & x3 in car &
for f11,f12,f13 being morphism of C1,
f21,f22,f23 being morphism of C2 st x1 = [f11,f21] & x2 = [f12,f22] &
x3 = [f13,f23] holds f11 |> f12 & f21 |> f22 & f13 = f11 (*) f12 &
f23 = f21 (*) f22;
reconsider f1=x1, f2=x2, f3=x3 as morphism of D by CAT_6:def 1;
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 by A76;
hence x in {[[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} by A76;
end;
assume x in {[[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};
then consider f1,f2,f3 be morphism of D such that
A77: x = [[f1,f2],f3] & 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;
reconsider x1=f1, x2=f2, x3=f3 as Element of car by A77;
thus x in comp by A77;
end;
ex P1 being Functor of D,C1, P2 being Functor of D,C2 st
P1 is covariant & P2 is covariant & 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
proof
per cases;
suppose
A78: D is empty;
then reconsider D0 = D as empty category;
reconsider P1 = the covariant Functor of D0,C1 as Functor of D,C1;
reconsider P2 = the covariant Functor of D0,C2 as Functor of D,C2;
take P1,P2;
thus P1 is covariant & P2 is covariant & F1(*)P1 = F2(*)P2;
let D1 be category, G1 be Functor of D1,C1, G2 be Functor of D1,C2;
assume
A79: G1 is covariant;
assume
A80: G2 is covariant;
assume
A81: F1(*)G1 = F2(*)G2;
D1 is empty
proof
assume
A82: D1 is non empty;
then consider x be object such that
A83: x in the carrier of D1 by XBOOLE_0:def 1;
reconsider d = x as morphism of D1 by A83,CAT_6:def 1;
set f1 = G1.d;
set f2 = G2.d;
A84: C1 is non empty & C2 is non empty by A82,A79,A80,CAT_6:31;
A85: x in dom G1 & x in dom G2 by A84,A83,FUNCT_2:def 1;
A86: G1.d = G1.x by A82,CAT_6:def 21;
A87: G2.d = G2.x by A82,CAT_6:def 21;
A88: F1.f1 = F1.(G1.x) by A86,A84,CAT_6:def 21
.= (G1*F1).x by A85,FUNCT_1:13
.= (F2(*)G2).x by A81,A1,A79,CAT_6:def 27
.= (G2*F2).x by A1,A80,CAT_6:def 27
.= F2.(G2.x) by A85,FUNCT_1:13
.= F2.f2 by A87,A84,CAT_6:def 21;
f1 in the carrier of C1 & f2 in the carrier of C2 by A84,Th1;
then [f1,f2] in the carrier of D by A88;
hence contradiction by A78;
end;
then reconsider D01 = D1 as empty category;
reconsider H = the covariant Functor of D01,D as Functor of D1,D;
take H;
thus H is covariant & P1(*)H = G1 & P2(*)H = G2;
let H1 be Functor of D1,D;
assume H1 is covariant & P1(*)H1 = G1 & P2(*)H1 = G2;
thus H = H1;
end;
suppose
A89: D is non empty;
deffunc PF1(object) = $1`1;
A90: for x being object st x in the carrier of D
holds PF1(x) in the carrier of C1
proof
let x be object;
assume x in the carrier of D;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A91: x = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 &
F1.f1 = F2.f2;
thus PF1(x) in the carrier of C1 by A91;
end;
consider P1 be Function of the carrier of D,the carrier of C1 such that
A92: for x being object st x in the carrier of D holds P1.x = PF1(x)
from FUNCT_2:sch 2(A90);
reconsider P1 as Functor of D,C1;
deffunc PF2(object) = $1`2;
A93: for x being object st x in the carrier of D
holds PF2(x) in the carrier of C2
proof
let x be object;
assume x in the carrier of D;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A94: x = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 &
F1.f1 = F2.f2;
thus PF2(x) in the carrier of C2 by A94;
end;
consider P2 be Function of the carrier of D,the carrier of C2 such that
A95: for x being object st x in the carrier of D holds P2.x = PF2(x)
from FUNCT_2:sch 2(A93);
reconsider P2 as Functor of D,C2;
take P1,P2;
A96: for g being morphism of D st g is identity holds
ex f1 being morphism of C1, f2 being morphism of C2 st g = [f1,f2]
& f1 is identity & f2 is identity
proof
let g be morphism of D;
assume
A97: g is identity;
g in the carrier of D by A89,Th1;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A98: g = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 &
F1.f1 = F2.f2;
take f1,f2;
A99: C1 is non empty by A98;
then consider d1 be morphism of C1 such that
A100: dom f1 = d1 & f1 |> d1 & d1 is identity by CAT_6:def 18;
A101: C2 is non empty by A98;
then consider d2 be morphism of C2 such that
A102: dom f2 = d2 & f2 |> d2 & d2 is identity by CAT_6:def 18;
set g1 = [d1,d2];
A103: C is non empty by A1,A99,CAT_6:31;
A104: d1 in the carrier of C1 & d2 in the carrier of C2 by A99,A101,Th1;
A105: F1.d1 = F1.(dom f1) by A99,A100,CAT_6:def 21
.= dom(F2.f2) by A98,A1,A99,A103,CAT_6:32
.= F2.(dom f2) by A1,A101,A103,CAT_6:32
.= F2.d2 by A101,A102,CAT_6:def 21;
then g1 in the carrier of D by A104;
then reconsider g1 as morphism of D by CAT_6:def 1;
A106: g |> g1 by A22,A98,A105,A100,A102;
thus g = [f1,f2] by A98;
consider f11,f12,f13 be morphism of C1,
f21,f22,f23 be morphism of C2 such that
A107: g = [f11,f21] & g1 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22 &
g(*)g1 = [f13,f23] by A13,A22,A98,A105,A100,A102;
A108: f11 = f1 & f21 = f2 & f12 = d1 & f22 = d2 by A98,A107,XTUPLE_0:1;
f1 = f1(*)d1 & f2 = f2(*)d2 by A100,A102,CAT_6:def 5,def 14;
then g = g1 by A106,A97,CAT_6:def 14,def 4,A108,A107;
hence thesis by A100,A102,A98,XTUPLE_0:1;
end;
for g being morphism of D st g is identity holds P1.g is identity
& P2.g is identity
proof
let g be morphism of D;
assume g is identity;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A109: g = [f1,f2] & f1 is identity & f2 is identity by A96;
reconsider x = g as object;
P1.g = P1.x by CAT_6:def 21,A89
.= PF1(x) by A92,A89,Th1
.= f1 by A109;
hence P1.g is identity by A109;
P2.g = P2.x by CAT_6:def 21,A89
.= PF2(x) by A95,A89,Th1
.= f2 by A109;
hence P2.g is identity by A109;
end;
then (for g being morphism of D st g is identity holds P1.g is identity)
& (for g being morphism of D st g is identity holds P2.g is identity);
then
A110: P1 is identity-preserving & P2 is identity-preserving by CAT_6:def 22;
for g1,g2 being morphism of D st g1 |> g2 holds
P1.g1 |> P1.g2 & P1.(g1 (*) g2) = (P1.g1) (*) (P1.g2) &
P2.g1 |> P2.g2 & P2.(g1 (*) g2) = (P2.g1) (*) (P2.g2)
proof
let g1,g2 be morphism of D;
assume g1 |> g2;
then consider f11,f12,f13 be morphism of C1,
f21,f22,f23 be morphism of C2 such that
A111: g1 = [f11,f21] & g2 = [f12,f22] & F1.f11 = F2.f21 & F1.f12 = F2.f22 &
f11 |> f12 & f21 |> f22 & f13 = f11(*)f12 & f23 = f21(*)f22 &
g1(*)g2 = [f13,f23] by A13;
reconsider x1 = g1, x2 = g2, x12 = g1(*)g2 as object;
A112: P1.g1 = P1.x1 by CAT_6:def 21,A89
.= PF1(x1) by A92,A89,Th1
.= f11 by A111;
A113: P1.g2 = P1.x2 by CAT_6:def 21,A89
.= PF1(x2) by A92,A89,Th1
.= f12 by A111;
A114: P1.(g1(*)g2) = P1.x12 by CAT_6:def 21,A89
.= PF1(x12) by A92,A89,Th1
.= f13 by A111;
thus P1.g1 |> P1.g2 by A112,A113,A111;
thus P1.(g1 (*) g2) = (P1.g1) (*) (P1.g2) by A112,A113,A114,A111;
A115: P2.g1 = P2.x1 by CAT_6:def 21,A89
.= PF2(x1) by A95,A89,Th1
.= f21 by A111;
A116: P2.g2 = P2.x2 by CAT_6:def 21,A89
.= PF2(x2) by A95,A89,Th1
.= f22 by A111;
A117: P2.(g1(*)g2) = P2.x12 by CAT_6:def 21,A89
.= PF2(x12) by A95,A89,Th1
.= f23 by A111;
thus P2.g1 |> P2.g2 by A115,A116,A111;
thus P2.(g1 (*) g2) = (P2.g1) (*) (P2.g2) by A115,A116,A117,A111;
end;
then (for g1,g2 being morphism of D st g1 |> g2 holds
P1.g1 |> P1.g2 & P1.(g1 (*) g2) = (P1.g1) (*) (P1.g2))&
(for g1,g2 being morphism of D st g1 |> g2 holds
P2.g1 |> P2.g2 & P2.(g1 (*) g2) = (P2.g1) (*) (P2.g2));
hence
A118: P1 is covariant & P2 is covariant by A110,CAT_6:def 23,def 25;
for x being object st x in the carrier of D holds
(F1(*)P1).x = (F2(*)P2).x
proof
let x be object;
assume
A119: x in the carrier of D;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A120: x = [f1,f2] & f1 in the carrier of C1 & f2 in the carrier of C2 &
F1.f1 = F2.f2;
reconsider g = x as morphism of D by A119,CAT_6:def 1;
A121: P1.g = P1.x by CAT_6:def 21,A89
.= PF1(x) by A92,A119
.= f1 by A120;
A122: P2.g = P2.x by CAT_6:def 21,A89
.= PF2(x) by A95,A119
.= f2 by A120;
thus (F1(*)P1).x = (F1(*)P1).g by A89,CAT_6:def 21
.= F1.f1 by A121,A89,A1,A118,CAT_6:34
.= (F2(*)P2).g by A89,A1,A118,CAT_6:34,A122,A120
.= (F2(*)P2).x by A89,CAT_6:def 21;
end;
hence F1(*)P1 = F2(*)P2 by FUNCT_2:12;
let D1 be category;
let G1 be Functor of D1,C1;
let G2 be Functor of D1,C2;
assume
A123: G1 is covariant;
assume
A124: G2 is covariant;
assume
A125: F1(*)G1 = F2(*)G2;
deffunc H2(object) = [G1.$1,G2.$1];
A126: for x being object st x in the carrier of D1
holds H2(x) in the carrier of D
proof
let x be object;
assume
A127: x in the carrier of D1;
then
A128: D1 is non empty;
reconsider d = x as morphism of D1 by A127,CAT_6:def 1;
A129: C1 is non empty & C2 is non empty by A89,A118,CAT_6:31;
A130: G1.d in the carrier of C1 & G2.d in the carrier of C2 by A129,Th1;
A131: G1.d = G1.x & G2.d = G2.x by A128,CAT_6:def 21;
F1.(G1.d) = (F1(*)G1).d by A123,A128,A1,CAT_6:34
.= F2.(G2.d) by A124,A125,A128,A1,CAT_6:34;
hence H2(x) in the carrier of D by A130,A131;
end;
consider H be Function of the carrier of D1, the carrier of D such that
A132: for x being object st x in the carrier of D1 holds H.x = H2(x)
from FUNCT_2:sch 2(A126);
reconsider H as Functor of D1,D;
take H;
for d being morphism of D1 st d is identity holds H.d is identity
proof
let d be morphism of D1;
assume
A133: d is identity;
per cases;
suppose D1 is empty;
then H.d = the Object of D by CAT_6:def 21;
hence thesis by A89,CAT_6:22;
end;
suppose
A134: D1 is non empty;
for g1 being morphism of D st (H.d) |> g1 holds (H.d)(*)g1 = g1
proof
let g1 be morphism of D;
assume (H.d) |> g1;
then consider d1,f1,f13 be morphism of C1,
d2,f2,f23 be morphism of C2 such that
A135: H.d = [d1,d2] & g1 = [f1,f2] & F1.d1 = F2.d2 & F1.f1 = F2.f2 &
d1 |> f1 & d2 |> f2 & f13 = d1(*)f1 & f23 = d2(*)f2 &
(H.d)(*)g1 = [f13,f23] by A13;
reconsider x = d as object;
A136: G1.x = G1.d & G2.x = G2.d by A134,CAT_6:def 21;
H.d = H.x by A134,CAT_6:def 21
.= [G1.d,G2.d] by A136,A134,Th1,A132;
then d1 = G1.d & d2 = G2.d by A135,XTUPLE_0:1;
then d1 is identity & d2 is identity
by A133,CAT_6:def 22,A123,A124,CAT_6:def 25;
then d1(*)f1 = f1 & d2(*)f2 = f2 by A135,CAT_6:def 14,def 4;
hence (H.d)(*)g1 = g1 by A135;
end;
then
A137: H.d is left_identity by CAT_6:def 4;
for g1 being morphism of D st g1 |> (H.d) holds g1(*)(H.d) = g1
proof
let g1 be morphism of D;
assume g1 |> (H.d);
then consider f1,d1,f13 be morphism of C1,
f2,d2,f23 be morphism of C2 such that
A138: g1 = [f1,f2] & H.d = [d1,d2] & F1.f1 = F2.f2 & F1.d1 = F2.d2 &
f1 |> d1 & f2 |> d2 & f13 = f1(*)d1 & f23 = f2(*)d2 &
g1(*)(H.d) = [f13,f23] by A13;
reconsider x = d as object;
A139: G1.x = G1.d & G2.x = G2.d by A134,CAT_6:def 21;
H.d = H.x by A134,CAT_6:def 21
.= [G1.d,G2.d] by A139,A134,Th1,A132;
then d1 = G1.d & d2 = G2.d by A138,XTUPLE_0:1;
then d1 is identity & d2 is identity
by A133,CAT_6:def 22,A123,A124,CAT_6:def 25;
then f1(*)d1 = f1 & f2(*)d2 = f2 by A138,CAT_6:def 14,def 5;
hence g1(*)(H.d) = g1 by A138;
end;
hence H.d is identity by A137,CAT_6:def 5,def 14;
end;
end;
then
A140: H is identity-preserving by CAT_6:def 22;
for d1,d2 being morphism of D1 st d1 |> d2 holds
H.d1 |> H.d2 & H.(d1 (*) d2) = (H.d1) (*) (H.d2)
proof
let d1,d2 be morphism of D1;
assume
A141: d1 |> d2;
then
A142: D1 is non empty by CAT_6:1;
reconsider x1 = d1, x2 = d2 as object;
A143: G1.x1 = G1.d1 & G2.x1 = G2.d1 by A142,CAT_6:def 21;
A144: G1.x2 = G1.d2 & G2.x2 = G2.d2 by A142,CAT_6:def 21;
A145: G1 is multiplicative & G2 is multiplicative by A123,A124,CAT_6:def 25;
A146: d1 in the carrier of D1 by A141,Th1,CAT_6:1;
A147: H.d1 = H.x1 by A142,CAT_6:def 21
.= [G1.d1,G2.d1] by A143,A146,A132;
H.d1 in the carrier of D by A89,Th1;
then consider f11 be morphism of C1, f21 be morphism of C2 such that
A148: H.d1 = [f11,f21] & f11 in the carrier of C1 &
f21 in the carrier of C2 & F1.f11 = F2.f21;
A149: d2 in the carrier of D1 by A141,Th1,CAT_6:1;
A150: H.d2 = H.x2 by A142,CAT_6:def 21
.= [G1.d2,G2.d2] by A144,A149,A132;
H.d2 in the carrier of D by A89,Th1;
then consider f12 be morphism of C1, f22 be morphism of C2 such that
A151: H.d2 = [f12,f22] & f12 in the carrier of C1 &
f22 in the carrier of C2 & F1.f12 = F2.f22;
A152: f11 = G1.d1 & f21 = G2.d1 by A148,A147,XTUPLE_0:1;
A153: f12 = G1.d2 & f22 = G2.d2 by A151,A150,XTUPLE_0:1;
A154: G1.d1 |> G1.d2 & G1.(d1(*)d2) = (G1.d1)(*)(G1.d2)
by A141,A145,CAT_6:def 23;
A155: G2.d1 |> G2.d2 & G2.(d1(*)d2) = (G2.d1)(*)(G2.d2)
by A141,A145,CAT_6:def 23;
thus H.d1 |> H.d2 by A22,A152,A153,A154,A155,A148,A151;
consider f011,f012,f013 be morphism of C1,
f021,f022,f023 be morphism of C2 such that
A156: H.d1 = [f011,f021] & H.d2 = [f012,f022] & F1.f011 = F2.f021 &
F1.f012 = F2.f022 & f011 |> f012 & f021 |> f022 & f013 = f011(*)f012 &
f023 = f021(*)f022 & (H.d1)(*)(H.d2) = [f013,f023]
by A13,A22,A152,A153,A154,A155,A148,A151;
A157: f011 = G1.d1 & f021 = G2.d1 & f012 = G1.d2 & f022 = G2.d2
by A156,A150,A147,XTUPLE_0:1;
reconsider x12 = d1(*)d2 as object;
A158: G1.x12 = G1.(d1(*)d2) & G2.x12 = G2.(d1(*)d2) by A142,CAT_6:def 21;
thus H.(d1(*)d2) = H.x12 by A142,CAT_6:def 21
.= (H.d1) (*) (H.d2) by A154,A155,A156,A157,A158,A142,Th1,A132;
end;
hence
A159: H is covariant by A140,CAT_6:def 23,def 25;
for x being object st x in the carrier of D1 holds (P1(*)H).x = G1.x
proof
let x be object;
assume
A160: x in the carrier of D1;
then
A161: D1 is non empty;
reconsider d = x as morphism of D1 by A160,CAT_6:def 1;
A162: H.d = H.x by A161,CAT_6:def 21
.= [G1.x,G2.x] by A160,A132;
reconsider x1 = H.d as object;
thus (P1(*)H).x = (P1(*)H).d by A161,CAT_6:def 21
.= P1.(H.d) by A161,A118,A159,CAT_6:34
.= P1.x1 by A89,CAT_6:def 21
.= PF1([G1.x,G2.x]) by A92,A89,Th1,A162
.= G1.x;
end;
hence P1(*)H = G1 by FUNCT_2:12;
for x being object st x in the carrier of D1 holds (P2(*)H).x = G2.x
proof
let x be object;
assume
A163: x in the carrier of D1;
then
A164: D1 is non empty;
reconsider d = x as morphism of D1 by A163,CAT_6:def 1;
A165: H.d = H.x by A164,CAT_6:def 21
.= [G1.x,G2.x] by A163,A132;
reconsider x2 = H.d as object;
thus (P2(*)H).x = (P2(*)H).d by A164,CAT_6:def 21
.= P2.(H.d) by A164,A118,A159,CAT_6:34
.= P2.x2 by A89,CAT_6:def 21
.= PF2([G1.x,G2.x]) by A165,A95,A89,Th1
.= G2.x;
end;
hence P2(*)H = G2 by FUNCT_2:12;
let H1 be Functor of D1,D;
assume
A166: H1 is covariant;
assume
A167: P1(*)H1 = G1;
assume
A168: P2(*)H1 = G2;
for x being object st x in the carrier of D1 holds H.x = H1.x
proof
let x be object;
assume
A169: x in the carrier of D1;
then
A170: D1 is non empty;
reconsider d = x as morphism of D1 by A169,CAT_6:def 1;
A171: G1.x = G1.d & G2.x = G2.d by A170,CAT_6:def 21;
H1.d in the carrier of D by A89,Th1;
then consider f1 be morphism of C1, f2 be morphism of C2 such that
A172: H1.d = [f1,f2] & f1 in the carrier of C1 &
f2 in the carrier of C2 & F1.f1 = F2.f2;
reconsider x1 = H1.d as object;
A173: G1.d
= P1.(H1.d) by A167,A170,A166,A118,CAT_6:34
.= P1.x1 by A89,CAT_6:def 21
.= PF1([f1,f2]) by A172,A92,A89,Th1
.= f1;
A174: G2.d
= P2.(H1.d) by A168,A170,A166,A118,CAT_6:34
.= P2.x1 by A89,CAT_6:def 21
.= PF2([f1,f2]) by A172,A95,A89,Th1
.= f2;
thus H.x
= H1.d by A173,A174,A172,A171,A169,A132
.= H1.x by A170,CAT_6:def 21;
end;
hence H = H1 by FUNCT_2:12;
end;
end;
then
consider P1 be Functor of D,C1, P2 be Functor of D,C2 such that
A175: P1 is covariant & P2 is covariant & 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;
take D,P1,P2;
thus thesis by A75,A175,A1,Def20,TARSKI:2;
end;
definition
let C,C1,C2 be category;
let F1 be Functor of C1,C such that
A1: F1 is covariant;
let F2 be Functor of C2,C such that
A2: F2 is covariant;
mode pullback of F1,F2 -> triple object means :Def21:
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;
correctness
proof
consider D be strict category, P1 be Functor of D,C1,
P2 be Functor of D,C2 such that
A3: 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 by A1,A2,Th51;
take [D,P1,P2];
thus thesis by A3;
end;
end;
definition
let C,C1,C2 be category;
let F1 be Functor of C1,C such that
A1: F1 is covariant;
let F2 be Functor of C2,C such that
A2: F2 is covariant;
func [| F1, F2 |] -> strict category equals :Def22:
(the pullback of F1,F2)`1_3;
correctness
proof
set T = the pullback of F1,F2;
consider D be strict category, P1 be Functor of D,C1,
P2 be Functor of D,C2 such that
A3: T = [D,P1,P2] & P1 is covariant & P2 is covariant &
D,P1,P2 is_pullback_of F1,F2 by A1,A2,Def21;
thus thesis by A3;
end;
end;
definition
let C,C1,C2 be category;
let F1 be Functor of C1,C such that
A1: F1 is covariant;
let F2 be Functor of C2,C such that
A2: F2 is covariant;
func pr1(F1,F2) -> Functor of [|F1,F2|], C1 equals :Def23:
(the pullback of F1,F2)`2_3;
correctness
proof
set T = the pullback of F1,F2;
consider D be strict category, P1 be Functor of D,C1,
P2 be Functor of D,C2 such that
A3: T = [D,P1,P2] & P1 is covariant & P2 is covariant &
D,P1,P2 is_pullback_of F1,F2 by A1,A2,Def21;
[D,P1,P2]`1_3 = D & [D,P1,P2]`2_3 = P1;
then D = [|F1,F2|] by A1,A2,A3,Def22;
then reconsider P1 as Functor of [|F1,F2|],C1;
P1 = (the pullback of F1,F2)`2_3 by A3;
hence thesis;
end;
func pr2(F1,F2) -> Functor of [|F1,F2|], C2 equals :Def24:
(the pullback of F1,F2)`3_3;
correctness
proof
set T = the pullback of F1,F2;
consider D be strict category, P1 be Functor of D,C1,
P2 be Functor of D,C2 such that
A4: T = [D,P1,P2] & P1 is covariant & P2 is covariant &
D,P1,P2 is_pullback_of F1,F2 by A1,A2,Def21;
[D,P1,P2]`1_3 = D & [D,P1,P2]`3_3 = P2;
then D = [|F1,F2|] by A1,A2,A4,Def22;
then reconsider P2 as Functor of [|F1,F2|],C2;
P2 = (the pullback of F1,F2)`3_3 by A4;
hence thesis;
end;
end;
theorem Th52:
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
proof
let C,C1,C2 be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
assume
A1: F1 is covariant & F2 is covariant;
set T = the pullback of F1,F2;
consider D0 be strict category, P01 be Functor of D0,C1,
P02 be Functor of D0,C2 such that
A2: T = [D0,P01,P02] & P01 is covariant & P02 is covariant &
D0,P01,P02 is_pullback_of F1,F2 by A1,Def21;
A3: F1 (*) P01 = F2 (*) P02 &
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,D0 st H is covariant
& P01 (*) H = G1 & P02 (*) H = G2 & for H1 being Functor of D1,D0
st H1 is covariant & P01 (*) H1 = G1 & P02 (*) H1 = G2 holds H = H1
by A1,A2,Def20;
A4: [D0,P01,P02]`1_3 = D0 & [D0,P01,P02]`2_3 = P01 & [D0,P01,P02]`3_3 = P02;
then
A5: D0 = [|F1,F2|] by A1,A2,Def22;
reconsider P1 = P01 as Functor of [|F1,F2|], C1 by A5;
reconsider P2 = P02 as Functor of [|F1,F2|], C2 by A5;
pr1(F1,F2) is covariant & pr2(F1,F2) is covariant &
F1(*)pr1(F1,F2) = F2(*)pr2(F1,F2) &
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,[|F1,F2|] st H is covariant &
pr1(F1,F2)(*)H = G1 & pr2(F1,F2)(*)H = G2 &
(for H1 being Functor of D1,[|F1,F2|] st
H1 is covariant & pr1(F1,F2)(*)H1 = G1 & pr2(F1,F2)(*)H1 = G2 holds H = H1)
proof
thus
A6: pr1(F1,F2) is covariant by A2,A5,A4,A1,Def23;
thus
A7: pr2(F1,F2) is covariant by A2,A5,A4,A1,Def24;
thus F1(*)pr1(F1,F2) = pr1(F1,F2)*F1 by A6,A1,CAT_6:def 27
.= P01*F1 by A4,A2,A1,Def23
.= F1(*)P01 by A2,A1,CAT_6:def 27
.= P02*F2 by A2,A1,A3,CAT_6:def 27
.= pr2(F1,F2)*F2 by A4,A2,A1,Def24
.= F2(*)pr2(F1,F2) by A7,A1,CAT_6:def 27;
let D1 be category;
let G1 be Functor of D1,C1;
let G2 be Functor of D1,C2;
assume G1 is covariant & G2 is covariant & F1(*)G1 = F2(*)G2;
then consider H0 be Functor of D1,D0 such that
A8: H0 is covariant &
P01(*)H0 = G1 & P02(*)H0 = G2 & (for H1 being Functor of D1,D0 st
H1 is covariant & P01(*)H1 = G1 & P02(*)H1 = G2 holds H0 = H1)
by A1,A2,Def20;
reconsider H = H0 as Functor of D1,[|F1,F2|] by A5;
take H;
thus H is covariant by A5,A8;
thus pr1(F1,F2)(*)H = H*pr1(F1,F2) by A5,A8,A6,CAT_6:def 27
.= H0*P01 by A4,A2,A1,Def23
.= G1 by A2,A8,CAT_6:def 27;
thus pr2(F1,F2)(*)H = H*pr2(F1,F2) by A5,A8,A7,CAT_6:def 27
.= H0*P02 by A4,A2,A1,Def24
.= G2 by A2,A8,CAT_6:def 27;
let H1 be Functor of D1,[|F1,F2|];
assume
A9: H1 is covariant & pr1(F1,F2)(*)H1 = G1 & pr2(F1,F2)(*)H1 = G2;
reconsider H01 = H1 as Functor of D1,D0 by A5;
A10: P01(*)H01 = H01*P01 by A2,A9,A5,CAT_6:def 27
.= H1*pr1(F1,F2) by A4,A2,A1,Def23
.= G1 by A9,A6,CAT_6:def 27;
P02(*)H01 = H01*P02 by A2,A9,A5,CAT_6:def 27
.= H1*pr2(F1,F2) by A4,A2,A1,Def24
.= G2 by A9,A7,CAT_6:def 27;
hence H = H1 by A8,A9,A5,A10;
end;
hence thesis by A1,Def20;
end;
theorem
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|]
proof
let C,C1,C2 be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
assume
A1: F1 is covariant & F2 is covariant;
A2: pr1(F1,F2) is covariant & pr2(F1,F2) is covariant &
[|F1,F2|], pr1(F1,F2), pr2(F1,F2) is_pullback_of F1,F2 by A1,Th52;
A3: pr1(F2,F1) is covariant & pr2(F2,F1) is covariant &
[|F2,F1|], pr1(F2,F1), pr2(F2,F1) is_pullback_of F2,F1 by A1,Th52;
then [|F2,F1|], pr2(F2,F1), pr1(F2,F1) is_pullback_of F1,F2 by A1,Th47;
hence [|F1,F2|] ~= [|F2,F1|] by A1,A2,A3,Th46;
end;
theorem
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
proof
set C = Alter OrdC 2;
set C1 = Alter OrdC 2;
set C2 = Alter OrdC 2;
consider f be morphism of OrdC 2 such that
f is not identity and
Ob OrdC 2 = {dom f, cod f} and
A1: Mor OrdC 2 = {dom f, cod f, f} and
A2: dom f, cod f, f are_mutually_distinct by Th39;
reconsider g1 = dom f,g2 = cod f as morphism of OrdC 2
by A1,ENUMSET1:def 1;
reconsider F1 = MORPHISM(g1) as Functor of C1,C by CAT_6:47;
reconsider F2 = MORPHISM(g2) as Functor of C2,C by CAT_6:47;
take C,C1,C2,F1,F2;
assume 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;
then consider D be Category, P1 be Functor of D,C1,
P2 be Functor of D,C2 such that
A3: 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;
set g = the Morphism of D;
A4: g in the carrier' of D;
then
A5: g in dom P1 by FUNCT_2:def 1;
A6: g in dom P2 by A4,FUNCT_2:def 1;
A7: Alter OrdC 2 = CatStr(# Ob OrdC 2,Mor OrdC 2,
SourceMap OrdC 2, TargetMap OrdC 2,
CompMap OrdC 2 #) by CAT_6:def 33;
reconsider f1 = P1.g as morphism of OrdC 2 by A7;
reconsider f2 = P2.g as morphism of OrdC 2 by A7;
A8: (F1 * P1).g = F1.(P1.g) by A5,FUNCT_1:13
.= (MORPHISM g1).f1 by CAT_6:def 21
.= g1 by Th40,CAT_6:22;
(F2 * P2).g = F2.(P2.g) by A6,FUNCT_1:13
.= (MORPHISM g2).f2 by CAT_6:def 21
.= g2 by Th40,CAT_6:22;
hence contradiction by A8,A3,A2,ZFMISC_1:def 5;
end;