:: Concrete Categories
:: by Grzegorz Bancerek
::
:: Received January 12, 2001
:: Copyright (c) 2001-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 XBOOLE_0, STRUCT_0, RELAT_2, ALTCAT_1, CAT_1, RELAT_1, SUBSET_1,
PBOOLE, ZFMISC_1, FUNCT_1, TARSKI, BINOP_1, MCART_1, FUNCOP_1, ALTCAT_2,
FUNCTOR0, MSUALG_6, FUNCT_2, MSUALG_3, WELLORD1, REWRITE1, NATTRA_1,
MEMBER_1, REALSET1, PZFMISC1, ALTCAT_3, ARYTM_0, CAT_3, NUMBERS,
VALUED_1, CARD_3, YELLOW18;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
NUMBERS, RELAT_1, RELSET_1, FUNCT_1, PBOOLE, PARTFUN1, FUNCT_2, MCART_1,
ZF_FUND1, BINOP_1, MULTOP_1, CARD_3, FUNCT_4, STRUCT_0, FUNCOP_1,
MSUALG_3, FUNCT_3, ALTCAT_1, ALTCAT_2, FUNCTOR0, ALTCAT_3, FUNCTOR2,
FUNCTOR3;
constructors ZF_FUND1, MSUALG_3, ALTCAT_3, FUNCTOR3, CARD_3, RELSET_1,
XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, PBOOLE, STRUCT_0, ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCTOR2,
ALTCAT_4, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, MSUALG_3, ALTCAT_2, ALTCAT_1, ALTCAT_3, FUNCTOR0,
FUNCTOR2, FUNCTOR3, FUNCT_2, XBOOLE_0;
equalities TARSKI, ALTCAT_1, FUNCTOR0, BINOP_1;
expansions TARSKI, FUNCT_1, ALTCAT_2, ALTCAT_1, ALTCAT_3, FUNCTOR0, FUNCTOR2,
FUNCT_2, BINOP_1;
theorems ZFMISC_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, FUNCT_2, FUNCT_3,
MULTOP_1, ALTCAT_1, CARD_3, MCART_1, TARSKI, FUNCTOR0, FUNCT_4, FUNCTOR1,
FUNCTOR2, FUNCTOR3, MSUALG_3, ALTCAT_2, ALTCAT_3, PARTFUN1, XTUPLE_0;
schemes FUNCT_1, CARD_3, ALTCAT_1, CLASSES1, PBOOLE, MSSUBFAM, XBOOLE_0;
begin
:: <section1>Definability of categories and functors</section1>
scheme AltCatStrLambda { A() -> non empty set, B(object,object) -> set,
C(object,object,object,object,object) -> object }:
ex C being strict non empty transitive AltCatStr st the carrier of C = A() &
(for a,b being Object of C holds <^a,b^> = B(a,b)) &
for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g)
provided
A1: for a,b,c being Element of A(), f,g being set
st f in B(a,b) & g in B(b,c) holds C(a,b,c,f,g) in B(a,c)
proof
consider B being ManySortedSet of [:A(), A():] such that
A2: for a,b being Element of A() holds B.(a,b) = B(a,b) from ALTCAT_1:sch 2;
defpred P[object,object] means
ex a,b,c being Element of A(),
F being Function of {|B,B|}.(a,b,c), {|B|}.(a,b,c)
st $1 = [a,b,c] & $2 = F &
for f,g being object st f in B(a,b) & g in B(b,c)
holds F.[g,f] = C(a,b,c,f,g);
A3: for i being object st i in [:A(), A(), A():]
ex j being object st P[i,j]
proof
let i be object;
assume i in [:A(), A(), A():];
then consider a,b,c being object such that
A4: a in A() and
A5: b in A() and
A6: c in A() and
A7: i = [a,b,c] by MCART_1:68;
reconsider a,b,c as Element of A() by A4,A5,A6;
defpred P[object,object] means
ex f,g being object st $1 = [g,f] & $2 = C(a,b,c,f,g);
A8: for x being object st x in [:B(b,c), B(a,b):]
ex y being object st y in B(a,c) & P[x, y]
proof
let x be object;
assume x in [:B(b,c), B(a,b):];
then consider x1, x2 being object such that
A9: x1 in B(b,c) and
A10: x2 in B(a,b) and
A11: x = [x1,x2] by ZFMISC_1:def 2;
take y = C(a,b,c,x2,x1);
thus y in B(a,c) by A1,A9,A10;
thus thesis by A11;
end;
consider F being Function such that
A12: dom F = [:B(b,c), B(a,b):] & rng F c= B(a,c) and
A13: for x being object st x in [:B(b,c), B(a,b):] holds P[x, F.x]
from FUNCT_1:sch 6(A8);
A14: B.(a,b) = B(a,b) by A2;
A15: B.(b,c) = B(b,c) by A2;
A16: B.(a,c) = B(a,c) by A2;
A17: {|B,B|}.(a,b,c) = [:B(b,c), B(a,b):] by A14,A15,ALTCAT_1:def 4;
{|B|}.(a,b,c) = B(a,c) by A16,ALTCAT_1:def 3;
then reconsider F as Function of {|B,B|}.(a,b,c), {|B|}.(a,b,c)
by A12,A17,FUNCT_2:2;
take j = F, a, b, c, F;
thus i = [a,b,c] & j = F by A7;
let f,g be object;
assume that
A18: f in B(a,b) and
A19: g in B(b,c);
[g,f] in [:B(b,c), B(a,b):] by A18,A19,ZFMISC_1:87;
then consider f9,g9 being object such that
A20: [g,f] = [g9,f9] and
A21: F.[g,f] = C(a,b,c,f9,g9) by A13;
g = g9 by A20,XTUPLE_0:1;
hence thesis by A20,A21,XTUPLE_0:1;
end;
consider C being Function such that
A22: dom C = [:A(), A(), A():] and
A23: for i being object st i in [:A(), A(), A():] holds P[i, C.i]
from CLASSES1:sch 1(A3);
reconsider C as ManySortedSet of [:A(), A(), A():] by A22,PARTFUN1:def 2
,RELAT_1:def 18;
now
let i be object;
assume i in [:A(), A(), A():];
then consider a,b,c being Element of A(),
F being Function of {|B,B|}.(a,b,c), {|B|}.(a,b,c) such that
A24: i = [a,b,c] and
A25: C.i = F and
for f,g being object st f in B(a,b) & g in B(b,c)
holds F.[g,f] = C(a,b,c,f,g) by A23;
A26: {|B|}.(a,b,c) = {|B|}.i by A24,MULTOP_1:def 1;
{|B,B|}.(a,b,c) = {|B,B|}.i by A24,MULTOP_1:def 1;
hence C.i is Function of {|B,B|}.i, {|B|}.i by A25,A26;
end;
then reconsider C as ManySortedFunction of {|B,B|}, {|B|} by PBOOLE:def 15;
set alt = AltCatStr (# A(), B, C #);
alt is transitive
proof
let o1,o2,o3 be Object of alt;
reconsider a = o1, b = o2, c = o3 as Element of A();
set f = the Element of <^o1,o2^>,g = the Element of <^o2,o3^>;
assume that
A27: <^o1,o2^> <> {} and
A28: <^o2,o3^> <> {};
A29: f in <^o1,o2^> by A27;
A30: g in <^o2,o3^> by A28;
A31: f in B(a,b) by A2,A29;
g in B(b,c) by A2,A30;
then C(a,b,c,f,g) in B(a,c) by A1,A31;
hence thesis by A2;
end;
then reconsider alt as strict transitive non empty AltCatStr;
take alt;
thus the carrier of alt = A();
thus for a,b being Object of alt holds <^a,b^> = B(a,b) by A2;
let a,b,c be Object of alt such that
A32: <^a,b^> <> {} and
A33: <^b,c^> <> {};
[a,b,c] in [:A(), A(), A():] by MCART_1:69;
then consider a9,b9,c9 being Element of A(),
F being Function of {|B,B|}.(a9,b9,c9), {|B|}.(a9,b9,c9) such that
A34: [a,b,c] = [a9,b9,c9] and
A35: C.[a,b,c] = F and
A36: for f,g being object st f in B(a9,b9) & g in B(b9,c9)
holds F.[g,f] = C(a9,b9,c9,f,g) by A23;
A37: a = a9 by A34,XTUPLE_0:3;
A38: b = b9 by A34,XTUPLE_0:3;
A39: c = c9 by A34,XTUPLE_0:3;
let f be Morphism of a,b, g be Morphism of b,c;
A40: <^a,b^> = B(a,b) by A2;
<^b,c^> = B(b,c) by A2;
then
A41: F.[g,f] = C(a,b,c,f,g) by A32,A33,A36,A37,A38,A39,A40;
thus g*f = (the Comp of alt).(a,b,c).(g,f) by A32,A33,ALTCAT_1:def 8
.= C(a,b,c,f,g) by A35,A41,MULTOP_1:def 1;
end;
scheme CatAssocSch { A() -> non empty transitive AltCatStr,
C(object,object,object,object,object) -> object }: A() is associative
provided
A1: for a,b,c being Object of A() st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g)
and
A2: for a,b,c,d being Object of A(), f,g,h being set
st f in <^a,b^> & g in <^b,c^> & h in <^c,d^>
holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h))
proof
let i,j,k,l be Element of A();
set alt = A(), IT = the Comp of alt;
set B = the Arrows of alt;
reconsider i9 = i, j9 = j, k9 = k, l9 = l as Object of alt;
let f,g,h be set such that
A3: f in B.(i,j) and
A4: g in B.(j,k) and
A5: h in B.(k,l);
A6: B.(i,j) = <^i9,j9^>;
reconsider f9 = f as Morphism of i9, j9 by A3;
A7: B.(j,k) = <^j9,k9^>;
reconsider g9 = g as Morphism of j9, k9 by A4;
A8: B.(k,l) = <^k9,l9^>;
reconsider h9 = h as Morphism of k9, l9 by A5;
A9: <^i9,k9^> <> {} by A3,A4,A6,A7,ALTCAT_1:def 2;
A10: <^j9,l9^> <> {} by A4,A5,A7,A8,ALTCAT_1:def 2;
thus IT.(i,k,l).(h,IT.(i,j,k).(g,f))
= IT.(i,k,l).(h,g9*f9) by A3,A4,ALTCAT_1:def 8
.= h9*(g9*f9) by A5,A9,ALTCAT_1:def 8
.= C(i,k,l,g9*f9,h9) by A1,A5,A9
.= C(i,k,l,C(i,j,k,f,g),h) by A1,A3,A4
.= C(i9,j9,l9,f,C(j9,k9,l9,g,h)) by A2,A3,A4,A5,A6,A7,A8
.= C(i9,j9,l9,f,h9*g9) by A1,A4,A5
.= (h9*g9)*f9 by A1,A3,A10
.= IT.(i,j,l).(h9*g9,f) by A3,A10,ALTCAT_1:def 8
.= IT.(i,j,l).(IT.(j,k,l).(h,g),f) by A4,A5,ALTCAT_1:def 8;
end;
scheme CatUnitsSch { A() -> non empty transitive AltCatStr,
C(object,object,object,object,object) -> object }: A() is with_units
provided
A1: for a,b,c being Object of A() st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c holds g*f = C(a,b,c,f,g)
and
A2: for a being Object of A() ex f being set st f in <^a,a^> &
for b being Object of A(), g being set st g in <^a,b^> holds C(a,a,b,f,g) = g
and
A3: for a being Object of A() ex f being set st f in <^a,a^> &
for b being Object of A(), g being set st g in <^b,a^> holds C(b,a,a,g,f) = g
proof
set alt = A(), IT = the Comp of alt, I = the carrier of alt;
set G = the Arrows of alt;
hereby
let j be Element of I;
reconsider j9 = j as Object of alt;
consider f be set such that
A4: f in <^j9,j9^> and
A5: for b being Element of A(), g being set st g in <^b,j9^>
holds C(b,j9,j9,g,f) = g by A3;
take f;
thus f in G.(j,j) by A4;
let i be Element of I, g be set such that
A6: g in G.(i,j);
reconsider i9 = i as Object of alt;
G.(i,j) = <^i9,j9^>;
then
A7: C(i,j,j,g,f) = g by A5,A6;
reconsider f9 = f as Morphism of j9,j9 by A4;
reconsider g9 = g as Morphism of i9,j9 by A6;
thus IT.(i,j,j).(f,g) = f9*g9 by A4,A6,ALTCAT_1:def 8
.= g by A1,A4,A6,A7;
end;
let i be Element of I;
reconsider i9 = i as Object of alt;
consider e being set such that
A8: e in <^i9,i9^> and
A9: for b being Element of A(), g being set st g in <^i9,b^>
holds C(i,i,b,e,g) = g by A2;
take e;
thus e in G.(i,i) by A8;
reconsider e9 = e as Morphism of i9,i9 by A8;
let j be Element of I, f be set such that
A10: f in G.(i,j);
reconsider j9 = j as Object of alt;
G.(i,j) = <^i9,j9^>;
then
A11: C(i,i,j,e,f) = f by A9,A10;
reconsider f9 = f as Morphism of i9, j9 by A10;
thus IT.(i,i,j).(f,e) = f9*e9 by A8,A10,ALTCAT_1:def 8
.= f by A1,A8,A10,A11;
end;
scheme CategoryLambda { A() -> non empty set, B(object,object) -> set,
C(object,object,object,object,object) -> object }:
ex C being strict category st the carrier of C = A() &
(for a,b being Object of C holds <^a,b^> = B(a,b)) &
for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g)
provided
A1: for a,b,c being Element of A(), f,g being set
st f in B(a,b) & g in B(b,c) holds C(a,b,c,f,g) in B(a,c) and
A2: for a,b,c,d being Element of A(), f,g,h being set
st f in B(a,b) & g in B(b,c) & h in B(c,d)
holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h)) and
A3: for a being Element of A() ex f being set st f in B(a,a) &
for b being Element of A(), g being set st g in B(a,b) holds C(a,a,b,f,g) = g
and
A4: for a being Element of A() ex f being set st f in B(a,a) &
for b being Element of A(), g being set st g in B(b,a) holds C(b,a,a,g,f) = g
proof
A5: for a,b,c being Element of A(), f,g being set
st f in B(a,b) & g in B(b,c) holds C(a,b,c,f,g) in B(a,c) by A1;
consider C being strict non empty transitive AltCatStr such that
A6: the carrier of C = A() and
A7: for a,b being Object of C holds <^a,b^> = B(a,b) and
A8: for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g) from AltCatStrLambda(A5);
A9: for a,b,c,d being Object of C, f,g,h being set
st f in <^a,b^> & g in <^b,c^> & h in <^c,d^>
holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h))
proof
let a,b,c,d be Object of C, f,g,h be set such that
A10: f in <^a,b^> and
A11: g in <^b,c^> and
A12: h in <^c,d^>;
A13: <^a,b^> = B(a,b) by A7;
A14: <^b,c^> = B(b,c) by A7;
<^c,d^> = B(c,d) by A7;
hence thesis by A2,A6,A10,A11,A12,A13,A14;
end;
A15: for a being Object of C ex f being set st f in <^a,a^> &
for b being Object of C, g being set st g in <^a,b^> holds C(a,a,b,f,g) = g
proof
let a be Object of C;
consider f being set such that
A16: f in B(a,a) and
A17: for b being Element of A(), g being set st g in B(a,b)
holds C(a,a,b,f,g) = g by A3,A6;
take f;
thus f in <^a,a^> by A7,A16;
let b be Object of C;
<^a,b^> = B(a,b) by A7;
hence thesis by A6,A17;
end;
A18: for a being Object of C ex f being set st f in <^a,a^> &
for b being Object of C, g being set st g in <^b,a^> holds C(b,a,a,g,f) = g
proof
let a be Object of C;
consider f being set such that
A19: f in B(a,a) and
A20: for b being Element of A(), g being set st g in B(b,a)
holds C(b,a,a,g,f) = g by A4,A6;
take f;
thus f in <^a,a^> by A7,A19;
let b be Object of C;
<^b,a^> = B(b,a) by A7;
hence thesis by A6,A20;
end;
A21: C is associative from CatAssocSch(A8,A9);
C is with_units from CatUnitsSch(A8,A15,A18);
hence thesis by A6,A7,A8,A21;
end;
scheme CategoryLambdaUniq { A() -> non empty set, B(object,object) -> object,
C(object,object,object,object,object) -> object }:
for C1,C2 being non empty transitive AltCatStr st the carrier of C1 = A() &
(for a,b being Object of C1 holds <^a,b^> = B(a,b)) &
(for a,b,c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g)) & the carrier of C2 = A() &
(for a,b being Object of C2 holds <^a,b^> = B(a,b)) &
(for a,b,c being Object of C2 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g)) holds the AltCatStr of C1 = the AltCatStr of C2
proof
let C1,C2 be non empty transitive AltCatStr such that
A1: the carrier of C1 = A() and
A2: for a,b being Object of C1 holds <^a,b^> = B(a,b) and
A3: for a,b,c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g) and
A4: the carrier of C2 = A() and
A5: for a,b being Object of C2 holds <^a,b^> = B(a,b) and
A6: for a,b,c being Object of C2 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g);
A7: now
let i be object;
assume i in [:A(),A():];
then consider a,b being object such that
A8: a in A() and
A9: b in A() and
A10: i = [a,b] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b as Object of C1 by A1,A8,A9;
reconsider a2 = a, b2 = b as Object of C2 by A4,A8,A9;
thus (the Arrows of C1).i = <^a1,b1^> by A10
.= B(a1,b1) by A2
.= <^a2,b2^>by A5
.= (the Arrows of C2).i by A10;
end;
then
A11: the Arrows of C1 = the Arrows of C2 by A1,A4,PBOOLE:3;
now
let i be object;
assume i in [:A(), A(), A():];
then consider a,b,c being object such that
A12: a in A() and
A13: b in A() and
A14: c in A() and
A15: i = [a,b,c] by MCART_1:68;
reconsider a1 = a, b1 = b, c1 = c as Object of C1 by A1,A12,A13,A14;
reconsider a2 = a, b2 = b, c2 = c as Object of C2 by A4,A12,A13,A14;
A16: (the Comp of C1).i = (the Comp of C1).(a1,b1,c1) by A15,MULTOP_1:def 1;
A17: (the Comp of C2).i = (the Comp of C2).(a2,b2,c2) by A15,MULTOP_1:def 1;
A18: now
assume
A19: [:<^b1,c1^>, <^a1,b1^>:] <> {};
then
A20: <^b1,c1^> <> {} by ZFMISC_1:90;
<^a1,b1^> <> {} by A19,ZFMISC_1:90;
hence <^a1,c1^> <> {} by A20,ALTCAT_1:def 2;
end;
then
A21: dom ((the Comp of C1).(a1,b1,c1)) = [:<^b1,c1^>, <^a1,b1^>:] by
FUNCT_2:def 1;
A22: dom ((the Comp of C2).(a2,b2,c2)) = [:<^b1,c1^>, <^a1,b1^>:] by A11,A18,
FUNCT_2:def 1;
now
let j be object;
assume j in [:<^b1,c1^>, <^a1,b1^>:];
then consider j1,j2 being object such that
A23: j1 in <^b1,c1^> and
A24: j2 in <^a1,b1^> and
A25: j = [j1,j2] by ZFMISC_1:def 2;
reconsider j1 as Morphism of b1,c1 by A23;
reconsider j2 as Morphism of a1,b1 by A24;
reconsider f1 = j1 as Morphism of b2,c2 by A1,A4,A7,PBOOLE:3;
reconsider f2 = j2 as Morphism of a2,b2 by A1,A4,A7,PBOOLE:3;
thus (the Comp of C1).(a1,b1,c1).j
= (the Comp of C1).(a1,b1,c1).(j1,j2) by A25
.= j1*j2 by A23,A24,ALTCAT_1:def 8
.= C(a1,b1,c1,j2,j1) by A3,A23,A24
.= f1*f2 by A6,A11,A23,A24
.= (the Comp of C2).(a2,b2,c2).(f1,f2) by A11,A23,A24,ALTCAT_1:def 8
.= (the Comp of C2).(a2,b2,c2).j by A25;
end;
hence (the Comp of C1).i = (the Comp of C2).i by A16,A17,A21,A22;
end;
hence thesis by A1,A4,A11,PBOOLE:3;
end;
scheme CategoryQuasiLambda { A() -> non empty set,
P[object,object,object],
B(object,object) -> set, C(object,object,object,object,object) -> object }:
ex C being strict category st the carrier of C = A() &
(for a,b being Object of C
for f being set holds f in <^a,b^> iff f in B(a,b) & P[a,b,f]) &
for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g)
provided
A1: for a,b,c being Element of A(), f,g being set
st f in B(a,b) & P[a,b,f] & g in B(b,c) & P[b,c,g]
holds C(a,b,c,f,g) in B(a,c) & P[a,c, C(a,b,c,f,g)] and
A2: for a,b,c,d being Element of A(), f,g,h being set
st f in B(a,b) & P[a,b,f] & g in B(b,c) & P[b,c,g] & h in B(c,d) & P[c,d,h]
holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h)) and
A3: for a being Element of A() ex f being set st f in B(a,a) & P[a,a,f] &
for b being Element of A(), g being set st g in B(a,b) & P[a,b,g]
holds C(a,a,b,f,g) = g and
A4: for a being Element of A() ex f being set st f in B(a,a) & P[a,a,f] &
for b being Element of A(), g being set st g in B(b,a) & P[b,a,g]
holds C(b,a,a,g,f) = g
proof
deffunc F(object) = B($1`1,$1`2);
defpred Q[object,object] means P[$1`1,$1`2,$2];
consider P being Function such that dom P = [:A(),A():] and
A5: for i being object st i in [:A(),A():]
for x being object holds x in P.i iff x in F(i) & Q[i,x] from CARD_3:sch 2;
deffunc b(set,set) = P.($1,$2);
A6: now
let a,b be Element of A();
let x be set;
A7: [a,b]`1 = a;
A8: [a,b]`2 = b;
[a,b] in [:A(),A() :] by ZFMISC_1:def 2;
hence x in P.(a,b) iff x in B(a,b) & P[a,b,x] by A5,A7,A8;
end;
A9: now
let a,b,c be Element of A(), f,g be set;
assume that
A10: f in b(a,b) and
A11: g in b(b,c);
A12: f in B(a,b) by A6,A10;
A13: P[a,b,f] by A6,A10;
A14: g in B(b,c) by A6,A11;
A15: P[b,c,g] by A6,A11;
then
A16: C(a,b,c,f,g) in B(a,c) by A1,A12,A13,A14;
P[a,c, C(a,b,c,f,g)] by A1,A12,A13,A14,A15;
hence C(a,b,c,f,g) in b(a,c) by A6,A16;
end;
A17: now
let a,b,c,d be Element of A(), f,g,h be set;
assume that
A18: f in b(a,b) and
A19: g in b(b,c) and
A20: h in b(c,d);
A21: f in B(a,b) by A6,A18;
A22: P[a,b,f] by A6,A18;
A23: g in B(b,c) by A6,A19;
A24: P[b,c,g] by A6,A19;
A25: h in B(c,d) by A6,A20;
P[c,d,h] by A6,A20;
hence C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h)) by A2,A21,A22,A23
,A24,A25;
end;
A26: now
let a be Element of A();
consider f being set such that
A27: f in B(a,a) and
A28: P[a,a,f] and
A29: for b being Element of A(), g being set st g in B(a,b) & P[a,b,g]
holds C(a,a,b,f,g) = g by A3;
take f;
thus f in b(a,a) by A6,A27,A28;
let b be Element of A(), g be set;
assume
A30: g in b(a,b);
then
A31: g in B(a,b) by A6;
P[a,b,g] by A6,A30;
hence C(a,a,b,f,g) = g by A29,A31;
end;
A32: now
let a be Element of A();
consider f being set such that
A33: f in B(a,a) and
A34: P[a,a,f] and
A35: for b being Element of A(), g being set st g in B(b,a) & P[b,a,g]
holds C(b,a,a,g,f) = g by A4;
take f;
thus f in b(a,a) by A6,A33,A34;
let b be Element of A(), g be set;
assume
A36: g in b(b,a);
then
A37: g in B(b,a) by A6;
P[b,a,g] by A6,A36;
hence C(b,a,a,g,f) = g by A35,A37;
end;
consider C being strict category such that
A38: the carrier of C = A() and
A39: for a,b being Object of C holds <^a,b^> = b(a,b) and
A40: for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g) from CategoryLambda(A9,A17,A26,A32);
take C;
thus the carrier of C = A() by A38;
hereby
let a,b be Object of C, f be set;
<^a,b^> = P.(a,b) by A39;
hence f in <^a,b^> iff f in B(a,b) & P[a,b,f] by A6,A38;
end;
thus thesis by A40;
end;
registration
let f be Function-yielding Function;
let a,b,c be set;
cluster f.(a,b,c) -> Relation-like Function-like;
coherence
proof f.(a,b,c) = f.[a,b,c] by MULTOP_1:def 1;
hence thesis;
end;
end;
scheme SubcategoryEx { A() -> category, P[object], Q[object,object,object]}:
ex B being strict non empty subcategory of A() st
(for a being Object of A() holds a is Object of B iff P[a]) &
for a,b being Object of A(), a9,b9 being Object of B
st a9 = a & b9 = b & <^a,b^> <> {}
for f being Morphism of a,b holds f in <^a9,b9^> iff Q[a,b,f]
provided
A1: ex a being Object of A() st P[a] and
A2: for a,b,c being Object of A()
st P[a] & P[b] & P[c] & <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c st Q[a,b,f] & Q[b,c,g]
holds Q[a,c,g*f] and
A3: for a being Object of A() st P[a] holds Q[a,a, idm a]
proof
consider X being set such that
A4: for x being object holds x in X iff x in the carrier of A() & P[x]
from XBOOLE_0:sch 1;
reconsider X as non empty set by A1,A4;
A5: X c= the carrier of A()
by A4;
deffunc B(set,set) = (the Arrows of A()).($1,$2);
deffunc C(set,set,set,set,set) = (the Comp of A()).($1,$2,$3).($5,$4);
A6: now
let a,b,c be Element of X, f,g be set such that
A7: f in B(a,b) and
A8: Q[a,b,f] and
A9: g in B(b,c) and
A10: Q[b,c,g];
reconsider a9 = a, b9 = b, c9 = c as Object of A() by A4;
A11: B(a,b) = <^a9,b9^>;
reconsider f9 = f as Morphism of a9, b9 by A7;
A12: B(b,c) = <^b9,c9^>;
reconsider g9 = g as Morphism of b9, c9 by A9;
A13: C(a,b,c,f,g) = g9*f9 by A7,A9,ALTCAT_1:def 8;
<^a9,c9^> <> {} by A7,A9,A11,A12,ALTCAT_1:def 2;
hence C(a,b,c,f,g) in B(a,c) by A13;
A14: P[a9] by A4;
A15: P[b9] by A4;
P[c9] by A4;
hence Q[a,c, C(a,b,c,f,g)] by A2,A7,A8,A9,A10,A13,A14,A15;
end;
A16: now
let a,b,c,d be Element of X, f,g,h being set such that
A17: f in B(a,b) and Q[a,b,f] and
A18: g in B(b,c) and Q[b,c,g] and
A19: h in B(c,d) and Q[c,d,h];
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Object of A() by A4;
A20: B(a,b) = <^a9,b9^>;
reconsider f9 = f as Morphism of a9, b9 by A17;
A21: B(b,c) = <^b9,c9^>;
reconsider g9 = g as Morphism of b9, c9 by A18;
A22: B(c,d) = <^c9,d9^>;
reconsider h9 = h as Morphism of c9, d9 by A19;
A23: <^a9,c9^> <> {} by A17,A18,A20,A21,ALTCAT_1:def 2;
A24: <^b9,d9^> <> {} by A18,A19,A21,A22,ALTCAT_1:def 2;
thus C(a,c,d,C(a,b,c,f,g),h)
= C(a9,c9,d9,g9*f9,h) by A17,A18,ALTCAT_1:def 8
.= h9*(g9*f9) by A19,A23,ALTCAT_1:def 8
.= h9*g9*f9 by A17,A18,A19,ALTCAT_1:21
.= C(a,b,d,f,h9*g9) by A17,A24,ALTCAT_1:def 8
.= C(a,b,d,f,C(b,c,d,g,h)) by A18,A19,ALTCAT_1:def 8;
end;
A25: now
let a be Element of X;
reconsider b = a as Object of A() by A4;
reconsider f = idm b as set;
take f;
P[b] by A4;
hence f in B(a,a) & Q[a,a,f] by A3;
let c be Element of X, g be set such that
A26: g in B(a,c) and Q[a,c,g];
reconsider d = c as Object of A() by A4;
reconsider g9 = g as Morphism of b,d by A26;
thus C(a,a,c,f,g) = g9* idm b by A26,ALTCAT_1:def 8
.= g by A26,ALTCAT_1:def 17;
end;
A27: now
let a be Element of X;
reconsider b = a as Object of A() by A4;
reconsider f = idm b as set;
take f;
P[b] by A4;
hence f in B(a,a) & Q[a,a,f] by A3;
let c be Element of X, g be set such that
A28: g in B(c,a) and Q[c,a,g];
reconsider d = c as Object of A() by A4;
reconsider g9 = g as Morphism of d,b by A28;
thus C(c,a,a,g,f) = (idm b)*g9 by A28,ALTCAT_1:def 8
.= g by A28,ALTCAT_1:20;
end;
consider C being strict category such that
A29: the carrier of C = X and
A30: for a,b being Object of C for f being set holds f in <^a,b^> iff
f in B(a,b) & Q[a,b,f] and
A31: for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g) from CategoryQuasiLambda(A6,A16,A25,A27);
C is SubCatStr of A()
proof
thus the carrier of C c= the carrier of A() by A5,A29;
thus [:the carrier of C, the carrier of C:] c=
[:the carrier of A(), the carrier of A():] by A5,A29,ZFMISC_1:96;
hereby
let i be set;
assume i in [:the carrier of C, the carrier of C:];
then consider a,b being object such that
A32: a in the carrier of C and
A33: b in the carrier of C and
A34: [a,b] = i by ZFMISC_1:def 2;
reconsider a,b as Object of C by A32,A33;
A35: (the Arrows of C).i = <^a,b^> by A34;
A36: (the Arrows of A()).i = (the Arrows of A()).(a,b) by A34;
thus (the Arrows of C).i c= (the Arrows of A()).i
by A30,A35,A36;
end;
thus [:the carrier of C, the carrier of C, the carrier of C:] c=
[:the carrier of A(), the carrier of A(), the carrier of A():]
by A5,A29,MCART_1:73;
let i be set;
assume i in [:the carrier of C, the carrier of C, the carrier of C:];
then consider a,b,c being object such that
A37: a in the carrier of C and
A38: b in the carrier of C and
A39: c in the carrier of C and
A40: [a,b,c] = i by MCART_1:68;
reconsider a,b,c as Object of C by A37,A38,A39;
reconsider a9 = a, b9 = b, c9 = c as Object of A() by A4,A29;
let x be object;
assume x in (the Comp of C).i;
then
A41: x in (the Comp of C).(a,b,c) by A40,MULTOP_1:def 1;
then consider gf, h being object such that
A42: x = [gf,h] and
A43: gf in [:(the Arrows of C).(b,c), (the Arrows of C).(a,b):] and
A44: h in (the Arrows of C).(a,c) by RELSET_1:2;
consider g,f being object such that
A45: g in (the Arrows of C).(b,c) and
A46: f in (the Arrows of C).(a,b) and
A47: [g,f] = gf by A43,ZFMISC_1:def 2;
reconsider f as Morphism of a,b by A46;
reconsider g as Morphism of b,c by A45;
reconsider h as Morphism of a,c by A44;
A48: (the Comp of A()).(a9,b9,c9) = (the Comp of A()).i by A40,MULTOP_1:def 1;
A49: g in (the Arrows of A()).(b9,c9) by A30,A45;
A50: f in (the Arrows of A()).(a9,b9) by A30,A46;
A51: h = (the Comp of C).(a,b,c).(g,f) by A41,A42,A47,FUNCT_1:1
.= g*f by A45,A46,ALTCAT_1:def 8
.= (the Comp of A()).(a9,b9,c9).(g,f) by A31,A45,A46;
h in (the Arrows of A()).(a9,c9) by A30,A44;
then dom ((the Comp of A()).(a9,b9,c9)) =
[:(the Arrows of A()).(b9,c9), (the Arrows of A()).(a9,b9):]
by FUNCT_2:def 1;
then gf in dom ((the Comp of A()).(a9,b9,c9)) by A47,A49,A50,ZFMISC_1:def 2
;
hence thesis by A42,A47,A48,A51,FUNCT_1:def 2;
end;
then reconsider C as non empty SubCatStr of A();
for o being Object of C, o9 being Object of A() st o = o9
holds idm o9 in <^o,o^>
proof
let a be Object of C, b be Object of A();
assume
A52: a = b;
then P[b] by A4,A29;
then Q[b,b, idm b] by A3;
hence thesis by A30,A52;
end;
then reconsider C as strict non empty subcategory of A() by ALTCAT_2:def 14;
take C;
thus for a be Object of A() holds a is Object of C iff P[a] by A4,A29;
let a,b be Object of A(), a9,b9 be Object of C such that
A53: a9 = a and
A54: b9 = b and
A55: <^a,b^> <> {};
let f be Morphism of a,b;
thus thesis by A30,A53,A54,A55;
end;
scheme CovariantFunctorLambda { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }:
ex F being covariant strict Functor of A(),B() st
(for a being Object of A() holds F.a = O(a)) &
for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f)
provided
A1: for a being Object of A() holds O(a) is Object of B() and
A2: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
holds F(a,b,f) in (the Arrows of B()).(O(a), O(b)) and
A3: for a,b,c being Object of A() st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
for a9,b9,c9 being Object of B() st a9 = O(a) & b9 = O(b) & c9 = O(c)
for f9 being Morphism of a9,b9, g9 being Morphism of b9,c9
st f9 = F(a,b,f) & g9 = F(b,c,g) holds F(a,c,g*f) = g9*f9 and
A4: for a being Object of A(), a9 being Object of B() st a9 = O(a)
holds F(a,a,idm a) = idm a9
proof
consider O being Function such that
A5: dom O = the carrier of A() and
A6: for x being object st x in the carrier of A() holds O.x = O(x) from
FUNCT_1:sch 3;
rng O c= the carrier of B()
proof
let y be object;
assume y in rng O;
then consider x being object such that
A7: x in dom O and
A8: y = O.x by FUNCT_1:def 3;
reconsider x as Object of A() by A5,A7;
A9: y = O(x) by A6,A8;
O(x) is Object of B() by A1;
hence thesis by A9;
end;
then reconsider O as Function of the carrier of A(), the carrier of B()
by A5,FUNCT_2:2;
reconsider OM = [:O,O:] as
bifunction of the carrier of A(), the carrier of B();
defpred P[object,object,object] means $1 = F($3`1,$3`2,$2);
A10: for i being object st i in [:the carrier of A(), the carrier of A():]
for x being object st x in (the Arrows of A()).i
ex y being object st y in ((the Arrows of B())*OM).i & P[y,x,i]
proof
let i be object;
assume
A11: i in [:the carrier of A(), the carrier of A():];
then consider a,b being object such that
A12: a in the carrier of A() and
A13: b in the carrier of A() and
A14: [a,b] = i by ZFMISC_1:def 2;
reconsider a,b as Object of A() by A12,A13;
let x be object;
assume
A15: x in (the Arrows of A()).i;
then reconsider f = x as Morphism of a,b by A14;
take y = F(a,b,f);
A16: y in (the Arrows of B()).(O(a), O(b)) by A2,A14,A15;
A17: O(a) = O.a by A6;
i in dom OM by A5,A11,FUNCT_3:def 8;
then ((the Arrows of B())*OM).i
= (the Arrows of B()).(OM.(a,b)) by A14,FUNCT_1:13
.= (the Arrows of B()).(O.a,O.b) by A5,FUNCT_3:def 8;
hence y in ((the Arrows of B())*OM).i by A6,A16,A17;
thus thesis by A14;
end;
consider M being ManySortedFunction of the Arrows of A(),
(the Arrows of B())*OM such that
A18: for i be object st i in [:the carrier of A(), the carrier of A():]
ex f be Function of (the Arrows of A()).i, ((the Arrows of B())*OM).i
st f = M.i & for x be object st x in (the Arrows of A()).i
holds P[f.x, x, i]
from MSSUBFAM:sch 1(A10);
reconsider M as MSUnTrans of OM, the Arrows of A(), the Arrows of B()
by FUNCTOR0:def 4;
FunctorStr(#OM, M#) is Covariant
proof
take O;
thus thesis;
end;
then reconsider F = FunctorStr(#OM, M#) as
Covariant FunctorStr over A(), B();
A19: now
let a be Object of A();
thus F.a = ([O.a,O.a])`1 by A5,FUNCT_3:def 8
.= O.a
.= O(a) by A6;
end;
A20: now
let o1,o2 be Object of A() such that
A21: <^o1,o2^> <> {};
let g be Morphism of o1,o2;
[o1,o2] in [:the carrier of A(), the carrier of A():] by ZFMISC_1:def 2;
then
consider f being
Function of (the Arrows of A()).[o1,o2], ((the Arrows of B())*OM).[o1,o2]
such that
A22: f = M.[o1,o2] and
A23: for x be object st x in (the Arrows of A()).[o1,o2]
holds P[f.x, x, [o1,o2]] by A18;
:: then consider f being Function of (the Arrows of A()).[o1,o2],
:: ((the Arrows of B())*OM).[o1,o2] such that
:: A22: f = M.[o1,o2] and
:: A23: for x being set st x in (the Arrows of A()).[o1,o2]
:: holds f.x = F([o1,o2]`1,[o1,o2]`2,x) by A18;
f.g = F([o1,o2]`1,[o1,o2]`2,g) by A21,A23
.= F(o1,[o1,o2]`2,g)
.= F(o1,o2,g);
hence Morph-Map(F,o1,o2).g = F(o1,o2,g) by A22;
end;
A24: F is feasible
proof
let o1,o2 be Object of A();
set g = the Morphism of o1,o2;
assume
A25: <^o1,o2^> <> {};
then Morph-Map(F,o1,o2).g = F(o1,o2,g) by A20;
then Morph-Map(F,o1,o2).g in (the Arrows of B()).(O(o1), O(o2)) by A2,A25;
then Morph-Map(F,o1,o2).g in (the Arrows of B()).(F.o1, O(o2)) by A19;
hence thesis by A19;
end;
A26: now
let o1,o2 be Object of A();
assume
A27: <^o1,o2^> <> {};
let g be Morphism of o1,o2;
A28: Morph-Map(F,o1,o2).g = F(o1,o2,g) by A20,A27;
<^F.o1, F.o2^> <> {} by A24,A27;
hence F.g = F(o1,o2,g) by A27,A28,FUNCTOR0:def 15;
end;
A29: F is comp-preserving
proof
let o1,o2,o3 be Object of A() such that
A30: <^o1,o2^> <> {} and
A31: <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
set a = O.o1, b = O.o2, c = O.o3;
A32: a = O(o1) by A6;
A33: b = O(o2) by A6;
A34: c = O(o3) by A6;
reconsider f9 = F(o1,o2,f) as Morphism of a,b by A2,A30,A32,A33;
reconsider g9 = F(o2,o3,g) as Morphism of b,c by A2,A31,A33,A34;
A35: a = F.o1 by A19,A32;
A36: b = F.o2 by A19,A33;
A37: c = F.o3 by A19,A34;
reconsider ff = f9 as Morphism of F.o1, F.o2 by A19,A32,A36;
reconsider gg = g9 as Morphism of F.o2, F.o3 by A19,A34,A36;
take ff, gg;
A38: <^o1, o3^> <> {} by A30,A31,ALTCAT_1:def 2;
F(o1,o3,g*f) = gg*ff by A3,A30,A31,A32,A33,A34,A35,A36,A37;
hence ff = Morph-Map(F,o1,o2).f & gg = Morph-Map(F,o2,o3).g &
Morph-Map(F,o1,o3).(g*f) = gg*ff by A20,A30,A31,A38;
end;
F is Functor of A(), B()
proof
thus F is feasible by A24;
hereby
let o be Object of A();
A39: F.o = O(o) by A19;
thus Morph-Map(F,o,o).idm o = F(o,o,idm o) by A20
.= idm F.o by A4,A39;
end;
thus thesis by A29;
end;
then reconsider F as covariant strict Functor of A(), B()
by A29;
take F;
thus thesis by A19,A26;
end;
theorem Th1:
for A,B being category, F,G being covariant Functor of A,B
st (for a being Object of A holds F.a = G.a) &
(for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = G.f)
holds the FunctorStr of F = the FunctorStr of G
proof
let A,B be category, F,G be covariant Functor of A,B such that
A1: for a being Object of A holds F.a = G.a and
A2: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = G.f;
the ObjectMap of F is Covariant by FUNCTOR0:def 12;
then consider ff being Function of the carrier of A, the carrier of B such
that
A3: the ObjectMap of F = [:ff, ff:];
the ObjectMap of G is Covariant by FUNCTOR0:def 12;
then consider gg being Function of the carrier of A, the carrier of B such
that
A4: the ObjectMap of G = [:gg, gg:];
now
let a,b be Element of A;
reconsider x = a, y = b as Object of A;
A5: dom ff = the carrier of A by FUNCT_2:def 1;
A6: dom gg = the carrier of A by FUNCT_2:def 1;
A7: (the ObjectMap of F).(x,x) = [ff.x, ff.x] by A3,A5,FUNCT_3:def 8;
A8: (the ObjectMap of F).(y,y) = [ff.y, ff.y] by A3,A5,FUNCT_3:def 8;
A9: (the ObjectMap of G).(x,x) = [gg.x, gg.x] by A4,A6,FUNCT_3:def 8;
A10: (the ObjectMap of G).(y,y) = [gg.y, gg.y] by A4,A6,FUNCT_3:def 8;
A11: F.x = ff.x by A7;
A12: F.y = ff.y by A8;
A13: G.x = gg.x by A9;
A14: G.y = gg.y by A10;
A15: F.x = G.x by A1;
A16: F.y = G.y by A1;
thus (the ObjectMap of F).(a,b) = [ff.a,ff.b] by A3,A5,FUNCT_3:def 8
.= (the ObjectMap of G).(a,b) by A4,A6,A11,A12,A13,A14,A15,A16,
FUNCT_3:def 8;
end;
then
A17: the ObjectMap of F = the ObjectMap of G;
now
let i be object;
assume i in [:the carrier of A, the carrier of A:];
then consider a,b being object such that
A18: a in the carrier of A and
A19: b in the carrier of A and
A20: i = [a,b] by ZFMISC_1:def 2;
reconsider x = a, y = b as Object of A by A18,A19;
A21: <^x,y^> <> {} implies <^F.x,F.y^> <> {} by FUNCTOR0:def 18;
A22: <^x,y^> <> {} implies <^G.x,G.y^> <> {} by FUNCTOR0:def 18;
A23: dom Morph-Map(F,x,y) = <^x,y^> by A21,FUNCT_2:def 1;
A24: dom Morph-Map(G,x,y) = <^x,y^> by A22,FUNCT_2:def 1;
now
let z be object;
assume
A25: z in <^x,y^>;
then reconsider f = z as Morphism of x,y;
thus Morph-Map(F,x,y).z = F.f by A21,A25,FUNCTOR0:def 15
.= G.f by A2,A25
.= Morph-Map(G,x,y).z by A22,A25,FUNCTOR0:def 15;
end;
hence (the MorphMap of F).i = (the MorphMap of G).i by A20,A23,A24;
end;
hence thesis by A17,PBOOLE:3;
end;
scheme ContravariantFunctorLambda { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }:
ex F being contravariant strict Functor of A(),B() st
(for a being Object of A() holds F.a = O(a)) &
for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f)
provided
A1: for a being Object of A() holds O(a) is Object of B() and
A2: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
holds F(a,b,f) in (the Arrows of B()).(O(b), O(a)) and
A3: for a,b,c being Object of A() st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
for a9,b9,c9 being Object of B() st a9 = O(a) & b9 = O(b) & c9 = O(c)
for f9 being Morphism of b9,a9, g9 being Morphism of c9,b9
st f9 = F(a,b,f) & g9 = F(b,c,g) holds F(a,c,g*f) = f9*g9 and
A4: for a being Object of A(), a9 being Object of B() st a9 = O(a)
holds F(a,a,idm a) = idm a9
proof
consider O being Function such that
A5: dom O = the carrier of A() and
A6: for x being object st x in the carrier of A() holds O.x = O(x) from
FUNCT_1:sch 3;
rng O c= the carrier of B()
proof
let y be object;
assume y in rng O;
then consider x being object such that
A7: x in dom O and
A8: y = O.x by FUNCT_1:def 3;
reconsider x as Object of A() by A5,A7;
A9: y = O(x) by A6,A8;
O(x) is Object of B() by A1;
hence thesis by A9;
end;
then reconsider O as Function of the carrier of A(), the carrier of B()
by A5,FUNCT_2:2;
reconsider OM = ~[:O,O:] as
bifunction of the carrier of A(), the carrier of B();
dom [:O,O:] = [:the carrier of A(), the carrier of A():] by A5,FUNCT_3:def 8;
then
A10: dom OM = [:the carrier of A(), the carrier of A():] by FUNCT_4:46;
defpred P[object,object,object] means $1 = F($3`1,$3`2,$2);
A11: for i being object st i in [:the carrier of A(), the carrier of A():]
for x being object st x in (the Arrows of A()).i
ex y being object st y in ((the Arrows of B())*OM).i & P[y,x,i]
proof
let i be object;
assume
A12: i in [:the carrier of A(), the carrier of A():];
then consider a,b being object such that
A13: a in the carrier of A() and
A14: b in the carrier of A() and
A15: [a,b] = i by ZFMISC_1:def 2;
reconsider a,b as Object of A() by A13,A14;
let x be object;
assume
A16: x in (the Arrows of A()).i;
then reconsider f = x as Morphism of a,b by A15;
take y = F(a,b,f);
A17: y in (the Arrows of B()).(O(b), O(a)) by A2,A15,A16;
A18: O(a) = O.a by A6;
((the Arrows of B())*OM).i
= (the Arrows of B()).(OM.(a,b)) by A10,A12,A15,FUNCT_1:13
.= (the Arrows of B()).([:O,O:].(b,a)) by A10,A12,A15,FUNCT_4:43
.= (the Arrows of B()).(O.b,O.a) by A5,FUNCT_3:def 8;
hence y in ((the Arrows of B())*OM).i by A6,A17,A18;
thus thesis by A15;
end;
consider M being ManySortedFunction of the Arrows of A(),
(the Arrows of B())*OM such that
A19: for i be object st i in [:the carrier of A(), the carrier of A():]
ex f be Function of (the Arrows of A()).i, ((the Arrows of B())*OM).i
st f = M.i &
for x be object st x in (the Arrows of A()).i holds P[f.x,x,i]
from MSSUBFAM:sch 1(A11);
reconsider M as MSUnTrans of OM, the Arrows of A(), the Arrows of B()
by FUNCTOR0:def 4;
FunctorStr(#OM, M#) is Contravariant
proof
take O;
thus thesis;
end;
then reconsider F = FunctorStr(#OM, M#) as
Contravariant FunctorStr over A(), B();
A20: now
let a be Object of A();
[a,a] in dom OM by A10,ZFMISC_1:def 2;
hence F.a = ([:O,O:].(a,a))`1 by FUNCT_4:43
.= ([O.a,O.a])`1 by A5,FUNCT_3:def 8
.= O.a
.= O(a) by A6;
end;
A21: now
let o1,o2 be Object of A() such that
A22: <^o1,o2^> <> {};
let g be Morphism of o1,o2;
[o1,o2] in [:the carrier of A(), the carrier of A():] by ZFMISC_1:def 2;
then consider f being Function of (the Arrows of A()).[o1,o2],
((the Arrows of B())*OM).[o1,o2] such that
A23: f = M.[o1,o2] and
A24: for x being object st x in (the Arrows of A()).[o1,o2]
holds f.x = F([o1,o2]`1,[o1,o2]`2,x) by A19;
f.g = F([o1,o2]`1,[o1,o2]`2,g) by A22,A24
.= F(o1,[o1,o2]`2,g)
.= F(o1,o2,g);
hence Morph-Map(F,o1,o2).g = F(o1,o2,g) by A23;
end;
A25: F is feasible
proof
let o1,o2 be Object of A();
set g = the Morphism of o1,o2;
assume
A26: <^o1,o2^> <> {};
then Morph-Map(F,o1,o2).g = F(o1,o2,g) by A21;
then Morph-Map(F,o1,o2).g in (the Arrows of B()).(O(o2), O(o1)) by A2,A26;
then Morph-Map(F,o1,o2).g in (the Arrows of B()).(F.o2, O(o1)) by A20;
hence thesis by A20;
end;
A27: now
let o1,o2 be Object of A();
assume
A28: <^o1,o2^> <> {};
let g be Morphism of o1,o2;
A29: Morph-Map(F,o1,o2).g = F(o1,o2,g) by A21,A28;
<^F.o2, F.o1^> <> {} by A25,A28;
hence F.g = F(o1,o2,g) by A28,A29,FUNCTOR0:def 16;
end;
A30: F is comp-reversing
proof
let o1,o2,o3 be Object of A() such that
A31: <^o1,o2^> <> {} and
A32: <^o2,o3^> <> {};
let f be Morphism of o1,o2, g be Morphism of o2,o3;
set a = O.o1, b = O.o2, c = O.o3;
A33: a = O(o1) by A6;
A34: b = O(o2) by A6;
A35: c = O(o3) by A6;
reconsider f9 = F(o1,o2,f) as Morphism of b, a by A2,A31,A33,A34;
reconsider g9 = F(o2,o3,g) as Morphism of c, b by A2,A32,A34,A35;
A36: a = F.o1 by A20,A33;
A37: b = F.o2 by A20,A34;
A38: c = F.o3 by A20,A35;
reconsider ff = f9 as Morphism of F.o2, F.o1 by A20,A33,A37;
reconsider gg = g9 as Morphism of F.o3, F.o2 by A20,A35,A37;
take ff, gg;
A39: <^o1, o3^> <> {} by A31,A32,ALTCAT_1:def 2;
F(o1,o3,g*f) = ff*gg by A3,A31,A32,A33,A34,A35,A36,A37,A38;
hence ff = Morph-Map(F,o1,o2).f & gg = Morph-Map(F,o2,o3).g &
Morph-Map(F,o1,o3).(g*f) = ff*gg by A21,A31,A32,A39;
end;
F is Functor of A(), B()
proof
thus F is feasible by A25;
hereby
let o be Object of A();
A40: F.o = O(o) by A20;
thus Morph-Map(F,o,o).idm o = F(o,o,idm o) by A21
.= idm F.o by A4,A40;
end;
thus thesis by A30;
end;
then reconsider F as contravariant strict Functor of A(), B()
by A30;
take F;
thus thesis by A20,A27;
end;
theorem Th2:
for A,B being category, F,G being contravariant Functor of A,B
st (for a being Object of A holds F.a = G.a) &
(for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = G.f)
holds the FunctorStr of F = the FunctorStr of G
proof
let A,B be category, F,G be contravariant Functor of A,B such that
A1: for a being Object of A holds F.a = G.a and
A2: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = G.f;
the ObjectMap of F is Contravariant by FUNCTOR0:def 13;
then consider ff being Function of the carrier of A, the carrier of B such
that
A3: the ObjectMap of F = ~[:ff, ff:];
the ObjectMap of G is Contravariant by FUNCTOR0:def 13;
then consider gg being Function of the carrier of A, the carrier of B such
that
A4: the ObjectMap of G = ~[:gg, gg:];
now
let a,b be Element of A;
reconsider x = a, y = b as Object of A;
A5: dom ff = the carrier of A by FUNCT_2:def 1;
A6: dom gg = the carrier of A by FUNCT_2:def 1;
A7: dom [:ff,ff:] = [:the carrier of A, the carrier of A:] by FUNCT_2:def 1;
then
A8: [b,a] in dom [:ff,ff:] by ZFMISC_1:def 2;
A9: dom
[:gg,gg:] = [:the carrier of A, the carrier of A:] by FUNCT_2:def 1;
then
A10: [b,a] in dom [:gg,gg:] by ZFMISC_1:def 2;
A11: [a,a] in dom [:gg,gg:] by A9,ZFMISC_1:def 2;
A12: [b,b] in dom [: gg, gg:] by A9,ZFMISC_1:def 2;
A13: (the ObjectMap of F).(x,x) = [:ff,ff:].(x,x) by A3,A7,A11,FUNCT_4:def 2;
A14: (the ObjectMap of F).(y,y) = [:ff,ff:].(y,y) by A3,A7,A12,FUNCT_4:def 2;
A15: (the ObjectMap of G).(x,x) = [:gg,gg:].(x,x) by A4,A11,FUNCT_4:def 2;
A16: (the ObjectMap of G).(y,y) = [:gg,gg:].(y,y) by A4,A12,FUNCT_4:def 2;
A17: (the ObjectMap of F).(x,x) = [ff.x, ff.x] by A5,A13,FUNCT_3:def 8;
A18: (the ObjectMap of F).(y,y) = [ff.y, ff.y] by A5,A14,FUNCT_3:def 8;
A19: (the ObjectMap of G).(x,x) = [gg.x, gg.x] by A6,A15,FUNCT_3:def 8;
A20: (the ObjectMap of G).(y,y) = [gg.y, gg.y] by A6,A16,FUNCT_3:def 8;
A21: F.x = ff.x by A17;
A22: F.y = ff.y by A18;
A23: G.x = gg.x by A19;
A24: G.y = gg.y by A20;
A25: F.x = G.x by A1;
A26: F.y = G.y by A1;
thus (the ObjectMap of F).(a,b) = [:ff,ff:].(b,a) by A3,A8,FUNCT_4:def 2
.= [ff.b,ff.a] by A5,FUNCT_3:def 8
.= [:gg,gg:].(b,a) by A6,A21,A22,A23,A24,A25,A26,FUNCT_3:def 8
.= (the ObjectMap of G).(a,b) by A4,A10,FUNCT_4:def 2;
end;
then
A27: the ObjectMap of F = the ObjectMap of G;
now
let i be object;
assume i in [:the carrier of A, the carrier of A:];
then consider a,b being object such that
A28: a in the carrier of A and
A29: b in the carrier of A and
A30: i = [a,b] by ZFMISC_1:def 2;
reconsider x = a, y = b as Object of A by A28,A29;
A31: <^x,y^> <> {} implies <^F.y,F.x^> <> {} by FUNCTOR0:def 19;
A32: <^x,y^> <> {} implies <^G.y,G.x^> <> {} by FUNCTOR0:def 19;
A33: dom Morph-Map(F,x,y) = <^x,y^> by A31,FUNCT_2:def 1;
A34: dom Morph-Map(G,x,y) = <^x,y^> by A32,FUNCT_2:def 1;
now
let z be object;
assume
A35: z in <^x,y^>;
then reconsider f = z as Morphism of x,y;
thus Morph-Map(F,x,y).z = F.f by A31,A35,FUNCTOR0:def 16
.= G.f by A2,A35
.= Morph-Map(G,x,y).z by A32,A35,FUNCTOR0:def 16;
end;
hence (the MorphMap of F).i = (the MorphMap of G).i by A30,A33,A34;
end;
hence thesis by A27,PBOOLE:3;
end;
begin
:: <section2>Isomorphism and equivalence of categories</section2>
definition
let A,B,C be non empty set;
let f be Function of [:A,B:], C;
redefine attr f is one-to-one means :: redefines one-to-one (FUNCT_1, definition)
for a1,a2 being Element of A, b1,b2 being Element of B
st f.(a1,b1) = f.(a2,b2) holds a1 = a2 & b1 = b2;
compatibility
proof
A1: dom f = [:A,B:] by FUNCT_2:def 1;
thus f is one-to-one implies
for a1,a2 being Element of A, b1,b2 being Element of B
st f.(a1,b1) = f.(a2,b2) holds a1 = a2 & b1 = b2
proof
assume
A2: for x,y being object st x in dom f & y in dom f & f.x = f.y holds x = y;
let a1,a2 be Element of A, b1,b2 be Element of B;
A3: [a1,b1] in [:A,B :] by ZFMISC_1:def 2;
[a2,b2] in [:A,B:] by ZFMISC_1:def 2;
then f.(a1,b1) = f.(a2,b2) implies [a1,b1] = [a2,b2] by A1,A2,A3;
hence thesis by XTUPLE_0:1;
end;
assume
A4: for a1,a2 being Element of A, b1,b2 being Element of B
st f.(a1,b1) = f.(a2,b2) holds a1 = a2 & b1 = b2;
let x,y be object;
assume x in dom f;
then consider a1,b1 being object such that
A5: a1 in A and
A6: b1 in B and
A7: x = [a1,b1] by ZFMISC_1:def 2;
assume y in dom f;
then consider a2,b2 being object such that
A8: a2 in A and
A9: b2 in B and
A10: y = [a2,b2] by ZFMISC_1:def 2;
reconsider a1, a2 as Element of A by A5,A8;
reconsider b1, b2 as Element of B by A6,A9;
assume f.x = f.y;
then
A11: f.(a1,b1) = f.(a2,b2) by A7,A10;
then a1 = a2 by A4;
hence thesis by A4,A7,A10,A11;
end;
end;
scheme CoBijectiveSch
{ A,B() -> category, F() -> covariant Functor of A(), B(),
O(object) -> object,
F(object,object,object) -> object }: F() is bijective
provided
A1: for a being Object of A() holds F().a = O(a) and
A2: for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F().f = F(a,b,f) and
A3: for a,b being Object of A() st O(a) = O(b) holds a = b and
A4: for a,b being Object of A() st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and
A5: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
ex c,d being Object of A(), g being Morphism of c,d
st a = O(c) & b = O(d) & <^c,d^> <> {} & f = F(c,d,g)
proof
set F = F();
thus the ObjectMap of F is one-to-one
proof
let x1,x2,y1,y2 be Element of A();
reconsider a1 = x1, a2 = x2, b1 = y1, b2 = y2 as Object of A();
assume (the ObjectMap of F).(x1,y1) = (the ObjectMap of F).(x2,y2);
then
A6: [F.a1,F.b1] = (the ObjectMap of F).(x2,y2) by FUNCTOR0:22
.= [F.a2,F.b2] by FUNCTOR0:22;
then
A7: F.a1 = F.a2 by XTUPLE_0:1;
A8: F.b1 = F.b2 by A6,XTUPLE_0:1;
A9: O(a1) = F.a2 by A1,A7;
A10: O(b1) = F.b2 by A1,A8;
A11: O(a1) = O(a2) by A1,A9;
O(b1) = O(b2) by A1,A10;
hence thesis by A3,A11;
end;
now
let i be set;
assume i in [:the carrier of A(), the carrier of A():];
then consider a,b being object such that
A12: a in the carrier of A() and
A13: b in the carrier of A() and
A14: i = [a,b] by ZFMISC_1:def 2;
reconsider a, b as Object of A() by A12,A13;
A15: <^a,b^> <> {} implies <^F.a, F.b^> <> {} by FUNCTOR0:def 18;
Morph-Map(F,a,b) is one-to-one
proof
let x,y be object;
assume that
A16: x in dom Morph-Map(F,a,b) and
A17: y in dom Morph-Map(F,a,b);
reconsider f = x, g = y as Morphism of a,b by A16,A17;
A18: F.f = Morph-Map(F,a,b).x by A15,A16,FUNCTOR0:def 15;
A19: F.g = Morph-Map(F,a,b).y by A15,A16,FUNCTOR0:def 15;
A20: F(a,b,f) = Morph-Map(F,a,b).x by A2,A16,A18;
F(a,b,g) = Morph-Map(F,a,b).y by A2,A16,A19;
hence thesis by A4,A16,A20;
end;
hence (the MorphMap of F).i is one-to-one by A14;
end;
hence the MorphMap of F is "1-1" by MSUALG_3:1;
reconsider G = the MorphMap of F as ManySortedFunction of the Arrows of A(),
(the Arrows of B())*the ObjectMap of F by FUNCTOR0:def 4;
thus F is full
proof
take G;
thus G = the MorphMap of F;
let i be set;
assume i in [:the carrier of A(), the carrier of A():];
then reconsider ab = i as
Element of [:the carrier of A(), the carrier of A():];
G.ab is Function of (the Arrows of A()).ab,
((the Arrows of B())*the ObjectMap of F).ab;
hence rng(G.i) c= ((the Arrows of B())*the ObjectMap of F).i
by RELAT_1:def 19;
consider a,b being object such that
A21: a in the carrier of A() and
A22: b in the carrier of A() and
A23: ab = [a,b] by ZFMISC_1:def 2;
reconsider a, b as Object of A() by A21,A22;
A24: (the ObjectMap of F).ab = (the ObjectMap of F).(a,b) by A23
.= [F.a, F.b] by FUNCTOR0:22;
then
A25: ((the Arrows of B())*the ObjectMap of F).ab = <^F.a, F.b^> by FUNCT_2:15;
let x be object;
assume
A26: x in ((the Arrows of B())*the ObjectMap of F).i;
then reconsider f = x as Morphism of F.a, F.b by A24,FUNCT_2:15;
consider c,d being Object of A(), g being Morphism of c,d such that
A27: F.a = O(c) and
A28: F.b = O(d) and
A29: <^c,d^> <> {} and
A30: f = F(c,d,g) by A5,A25,A26;
A31: O(a) = O(c) by A1,A27;
A32: O(b) = O(d) by A1,A28;
A33: a = c by A3,A31;
A34: b = d by A3,A32;
A35: f = F.g by A2,A29,A30
.= Morph-Map(F,c,d).g by A25,A26,A29,A33,A34,FUNCTOR0:def 15;
dom Morph-Map(F,a,b) = <^a, b^> by A25,A26,FUNCT_2:def 1;
hence thesis by A23,A29,A33,A34,A35,FUNCT_1:def 3;
end;
thus
rng the ObjectMap of F c= [:the carrier of B(), the carrier of B():];
let x be object;
assume x in [:the carrier of B(), the carrier of B():];
then consider a, b being object such that
A36: a in the carrier of B() and
A37: b in the carrier of B() and
A38: x = [a,b] by ZFMISC_1:def 2;
reconsider a, b as Object of B() by A36,A37;
consider c,c9 being Object of A(), g being Morphism of c,c9 such that
A39: a = O(c) and a = O(c9)
and <^c,c9^> <> {}
and idm a = F(c,c9,g) by A5;
consider d,d9 being Object of A(), h being Morphism of d,d9 such that
A40: b = O(d) and b = O(d9)
and <^d,d9^> <> {}
and idm b = F(d,d9,h) by A5;
[c,d] in [:the carrier of A(), the carrier of A():] by ZFMISC_1:def 2;
then
A41: [c,d] in dom the ObjectMap of F by FUNCT_2:def 1;
(the ObjectMap of F).[c,d] = (the ObjectMap of F).(c,d)
.= [F.c, F.d] by FUNCTOR0:22
.= [a, F.d] by A1,A39
.= x by A1,A38,A40;
hence thesis by A41,FUNCT_1:def 3;
end;
scheme CatIsomorphism { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }: A(), B() are_isomorphic
provided
A1: ex F being covariant Functor of A(),B() st
(for a being Object of A() holds F.a = O(a)) &
for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f) and
A2: for a,b being Object of A() st O(a) = O(b) holds a = b and
A3: for a,b being Object of A() st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and
A4: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
ex c,d being Object of A(), g being Morphism of c,d
st a = O(c) & b = O(d) & <^c,d^> <> {} & f = F(c,d,g)
proof
A5: for a,b being Object of A() st O(a) = O(b) holds a = b by A2;
A6: for a,b being Object of A() st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g by A3;
A7: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
ex c,d being Object of A(), g being Morphism of c,d
st a = O(c) & b = O(d) & <^c,d^> <> {} & f = F(c,d,g) by A4;
consider F being covariant Functor of A(),B() such that
A8: for a being Object of A() holds F.a = O(a) and
A9: for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f) by A1;
take F;
thus F is bijective from CoBijectiveSch(A8,A9,A5,A6,
A7);
thus thesis;
end;
scheme ContraBijectiveSch
{ A,B() -> category, F() -> contravariant Functor of A(), B(),
O(object) -> object, F(object,object,object) -> object }: F() is bijective
provided
A1: for a being Object of A() holds F().a = O(a) and
A2: for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F().f = F(a,b,f) and
A3: for a,b being Object of A() st O(a) = O(b) holds a = b and
A4: for a,b being Object of A() st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and
A5: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
ex c,d being Object of A(), g being Morphism of c,d
st b = O(c) & a = O(d) & <^c,d^> <> {} & f = F(c,d,g)
proof
set F = F();
thus the ObjectMap of F is one-to-one
proof
let x1,x2,y1,y2 be Element of A();
reconsider a1 = x1, a2 = x2, b1 = y1, b2 = y2 as Object of A();
assume (the ObjectMap of F).(x1,y1) = (the ObjectMap of F).(x2,y2);
then
A6: [F.b1,F.a1] = (the ObjectMap of F).(x2,y2) by FUNCTOR0:23
.= [F.b2,F.a2] by FUNCTOR0:23;
then
A7: F.a1 = F.a2 by XTUPLE_0:1;
A8: F.b1 = F.b2 by A6,XTUPLE_0:1;
A9: O(a1) = F.a2 by A1,A7;
A10: O(b1) = F.b2 by A1,A8;
A11: O(a1) = O(a2) by A1,A9;
O(b1) = O(b2) by A1,A10;
hence thesis by A3,A11;
end;
now
let i be set;
assume i in [:the carrier of A(), the carrier of A():];
then consider a,b being object such that
A12: a in the carrier of A() and
A13: b in the carrier of A() and
A14: i = [a,b] by ZFMISC_1:def 2;
reconsider a, b as Object of A() by A12,A13;
A15: <^a,b^> <> {} implies <^F.b, F.a^> <> {} by FUNCTOR0:def 19;
Morph-Map(F,a,b) is one-to-one
proof
let x,y be object;
assume that
A16: x in dom Morph-Map(F,a,b) and
A17: y in dom Morph-Map(F,a,b);
reconsider f = x, g = y as Morphism of a,b by A16,A17;
A18: F.f = Morph-Map(F,a,b).x by A15,A16,FUNCTOR0:def 16;
A19: F.g = Morph-Map(F,a,b).y by A15,A16,FUNCTOR0:def 16;
A20: F(a,b,f) = Morph-Map(F,a,b).x by A2,A16,A18;
F(a,b,g) = Morph-Map(F,a,b).y by A2,A16,A19;
hence thesis by A4,A16,A20;
end;
hence (the MorphMap of F).i is one-to-one by A14;
end;
hence the MorphMap of F is "1-1" by MSUALG_3:1;
reconsider G = the MorphMap of F as ManySortedFunction of the Arrows of A(),
(the Arrows of B())*the ObjectMap of F by FUNCTOR0:def 4;
thus F is full
proof
take G;
thus G = the MorphMap of F;
let i be set;
assume i in [:the carrier of A(), the carrier of A():];
then reconsider ab = i as
Element of [:the carrier of A(), the carrier of A():];
G.ab is Function of (the Arrows of A()).ab,
((the Arrows of B())*the ObjectMap of F).ab;
hence rng(G.i) c= ((the Arrows of B())*the ObjectMap of F).i
by RELAT_1:def 19;
consider a,b being object such that
A21: a in the carrier of A() and
A22: b in the carrier of A() and
A23: ab = [a,b] by ZFMISC_1:def 2;
reconsider a, b as Object of A() by A21,A22;
A24: (the ObjectMap of F).ab = (the ObjectMap of F).(a,b) by A23
.= [F.b, F.a] by FUNCTOR0:23;
then
A25: ((the Arrows of B())*the ObjectMap of F).ab = <^F.b, F.a^> by FUNCT_2:15;
let x be object;
assume
A26: x in ((the Arrows of B())*the ObjectMap of F).i;
then reconsider f = x as Morphism of F.b, F.a by A24,FUNCT_2:15;
consider c,d being Object of A(), g being Morphism of c,d such that
A27: F.a = O(c) and
A28: F.b = O(d) and
A29: <^c,d^> <> {} and
A30: f = F(c,d,g) by A5,A25,A26;
A31: O(a) = O(c) by A1,A27;
A32: O(b) = O(d) by A1,A28;
A33: a = c by A3,A31;
A34: b = d by A3,A32;
A35: f = F.g by A2,A29,A30
.= Morph-Map(F,c,d).g by A25,A26,A29,A33,A34,FUNCTOR0:def 16;
dom Morph-Map(F,a,b) = <^a, b^> by A25,A26,FUNCT_2:def 1;
hence thesis by A23,A29,A33,A34,A35,FUNCT_1:def 3;
end;
thus
rng the ObjectMap of F c= [:the carrier of B(), the carrier of B():];
let x be object;
assume x in [:the carrier of B(), the carrier of B():];
then consider a, b being object such that
A36: a in the carrier of B() and
A37: b in the carrier of B() and
A38: x = [a,b] by ZFMISC_1:def 2;
reconsider a, b as Object of B() by A36,A37;
consider c,c9 being Object of A(), g being Morphism of c,c9 such that
A39: a = O(c) and a = O(c9)
and <^c,c9^> <> {}
and idm a = F(c,c9,g) by A5;
consider d,d9 being Object of A(), h being Morphism of d,d9 such that
A40: b = O(d) and b = O(d9)
and <^d,d9^> <> {}
and idm b = F(d,d9,h) by A5;
[d,c] in [:the carrier of A(), the carrier of A():] by ZFMISC_1:def 2;
then
A41: [d,c] in dom the ObjectMap of F by FUNCT_2:def 1;
(the ObjectMap of F).[d,c] = (the ObjectMap of F).(d,c)
.= [F.c, F.d] by FUNCTOR0:23
.= [a, F.d] by A1,A39
.= x by A1,A38,A40;
hence thesis by A41,FUNCT_1:def 3;
end;
scheme CatAntiIsomorphism { A,B() -> category, O(object) -> object,
F(object,object,object) -> object }: A(), B() are_anti-isomorphic
provided
A1: ex F being contravariant Functor of A(),B() st
(for a being Object of A() holds F.a = O(a)) &
for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f) and
A2: for a,b being Object of A() st O(a) = O(b) holds a = b and
A3: for a,b being Object of A() st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g and
A4: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
ex c,d being Object of A(), g being Morphism of c,d
st b = O(c) & a = O(d) & <^c,d^> <> {} & f = F(c,d,g)
proof
consider F being contravariant Functor of A(),B() such that
A5: for a being Object of A() holds F.a = O(a) and
A6: for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f) by A1;
A7: for a,b being Object of A() st O(a) = O(b) holds a = b by A2;
A8: for a,b being Object of A() st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g by A3;
A9: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
ex c,d being Object of A(), g being Morphism of c,d
st b = O(c) & a = O(d) & <^c,d^> <> {} & f = F(c,d,g) by A4;
take F;
thus F is bijective from ContraBijectiveSch(A5,A6,A7,A8
,A9);
thus thesis;
end;
definition
let A,B be category;
pred A,B are_equivalent means
ex F being covariant Functor of A,B,
G being covariant Functor of B,A st G*F, id A are_naturally_equivalent &
F*G, id B are_naturally_equivalent;
reflexivity
proof
let A be category;
take id A, id A;
thus thesis by FUNCTOR3:4;
end;
symmetry;
end;
theorem Th3:
for A,B,C being non empty reflexive AltGraph
for F1,F2 being feasible FunctorStr over A,B
for G1,G2 being FunctorStr over B,C
st the FunctorStr of F1 = the FunctorStr of F2 &
the FunctorStr of G1 = the FunctorStr of G2 holds G1*F1 = G2*F2
proof
let A,B,C be non empty reflexive AltGraph;
let F1,F2 be feasible FunctorStr over A,B;
let G1,G2 be FunctorStr over B,C such that
A1: the FunctorStr of F1 = the FunctorStr of F2 and
A2: the FunctorStr of G1 = the FunctorStr of G2;
A3: the ObjectMap of (G1*F1) = (the ObjectMap of G1)*the ObjectMap of F1 by
FUNCTOR0:def 36;
the MorphMap of (G1*F1) = ((the MorphMap of G1)*the ObjectMap of F1)**
the MorphMap of F1 by FUNCTOR0:def 36;
hence thesis by A1,A2,A3,FUNCTOR0:def 36;
end;
theorem Th4:
for A,B,C being category st A,B are_equivalent & B,C are_equivalent
holds A,C are_equivalent
proof
let A,B,C be category;
given F1 being covariant Functor of A,B,
G1 being covariant Functor of B,A such that
A1: G1*F1, id A are_naturally_equivalent and
A2: F1*G1, id B are_naturally_equivalent;
given F2 being covariant Functor of B,C,
G2 being covariant Functor of C,B such that
A3: G2*F2, id B are_naturally_equivalent and
A4: F2*G2, id C are_naturally_equivalent;
take F = F2*F1, G = G1*G2;
the FunctorStr of F1 = the FunctorStr of F1;
then
A5: (the FunctorStr of G1)*F1 = G1*F1 by Th3;
the FunctorStr of G2 = the FunctorStr of G2;
then
A6: (the FunctorStr of F2)*G2 = F2*G2 by Th3;
A7: G1* id B = the FunctorStr of G1 by FUNCTOR3:5;
A8: F2* id B = the FunctorStr of F2 by FUNCTOR3:5;
A9: G*F2 = G1*(G2*F2) by FUNCTOR0:32;
A10: F*G1 = F2*(F1*G1) by FUNCTOR0:32;
A11: G*F2*F1 = G*F by FUNCTOR0:32;
A12: F*G1*G2 = F*G by FUNCTOR0:32;
A13: G*F2, G1* id B are_naturally_equivalent by A3,A9,FUNCTOR3:35;
A14: F*G1, F2* id B are_naturally_equivalent by A2,A10,FUNCTOR3:35;
A15: G*F, G1*F1 are_naturally_equivalent by A5,A7,A11,A13,FUNCTOR3:36;
F*G, F2*G2 are_naturally_equivalent by A6,A8,A12,A14,FUNCTOR3:36;
hence thesis by A1,A4,A15,FUNCTOR3:33;
end;
theorem Th5:
for A,B being category st A,B are_isomorphic holds A,B are_equivalent
proof
let A,B be category;
assume A,B are_isomorphic;
then consider F being Functor of A,B such that
A1: F is bijective covariant;
reconsider F as covariant Functor of A,B by A1;
consider G being Functor of B,A such that
A2: G = F" and
A3: G is bijective covariant by A1,FUNCTOR0:48;
reconsider G as covariant Functor of B,A by A3;
take F, G;
thus thesis by A1,A2,FUNCTOR1:18,19;
end;
scheme NatTransLambda { A, B() -> category,
F, G() -> covariant Functor of A(), B(), T(object) -> object }:
ex t being natural_transformation of F(), G() st
F() is_naturally_transformable_to G() &
for a being Object of A() holds t!a = T(a)
provided
A1: for a being Object of A() holds T(a) in <^F().a, G().a^> and
A2: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
for g1 being Morphism of F().a, G().a st g1 = T(a)
for g2 being Morphism of F().b, G().b st g2 = T(b) holds g2*F().f = G().f*g1
proof
consider t being ManySortedSet of the carrier of A() such that
A3: for a being Element of A() holds t.a = T(a) from PBOOLE:sch 5;
A4: F() is_transformable_to G()
by A1;
now
let a be Object of A();
t.a = T(a) by A3;
hence t.a is Morphism of F().a, G().a by A1;
end;
then reconsider t as transformation of F(), G() by A4,FUNCTOR2:def 2;
A5: now
let a be Object of A();
t.a = T(a) by A3;
hence t!a = T(a) by A4,FUNCTOR2:def 4;
end;
A6: F() is_naturally_transformable_to G()
proof
thus F() is_transformable_to G() by A4;
take t;
let a,b be Object of A();
A7: t!a = T(a) by A5;
t!b = T(b) by A5;
hence thesis by A2,A7;
end;
now
let a,b be Object of A();
A8: t!a = T(a) by A5;
t!b = T(b) by A5;
hence <^a,b^> <> {} implies
for f being Morphism of a,b holds t!b*F().f = G().f*(t!a) by A2,A8;
end;
then t is natural_transformation of F(), G() by A6,FUNCTOR2:def 7;
hence thesis by A5,A6;
end;
scheme NatEquivalenceLambda { A, B() -> category,
F, G() -> covariant Functor of A(), B(), T(object) -> object }:
ex t being natural_equivalence of F(), G() st
F(), G() are_naturally_equivalent &
for a being Object of A() holds t!a = T(a)
provided
A1: for a being Object of A() holds
T(a) in <^F().a, G().a^> & <^G().a, F().a^> <> {} &
for f being Morphism of F().a, G().a st f = T(a) holds f is iso and
A2: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
for g1 being Morphism of F().a, G().a st g1 = T(a)
for g2 being Morphism of F().b, G().b st g2 = T(b) holds g2*F().f = G().f*g1
proof
A3: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
for g1 being Morphism of F().a, G().a st g1 = T(a)
for g2 being Morphism of F().b, G().b st g2 = T(b)
holds g2*F().f = G().f*g1 by A2;
A4: for a being Object of A() holds T(a) in <^F().a, G().a^> by A1;
consider t being natural_transformation of F(), G() such that
A5: F() is_naturally_transformable_to G() and
A6: for a being Object of A() holds t!a = T(a) from NatTransLambda(A4,A3
);
A7: G() is_transformable_to F()
by A1;
A8: F(), G() are_naturally_equivalent
proof
thus F() is_naturally_transformable_to G() by A5;
thus G() is_transformable_to F() by A7;
take t;
let a be Object of A();
t!a = T(a) by A6;
hence thesis by A1;
end;
now
let a be Object of A();
t!a = T(a) by A6;
hence t!a is iso by A1;
end;
then t is natural_equivalence of F(), G() by A8,FUNCTOR3:def 5;
hence thesis by A6,A8;
end;
begin
:: <section3>Dual categories</section3>
definition
let C1,C2 be non empty AltCatStr;
pred C1, C2 are_opposite means
the carrier of C2 = the carrier of C1 &
the Arrows of C2 = ~the Arrows of C1 & for a,b,c being Object of C1
for a9,b9,c9 being Object of C2 st a9 = a & b9 = b & c9 = c
holds (the Comp of C2).(a9,b9,c9) = ~((the Comp of C1).(c,b,a));
symmetry
proof
let C1,C2 be non empty AltCatStr;
assume that
A1: the carrier of C2 = the carrier of C1 and
A2: the Arrows of C2 = ~the Arrows of C1 and
A3: for a,b,c being Object of C1
for a9,b9,c9 being Object of C2 st a9 = a & b9 = b & c9 = c
holds (the Comp of C2).(a9,b9,c9) = ~((the Comp of C1).(c,b,a));
thus the carrier of C1 = the carrier of C2 by A1;
dom the Arrows of C1 = [:the carrier of C1, the carrier of C1:]
by PARTFUN1:def 2;
hence the Arrows of C1 = ~the Arrows of C2 by A2,FUNCT_4:52;
let a,b,c be Object of C2;
let a9,b9,c9 be Object of C1;
assume that
A4: a9 = a and
A5: b9 = b and
A6: c9 = c;
A7: (the Comp of C2).(c,b,a) = ~((the Comp of C1).(a9,b9,c9)) by A3,A4,A5,A6;
dom ((the Comp of C1).(a9,b9,c9)) c=
[:(the Arrows of C1).(b9,c9), (the Arrows of C1).(a9,b9):];
hence thesis by A7,FUNCT_4:52;
end;
end;
theorem
for A,B being non empty AltCatStr st A, B are_opposite
for a being Object of A holds a is Object of B;
theorem Th7:
for A,B being non empty AltCatStr st A, B are_opposite
for a,b being Object of A, a9,b9 being Object of B st a9 = a & b9 = b
holds <^a,b^> = <^b9,a9^>
by ALTCAT_2:6;
theorem
for A,B being non empty AltCatStr st A, B are_opposite
for a,b being Object of A, a9,b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b holds f is Morphism of b9, a9 by Th7;
theorem Th9:
for C1,C2 being non empty transitive AltCatStr holds C1, C2 are_opposite iff
the carrier of C2 = the carrier of C1 & for a,b,c being Object of C1
for a9,b9,c9 being Object of C2 st a9 = a & b9 = b & c9 = c holds
<^a,b^> = <^b9,a9^> & (<^a,b^> <> {} & <^b,c^> <> {} implies
for f being Morphism of a,b, g being Morphism of b,c
for f9 being Morphism of b9,a9, g9 being Morphism of c9,b9
st f9 = f & g9 = g holds f9*g9 = g*f)
proof
let C1,C2 be non empty transitive AltCatStr;
A1: dom the Arrows of C1 = [:the carrier of C1, the carrier of C1:] by
PARTFUN1:def 2;
A2: dom the Arrows of C2 = [:the carrier of C2, the carrier of C2:] by
PARTFUN1:def 2;
hereby
assume
A3: C1, C2 are_opposite;
hence the carrier of C2 = the carrier of C1;
let a,b,c be Object of C1;
let a9,b9,c9 be Object of C2 such that
A4: a9 = a and
A5: b9 = b and
A6: c9 = c;
A7: [a,b] in dom the Arrows of C1 by A1,ZFMISC_1:def 2;
A8: [b,c] in dom the Arrows of C1 by A1,ZFMISC_1:def 2;
thus
A9: <^a,b^> = (~the Arrows of C1).(b,a) by A7,FUNCT_4:def 2
.= <^b9,a9^> by A3,A4,A5;
A10: <^b,c^> = (~the Arrows of C1).(c,b) by A8,FUNCT_4:def 2
.= <^c9,b9^> by A3,A5,A6;
A11: (the Comp of C2).(c9,b9,a9) = ~((the Comp of C1).(a,b,c)) by A3,A4,A5,A6;
assume that
A12: <^a,b^> <> {} and
A13: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
<^a,c^> <> {} by A12,A13,ALTCAT_1:def 2;
then dom ((the Comp of C1).(a,b,c)) =
[:(the Arrows of C1).(b,c), (the Arrows of C1).(a,b):] by FUNCT_2:def 1;
then
A14: [g,f] in dom ((the Comp of C1).(a,b,c)) by A12,A13,ZFMISC_1:def 2;
let f9 be Morphism of b9,a9, g9 be Morphism of c9,b9;
assume that
A15: f9 = f and
A16: g9 = g;
thus f9*g9
= (~((the Comp of C1).(a,b,c))).(f,g) by A9,A10,A11,A12,A13,A15,A16,
ALTCAT_1:def 8
.= ((the Comp of C1).(a,b,c)).(g,f) by A14,FUNCT_4:def 2
.= g*f by A12,A13,ALTCAT_1:def 8;
end;
assume that
A17: the carrier of C2 = the carrier of C1 and
A18: for a,b,c being Object of C1
for a9,b9,c9 being Object of C2 st a9 = a & b9 = b & c9 = c
holds <^a,b^> = <^b9,a9^> & (<^a,b^> <> {} & <^b,c^> <> {} implies
for f being Morphism of a,b, g being Morphism of b,c
for f9 being Morphism of b9,a9, g9 being Morphism of c9,b9
st f9 = f & g9 = g holds f9*g9 = g*f);
thus the carrier of C2 = the carrier of C1 by A17;
A19: now
let x be object;
hereby
assume x in dom the Arrows of C2;
then consider y,z being object such that
A20: y in the carrier of C1 and
A21: z in the carrier of C1 and
A22: [y,z] = x by A17,ZFMISC_1:def 2;
take z,y;
thus x = [y,z] & [z,y] in dom the Arrows of C1 by A1,A20,A21,A22,
ZFMISC_1:def 2;
end;
given z,y being object such that
A23: x = [y,z] and
A24: [z,y] in dom the Arrows of C1;
A25: z in the carrier of C1 by A24,ZFMISC_1:87;
y in the carrier of C1 by A24,ZFMISC_1:87;
hence x in dom the Arrows of C2 by A2,A17,A23,A25,ZFMISC_1:def 2;
end;
now
let y,z be object;
assume [y,z] in dom the Arrows of C1;
then reconsider a = y, b = z as Object of C1 by ZFMISC_1:87;
reconsider a9 = a, b9 = b as Object of C2 by A17;
thus (the Arrows of C2).(z,y) = <^b9,a9^> .= <^a,b^> by A18
.= (the Arrows of C1).(y,z);
end;
hence the Arrows of C2 = ~the Arrows of C1 by A19,FUNCT_4:def 2;
let a,b,c be Object of C1, a9,b9,c9 be Object of C2 such that
A26: a9 = a and
A27: b9 = b and
A28: c9 = c;
A29: <^a9,b9^> = <^b,a^> by A18,A26,A27;
A30: <^b9,c9^> = <^c,b^> by A18,A27,A28;
A31: <^a9,c9^> = <^c,a^> by A18,A26,A28;
[:<^b,a^>,<^c,b^>:] <> {} implies <^b,a^> <> {} & <^c,b^> <> {}
by ZFMISC_1:90;
then [:<^b,a^>,<^c,b^>:] <> {} implies <^c,a^> <> {} by ALTCAT_1:def 2;
then
A32: dom ((the Comp of C1).(c,b,a))
= [:(the Arrows of C1).(b,a), (the Arrows of C1).(c,b):] by FUNCT_2:def 1;
[:<^c,b^>,<^b,a^>:] <> {} implies <^b,a^> <> {} & <^c,b^> <> {}
by ZFMISC_1:90;
then [:<^c,b^>,<^b,a^>:] <> {} implies <^c,a^> <> {} by ALTCAT_1:def 2;
then
A33: dom ((the Comp of C2).(a9,b9,c9))
= [:(the Arrows of C2).(b9,c9), (the Arrows of C2).(a9,b9):]
by A29,A30,A31,FUNCT_2:def 1;
A34: now
let x be object;
hereby
assume x in dom ((the Comp of C2).(a9,b9,c9));
then consider y,z being object such that
A35: y in <^b9,c9^> and
A36: z in <^a9,b9^> and
A37: [y,z] = x by ZFMISC_1:def 2;
take z,y;
thus x = [y,z] & [z,y] in dom ((the Comp of C1).(c,b,a))
by A29,A30,A32,A35,A36,A37,ZFMISC_1:def 2;
end;
given z,y being object such that
A38: x = [y,z] and
A39: [z,y] in dom ((the Comp of C1).(c,b,a));
A40: z in <^b,a^> by A39,ZFMISC_1:87;
y in <^c,b^> by A39,ZFMISC_1:87;
hence x in dom ((the Comp of C2).(a9,b9,c9)) by A29,A30,A33,A38,A40,
ZFMISC_1:def 2;
end;
now
let y,z be object;
assume
A41: [y,z] in dom ((the Comp of C1).(c,b,a ) );
then
A42: y in <^b,a^> by ZFMISC_1:87;
A43: z in <^c,b^> by A41,ZFMISC_1:87;
reconsider f = y as Morphism of b,a by A41,ZFMISC_1:87;
reconsider g = z as Morphism of c,b by A41,ZFMISC_1:87;
reconsider f9 = y as Morphism of a9,b9 by A18,A26,A27,A42;
reconsider g9 = z as Morphism of b9,c9 by A18,A27,A28,A43;
thus ((the Comp of C2).(a9,b9,c9)).(z,y)
= g9*f9 by A29,A30,A42,A43,ALTCAT_1:def 8
.= f*g by A18,A26,A27,A28,A42,A43
.= ((the Comp of C1).(c,b,a)).(y,z) by A42,A43,ALTCAT_1:def 8;
end;
hence thesis by A34,FUNCT_4:def 2;
end;
theorem Th10:
for A,B being category st A, B are_opposite
for a being Object of A, b being Object of B st a = b holds idm a = idm b
proof
let A,B be category such that
A1: A, B are_opposite;
let a be Object of A, b be Object of B such that
A2: a = b;
reconsider i = idm b as Morphism of a,a by A1,A2,Th9;
now
let c be Object of A;
assume
A3: <^a,c^> <> {};
let f be Morphism of a,c;
reconsider d = c as Object of B by A1;
A4: <^a,c^> = <^d,b^> by A1,A2,Th9;
reconsider g = f as Morphism of d,b by A1,A2,Th9;
thus f*i = (idm b)*g by A1,A2,A3,Th9
.= f by A3,A4,ALTCAT_1:20;
end;
hence thesis by ALTCAT_1:def 17;
end;
theorem Th11:
for A,B being transitive non empty AltCatStr st A,B are_opposite
holds A is associative implies B is associative
proof
let A,B be transitive non empty AltCatStr such that
A1: A,B are_opposite and
A2: A is associative;
deffunc C(set,set,set,set,set) = ((the Comp of A).($3,$2,$1)).($4,$5);
A3: now
let a,b,c be Object of B such that
A4: <^a,b^> <> {} and
A5: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
reconsider a9 = a, b9 = b, c9 = c as Object of A by A1;
A6: <^a,b^> = <^b9,a9^> by A1,Th7;
A7: <^b,c^> = <^c9,b9^> by A1,Th7;
reconsider f9 = f as Morphism of b9, a9 by A1,Th7;
reconsider g9 = g as Morphism of c9, b9 by A1,Th7;
thus g*f = f9*g9 by A1,A4,A5,Th9
.= C(a,b,c,f,g) by A4,A5,A6,A7,ALTCAT_1:def 8;
end;
A8: now
let a,b,c,d be Object of B, f,g,h be set;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Object of A by A1;
assume
A9: f in <^a,b^>;
then
A10: f in <^b9,a9^> by A1,Th9;
reconsider f9 = f as Morphism of b9,a9 by A1,A9,Th9;
assume
A11: g in <^b,c^>;
then
A12: g in <^c9,b9^> by A1,Th9;
reconsider g9 = g as Morphism of c9,b9 by A1,A11,Th9;
assume
A13: h in <^c,d^>;
then
A14: h in <^d9,c9^> by A1,Th9;
reconsider h9 = h as Morphism of d9,c9 by A1,A13,Th9;
A15: <^c9,a9^> <> {} by A10,A12,ALTCAT_1:def 2;
A16: <^d9,b9^> <> {} by A12,A14,ALTCAT_1:def 2;
thus C(a,c,d,C(a,b,c,f,g),h) = C(a,c,d,f9*g9,h) by A10,A12,ALTCAT_1:def 8
.= (f9*g9)*h9 by A14,A15,ALTCAT_1:def 8
.= f9*(g9*h9) by A2,A10,A12,A14
.= C(a,b,d,f,g9*h9) by A10,A16,ALTCAT_1:def 8
.= C(a,b,d,f,C(b,c,d,g,h)) by A12,A14,ALTCAT_1:def 8;
end;
thus thesis from CatAssocSch(A3,A8);
end;
theorem Th12:
for A,B being transitive non empty AltCatStr st A,B are_opposite
holds A is with_units implies B is with_units
proof
let A,B be transitive non empty AltCatStr such that
A1: A,B are_opposite;
assume A is with_units;
then reconsider A as with_units transitive non empty AltCatStr;
deffunc C(set,set,set,set,set) = ((the Comp of A).($3,$2,$1)).($4,$5);
A2: now
let a,b,c be Object of B such that
A3: <^a,b^> <> {} and
A4: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
reconsider a9 = a, b9 = b, c9 = c as Object of A by A1;
A5: <^a,b^> = <^b9,a9^> by A1,Th7;
A6: <^b,c^> = <^c9,b9^> by A1,Th7;
reconsider f9 = f as Morphism of b9, a9 by A1,Th7;
reconsider g9 = g as Morphism of c9, b9 by A1,Th7;
thus g*f = f9*g9 by A1,A3,A4,Th9
.= C(a,b,c,f,g) by A3,A4,A5,A6,ALTCAT_1:def 8;
end;
A7: now
let a be Object of B;
reconsider a9 = a as Object of A by A1;
reconsider f = idm a9 as set;
take f;
idm a9 in <^a9,a9^>;
hence f in <^a,a^> by A1,Th7;
let b be Object of B, g be set;
reconsider b9 = b as Object of A by A1;
assume
A8: g in <^a,b^>;
then
A9: g in <^b9,a9^> by A1,Th7;
reconsider g9 = g as Morphism of b9,a9 by A1,A8,Th7;
thus C(a,a,b,f,g) = (idm a9)*g9 by A9,ALTCAT_1:def 8
.= g by A9,ALTCAT_1:20;
end;
A10: now
let a be Object of B;
reconsider a9 = a as Object of A by A1;
reconsider f = idm a9 as set;
take f;
idm a9 in <^a9,a9^>;
hence f in <^a,a^> by A1,Th7;
let b be Object of B, g be set;
reconsider b9 = b as Object of A by A1;
assume
A11: g in <^b,a^>;
then
A12: g in <^a9,b9^> by A1,Th7;
reconsider g9 = g as Morphism of a9,b9 by A1,A11,Th7;
thus C(b,a,a,g,f) = g9*(idm a9) by A12,ALTCAT_1:def 8
.= g by A12,ALTCAT_1:def 17;
end;
thus thesis from CatUnitsSch(A2,A7,A10);
end;
theorem Th13:
for C,C1,C2 being non empty AltCatStr st C, C1 are_opposite
holds C, C2 are_opposite iff the AltCatStr of C1 = the AltCatStr of C2
proof
let C, C1, C2 be non empty AltCatStr such that
A1: the carrier of C1 = the carrier of C and
A2: the Arrows of C1 = ~the Arrows of C and
A3: for a,b,c being Object of C
for a9,b9,c9 being Object of C1 st a9 = a & b9 = b & c9 = c
holds (the Comp of C1).(a9,b9,c9) = ~((the Comp of C).(c,b,a));
thus
C, C2 are_opposite implies the AltCatStr of C1 = the AltCatStr of C2
proof
assume that
A4: the carrier of C2 = the carrier of C and
A5: the Arrows of C2 = ~the Arrows of C and
A6: for a,b,c being Object of C
for a9,b9,c9 being Object of C2 st a9 = a & b9 = b & c9 = c
holds (the Comp of C2).(a9,b9,c9) = ~((the Comp of C).(c,b,a));
A7: dom the Comp of C1 = [:the carrier of C1, the carrier of C1,
the carrier of C1:] by PARTFUN1:def 2;
A8: dom the Comp of C2 = [:the carrier of C2, the carrier of C2,
the carrier of C2:] by PARTFUN1:def 2;
now
let x be object;
assume x in [:the carrier of C, the carrier of C, the carrier of C:];
then consider a,b,c being object such that
A9: a in the carrier of C and
A10: b in the carrier of C and
A11: c in the carrier of C and
A12: x = [a,b,c] by MCART_1:68;
reconsider a, b, c as Object of C by A9,A10,A11;
reconsider a1 = a, b1 = b, c1 = c as Object of C1 by A1;
reconsider a2 = a, b2 = b, c2 = c as Object of C2 by A4;
A13: (the Comp of C1).(a1,b1,c1) = ~((the Comp of C).(c,b,a)) by A3;
(the Comp of C2).(a2,b2,c2) = ~((the Comp of C).(c,b,a)) by A6;
hence (the Comp of C1).x = (the Comp of C2).(a2,b2,c2)
by A12,A13,MULTOP_1:def 1
.= (the Comp of C2).x by A12,MULTOP_1:def 1;
end;
hence thesis by A1,A2,A4,A5,A7,A8,FUNCT_1:2;
end;
assume
A14: the AltCatStr of C1 = the AltCatStr of C2;
hence the carrier of C2 = the carrier of C &
the Arrows of C2 = ~the Arrows of C by A1,A2;
let a,b,c be Object of C, a9,b9,c9 be Object of C2;
thus thesis by A3,A14;
end;
definition
let C be transitive non empty AltCatStr;
func C opp -> strict transitive non empty AltCatStr means
:
Def4: C, it are_opposite;
uniqueness by Th13;
existence
proof
deffunc B(set,set) = (the Arrows of C).($2,$1);
deffunc C(set,set,set,set,set) = ((the Comp of C).($3,$2,$1)).($4,$5);
A1: now
let a,b,c be Element of C, f,g be set;
reconsider a9 = a, b9 = b, c9 = c as Object of C;
assume
A2: f in B(a,b);
then
A3: f in <^b9,a9^>;
reconsider f9 = f as Morphism of b9,a9 by A2;
assume
A4: g in B(b,c);
then
A5: g in <^c9,b9^>;
reconsider g9 = g as Morphism of c9,b9 by A4;
A6: <^c9,a9^> <> {} by A3,A5,ALTCAT_1:def 2;
C(a,b,c,f,g) = f9*g9 by A2,A4,ALTCAT_1:def 8;
hence C(a,b,c,f,g) in B(a,c) by A6;
end;
ex C1 being strict non empty transitive AltCatStr st
the carrier of C1 = the carrier of C &
(for a,b being Object of C1 holds <^a,b^> = B(a,b)) &
for a,b,c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g) from AltCatStrLambda(A1);
then consider C1 being strict transitive non empty AltCatStr such that
A7: the carrier of C1 = the carrier of C and
A8: for a,b being Object of C1 holds <^a,b^> = (the Arrows of C).(b,a) and
A9: for a,b,c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = ((the Comp of C).(c,b,a)).(f,g);
take C1;
now
let a,b,c be Object of C;
let a9,b9,c9 be Object of C1;
assume that
A10: a9 = a and
A11: b9 = b and
A12: c9 = c;
thus
A13: <^a,b^> = <^b9,a9^> by A8,A10,A11;
A14: <^b,c^> = <^c9,b9^> by A8,A11,A12;
assume that
A15: <^a,b^> <> {} and
A16: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
let f9 be Morphism of b9,a9, g9 be Morphism of c9,b9;
assume that
A17: f9 = f and
A18: g9 = g;
thus f9*g9 = ((the Comp of C).(a,b,c)).(g,f) by A9,A10,A11,A12,A13,A14,A15
,A16,A17,A18
.= g*f by A15,A16,ALTCAT_1:def 8;
end;
hence thesis by A7,Th9;
end;
end;
registration
let C be associative transitive non empty AltCatStr;
cluster C opp -> associative;
coherence
by Def4,Th11;
end;
registration
let C be with_units transitive non empty AltCatStr;
cluster C opp -> with_units;
coherence
by Def4,Th12;
end;
definition
let A,B be category such that
A1: A, B are_opposite;
deffunc O(set) = $1;
deffunc F(set,set,set) = $3;
A2: for a being Object of A holds O(a) is Object of B by A1;
A3: now
let a,b be Object of A such that
A4: <^a,b^> <> {};
let f be Morphism of a,b;
reconsider a9 = a, b9 = b as Object of B by A2;
<^a,b^> = <^b9,a9^> by A1,Th9
.= (the Arrows of B).(b, a);
hence F(a,b,f) in (the Arrows of B).(O(b), O(a)) by A4;
end;
A5: for a,b,c being Object of A st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
for a9,b9,c9 being Object of B st a9 = O(a) & b9 = O(b) & c9 = O(c)
for f9 being Morphism of b9,a9, g9 being Morphism of c9,b9
st f9 = F(a,b,f) & g9 = F(b,c,g) holds F(a,c,g*f) = f9*g9 by A1,Th9;
A6: for a being Object of A, a9 being Object of B st a9 = O(a)
holds F(a,a,idm a) = idm a9 by A1,Th10;
func dualizing-func(A,B) -> contravariant strict Functor of A,B means
:
Def5: (for a being Object of A holds it.a = a) &
for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds it.f = f;
existence
proof
thus ex F being contravariant strict Functor of A,B st
(for a being Object of A holds F.a = O(a)) &
for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f)
from ContravariantFunctorLambda(A2,A3,A5,A6);
end;
uniqueness
proof
let F,G be contravariant strict Functor of A,B such that
A7: for a being Object of A holds F.a = a and
A8: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = f and
A9: for a being Object of A holds G.a = a and
A10: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds G.f = f;
A11: now
let a be Object of A;
thus F.a = a by A7
.= G.a by A9;
end;
now
let a,b be Object of A such that
A12: <^a,b^> <> {};
let f be Morphism of a,b;
thus F.f = f by A8,A12
.= G.f by A10,A12;
end;
hence thesis by A11,Th2;
end;
end;
theorem Th14:
for A,B being category st A,B are_opposite
holds dualizing-func(A,B)*dualizing-func(B,A) = id B
proof
let A,B be category such that
A1: A, B are_opposite;
A2: now
let a be Object of B;
thus (dualizing-func(A,B)*dualizing-func(B,A)).a
= dualizing-func(A,B).(dualizing-func(B,A).a) by FUNCTOR0:33
.= dualizing-func(B,A).a by A1,Def5
.= a by A1,Def5
.= (id B).a by FUNCTOR0:29;
end;
now
let a,b be Object of B;
assume
A3: <^a,b^> <> {};
then
A4: <^dualizing-func(B,A).b,dualizing-func(B,A).a^> <> {} by FUNCTOR0:def 19;
let f be Morphism of a,b;
thus (dualizing-func(A,B)*dualizing-func(B,A)).f
= dualizing-func(A,B).(dualizing-func(B,A).f) by A3,FUNCTOR3:7
.= dualizing-func(B,A).f by A1,A4,Def5
.= f by A1,A3,Def5
.= (id B).f by A3,FUNCTOR0:31;
end;
hence thesis by A2,Th1;
end;
theorem Th15:
for A, B being category st A, B are_opposite
holds dualizing-func(A,B) is bijective
proof
let A, B be category such that
A1: A, B are_opposite;
set F = dualizing-func(A,B);
deffunc O(set) = $1;
deffunc F(set,set,set) = $3;
A2: for a being Object of A holds F.a = O(a) by A1,Def5;
A3: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F(a,b,f) by A1,Def5;
A4: for a,b being Object of A st O(a) = O(b) holds a = b;
A5: for a,b being Object of A st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g;
A6: now
let a,b be Object of B;
reconsider a9 = a, b9 = b as Object of A by A1;
A7: <^a,b^> = <^b9,a9^> by A1,Th9;
assume
A8: <^a,b^> <> {};
let f be Morphism of a,b;
thus ex c,d being Object of A, g being Morphism of c,d
st b = O(c) & a = O(d) & <^c,d^> <> {} & f = F(c,d,g) by A7,A8;
end;
F is bijective from ContraBijectiveSch(A2,A3,A4,A5,A6);
hence thesis;
end;
registration
let A be category;
cluster dualizing-func(A, A opp) -> bijective;
coherence
by Def4,Th15;
cluster dualizing-func(A opp, A) -> bijective;
coherence
proof A, A opp are_opposite by Def4;
hence thesis by Th15;
end;
end;
theorem
for A, B being category st A, B are_opposite holds A, B are_anti-isomorphic
proof
let A, B be category;
assume A, B are_opposite;
then dualizing-func(A,B) is bijective by Th15;
hence thesis;
end;
theorem Th17:
for A, B, C being category st A, B are_opposite
holds A, C are_isomorphic iff B, C are_anti-isomorphic
proof
let A,B,C be category;
assume A, B are_opposite;
then
A1: dualizing-func(A,B) is bijective by Th15;
hereby
assume A, C are_isomorphic;
then consider F being Functor of C,A such that
A2: F is bijective covariant by FUNCTOR0:def 39;
reconsider F as covariant Functor of C,A by A2;
dualizing-func(A,B)*F is bijective contravariant by A1,A2,FUNCTOR1:12;
hence B, C are_anti-isomorphic by FUNCTOR0:def 40;
end;
assume B, C are_anti-isomorphic;
then consider F being Functor of B,C such that
A3: F is bijective contravariant;
reconsider F as contravariant Functor of B,C by A3;
F*dualizing-func(A,B) is bijective covariant by A1,A3,FUNCTOR1:12;
hence thesis;
end;
theorem
for A, B, C, D being category st A, B are_opposite & C, D are_opposite
holds A, C are_isomorphic implies B, D are_isomorphic
proof
let A, B, C, D be category;
assume that
A1: A, B are_opposite and
A2: C, D are_opposite;
A, C are_isomorphic implies B, C are_anti-isomorphic by A1,Th17;
hence thesis by A2,Th17;
end;
theorem
for A, B, C, D being category st A, B are_opposite & C, D are_opposite
holds A, C are_anti-isomorphic implies B, D are_anti-isomorphic
proof
let A, B, C, D be category;
assume that
A1: A, B are_opposite and
A2: C, D are_opposite;
A, C are_anti-isomorphic implies B, C are_isomorphic by A1,Th17;
hence thesis by A2,Th17;
end;
Lm1: now
let A, B be category such that
A1: A, B are_opposite;
let a, b be Object of A such that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
let a9, b9 be Object of B such that
A4: a9 = a and
A5: b9 = b;
let f be Morphism of a,b, f9 be Morphism of b9,a9 such that
A6: f9 = f;
thus f is retraction implies f9 is coretraction
proof
given g being Morphism of b,a such that
A7: g is_right_inverse_of f;
reconsider g9 = g as Morphism of a9, b9 by A1,A4,A5,Th7;
take g9;
f*g = idm b by A7
.= idm b9 by A1,A5,Th10;
hence g9*f9 = idm b9 by A1,A2,A3,A4,A5,A6,Th9;
end;
thus f is coretraction implies f9 is retraction
proof
given g being Morphism of b,a such that
A8: g is_left_inverse_of f;
reconsider g9 = g as Morphism of a9, b9 by A1,A4,A5,Th7;
take g9;
g*f = idm a by A8
.= idm a9 by A1,A4,Th10;
hence f9*g9 = idm a9 by A1,A2,A3,A4,A5,A6,Th9;
end;
end;
theorem
for A, B being category st A, B are_opposite
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {}
for a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9 st f9 = f
holds f is retraction iff f9 is coretraction
proof
let A, B be category such that
A1: A, B are_opposite;
let a, b be Object of A such that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
let a9, b9 be Object of B such that
A4: a9 = a and
A5: b9 = b;
A6: <^b9,a9^> = <^a,b^> by A1,A4,A5,Th9;
<^a9,b9^> = <^b,a^> by A1,A4,A5,Th9;
hence thesis by A1,A2,A3,A4,A5,A6,Lm1;
end;
theorem
for A, B being category st A, B are_opposite
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {}
for a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9 st f9 = f
holds f is coretraction iff f9 is retraction
proof
let A, B be category such that
A1: A, B are_opposite;
let a, b be Object of A such that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
let a9, b9 be Object of B such that
A4: a9 = a and
A5: b9 = b;
A6: <^b9,a9^> = <^a,b^> by A1,A4,A5,Th9;
<^a9,b9^> = <^b,a^> by A1,A4,A5,Th9;
hence thesis by A1,A2,A3,A4,A5,A6,Lm1;
end;
theorem Th22:
for A, B being category st A, B are_opposite
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {}
for a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9
st f9 = f & f is retraction coretraction holds f9" = f"
proof
let A, B be category such that
A1: A, B are_opposite;
let a, b be Object of A such that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
let a9, b9 be Object of B such that
A4: a9 = a and
A5: b9 = b;
A6: <^b9,a9^> = <^a,b^> by A1,A4,A5,Th9;
A7: <^a9,b9^> = <^b,a^> by A1,A4,A5,Th9;
let f be Morphism of a,b, f9 be Morphism of b9,a9 such that
A8: f9 = f and
A9: f is retraction coretraction;
reconsider g = f" as Morphism of a9, b9 by A1,A4,A5,Th7;
A10: f"*f = idm a by A2,A3,A9,ALTCAT_3:2;
A11: f*f" = idm b by A2,A3,A9,ALTCAT_3:2;
A12: f9*g = idm a by A1,A2,A3,A4,A5,A8,A10,Th9;
A13: g*f9 = idm b by A1,A2,A3,A4,A5,A8,A11,Th9;
A14: f9*g = idm a9 by A1,A4,A12,Th10;
A15: g*f9 = idm b9 by A1,A5,A13,Th10;
A16: f9 is retraction coretraction by A1,A2,A3,A4,A5,A8,A9,Lm1;
A17: g is_left_inverse_of f9 by A15;
g is_right_inverse_of f9 by A14;
hence thesis by A2,A3,A6,A7,A16,A17,ALTCAT_3:def 4;
end;
theorem Th23:
for A, B being category st A, B are_opposite
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {}
for a9, b9 being Object of B st a9 = a & b9 = b
for f being Morphism of a,b, f9 being Morphism of b9,a9 st f9 = f
holds f is iso iff f9 is iso
proof
let A, B be category such that
A1: A, B are_opposite;
let a, b be Object of A such that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
let a9, b9 be Object of B such that
A4: a9 = a and
A5: b9 = b;
A6: <^b9,a9^> = <^a,b^> by A1,A4,A5,Th9;
A7: <^a9,b9^> = <^b,a^> by A1,A4,A5,Th9;
now
let A, B be category such that
A8: A, B are_opposite;
let a, b be Object of A such that
A9: <^a,b^> <> {} and
A10: <^b,a^> <> {};
let a9, b9 be Object of B such that
A11: a9 = a and
A12: b9 = b;
let f be Morphism of a,b, f9 be Morphism of b9,a9 such that
A13: f9 = f;
assume
A14: f is iso;
then
A15: f*f" = idm b;
A16: f"*f = idm a by A14;
f is retraction coretraction by A14,ALTCAT_3:5;
then
A17: f9" = f" by A8,A9,A10,A11,A12,A13,Th22;
A18: idm a = idm a9 by A8,A11,Th10;
A19: idm b = idm b9 by A8,A12,Th10;
A20: f9*f9" = idm a9 by A8,A9,A10,A11,A12,A13,A16,A17,A18,Th9;
f9"*f9 = idm b9 by A8,A9,A10,A11,A12,A13,A15,A17,A19,Th9;
hence f9 is iso by A20;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7;
end;
theorem Th24:
for A, B, C, D being category st A, B are_opposite & C, D are_opposite
for F, G being covariant Functor of B, C st F, G are_naturally_equivalent
holds dualizing-func(C,D)*G*dualizing-func(A,B),
dualizing-func(C,D)*F*dualizing-func(A,B) are_naturally_equivalent
proof
let A, B, C, D be category such that
A1: A, B are_opposite and
A2: C, D are_opposite;
let F, G be covariant Functor of B, C such that
A3: F is_naturally_transformable_to G and
A4: G is_transformable_to F;
given t being natural_transformation of F, G such that
A5: for a being Object of B holds t!a is iso;
set dAB = dualizing-func(A,B), dCD = dualizing-func(C,D),
dF = dCD*F*dAB, dG = dCD*G*dAB;
A6: F is_transformable_to G by A3;
A7: now
let a be Object of A;
A8: dG.a = (dCD*G).(dAB.a) by FUNCTOR0:33;
dF.a = (dCD*F).(dAB.a) by FUNCTOR0:33;
hence dG.a = dCD.(G.(dAB.a)) & dF.a = dCD.(F.(dAB.a)) by A8,FUNCTOR0:33;
hence dG.a = G.(dAB.a) & dF.a = F.(dAB.a) by A2,Def5;
hence <^dG.a, dF.a^> = <^F.(dAB.a), G.(dAB.a)^> by A2,Th9;
end;
A9: dG is_transformable_to dF
proof
let a be Object of A;
<^dG.a, dF.a^> = <^F.(dAB.a), G.(dAB.a)^> by A7;
hence thesis by A6;
end;
dom t = the carrier of B by PARTFUN1:def 2
.= the carrier of A by A1;
then reconsider dt = t as ManySortedSet of the carrier of A
by PARTFUN1:def 2,RELAT_1:def 18;
dt is transformation of dG, dF
proof
thus dG is_transformable_to dF by A9;
let a be Object of A;
set b = dAB.a;
A10: b = a by A1,Def5;
t.b = t!b by A6,FUNCTOR2:def 4;
hence thesis by A7,A10;
end;
then reconsider dt as transformation of dG, dF;
A11: now
let a,b be Object of A such that
A12: <^a,b^> <> {};
let f be Morphism of a,b;
set b9 = dAB.b, a9 = dAB.a, f9 = dAB.f;
A13: a9 = a by A1,Def5;
A14: b9 = b by A1,Def5;
then
A15: <^b9, a9^> = <^a,b^> by A1,A13,Th9;
A16: t!a9 = t.a by A6,A13,FUNCTOR2:def 4;
A17: t!b9 = t.b by A6,A14,FUNCTOR2:def 4;
A18: dt!a = t.a by A9,FUNCTOR2:def 4;
A19: dt!b = t.b by A9,FUNCTOR2:def 4;
A20: <^F.b9, F.a9^> <> {} by A12,A15,FUNCTOR0:def 18;
A21: <^G.b9, G.a9^> <> {} by A12,A15,FUNCTOR0:def 18;
A22: dF.f = (dCD*F).f9 by A12,FUNCTOR3:7;
A23: dG.f = (dCD*G).f9 by A12,FUNCTOR3:7;
A24: dF.f = dCD.(F.f9) by A12,A15,A22,FUNCTOR3:8;
A25: dG.f = dCD.(G.f9) by A12,A15,A23,FUNCTOR3:8;
A26: dF.f = F.f9 by A2,A20,A24,Def5;
A27: dG.f = G.f9 by A2,A21,A25,Def5;
A28: <^F.b9, G.b9^> <> {} by A6;
A29: <^F.a9, G.a9^> <> {} by A6;
A30: dG.a = G.a9 by A7;
A31: dF.a = F.a9 by A7;
A32: dG.b = G.b9 by A7;
A33: dF.b = F.b9 by A7;
hence dt!b*dG.f = G.f9*(t!b9) by A2,A17,A19,A21,A27,A28,A30,A32,Th9
.= t!a9*F.f9 by A3,A12,A15,FUNCTOR2:def 7
.= dF.f*(dt!a) by A2,A16,A18,A20,A26,A29,A30,A31,A33,Th9;
end;
thus
dG is_naturally_transformable_to dF
by A9,A11;
then reconsider dt as natural_transformation of dG, dF by A11,FUNCTOR2:def 7;
thus dF is_transformable_to dG
proof
let a be Object of A;
A34: dF.a = F.(dAB.a) by A7;
dG.a = G.(dAB.a) by A7;
then <^dF.a, dG.a^> = <^G.(dAB.a), F.(dAB.a)^> by A2,A34,Th9;
hence thesis by A4;
end;
take dt;
let a be Object of A;
A35: dG.a = G.(dAB.a) by A7;
A36: dF.a = F.(dAB.a) by A7;
A37: dAB.a = a by A1,Def5;
A38: dt!a = t.a by A9,FUNCTOR2:def 4;
A39: t!(dAB.a) = t.a by A6,A37,FUNCTOR2:def 4;
A40: t!(dAB.a) is iso by A5;
A41: <^F.(dAB.a), G.(dAB.a)^> <> {} by A6;
<^G.(dAB.a), F.(dAB.a)^> <> {} by A4;
hence thesis by A2,A35,A36,A38,A39,A40,A41,Th23;
end;
theorem Th25:
for A, B, C, D being category st A, B are_opposite & C, D are_opposite
holds A, C are_equivalent implies B, D are_equivalent
proof
let A, B, C, D be category;
assume that
A1: A, B are_opposite and
A2: C, D are_opposite;
given F being covariant Functor of A,C,
G being covariant Functor of C,A such that
A3: G*F, id A are_naturally_equivalent and
A4: F*G, id C are_naturally_equivalent;
take dF = dualizing-func(C,D)*F*dualizing-func(B,A),
dG = dualizing-func(A,B)*G*dualizing-func(D,C);
A5: G* id C = the FunctorStr of G by FUNCTOR3:5;
A6: dualizing-func(A,B)*(id A) = dualizing-func(A,B) by FUNCTOR3:5;
A7: id C = dualizing-func(D,C)*dualizing-func(C,D) by A2,Th14;
A8: dualizing-func(A,B)*(G*F)*dualizing-func(B,A)
= dualizing-func(A,B)*G*F*dualizing-func(B,A) by FUNCTOR0:32
.= dualizing-func(A,B)*G*(F*dualizing-func(B,A)) by FUNCTOR0:32
.= dualizing-func(A,B)*(G*(id C))*(F*dualizing-func(B,A)) by A5,Th3
.= dualizing-func(A,B)*G*(id C)*(F*dualizing-func(B,A)) by FUNCTOR0:32
.= dG*dualizing-func(C,D)*(F*dualizing-func(B,A)) by A7,FUNCTOR0:32
.= dG*(dualizing-func(C,D)*(F*dualizing-func(B,A))) by FUNCTOR0:32
.= dG*dF by FUNCTOR0:32;
dualizing-func(A,B)*(id A)*dualizing-func(B,A) = id B by A1,A6,Th14;
hence dG*dF, id B are_naturally_equivalent by A1,A3,A8,Th24;
A9: F* id A = the FunctorStr of F by FUNCTOR3:5;
A10: dualizing-func(C,D)*(id C) = dualizing-func(C,D) by FUNCTOR3:5;
A11: id A = dualizing-func(B,A)*dualizing-func(A,B) by A1,Th14;
A12: dualizing-func(C,D)*(F*G)*dualizing-func(D,C)
= dualizing-func(C,D)*F*G*dualizing-func(D,C) by FUNCTOR0:32
.= dualizing-func(C,D)*F*(G*dualizing-func(D,C)) by FUNCTOR0:32
.= dualizing-func(C,D)*(F*(id A))*(G*dualizing-func(D,C)) by A9,Th3
.= dualizing-func(C,D)*F*(id A)*(G*dualizing-func(D,C)) by FUNCTOR0:32
.= dF*dualizing-func(A,B)*(G*dualizing-func(D,C)) by A11,FUNCTOR0:32
.= dF*(dualizing-func(A,B)*(G*dualizing-func(D,C))) by FUNCTOR0:32
.= dF*dG by FUNCTOR0:32;
dualizing-func(C,D)*(id C)*dualizing-func(D,C) = id D by A2,A10,Th14;
hence thesis by A2,A4,A12,Th24;
end;
definition
let A,B be category;
pred A,B are_dual means
: Def6:
A, B opp are_equivalent;
symmetry
proof
let A,B be category;
A1: A, A opp are_opposite by Def4;
B, B opp are_opposite by Def4;
hence thesis by A1,Th25;
end;
end;
theorem
for A, B being category st A, B are_anti-isomorphic holds A, B are_dual
proof
let A, B be category;
A1: B, B opp are_opposite by Def4;
assume A, B are_anti-isomorphic;
then A, B opp are_isomorphic by A1,Th17;
hence A, B opp are_equivalent by Th5;
end;
theorem
for A, B, C being category st A, B are_opposite
holds A, C are_equivalent iff B, C are_dual
proof
let A, B, C be category such that
A1: A, B are_opposite;
C, C opp are_opposite by Def4;
hence thesis by A1,Th25;
end;
theorem
for A, B, C being category st A, B are_dual & B, C are_equivalent
holds A, C are_dual
proof
let A, B, C be category such that
A1: A, B opp are_equivalent and
A2: B, C are_equivalent;
A3: B, B opp are_opposite by Def4;
C, C opp are_opposite by Def4;
then B opp, C opp are_equivalent by A2,A3,Th25;
hence A, C opp are_equivalent by A1,Th4;
end;
theorem
for A, B, C being category st A, B are_dual & B, C are_dual
holds A, C are_equivalent
proof
let A, B, C be category such that
A1: A, B opp are_equivalent and
A2: B, C are_dual;
C, B opp are_equivalent by A2,Def6;
hence thesis by A1,Th4;
end;
begin
:: <section4>Concrete categories</section4>
theorem Th30:
for X,Y,x being set
holds x in Funcs(X,Y) iff x is Function & proj1 x = X & proj2 x c= Y
proof
let X,Y,x be set;
hereby
assume x in Funcs(X,Y);
then ex f being Function st x = f & dom f = X & rng f c= Y by FUNCT_2:def 2
;
hence x is Function & proj1 x = X & proj2 x c= Y;
end;
assume x is Function;
then reconsider x as Function;
dom x = proj1 x;
hence thesis by FUNCT_2:def 2;
end;
definition
let C be category;
attr C is para-functional means
ex F being ManySortedSet of C st
for a1,a2 being Object of C holds <^a1,a2^> c= Funcs(F.a1,F.a2);
end;
registration
cluster quasi-functional -> para-functional for category;
coherence
proof
let C be category such that
A1: for a1,a2 being Object of C holds <^a1,a2^> c= Funcs(a1,a2);
reconsider F = id the carrier of C as ManySortedSet of C;
take F;
let a1,a2 be Object of C;
thus thesis by A1;
end;
end;
definition
let C be category;
let a be set;
func C-carrier_of a -> set means
:
Def8: ex b being Object of C st b = a & it = proj1 idm b if a is Object of C
otherwise it = {};
consistency;
existence
proof
hereby
assume a is Object of C;
then reconsider b = a as Object of C;
take x = proj1 idm b, b;
thus b = a & x = proj1 idm b;
end;
thus thesis;
end;
uniqueness;
end;
notation
let C be category;
let a be Object of C;
synonym the_carrier_of a for C-carrier_of a;
end;
definition
let C be category;
let a be Object of C;
redefine func the_carrier_of a equals :: redefines the_carrier_of (YELLOW18, synonym) → -carrier_of (YELLOW18, definition)
proj1 idm a;
compatibility by Def8;
end;
theorem Th31:
for A being non empty set, a being Object of EnsCat A holds idm a = id a
proof
let A be non empty set, a be Object of EnsCat A;
<^a,a^> = Funcs(a, a) by ALTCAT_1:def 14;
then reconsider e = id a as Morphism of a,a by FUNCT_2:126;
now
let b being Object of EnsCat A such that
A1: <^a,b^> <> {};
let f be Morphism of a,b;
A2: <^a,b^> = Funcs(a, b) by ALTCAT_1:def 14;
then reconsider g = f as Function;
A3: dom g = a by A1,A2,Th30;
thus f*e = g* id a by A1,ALTCAT_1:def 12
.= f by A3,RELAT_1:52;
end;
hence thesis by ALTCAT_1:def 17;
end;
theorem Th32:
for A being non empty set for a being Object of EnsCat A
holds the_carrier_of a = a
proof
let A be non empty set;
let a be Object of EnsCat A;
thus the_carrier_of a = proj1 id a by Th31
.= a;
end;
definition
let C be category;
attr C is set-id-inheriting means
:
Def10: for a being Object of C holds idm a = id the_carrier_of a;
end;
registration
let A be non empty set;
cluster EnsCat A -> set-id-inheriting;
coherence
proof
let a be Object of EnsCat A;
thus idm a = id a by Th31
.= id the_carrier_of a by Th32;
end;
end;
definition
let C be category;
attr C is concrete means
C is para-functional semi-functional set-id-inheriting;
end;
registration
cluster concrete -> para-functional semi-functional set-id-inheriting
for category;
coherence;
cluster para-functional semi-functional set-id-inheriting -> concrete
for category;
coherence;
end;
registration
cluster concrete quasi-functional strict for category;
existence
proof
take EnsCat NAT;
thus thesis;
end;
end;
theorem Th33:
for C being category holds C is para-functional iff
for a1,a2 being Object of C
holds <^a1,a2^> c= Funcs(the_carrier_of a1, the_carrier_of a2)
proof
let C be category;
thus C is para-functional implies for a1,a2 being Object of C
holds <^a1,a2^> c= Funcs(the_carrier_of a1, the_carrier_of a2)
proof
given F being ManySortedSet of C such that
A1: for a1,a2 being Object of C holds <^a1,a2^> c= Funcs(F.a1,F.a2);
let a1,a2 be Object of C;
A2: idm a1 in <^a1,a1^>;
A3: <^a1,a1^> c= Funcs(F.a1, F.a1) by A1;
A4: <^a2,a2^> c= Funcs(F.a2, F.a2) by A1;
A5: idm a2 in <^a2,a2^>;
A6: ex f1 being Function st ( idm a1 = f1)&( dom f1 = F.a1)&(
rng f1 c= F.a1) by A2,A3,FUNCT_2:def 2;
ex f2 being Function st ( idm a2 = f2)&( dom f2 = F.a2)&(
rng f2 c= F.a2) by A4,A5,FUNCT_2:def 2;
hence thesis by A1,A6;
end;
assume
A7: for a1,a2 being Object of C
holds <^a1,a2^> c= Funcs(the_carrier_of a1, the_carrier_of a2);
deffunc O(set) = C-carrier_of $1;
consider F being ManySortedSet of the carrier of C such that
A8: for a being Element of C holds F.a = O(a) from PBOOLE:sch 5;
take F;
let a, b be Object of C;
A9: F.a = the_carrier_of a by A8;
F.b = the_carrier_of b by A8;
hence thesis by A7,A9;
end;
theorem Th34:
for C being para-functional category
for a,b being Object of C st <^a,b^> <> {} for f being Morphism of a,b
holds f is Function of the_carrier_of a, the_carrier_of b
proof
let C be para-functional category;
let a,b be Object of C such that
A1: <^a,b^> <> {};
let f be Morphism of a,b;
A2: <^a,b^> c= Funcs(the_carrier_of a, the_carrier_of b) by Th33;
f in <^a,b^> by A1;
hence thesis by A2,FUNCT_2:66;
end;
registration
let A be para-functional category;
let a,b be Object of A;
cluster -> Function-like Relation-like for Morphism of a,b;
coherence
proof
let f be Morphism of a,b;
per cases;
suppose <^a,b^> <> {};
hence thesis by Th34;
end;
suppose <^a,b^> = {};
hence thesis;
end;
end;
end;
theorem Th35:
for C being para-functional category
for a,b being Object of C st <^a,b^> <> {} for f being Morphism of a,b
holds dom f = the_carrier_of a & rng f c= the_carrier_of b
proof
let C be para-functional category;
let a,b be Object of C such that
A1: <^a,b^> <> {};
let f be Morphism of a,b;
A2: <^a,b^> c= Funcs(the_carrier_of a, the_carrier_of b) by Th33;
f in <^a,b^> by A1;
hence thesis by A2,FUNCT_2:92;
end;
theorem Th36:
for C being para-functional semi-functional category
for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = (g qua Function)*(f qua Function)
proof
let C be para-functional semi-functional category;
let a,b,c be Object of C such that
A1: <^a,b^> <> {} and
A2: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
<^a,c^> <> {} by A1,A2,ALTCAT_1:def 2;
hence thesis by A1,A2,ALTCAT_1:def 12;
end;
theorem Th37:
for C being para-functional semi-functional category
for a being Object of C st id the_carrier_of a in <^a,a^>
holds idm a = id the_carrier_of a
proof
let C be para-functional semi-functional category;
let a be Object of C;
assume id the_carrier_of a in <^a,a^>;
then reconsider f = id the_carrier_of a as Morphism of a,a;
now
let b be Object of C such that
A1: <^a,b^> <> {};
let g being Morphism of a,b;
A2: dom g = the_carrier_of a by A1,Th35;
thus g*f = g* id the_carrier_of a by A1,Th36
.= g by A2,RELAT_1:52;
end;
hence thesis by ALTCAT_1:def 17;
end;
scheme ConcreteCategoryLambda { A() -> non empty set,
B(object,object) -> set,
D(object) -> set }: ex C being concrete strict category
st the carrier of C = A() &
(for a being Object of C holds the_carrier_of a = D(a)) &
for a,b being Object of C holds <^a,b^> = B(a,b)
provided
A1: for a,b,c being Element of A(), f,g being Function
st f in B(a,b) & g in B(b,c) holds g*f in B(a,c) and
A2: for a,b being Element of A() holds B(a,b) c= Funcs(D(a), D(b)) and
A3: for a being Element of A() holds id D(a) in B(a,a)
proof
deffunc C(set,set,set,set,set) = $4(#)$5;
A4: now
let a,b be Element of A(), f be set such that
A5: f in B(a,b);
B(a,b) c= Funcs(D(a), D(b)) by A2;
hence f is Function by A5;
end;
A6: for a,b,c being Element of A(), f,g being set
st f in B(a,b) & g in B(b,c) holds C(a,b,c,f,g) in B(a,c)
proof
let a,b,c be Element of A(), f,g be set;
assume that
A7: f in B(a,b) and
A8: g in B(b,c);
reconsider f, g as Function by A4,A7,A8;
g*f = f(#)g;
hence thesis by A1,A7,A8;
end;
A9: for a,b,c,d being Element of A(), f,g,h being set
st f in B(a,b) & g in B(b,c) & h in B(c,d)
holds C(a,c,d,C(a,b,c,f,g),h) = C(a,b,d,f,C(b,c,d,g,h))
proof
let a,b,c,d be Element of A();
let f,g,h be set;
assume that
A10: f in B(a,b) and
A11: g in B(b,c) and
A12: h in B(c,d);
reconsider f, g, h as Function by A4,A10,A11,A12;
(f(#)g)(#)h = f(#)(h*g) by RELAT_1:36;
hence thesis;
end;
A13: for a being Element of A() ex f being set st f in B(a,a) &
for b being Element of A(), g being set st g in B(a,b)
holds C(a,a,b,f,g) = g
proof
let a be Element of A();
take f = id D(a);
thus f in B(a,a) by A3;
let b be Element of A(), g be set such that
A14: g in B(a,b);
B(a,b) c= Funcs(D(a), D(b)) by A2;
then consider h being Function such that
A15: g = h and
A16: dom h = D(a) and rng h c= D(b) by A14,FUNCT_2:def 2;
thus f(#)g = g by A15,A16,RELAT_1:52;
end;
A17: for a being Element of A() ex f being set st f in B(a,a) &
for b being Element of A(), g being set st g in B(b,a)
holds C(b,a,a,g,f) = g
proof
let a be Element of A();
take f = id D(a);
thus f in B(a,a) by A3;
let b be Element of A(), g be set such that
A18: g in B(b,a);
B(b,a) c= Funcs(D(b), D(a)) by A2;
then consider h being Function such that
A19: g = h and dom h = D(b) and
A20: rng h c= D(a) by A18,FUNCT_2:def 2;
thus g(#)f = g by A19,A20,RELAT_1:53;
end;
consider C being strict category such that
A21: the carrier of C = A() and
A22: for a,b being Object of C holds <^a,b^> = B(a,b) and
A23: for a,b,c being Object of C st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g) from CategoryLambda(A6,A9,A13,A17);
consider D being ManySortedSet of C such that
A24: for x being Element of C holds D.x = D(x) from PBOOLE:sch 5;
A25: C is para-functional
proof
take D;
let a1,a2 be Object of C;
A26: <^a1,a2^> = B(a1,a2) by A22;
A27: D(a1) = D.a1 by A24;
D(a2) = D.a2 by A24;
hence thesis by A2,A21,A26,A27;
end;
A28: C is semi-functional
by A23;
A29: now
let a be Object of C;
id D(a) in B(a,a) by A3,A21;
then reconsider e = id D(a) as Morphism of a,a by A22;
now
let b be Object of C such that
A30: <^a,b^> <> {};
let f be Morphism of a,b;
A31: <^a,b^> = B(a,b) by A22;
A32: B(a,b) c= Funcs(D(a), D(b)) by A2,A21;
f in <^a,b^> by A30;
then consider h being Function such that
A33: f = h and
A34: dom h = D(a) and rng h c= D(b) by A31,A32,FUNCT_2:def 2;
thus f*e = h* id D(a) by A28,A30,A33
.= f by A33,A34,RELAT_1:52;
end;
hence idm a = id D(a) by ALTCAT_1:def 17;
end;
A35: now
let i be set;
assume i in the carrier of C;
then reconsider a = i as Object of C;
thus C-carrier_of i = proj1 idm a by Def8
.= proj1 id D(a) by A29
.= D(a)
.= D.i by A24;
end;
C is set-id-inheriting
proof
let a be Object of C;
thus idm a = id D(a) by A29
.= id (D.a) by A24
.= id (the_carrier_of a) by A35;
end;
then reconsider C as para-functional semi-functional set-id-inheriting
strict category by A25,A28;
take C;
thus the carrier of C = A() by A21;
hereby
let a be Object of C;
thus the_carrier_of a = D.a by A35
.= D(a) by A24;
end;
thus thesis by A22;
end;
scheme ConcreteCategoryQuasiLambda { A() -> non empty set,
P[object,object,object], D(object) -> set }:
ex C being concrete strict category
st the carrier of C = A() &
(for a being Object of C holds the_carrier_of a = D(a)) &
for a,b being Element of A(), f being Function
holds f in (the Arrows of C).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f]
provided
A1: for a,b,c being Element of A(), f,g being Function
st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] and
A2: for a being Element of A() holds P[a,a,id D(a)]
proof
set A = A();
defpred P[object,object] means
ex a,b being object, c being set st $1 = [a,b] & c = $2 &
for f being object holds f in c iff f in Funcs(D(a), D(b)) & P[a,b,f];
A3: now
let x be object;
assume x in [:A,A:];
then consider a,b being object such that
a in A and b in A and
A4: x = [a,b] by ZFMISC_1:def 2;
defpred Q[object] means P[a,b,$1];
consider y being set such that
A5: for f being object holds f in y iff f in Funcs(D(a), D(b)) & Q[f]
from XBOOLE_0:sch 1;
reconsider y as object;
take y;
thus P[x,y] by A4,A5;
end;
consider F being Function such that dom F = [:A,A:] and
A6: for x being object st x in [:A,A:] holds P[x, F.x]
from CLASSES1:sch 1(
A3);
A7: now
let a,b be set;
assume that
A8: a in A and
A9: b in A;
[a,b] in [:A,A:] by A8,A9,ZFMISC_1:87;
then P[[a,b], F.[a,b]] by A6;
then consider a9,b9,c being object such that
A10: [a,b] = [a9,b9] & c = Funcs(D(a9), D(b9)) and
A11: for f being object holds f in F.[a,b] iff
f in Funcs(D(a9), D(b9)) & P[a9,b9,f];
A12: a = a9 by A10,XTUPLE_0:1;
A13: b = b9 by A10,XTUPLE_0:1;
let f be set;
thus f in F.[a,b] iff P[a,b,f] & f in Funcs(D(a), D(b)) by A11,A12,A13;
end;
deffunc B(set,set) = F.[$1,$2];
A14: now
let a,b,c be Element of A, f,g be Function;
assume that
A15: f in B(a,b) and
A16: g in B(b,c);
A17: P[a,b,f] by A7,A15;
A18: f in Funcs(D(a), D(b)) by A7,A15;
A19: P[b,c,g] by A7,A16;
A20: g in Funcs(D(b), D (c )) by A7,A16;
A21: dom f = D(a) by A18,Th30;
A22: rng f c= D(b) by A18,Th30;
A23: dom g = D(b) by A20,Th30;
A24: rng g c= D(c) by A20,Th30;
A25: rng (g*f) c= rng g by RELAT_1:26;
A26: dom (g*f) = D(a) by A21,A22,A23,RELAT_1:27;
rng (g*f) c= D(c) by A24,A25;
then
A27: g*f in Funcs(D(a), D(c)) by A26,FUNCT_2:def 2;
P[a,c,g*f] by A1,A17,A19;
hence g*f in B(a,c) by A7,A27;
end;
A28: for a,b be Element of A holds B(a,b) c= Funcs(D(a), D(b)) by A7;
A29: for a being Element of A() holds id D(a) in B(a,a)
proof
let a be Element of A();
A30: dom id D(a) = D(a);
A31: rng id D(a) = D(a);
A32: P[a,a, id D(a)] by A2;
id D(a) in Funcs(D(a), D(a)) by A30,A31,FUNCT_2:def 2;
hence thesis by A7,A32;
end;
consider C being para-functional semi-functional set-id-inheriting
strict category such that
A33: the carrier of C = A() and
A34: for a being Object of C holds the_carrier_of a = D(a) and
A35: for a,b being Object of C holds <^a,b^> = B(a,b)
from ConcreteCategoryLambda(A14,A28,A29);
take C;
thus the carrier of C = A() by A33;
thus for a being Object of C holds the_carrier_of a = D(a) by A34;
let a,b be Element of A(), f being Function;
reconsider a,b as Object of C by A33;
(the Arrows of C).(a,b) = <^a,b^> .= F.[a,b] by A35;
hence thesis by A7;
end;
scheme ConcreteCategoryEx { A() -> non empty set,
B(object) -> set, D[object, object], P[object,object,object] }:
ex C being concrete strict category
st the carrier of C = A() & (for a being Object of C
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) &
for a,b being Element of A(), f being Function
holds f in (the Arrows of C).(a,b) iff
f in Funcs(C-carrier_of a, C-carrier_of b) & P[a,b,f]
provided
A1: for a,b,c being Element of A(), f,g being Function
st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] and
A2: for a being Element of A(), X being set
st for x being set holds x in X iff x in B(a) & D[a,x] holds P[a,a,id X]
proof
A3: for a,b,c being Element of A(), f,g being Function
st P[a,b,f] & P[b,c,g] holds P[a,c,g*f] by A1;
consider D being Function such that dom D = A() and
A4: for a being object st a in A()
for y being object holds y in D.a iff y in B(a) & D[a,y] from CARD_3:sch 2;
deffunc D(set) = D.$1;
A5: now
let a be Element of A();
for y being set holds y in D.a iff y in B(a) & D[a,y] by A4;
hence P[a,a,id D(a)] by A2;
end;
consider C being
para-functional semi-functional set-id-inheriting strict category such that
A6: the carrier of C = A() and
A7: for a being Object of C holds the_carrier_of a = D(a) and
A8: for a,b being Element of A(), f being Function
holds f in (the Arrows of C).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f]
from ConcreteCategoryQuasiLambda(A3, A5);
take C;
thus the carrier of C = A() by A6;
hereby
let a be Object of C;
the_carrier_of a = D.a by A7;
hence
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]
by A4,A6;
end;
let a,b be Element of A();
A9: D.a = C-carrier_of a by A6,A7;
D.b = C-carrier_of b by A6,A7;
hence thesis by A8,A9;
end;
scheme ConcreteCategoryUniq1 { A() -> non empty set,
B(object,object) -> object }:
for C1, C2 being para-functional semi-functional category
st the carrier of C1 = A() &
(for a,b being Object of C1 holds <^a,b^> = B(a,b)) &
the carrier of C2 = A() &
(for a,b being Object of C2 holds <^a,b^> = B(a,b))
holds the AltCatStr of C1 = the AltCatStr of C2
proof
deffunc C(set,set,set,set,set) = $4(#)$5;
A1: for C1,C2 being non empty transitive AltCatStr st the carrier of C1 = A() &
(for a,b being Object of C1 holds <^a,b^> = B(a,b)) &
(for a,b,c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g)) & the carrier of C2 = A() &
(for a,b being Object of C2 holds <^a,b^> = B(a,b)) &
(for a,b,c being Object of C2 st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds g*f = C(a,b,c,f,g))
holds the AltCatStr of C1 = the AltCatStr of C2 from CategoryLambdaUniq;
let C1,C2 be para-functional semi-functional category;
A2: for C1 be para-functional semi-functional category,
a,b,c be Object of C1 st <^a,b^> <> {} & <^b,c^> <> {}
for f be Morphism of a,b, g be Morphism of b,c
holds g*f = f(#)g by Th36;
then
A3: for a,b,c being Object of C1 st <^a,b^> <> {} & <^b,c^> <> {} for f
being Morphism of a,b, g being Morphism of b,c holds g*f = f(#)g;
for a,b,c being Object of C2 st <^a,b^> <> {} & <^b,c^> <> {} for f
being Morphism of a,b, g being Morphism of b,c holds g*f = f(#)g by A2;
hence thesis by A1,A3;
end;
scheme ConcreteCategoryUniq2 { A() -> non empty set,
P[object,object,object], D(object) -> set }:
for C1,C2 being para-functional semi-functional category st
the carrier of C1 = A() & (for a,b being Element of A(), f being Function
holds f in (the Arrows of C1).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f]) &
the carrier of C2 = A() & (for a,b being Element of A(), f being Function
holds f in (the Arrows of C2).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f])
holds the AltCatStr of C1 = the AltCatStr of C2
proof
let C1,C2 be para-functional semi-functional category such that
A1: the carrier of C1 = A() and
A2: for a,b being Element of A(), f being Function
holds f in (the Arrows of C1).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f] and
A3: the carrier of C2 = A() and
A4: for a,b being Element of A(), f being Function
holds f in (the Arrows of C2).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f];
deffunc B(set,set) = (the Arrows of C1).($1,$2);
A5: for C1, C2 being para-functional semi-functional category
st the carrier of C1 = A() &
(for a,b being Object of C1 holds <^a,b^> = B(a,b)) &
the carrier of C2 = A() &
(for a,b being Object of C2 holds <^a,b^> = B(a,b))
holds the AltCatStr of C1 = the AltCatStr of C2 from ConcreteCategoryUniq1;
A6: for a,b being Object of C1 holds <^a,b^> = B(a,b);
now
let a,b be Object of C2;
reconsider x = a, y = b as Element of A() by A3;
reconsider a9 = x, b9 = y as Object of C1 by A1;
thus <^a,b^> = B(a,b)
proof
hereby
let z be object;
assume
A7: z in <^a,b^>;
then
A8: z in Funcs(D(x), D(y)) by A4;
P[x,y,z] by A4,A7;
hence z in B(a,b) by A2,A8;
end;
let z be object;
assume
A9: z in B(a,b);
then
A10: z is Morphism of a9,b9;
then
A11: z in Funcs(D(x), D(y)) by A2,A9;
P[x,y,z] by A2,A9,A10;
hence thesis by A4,A11;
end;
end;
hence thesis by A1,A3,A5,A6;
end;
scheme ConcreteCategoryUniq3 { A() -> non empty set, B(object) -> set,
D[object,object], P[object,object,object] }:
for C1,C2 being para-functional semi-functional category st
the carrier of C1 = A() & (for a being Object of C1
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) &
(for a,b being Element of A(), f being Function
holds f in (the Arrows of C1).(a,b) iff
f in Funcs(C1-carrier_of a, C1-carrier_of b) & P[a,b,f]) &
the carrier of C2 = A() & (for a being Object of C2
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) &
(for a,b being Element of A(), f being Function
holds f in (the Arrows of C2).(a,b) iff
f in Funcs(C2-carrier_of a, C2-carrier_of b) & P[a,b,f])
holds the AltCatStr of C1 = the AltCatStr of C2
proof
let C1,C2 be para-functional semi-functional category such that
A1: the carrier of C1 = A() and
A2: for a being Object of C1
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x] and
A3: for a,b being Element of A(), f being Function
holds f in (the Arrows of C1).(a,b) iff
f in Funcs(C1-carrier_of a, C1-carrier_of b) & P[a,b,f] and
A4: the carrier of C2 = A() and
A5: for a being Object of C2
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x] and
A6: for a,b being Element of A(), f being Function
holds f in (the Arrows of C2).(a,b) iff
f in Funcs(C2-carrier_of a, C2-carrier_of b) & P[a,b,f];
deffunc D(set) = C1-carrier_of $1;
A7: for C1,C2 being para-functional semi-functional category st
the carrier of C1 = A() & (for a,b being Element of A(), f being Function
holds f in (the Arrows of C1).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f]) &
the carrier of C2 = A() & (for a,b being Element of A(), f being Function
holds f in (the Arrows of C2).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f])
holds the AltCatStr of C1 = the AltCatStr of C2 from ConcreteCategoryUniq2;
A8: now
let a be Element of A();
reconsider a1 = a as Object of C1 by A1;
reconsider a2 = a as Object of C2 by A4;
now
let x be object;
x in the_carrier_of a1 iff x in B(a) & D[a,x] by A2;
hence x in the_carrier_of a1 iff x in the_carrier_of a2 by A5;
end;
hence C1-carrier_of a = C2-carrier_of a by TARSKI:2;
end;
now
let a,b be Element of A(), f be Function;
A9: D(a) = C2-carrier_of a by A8;
D(b) = C2-carrier_of b by A8;
hence
f in (the Arrows of C2).(a,b) iff f in Funcs(D(a), D(b)) & P[a,b,f ]
by A6,A9;
end;
hence thesis by A1,A3,A4,A7;
end;
begin
:: <section5>Equivalence between concrete categories</section5>
theorem Th38:
for C being concrete category
for a,b being Object of C st <^a,b^> <> {} & <^b,a^> <> {}
for f being Morphism of a,b st f is retraction
holds rng f = the_carrier_of b
proof
let C be concrete category;
let a,b be Object of C;
assume that
A1: <^a,b^> <> {} and
A2: <^b,a^> <> {};
let f be Morphism of a,b;
given g being Morphism of b,a such that
A3: g is_right_inverse_of f;
A4: f*g = idm b by A3;
A5: f qua Function*g = f*g by A1,A2,Th36;
A6: f is Function of the_carrier_of a, the_carrier_of b by A1,Th34;
A7: g is Function of the_carrier_of b, the_carrier_of a by A2,Th34;
idm b = id the_carrier_of b by Def10;
hence thesis by A4,A5,A6,A7,FUNCT_2:18;
end;
theorem Th39:
for C being concrete category
for a,b being Object of C st <^a,b^> <> {} & <^b,a^> <> {}
for f being Morphism of a,b st f is coretraction holds f is one-to-one
proof
let C be concrete category;
let a,b be Object of C;
assume that
A1: <^a,b^> <> {} and
A2: <^b,a^> <> {};
let f be Morphism of a,b;
given g being Morphism of b,a such that
A3: g is_left_inverse_of f;
A4: g*f = idm a by A3;
A5: g qua Function*f = g*f by A1,A2,Th36;
A6: dom f = the_carrier_of a by A1,Th35;
idm a = id the_carrier_of a by Def10;
hence thesis by A4,A5,A6,FUNCT_1:31;
end;
theorem Th40:
for C being concrete category
for a,b being Object of C st <^a,b^> <> {} & <^b,a^> <> {}
for f being Morphism of a,b st f is iso
holds f is one-to-one & rng f = the_carrier_of b
by ALTCAT_3:5,Th38,Th39;
theorem Th41:
for C being para-functional semi-functional category
for a,b being Object of C st <^a,b^> <> {} for f being Morphism of a,b
st f is one-to-one & (f qua Function)" in <^b,a^> holds f is iso
proof
let C be para-functional semi-functional category;
let a,b be Object of C such that
A1: <^a,b^> <> {};
let f be Morphism of a,b;
assume
A2: f is one-to-one;
assume
A3: f qua Function" in <^b,a^>;
then reconsider g = f qua Function" as Morphism of b,a;
dom g = the_carrier_of b by A3,Th35;
then
A4: rng f = the_carrier_of b by A2,FUNCT_1:33;
A5: f qua Function"*f = id dom f by A2,FUNCT_1:39;
A6: f*(f qua Function") = id rng f by A2,FUNCT_1:39;
A7: dom f = the_carrier_of a by A1,Th35;
A8: f*g = id the_carrier_of b by A1,A3,A4,A6,Th36;
A9: g*f = id the_carrier_of a by A1,A3,A5,A7,Th36;
A10: idm b = f*g by A8,Th37;
idm a = g*f by A9,Th37;
then
A11: g is_left_inverse_of f;
A12: g is_right_inverse_of f by A10;
then f is retraction coretraction by A11;
hence f*f" = idm b & f"*f = idm a by A1,A3,A11,A12,ALTCAT_3:def 4;
end;
theorem
for C being concrete category
for a,b being Object of C st <^a,b^> <> {} & <^b,a^> <> {}
for f being Morphism of a,b st f is iso holds f" = (f qua Function)"
proof
let C be concrete category;
let a,b be Object of C;
assume that
A1: <^a,b^> <> {} and
A2: <^b,a^> <> {};
let f be Morphism of a,b;
assume
A3: f is iso;
then
A4: f"*f = idm a;
A5: f"*(f qua Function) = f"*f by A1,A2,Th36;
A6: dom (f") = the_carrier_of b by A2,Th35;
A7: dom f = the_carrier_of a by A1,Th35;
A8: f is one-to-one by A1,A2,A3,Th40;
A9: rng f = the_carrier_of b by A1,A2,A3,Th40;
idm a = id the_carrier_of a by Def10;
hence thesis by A4,A5,A6,A7,A8,A9,FUNCT_1:41;
end;
scheme ConcreteCatEquivalence
{ A,B() -> para-functional semi-functional category,
O1, O2(object) -> object,
F1, F2(object,object,object) -> Function, A, B(object) -> Function }:
A(), B() are_equivalent
provided
A1: ex F being covariant Functor of A(),B() st
(for a being Object of A() holds F.a = O1(a)) &
for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F1(a,b,f) and
A2: ex G being covariant Functor of B(),A() st
(for a being Object of B() holds G.a = O2(a)) &
for a,b being Object of B() st <^a,b^> <> {}
for f being Morphism of a,b holds G.f = F2(a,b,f) and
A3: for a, b being Object of A() st a = O2(O1(b))
holds A(b) in <^a, b^> & A(b)" in <^b,a^> & A(b) is one-to-one and
A4: for a, b being Object of B() st b = O1(O2(a))
holds B(a) in <^a, b^> & B(a)" in <^b,a^> & B(a) is one-to-one and
A5: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
holds A(b)*F2(O1(a),O1(b),F1(a,b,f)) = f*A(a) and
A6: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
holds F1(O2(a),O2(b),F2(a,b,f))*B(a) = B(b)*f
proof consider F being covariant Functor of A(), B() such that
A7: for a being Object of A() holds F.a = O1(a) and
A8: for a,b being Object of A() st <^a,b^> <> {}
for f being Morphism of a,b holds F.f = F1(a,b,f) by A1;
consider G being covariant Functor of B(),A() such that
A9: for a being Object of B() holds G.a = O2(a) and
A10: for a,b being Object of B() st <^a,b^> <> {}
for f being Morphism of a,b holds G.f = F2(a,b,f) by A2;
take F, G;
set GF = G*F, I = id A();
A11: for a being Object of A() holds
A(a) in <^GF.a, I.a^> & <^I.a, GF.a^> <> {} &
for f being Morphism of GF.a, I.a st f = A(a) holds f is iso
proof
let a be Object of A();
A12: GF.a = G.(F.a) by FUNCTOR0:33
.= O2(F.a) by A9
.= O2(O1(a)) by A7;
A13: I.a = a by FUNCTOR0:29;
then
A14: A(a) in <^GF.a, I.a^> by A3,A12;
A15: A(a)" in <^I.a, GF.a^> by A3,A12,A13;
A(a) is one-to-one by A3,A12;
hence thesis by A14,A15,Th41;
end;
A16: for a,b being Object of A() st <^a,b^> <> {} for f being Morphism of a,b
for g1 being Morphism of GF.a, I.a st g1 = A(a)
for g2 being Morphism of GF.b, I.b st g2 = A(b) holds g2*GF.f = I.f*g1
proof
let a,b be Object of A() such that
A17: <^a,b^> <> {};
A18: A(a) in <^GF.a, I.a^> by A11;
A19: A(b) in <^GF.b, I.b^> by A11;
reconsider g2 = A(b) as Morphism of GF.b, I.b by A11;
A20: <^GF.a, GF.b^> <> {} by A17,FUNCTOR0:def 18;
A21: <^I.a, I.b^> <> {} by A17,FUNCTOR0:def 18;
let f be Morphism of a,b;
A22: GF.f = G.(F.f) by A17,FUNCTOR3:6;
A23: O1(a) = F.a by A7;
A24: O1(b) = F.b by A7;
A25: F1(a,b,f) = F.f by A8,A17;
<^F.a, F.b^> <> {} by A17,FUNCTOR0:def 18;
then F2(O1(a),O1(b),F1(a,b,f)) = GF.f by A10,A22,A23,A24,A25;
then g2*GF.f = A(b)*F2(O1(a),O1(b),F1(a,b,f)) by A19,A20,Th36
.= f*A(a) by A5,A17
.= I.f*A(a) by A17,FUNCTOR0:31;
hence thesis by A18,A21,Th36;
end;
ex t being natural_equivalence of G*F, id A() st
G*F, id A() are_naturally_equivalent &
for a being Object of A() holds t!a = A(a)
from NatEquivalenceLambda(A11,A16);
hence G*F, id A() are_naturally_equivalent;
set I = id B(), FG = F*G;
A26: for a being Object of B() holds
B(a) in <^I.a, FG.a^> & <^FG.a, I.a^> <> {} &
for f being Morphism of I.a, FG.a st f = B(a) holds f is iso
proof
let a be Object of B();
A27: FG.a = F.(G.a) by FUNCTOR0:33
.= O1(G.a) by A7
.= O1(O2(a)) by A9;
A28: I.a = a by FUNCTOR0:29;
then
A29: B(a) in <^I.a, FG.a^> by A4,A27;
A30: B(a)" in <^FG.a, I.a^> by A4,A27,A28;
B(a) is one-to-one by A4,A27;
hence thesis by A29,A30,Th41;
end;
A31: for a,b being Object of B() st <^a,b^> <> {} for f being Morphism of a,b
for g1 being Morphism of I.a, FG.a st g1 = B(a)
for g2 being Morphism of I.b, FG.b st g2 = B(b) holds g2*I.f = FG.f*g1
proof
let a,b be Object of B() such that
A32: <^a,b^> <> {};
A33: B(a) in <^I.a, FG.a^> by A26;
reconsider g1 = B(a) as Morphism of I.a, FG.a by A26;
A34: B(b) in <^I.b, FG.b^> by A26;
A35: <^FG.a, FG.b^> <> {} by A32,FUNCTOR0:def 18;
A36: <^I.a, I.b^> <> {} by A32,FUNCTOR0:def 18;
let f be Morphism of a,b;
A37: FG.f = F.(G.f) by A32,FUNCTOR3:6;
A38: O2(a) = G.a by A9;
A39: O2(b) = G.b by A9;
A40: F2(a,b,f) = G.f by A10,A32;
<^G.a, G.b^> <> {} by A32,FUNCTOR0:def 18;
then F1(O2(a),O2(b),F2(a,b,f)) = FG.f by A8,A37,A38,A39,A40;
then FG.f*g1 = F1(O2(a),O2(b),F2(a,b,f))*B(a) by A33,A35,Th36
.= B(b)*f by A6,A32
.= B(b)*I.f by A32,FUNCTOR0:31;
hence thesis by A34,A36,Th36;
end;
ex t being natural_equivalence of I, FG st I, FG are_naturally_equivalent &
for a being Object of B() holds t!a = B(a)
from NatEquivalenceLambda(A26,A31);
hence thesis;
end;
begin
:: <section6>Concretization of categories</section6>
definition
let C be category;
defpred D[set, set] means $1 = $2`22;
defpred P[set, set, Function] means
ex fa,fb being Object of C, g being Morphism of fa, fb
st fa = $1 & fb = $2 & <^fa, fb^> <> {} &
for o being Object of C st <^o, fa^> <> {}
for h being Morphism of o,fa holds $3.[h,[o,fa]] = [g*h,[o,fb]];
deffunc B(set) = Union disjoin the Arrows of C;
A1: for a,b,c being Element of C, f,g being Function
st P[a,b,f] & P[b,c,g] holds P[a,c,g*f]
proof
let a,b,c be Element of C, f,g be Function;
given fa,fb being Object of C, ff being Morphism of fa, fb such that
A2: fa = a and
A3: fb = b and
A4: <^fa, fb^> <> {} and
A5: for o being Object of C st <^o, fa^> <> {}
for h being Morphism of o,fa holds f.[h,[o,fa]] = [ff*h,[o,fb]];
given ga,gb being Object of C, gf being Morphism of ga, gb such that
A6: ga = b and
A7: gb = c and
A8: <^ga, gb^> <> {} and
A9: for o being Object of C st <^o, ga^> <> {}
for h being Morphism of o,ga holds g.[h,[o,ga]] = [gf*h,[o,gb]];
reconsider gf as Morphism of fb,gb by A3,A6;
take fa, gb, k = gf*ff;
thus fa = a & gb = c & <^fa, gb^> <> {} by A2,A3,A4,A6,A7,A8,ALTCAT_1:def 2
;
let o be Object of C such that
A10: <^o, fa^> <> {};
A11: <^o, fb^> <> {} by A4,A10,ALTCAT_1:def 2;
let h be Morphism of o,fa;
A12: f.[h,[o,fa]] = [ff*h,[o,fb]] by A5,A10;
then [h,[o,fa]] in dom f by FUNCT_1:def 2;
hence (g*f).[h,[o,fa]] = g.[ff*h,[o,fb]] by A12,FUNCT_1:13
.= [gf*(ff*h),[o,gb]] by A3,A6,A9,A11
.= [k*h, [o,gb]] by A3,A4,A6,A8,A10,ALTCAT_1:21;
end;
A13: for a being Element of C, X being set
st for x being set holds x in X iff x in B(a) & D[a,x] holds P[a,a,id X]
proof
let a be Element of C, X being set such that
A14: for x being set holds x in X iff
x in Union disjoin the Arrows of C & D[a,x];
reconsider fa = a as Object of C;
take fa, fa, g = idm fa;
thus fa = a & fa = a & <^fa, fa^> <> {};
let o be Object of C such that
A15: <^o, fa^> <> {};
let h be Morphism of o,fa;
A16: [h,[o,fa]]`1 = h;
A17: [h,[o,fa]]`2 = [o,fa];
A18: [h,[o,fa]]`22 = fa by MCART_1:85;
dom the Arrows of C = [:the carrier of C, the carrier of C:]
by PARTFUN1:def 2;
then [o,fa] in dom the Arrows of C by ZFMISC_1:def 2;
then [h,[o,fa]] in Union disjoin the Arrows of C by A15,A16,A17,CARD_3:22;
then [h,[o,fa]] in X by A14,A18;
hence (id X).[h,[o,fa]] = [h,[o,fa]] by FUNCT_1:18
.= [g*h,[o,fa]] by A15,ALTCAT_1:20;
end;
func Concretized C -> concrete strict category means
:
Def12: the carrier of it = the carrier of C & (for a being Object of it
for x being set holds x in the_carrier_of a iff
x in Union disjoin the Arrows of C & a = x`22) &
for a,b being Element of C, f being Function
holds f in (the Arrows of it).(a,b) iff
f in Funcs(it-carrier_of a, it-carrier_of b) &
ex fa,fb being Object of C, g being Morphism of fa, fb
st fa = a & fb = b & <^fa, fb^> <> {} &
for o being Object of C st <^o, fa^> <> {}
for h being Morphism of o,fa holds f.[h,[o,fa]] = [g*h,[o,fb]];
uniqueness
proof
for C1,C2 being para-functional semi-functional category st
the carrier of C1 = the carrier of C & (for a being Object of C1
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) &
(for a,b being Element of C, f being Function
holds f in (the Arrows of C1).(a,b) iff
f in Funcs(C1-carrier_of a, C1-carrier_of b) & P[a,b,f]) &
the carrier of C2 = the carrier of C & (for a being Object of C2
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) &
(for a,b being Element of C, f being Function
holds f in (the Arrows of C2).(a,b) iff
f in Funcs(C2-carrier_of a, C2-carrier_of b) & P[a,b,f])
holds the AltCatStr of C1 = the AltCatStr of C2
from ConcreteCategoryUniq3;
hence thesis;
end;
existence
proof
thus ex C9 being concrete strict category
st the carrier of C9 = the carrier of C & (for a being Object of C9
for x being set holds x in the_carrier_of a iff x in B(a) & D[a,x]) &
for a,b being Element of C, f being Function
holds f in (the Arrows of C9).(a,b) iff
f in Funcs(C9-carrier_of a, C9-carrier_of b) & P[a,b,f]
from ConcreteCategoryEx(A1,A13);
end;
end;
theorem Th43:
for A being category, a being Object of A, x being set
holds x in (Concretized A)-carrier_of a iff
ex b being Object of A, f being Morphism of b,a
st <^b,a^> <> {} & x = [f,[b,a]]
proof
let A be category, a be Object of A, x be set;
set B = Concretized A;
reconsider ac = a as Object of B by Def12;
A1: x in the_carrier_of ac iff
x in Union disjoin the Arrows of A & ac = x`22 by Def12;
A2: dom the Arrows of A = [:the carrier of A, the carrier of A:]
by PARTFUN1:def 2;
hereby
assume
A3: x in B-carrier_of a;
then
A4: x`2 in dom the Arrows of A by A1,CARD_3:22;
A5: x`1 in (the Arrows of A).(x`2) by A1,A3,CARD_3:22;
A6: x = [x`1,x`2] by A1,A3,CARD_3:22;
consider b,c being object such that
A7: b in the carrier of A and c in the carrier of A and
A8: x`2 = [b,c] by A4,ZFMISC_1:def 2;
reconsider b as Object of A by A7;
take b;
reconsider f = x`1 as Morphism of b,a by A1,A3,A5,A6,A8,MCART_1:85;
take f;
thus <^b,a^> <> {} & x = [f,[b,a]] by A1,A3,A5,A6,A8,MCART_1:85;
end;
given b being Object of A, f being Morphism of b,a such that
A9: <^b,a^> <> {} and
A10: x = [f,[b,a]];
A11: x`1 = f by A10;
A12: x`2 = [b,a] by A10;
[b,a] in dom the Arrows of A by A2,ZFMISC_1:def 2;
hence thesis by A1,A9,A10,A11,A12,CARD_3:22,MCART_1:85;
end;
registration
let A be category;
let a be Object of A;
cluster (Concretized A)-carrier_of a -> non empty;
coherence
proof
[idm a, [a,a]] in (Concretized A)-carrier_of a by Th43;
hence thesis;
end;
end;
theorem Th44:
for A being category, a, b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b ex F being Function of
(Concretized A)-carrier_of a, (Concretized A)-carrier_of b
st F in (the Arrows of Concretized A).(a,b) &
for c being Object of A, g being Morphism of c,a st <^c,a^> <> {}
holds F.[g, [c,a]] = [f*g, [c,b]]
proof
let A be category, a, b be Object of A such that
A1: <^a,b^> <> {};
set B = Concretized A;
let f be Morphism of a,b;
defpred P[object,object] means
ex o being Object of A, g being Morphism of o, a st
<^o,a^> <> {} & $1 = [g,[o,a]] & $2 = [f*g, [o,b]];
A2: for x being object st x in B-carrier_of a
ex y being object st y in B-carrier_of b & P[x, y]
proof
let x be object;
assume x in B-carrier_of a;
then consider o being Object of A, g being Morphism of o,a such that
A3: <^o,a^> <> {} and
A4: x = [g,[o,a]] by Th43;
take [f*g, [o,b]];
<^o,b^> <> {} by A1,A3,ALTCAT_1:def 2;
hence thesis by A3,A4,Th43;
end;
consider F being Function such that
A5: dom F = B-carrier_of a & rng F c= B-carrier_of b and
A6: for x being object st x in B-carrier_of a holds P[x, F.x]
from FUNCT_1:sch 6(A2);
A7: F in Funcs(B-carrier_of a, B-carrier_of b) by A5,FUNCT_2:def 2;
then reconsider F as Function of B-carrier_of a, B-carrier_of b by FUNCT_2:66
;
take F;
ex fa,fb being Object of A, g being Morphism of fa, fb
st fa = a & fb = b & <^fa, fb^> <> {} &
for o being Object of A st <^o, fa^> <> {}
for h being Morphism of o,fa holds F.[h,[o,fa]] = [g*h,[o,fb]]
proof
take fa = a, fb = b;
reconsider g = f as Morphism of fa,fb;
take g;
thus fa = a & fb = b & <^fa, fb^> <> {} by A1;
let o be Object of A such that
A8: <^o, fa^> <> {};
let h be Morphism of o,fa;
[h,[o,fa]] in B-carrier_of fa by A8,Th43;
then consider c being Object of A, k being Morphism of c, fa such that
<^c,fa^> <> {} and
A9: [h,[o,fa]] = [k,[c,fa]] and
A10: F.[h,[o,fa]] = [g*k, [c,fb]] by A6;
[o,fa] = [c,fa] by A9,XTUPLE_0:1;
then o = c by XTUPLE_0:1;
hence thesis by A9,A10,XTUPLE_0:1;
end;
hence F in (the Arrows of B).(a,b) by A7,Def12;
let c be Object of A, g be Morphism of c,a;
assume <^c,a^> <> {};
then [g, [c,a]] in B-carrier_of a by Th43;
then consider o being Object of A, h being Morphism of o, a such that
<^o,a^> <> {} and
A11: [g,[c,a]] = [h,[o,a]] and
A12: F.[g,[c,a]] = [f*h, [o,b]] by A6;
[c,a] = [o,a] by A11,XTUPLE_0:1;
then c = o by XTUPLE_0:1;
hence thesis by A11,A12,XTUPLE_0:1;
end;
theorem Th45:
for A being category, a, b being Object of A
for F1,F2 being Function st F1 in (the Arrows of Concretized A).(a,b) &
F2 in (the Arrows of Concretized A).(a,b) &
F1.[idm a, [a,a]] = F2.[idm a, [a,a]] holds F1 = F2
proof
let A be category, a, b be Object of A;
set B = Concretized A;
let F1,F2 be Function such that
A1: F1 in (the Arrows of Concretized A).(a,b) and
A2: F2 in (the Arrows of Concretized A).(a,b) and
A3: F1.[idm a, [a,a]] = F2.[idm a, [a,a]];
A4: F1 in Funcs(B-carrier_of a, B-carrier_of b) by A1,Def12;
A5: F2 in Funcs(B-carrier_of a, B-carrier_of b) by A2,Def12;
A6: dom F1 = B-carrier_of a by A4,FUNCT_2:92;
A7: dom F2 = B-carrier_of a by A5,FUNCT_2:92;
consider fa,fb being Object of A, f being Morphism of fa, fb such that
A8: fa = a and
A9: fb = b and
A10: <^fa, fb^> <> {} and
A11: for o being Object of A st <^o, fa^> <> {}
for h being Morphism of o,fa holds F1.[h,[o,fa]] = [f*h,[o,fb]] by A1,Def12;
consider ga,gb being Object of A, g being Morphism of ga, gb such that
A12: ga = a and
A13: gb = b and <^ga, gb^> <> {} and
A14: for o being Object of A st <^o, ga^> <> {}
for h being Morphism of o,ga holds F2.[h,[o,ga]] = [g*h,[o,gb]] by A2,Def12;
reconsider f, g as Morphism of a, b by A8,A9,A12,A13;
A15: F1.[idm a, [a,a]] = [f* idm a, [a,b]] by A8,A9,A11;
A16: f* idm a = f by A8,A9,A10,ALTCAT_1:def 17;
A17: g* idm a = g by A8,A9,A10,ALTCAT_1:def 17;
F2.[idm a, [a,a]] = [g* idm a, [a,b]] by A12,A13,A14;
then
A18: f = g by A3,A15,A16,A17,XTUPLE_0:1;
now
let x be object;
assume x in B-carrier_of a;
then consider bb being Object of A, ff being Morphism of bb,a such that
A19: <^bb,a^> <> {} and
A20: x = [ff,[bb,a]] by Th43;
thus F1.x = [f*ff, [bb,b]] by A8,A9,A11,A19,A20
.= F2.x by A12,A13,A14,A18,A19,A20;
end;
hence thesis by A6,A7;
end;
scheme NonUniqMSFunctionEx {I() -> set, A, B() -> ManySortedSet of I(),
P[object,object,object]}:
ex F being ManySortedFunction of A(), B() st
for i,x being object st i in I() & x in A().i
holds F.i.x in B().i & P[i,x,F.i.x]
provided
A1: for i,x being object st i in I() & x in A().i
ex y being object st y in B().i & P[i,x,y];
defpred P[object,object] means
ex f being Function of A().$1, B().$1 st $2 = f &
for x being set st x in A().$1 holds f.x in B().$1 & P[$1,x,f.x];
A2: for i being object st i in I() ex y being object st P[i,y]
proof
let i be object such that
A3: i in I();
defpred Q[object,object] means $2 in B().i & P[i,$1,$2];
A4: now
let x be object;
assume x in A().i;
then ex y being object st y in B().i & P[i,x,y] by A1,A3;
hence ex y being object st y in B().i & Q[x,y];
end;
consider f being Function such that
A5: dom f = A().i & rng f c= B().i and
A6: for x being object st x in A().i holds Q[x, f.x]
from FUNCT_1:sch 6(A4);
reconsider f as Function of A().i, B().i by A5,FUNCT_2:2;
take f, f;
thus thesis by A6;
end;
consider F being Function such that
A7: dom F = I() and
A8: for i being object st i in I() holds P[i, F.i]
from CLASSES1:sch 1(A2);
reconsider F as ManySortedSet of I() by A7,PARTFUN1:def 2,RELAT_1:def 18;
now
let i be object;
assume i in I();
then ex f being Function of A().i, B().i st F.i = f &
for x being set st x in A().i holds f.x in B().i & P[i,x,f.x] by A8;
hence F.i is Function of A().i, B().i;
end;
then reconsider F as ManySortedFunction of A(), B() by PBOOLE:def 15;
take F;
let i,x be object;
assume i in I();
then ex f being Function of A().i, B().i st F.i = f &
for x being set st x in A().i holds f.x in B().i & P[i,x,f.x] by A8;
hence thesis;
end;
definition
let A be category;
set B = Concretized A;
func Concretization A -> covariant strict Functor of A, Concretized A means
: Def13:
(for a being Object of A holds it.a = a) &
for a, b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds it.f.[idm a, [a,a]] = [f, [a,b]];
uniqueness
proof
let F,G be covariant strict Functor of A,B such that
A1: for a being Object of A holds F.a = a and
A2: for a, b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds F.f.[idm a, [a,a]] = [f, [a,b]] and
A3: for a being Object of A holds G.a = a and
A4: for a, b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds G.f.[idm a, [a,a]] = [f, [a,b]];
A5: now
let a be Object of A;
thus F.a = a by A1
.= G.a by A3;
end;
now
let a,b be Object of A;
assume
A6: <^a,b^> <> {};
let f be Morphism of a,b;
A7: F.f.[idm a, [a,a]] = [f, [a,b]] by A2,A6;
A8: G.f.[idm a, [a,a]] = [f, [a,b]] by A4,A6;
A9: <^F.a, F.b^> <> {} by A6,FUNCTOR0:def 18;
A10: F.a = a by A1;
A11: F.b = b by A1;
A12: G.a = a by A3;
G.b = b by A3;
hence F.f = G.f by A7,A8,A9,A10,A11,A12,Th45;
end;
hence thesis by A5,Th1;
end;
existence
proof
deffunc O(set) = $1;
A13: the carrier of B = the carrier of A by Def12;
A14: for a being Object of A holds O(a) is Object of B by Def12;
reconsider AA = the Arrows of B as
ManySortedSet of [:the carrier of A, the carrier of A:] by A13;
defpred P[object,object,object] means
ex a, b being Object of A, f being Morphism of a,b,
G being Function of B-carrier_of a, B-carrier_of b
st $1 = [a,b] & $2 = f & $3 = G &
for c being Object of A, g being Morphism of c,a st <^c,a^> <> {}
holds G.[g, [c,a]] = [f*g, [c,b]];
A15: for i,x being object
st i in [:the carrier of A, the carrier of A:] & x in (the Arrows of A).i
ex y being object st y in AA.i & P[i,x,y]
proof
let i,x be object;
assume i in [:the carrier of A, the carrier of A:];
then consider a,b being object such that
A16: a in the carrier of A and
A17: b in the carrier of A and
A18: i = [a,b] by ZFMISC_1:def 2;
reconsider a, b as Object of A by A16,A17;
assume
A19: x in (the Arrows of A).i;
then reconsider f = x as Morphism of a,b by A18;
consider G being Function of B-carrier_of a, B-carrier_of b such that
A20: G in AA.(a,b) and
A21: for c being Object of A, g being Morphism of c,a st <^c,a^> <> {}
holds G.[g, [c,a]] = [f*g, [c,b]] by A18,A19,Th44;
take G;
thus thesis by A18,A20,A21;
end;
consider F being ManySortedFunction of the Arrows of A, AA such that
A22: for i,x being object
st i in [:the carrier of A, the carrier of A:] & x in (the Arrows of A).i
holds F.i.x in AA.i & P[i,x,F.i.x] from NonUniqMSFunctionEx(A15);
deffunc F(set,set,set) = F.[$1,$2].$3;
A23: for a,b being Object of A st <^a,b^> <> {} for f being Morphism of a,b
holds F(a,b,f) in (the Arrows of B).(O(a), O(b))
proof
let a,b be Object of A such that
A24: <^a,b^> <> {};
let f be Morphism of a,b;
[a,b] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
hence thesis by A22,A24;
end;
A25: for a,b,c being Object of A st <^a,b^> <> {} & <^b,c^> <> {}
for f being Morphism of a,b, g being Morphism of b,c
for a9,b9,c9 being Object of B st a9 = O(a) & b9 = O(b) & c9 = O(c)
for f9 being Morphism of a9,b9, g9 being Morphism of b9,c9
st f9 = F(a,b,f) & g9 = F(b,c,g) holds F(a,c,g*f) = g9*f9
proof
let a,b,c be Object of A such that
A26: <^a,b^> <> {} and
A27: <^b,c^> <> {};
let f be Morphism of a,b, g be Morphism of b,c;
let a9,b9,c9 be Object of B such that
A28: a9 = a and
A29: b9 = b and
A30: c9 = c;
let f9 be Morphism of a9,b9, g9 be Morphism of b9,c9 such that
A31: f9 = F.[a,b].f and
A32: g9 = F.[b,c].g;
A33: [a,b] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider a1, b1 being Object of A, f1 being Morphism of a1,b1,
G1 being Function of B-carrier_of a1, B-carrier_of b1 such that
A34: [a,b] = [a1,b1] and
A35: f = f1 and
A36: F.[a,b].f = G1 and
A37: for c being Object of A, g being Morphism of c,a1 st <^c,a1^> <> {}
holds G1.[g, [c,a1]] = [f1*g, [c,b1]] by A22,A26;
A38: [b,c] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider b2, c2 being Object of A, g2 being Morphism of b2,c2,
G2 being Function of B-carrier_of b2, B-carrier_of c2 such that
A39: [b,c] = [b2,c2] and
A40: g = g2 and
A41: F.[b,c].g = G2 and
A42: for c being Object of A, g being Morphism of c,b2 st <^c,b2^> <> {}
holds G2.[g, [c,b2]] = [g2*g, [c,c2]] by A22,A27;
A43: <^a,c^> <> {} by A26,A27,ALTCAT_1:def 2;
[a,c] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider a3, c3 being Object of A, h3 being Morphism of a3,c3,
G3 being Function of B-carrier_of a3, B-carrier_of c3 such that
A44: [a,c] = [a3,c3] and
A45: g*f = h3 and
A46: F.[a,c].(g*f) = G3 and
A47: for c being Object of A, g being Morphism of c,a3 st <^c,a3^> <> {}
holds G3.[g, [c,a3]] = [h3*g, [c,c3]] by A22,A43;
A48: F.[a,b].f in <^a9,b9^> by A22,A26,A28,A29,A33;
A49: F.[b,c].g in <^b9,c9^> by A22,A27,A29,A30,A38;
A50: a = a1 by A34,XTUPLE_0:1;
A51: b = b1 by A34,XTUPLE_0:1;
A52: b = b2 by A39,XTUPLE_0:1;
A53: c = c2 by A39,XTUPLE_0:1;
A54: a = a3 by A44,XTUPLE_0:1;
A55: c = c3 by A44,XTUPLE_0:1;
reconsider G1 as Function of B-carrier_of a, B-carrier_of b by A34,A50,
XTUPLE_0:1;
reconsider G2 as Function of B-carrier_of b, B-carrier_of c by A39,A52,
XTUPLE_0:1;
reconsider G3 as Function of B-carrier_of a, B-carrier_of c by A44,A54,
XTUPLE_0:1;
now
let x be Element of B-carrier_of a;
consider bb being Object of A, ff being Morphism of bb,a such that
A56: <^bb,a^> <> {} and
A57: x = [ff,[bb,a]] by Th43;
A58: <^bb,b^> <> {} by A26,A56,ALTCAT_1:def 2;
thus G3.x = [g*f*ff, [bb,c]] by A45,A47,A54,A55,A56,A57
.= [g*(f*ff), [bb,c]] by A26,A27,A56,ALTCAT_1:21
.= G2.[f*ff, [bb,b]] by A40,A42,A52,A53,A58
.= G2.(G1.x) by A35,A37,A50,A51,A56,A57
.= (G2*G1).x by FUNCT_2:15;
end;
then G3 = G2*G1;
hence thesis by A31,A32,A36,A41,A46,A48,A49,Th36;
end;
A59: for a being Object of A, a9 being Object of B st a9 = O(a)
holds F(a,a,idm a) = idm a9
proof
let a be Object of A, a9 be Object of B such that
A60: a9 = a;
[a,a] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider c, b being Object of A, f being Morphism of c,b,
G being Function of B-carrier_of c, B-carrier_of b such that
A61: [a,a] = [c,b] and
A62: idm a = f and
A63: F.[a,a].idm a = G and
A64: for d being Object of A, g being Morphism of d,c st <^d,c^> <> {}
holds G.[g, [d,c]] = [f*g, [d,b]] by A22;
A65: idm a9 = id the_carrier_of a9 by Def10;
A66: a = c by A61,XTUPLE_0:1;
A67: a = b by A61,XTUPLE_0:1;
now
let x be Element of the_carrier_of a9;
consider bb being Object of A, ff being Morphism of bb,a such that
A68: <^bb,a^> <> {} and
A69: x = [ff,[bb,a]] by A60,Th43;
thus G.x = [(idm a)*ff, [bb,a]] by A62,A64,A66,A67,A68,A69
.= x by A68,A69,ALTCAT_1:20
.= (id the_carrier_of a9).x;
end;
hence thesis by A60,A63,A65,A66,A67,FUNCT_2:63;
end;
consider FF being covariant strict Functor of A,B such that
A70: for a being Object of A holds FF.a = O(a) and
A71: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds FF.f = F(a,b,f)
from CovariantFunctorLambda(A14,A23,A25,A59);
take FF;
thus for a being Object of A holds FF.a = a by A70;
let a, b be Object of A such that
A72: <^a,b^> <> {};
let f be Morphism of a,b;
[a,b] in [:the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider a9, b9 being Object of A, f9 being Morphism of a9,b9,
G being Function of B-carrier_of a9, B-carrier_of b9 such that
A73: [a,b] = [a9,b9] and
A74: f = f9 and
A75: F.[a,b].f = G and
A76: for c being Object of A, g being Morphism of c,a9 st <^c,a9^> <> {}
holds G.[g, [c,a9]] = [f9*g, [c,b9]] by A22,A72;
A77: G = FF.f by A71,A72,A75;
A78: a = a9 by A73,XTUPLE_0:1;
b = b9 by A73,XTUPLE_0:1;
hence FF.f.[idm a, [a,a]] = [f* idm a, [a,b]] by A74,A76,A77,A78
.= [f, [a,b]] by A72,ALTCAT_1:def 17;
end;
end;
registration
let A be category;
cluster Concretization A -> bijective;
coherence
proof
set B = Concretized A;
set FF = Concretization A;
deffunc O(set) = $1;
A1: for a being Object of A holds FF.a = O(a) by Def13;
deffunc F(Object of A, Object of A, Morphism of $1,$2) = FF.$3;
A2: for a,b being Object of A st <^a,b^> <> {}
for f being Morphism of a,b holds FF.f = F(a,b,f);
A3: for a,b being Object of A st O(a) = O(b) holds a = b;
A4: for a,b being Object of A st <^a,b^> <> {}
for f,g being Morphism of a,b st F(a,b,f) = F(a,b,g) holds f = g
proof
let a,b be Object of A such that
A5: <^a,b^> <> {};
let f,g be Morphism of a,b;
A6: FF.f.[idm a, [a,a]] = [f, [a,b]] by A5,Def13;
FF.g.[idm a, [a,a]] = [g, [a,b]] by A5,Def13;
hence thesis by A6,XTUPLE_0:1;
end;
A7: for a,b being Object of B st <^a,b^> <> {} for f being Morphism of a,b
ex c,d being Object of A, g being Morphism of c,d
st a = O(c) & b = O(d) & <^c,d^> <> {} & f = F(c,d,g)
proof
let a,b be Object of B such that
A8: <^a,b^> <> {};
reconsider c = a, d = b as Object of A by Def12;
let f be Morphism of a,b;
take c,d;
consider fa,fb being Object of A, g being Morphism of fa, fb such that
A9: fa = c and
A10: fb = d and
A11: <^fa, fb^> <> {} and
A12: for o being Object of A st <^o, fa^> <> {}
for h being Morphism of o,fa holds f.[h,[o,fa]] = [g*h,[o,fb]]
by A8,Def12;
reconsider g as Morphism of c,d by A9,A10;
take g;
A13: FF.g.[idm c, [c,c]] = [g, [c,d]] by A9,A10,A11,Def13;
g* idm c = g by A9,A10,A11,ALTCAT_1:def 17;
then
A14: FF.g.[idm c, [c,c]] = f.[idm c, [c,c]] by A9,A10,A12,A13;
A15: FF.c = a by Def13;
FF.d = b by Def13;
hence thesis by A8,A9,A10,A11,A14,A15,Th45;
end;
thus thesis from CoBijectiveSch(A1,A2,A3,A4,A7);
end;
end;
::$N Representation theorem for categories as concrete categories
theorem
for A being category holds A, Concretized A are_isomorphic
proof
let A be category;
take Concretization A;
thus thesis;
end;