:: Exponential Objects
:: by Marco Riccardi
::
:: Received August 15, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, SUBSET_1, WELLORD1,
CAT_1, CAT_4, ALTCAT_1, GRAPH_1, BINOP_1, STRUCT_0, PARTFUN1, MONOID_0,
NATTRA_1, MSSUBFAM, CARD_1, FUNCTOR0, MOD_4, CAT_6, XTUPLE_0, RECDEF_2,
MCART_1, PBOOLE, WELLORD2, FACIRC_1, FUNCT_2, NEWTON, POLYNOM2, CAT_7,
CAT_8, PZFMISC1, FUNCOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
ORDINAL1, PARTFUN1, FINSEQ_1, STRUCT_0, FUNCOP_1, RELSET_1, BINOP_1,
GRAPH_1, CAT_1, CAT_2, CAT_3, NUMBERS, NAT_1, XTUPLE_0, ALG_1, WELLORD2,
CARD_1, CAT_6, ENUMSET1, WELLORD1, CAT_7, NATTRA_1, ISOCAT_1;
constructors NUMBERS, FUNCT_2, CLASSES2, FINSEQ_1, FUNCOP_1, RELAT_2,
PARTFUN1, RELSET_1, BINOP_1, FUNCT_4, CAT_1, CAT_2, CAT_3, NAT_1,
XXREAL_0, WELLORD2, XREAL_0, CARD_1, VALUED_0, ISOCAT_1, STRUCT_0, CAT_6,
REALSET1, WELLORD1, ORDERS_2, CAT_7, NATTRA_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, XTUPLE_0, CARD_1, STRUCT_0,
RELSET_1, FUNCT_2, PARTFUN1, CAT_1, NAT_1, CAT_6, CAT_7;
requirements SUBSET, BOOLE, NUMERALS;
begin :: Preliminaries
theorem :: CAT_8:1
for C being composable associative CategoryStr,
f1,f2,f3 being morphism of C st f1 |> f2 & f2 |> f3 holds
f1(*)f2(*)f3 = f1(*)(f2(*)f3);
theorem :: CAT_8:2
for C being composable associative CategoryStr,
f1,f2,f3,f4 being morphism of C st f1 |> f2 & f2 |> f3 & f3 |> f4 holds
f1(*)f2(*)f3(*)f4 = (f1(*)f2)(*)(f3(*)f4) &
f1(*)f2(*)f3(*)f4 = f1(*)(f2(*)f3)(*)f4 &
f1(*)f2(*)f3(*)f4 = f1(*)(f2(*)f3(*)f4) &
f1(*)f2(*)f3(*)f4 = f1(*)(f2(*)(f3(*)f4));
theorem :: CAT_8:3
for C being composable CategoryStr,
f,f1,f2 being morphism of C st f1 |> f2
holds
(f1(*)f2 |> f iff f2 |> f) &
(f |> f1(*)f2 iff f |> f1);
theorem :: CAT_8:4
for C being composable with_identities CategoryStr,
f1,f2 being morphism of C st f1 |> f2
holds
(f1 is identity implies f1(*)f2 = f2) &
(f2 is identity implies f1(*)f2 = f1);
theorem :: CAT_8:5
for C being non empty with_identities CategoryStr, f being morphism of C
ex f1,f2 being morphism of C st f1 is identity & f2 is identity &
f1 |> f & f |> f2;
theorem :: CAT_8:6
for C being CategoryStr, a,b being Object of C
for f being Morphism of a,b st Hom(a,b) = {f} for g being
Morphism of a,b holds f = g;
theorem :: CAT_8:7
for C being CategoryStr, a,b being Object of C
for f being Morphism of a,b st Hom(a,b) <> {} & for g being
Morphism of a,b holds f = g holds Hom(a,b) = {f};
theorem :: CAT_8:8
for x being object, C being CategoryStr st
the carrier of C = {x} & the composition of C = {[[x,x],x]}
holds C is non empty category;
theorem :: CAT_8:9
for C1,C2 being category, F being Functor of C1,C2 st
F is isomorphism holds F is bijective;
theorem :: CAT_8:10
for C1,C2,C3 being composable with_identities CategoryStr
st C1 ~= C2 & C2 ~= C3 holds C1 ~= C3;
theorem :: CAT_8:11
for C1,C2 being category st C1 ~= C2 holds C1 is empty iff C2 is empty;
registration
let C1 be empty with_identities CategoryStr;
let C2 be with_identities CategoryStr;
cluster -> covariant for Functor of C1,C2;
end;
theorem :: CAT_8:12
for C1,C2 being with_identities CategoryStr,
f being morphism of C1, F being Functor of C1,C2
st F is covariant & f is identity holds F.f is identity;
theorem :: CAT_8:13
for C1,C2 being with_identities CategoryStr,
f1,f2 being morphism of C1, F being Functor of C1,C2
st F is covariant & f1 |> f2
holds F.f1 |> F.f2 & F.(f1(*)f2) = (F.f1) (*) (F.f2);
theorem :: CAT_8:14
for C being Category, f being (Morphism of C), g being morphism of alter C
st f = g holds dom g = id dom f & cod g = id cod f;
theorem :: CAT_8:15
ex f being morphism of OrdC 1 st f is identity &
Ob OrdC 1 = {f} & Mor OrdC 1 = {f};
theorem :: CAT_8:16
for C being non empty category, f1,f2 being morphism of C st
MORPHISM(f1) = MORPHISM(f2) holds f1 = f2;
theorem :: CAT_8:17
for C being non empty category, F1,F2 being covariant Functor of OrdC 2, C,
f being morphism of OrdC 2 st f is non identity & F1.f = F2.f
holds F1 = F2;
theorem :: CAT_8:18
ex f1,f2 being morphism of (OrdC 3) st
f1 is not identity & f2 is not identity & cod f1 = dom f2 &
Ob (OrdC 3) = {dom f1, cod f1, cod f2} &
Mor (OrdC 3) = {dom f1, cod f1, cod f2, f1, f2, f2(*)f1} &
dom f1, cod f1, cod f2, f1, f2, f2(*)f1 are_mutually_distinct;
definition
let C be non empty category;
let f1,f2 be morphism of C such that
f1 |> f2;
func COMPOSITION(f1,f2) -> covariant Functor of (OrdC 3), C means
:: CAT_8:def 1
for g1,g2 being morphism of OrdC 3 st g1 |> g2 & g1 is not identity &
g2 is not identity holds it.g1 = f1 & it.g2 = f2;
end;
begin :: Terminal Objects
definition
let C be CategoryStr;
let a be Object of C;
attr a is terminal means
:: CAT_8:def 2
for b being Object of C holds
Hom(b,a)<>{} & ex f being Morphism of b,a
st for g being Morphism of b,a holds f = g;
end;
theorem :: CAT_8:19
for C being CategoryStr, b being Object of C holds
b is terminal iff for a being Object of C
ex f being Morphism of a,b st Hom(a,b) = {f};
theorem :: CAT_8:20
for C being with_identities non empty CategoryStr, a being Object of C holds
a is terminal implies for h being Morphism of a,a holds id- a = h;
theorem :: CAT_8:21
for C being composable with_identities non empty CategoryStr,
a,b being Object of C
holds a is terminal & b is terminal implies a,b are_isomorphic;
theorem :: CAT_8:22
for C being non empty category, a,b being Object of C
holds b is terminal & a,b are_isomorphic implies a is terminal;
theorem :: CAT_8:23
for C being composable with_identities CategoryStr,
a,b being Object of C, f being Morphism of a,b
holds Hom(a,b) <> {} & a is terminal implies f is monomorphism;
definition
let C be category;
attr C is with_terminal_objects means
:: CAT_8:def 3
ex a being Object of C st a is terminal;
end;
theorem :: CAT_8:24
OrdC 1 is with_terminal_objects;
registration
cluster with_terminal_objects for category;
end;
definition
let C be category;
attr C is terminal means
:: CAT_8:def 4
for B being category holds ex F being Functor of B,C st F is covariant &
for G being Functor of B,C st G is covariant holds F = G;
end;
registration
cluster OrdC 1 -> non empty terminal;
end;
registration
cluster strict non empty terminal for category;
cluster strict non terminal for category;
end;
theorem :: CAT_8:25
for C,D being terminal category holds C ~= D;
theorem :: CAT_8:26
for C,D being category st C is terminal & C ~= D holds D is terminal;
theorem :: CAT_8:27
for C being category holds C is non empty trivial iff C ~= OrdC 1;
theorem :: CAT_8:28
for C,D being non empty category st C is trivial & D is trivial holds C ~= D;
registration
cluster non empty trivial -> terminal for category;
cluster terminal -> non empty trivial for category;
end;
definition
let C be category;
func C ->OrdC1 -> covariant Functor of C, OrdC 1 means
:: CAT_8:def 5
not contradiction;
end;
theorem :: CAT_8:29
for C,C1,C2 being category, F1 being Functor of C,C1,
F2 being Functor of C,C2 st F1 is covariant & F2 is covariant
holds (C1 ->OrdC1)(*)F1 = (C2 ->OrdC1)(*)F2;
begin :: Initial Objects
definition
let C be CategoryStr;
let a be Object of C;
attr a is initial means
:: CAT_8:def 6
for b being Object of C holds
Hom(a,b)<>{} & ex f being Morphism of a,b
st for g being Morphism of a,b holds f = g;
end;
theorem :: CAT_8:30
for C being CategoryStr, b being Object of C holds
b is initial iff for a being Object of C
ex f being Morphism of b,a st Hom(b,a) = {f};
theorem :: CAT_8:31
for C being with_identities non empty CategoryStr, a being Object of C holds
a is initial implies for h being Morphism of a,a holds id- a = h;
theorem :: CAT_8:32
for C being composable with_identities non empty CategoryStr,
a,b being Object of C
holds a is initial & b is initial implies a,b are_isomorphic;
theorem :: CAT_8:33
for C being non empty category, a,b being Object of C
holds b is initial & b,a are_isomorphic implies a is initial;
theorem :: CAT_8:34
for C being composable with_identities CategoryStr,
a,b being Object of C, f being Morphism of a,b
holds Hom(a,b) <> {} & b is initial implies f is epimorphism;
definition
let C be category;
attr C is with_initial_objects means
:: CAT_8:def 7
ex a being Object of C st a is initial;
end;
theorem :: CAT_8:35
OrdC 1 is with_initial_objects;
registration
cluster with_initial_objects for category;
end;
definition
let C be category;
attr C is initial means
:: CAT_8:def 8
for C1 being category ex F being Functor of C,C1 st F is covariant &
for F1 being Functor of C,C1 st F1 is covariant holds F = F1;
end;
registration
cluster OrdC 0 -> empty initial;
end;
registration
cluster strict empty initial for category;
cluster strict non initial for category;
end;
theorem :: CAT_8:36
for C,D being initial category holds C ~= D;
theorem :: CAT_8:37
for C,D being category st C is initial & C ~= D holds D is initial;
registration
cluster empty -> initial for category;
end;
definition
let C be category;
func OrdC0-> C -> covariant Functor of OrdC 0, C means
:: CAT_8:def 9
not contradiction;
end;
theorem :: CAT_8:38
for C,C1,C2 being category, F1 being Functor of C1,C,
F2 being Functor of C2,C st F1 is covariant & F2 is covariant
holds F1(*)(OrdC0-> C1) = F2(*)(OrdC0-> C2);
begin :: Categorical Products
definition
let C be category;
let a,b,c be Object of C;
let p1 be Morphism of c,a such that Hom(c,a) <> {};
let p2 be Morphism of c,b such that Hom(c,b) <> {};
pred c,p1,p2 is_product_of a,b means
:: CAT_8:def 10
for c1 being Object of C,
q1 being Morphism of c1,a, q2 being Morphism of c1,b
st Hom(c1,a) <> {} & Hom(c1,b) <> {}
holds Hom(c1,c) <> {} & ex h being Morphism of c1,c st
p1 * h = q1 & p2 * h = q2
& for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds h = h1;
end;
theorem :: CAT_8:39
for C being non empty category, c1,c2,a,b being Object of C,
p1 being Morphism of a,c1, p2 being Morphism of a,c2,
q1 being Morphism of b,c1, q2 being Morphism of b,c2
st Hom(a,c1) <> {} & Hom(a,c2) <> {} & Hom(b,c1) <> {} & Hom(b,c2) <> {} &
a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2
holds a,b are_isomorphic;
theorem :: CAT_8:40
for C being category, c1,c2,d being Object of C,
p1 being Morphism of d,c1, p2 being Morphism of d,c2
st Hom(d,c1) <> {} & Hom(d,c2) <> {} &
d,p1,p2 is_product_of c1,c2 holds d,p2,p1 is_product_of c2,c1;
definition
let C be category;
attr C is with_binary_products means
:: CAT_8:def 11
for a,b being Object of C holds ex d being Object of C,
p1 being Morphism of d,a, p2 being Morphism of d,b st
Hom(d,a) <> {} & Hom(d,b) <> {} & d,p1,p2 is_product_of a,b;
end;
theorem :: CAT_8:41
OrdC 1 is with_binary_products;
registration
cluster with_binary_products non empty for category;
end;
definition
let C be with_binary_products category;
let c1,c2 be Object of C;
mode categorical_product of c1,c2 -> triple object means
:: CAT_8:def 12
ex d being Object of C, p1 being Morphism of d,c1, p2 being Morphism of d,c2
st it = [d,p1,p2] & Hom(d,c1) <> {} & Hom(d,c2) <> {} &
d,p1,p2 is_product_of c1,c2;
end;
definition
let C be with_binary_products category;
let c1,c2 be Object of C;
func c1 [x] c2 -> Object of C equals
:: CAT_8:def 13
(the categorical_product of c1,c2)`1_3;
end;
definition
let C be with_binary_products category;
let c1,c2 be Object of C;
func pr1(c1,c2) -> Morphism of c1 [x] c2,c1 equals
:: CAT_8:def 14
(the categorical_product of c1,c2)`2_3;
func pr2(c1,c2) -> Morphism of c1 [x] c2,c2 equals
:: CAT_8:def 15
(the categorical_product of c1,c2)`3_3;
end;
theorem :: CAT_8:42
for C being with_binary_products category, a,b being Object of C holds
a [x] b, pr1(a,b), pr2(a,b) is_product_of a,b &
Hom(a [x] b,a) <> {} & Hom(a [x] b,b) <> {};
theorem :: CAT_8:43
for C being with_binary_products category, a,b,c being Object of C
st Hom(c,a) <> {} & Hom(c,b) <> {} holds Hom(c,a [x] b)<> {};
theorem :: CAT_8:44
for C being with_binary_products category, a,b,c,d being Object of C
st Hom(a,b) <> {} & Hom(c,d) <> {} holds Hom(a [x] c,b [x] d)<> {};
definition
let C be with_binary_products category;
let a,b,c,d be Object of C;
let f be Morphism of a,b such that
Hom(a,b) <> {};
let g be Morphism of c,d such that
Hom(c,d) <> {};
func f [x] g -> Morphism of a [x] c,b [x] d means
:: CAT_8:def 16
f * pr1(a,c) = pr1(b,d) * it & g * pr2(a,c) = pr2(b,d) * it;
end;
definition
let C1,C2,D be category;
let P1 be Functor of D,C1 such that P1 is covariant;
let P2 be Functor of D,C2 such that P2 is covariant;
pred D,P1,P2 is_product_of C1,C2 means
:: CAT_8:def 17
for D1 being category, G1 being Functor of D1,C1, G2 being Functor of D1,C2
st G1 is covariant & G2 is covariant holds
ex H being Functor of D1,D st H is covariant & P1 (*) H = G1 & P2 (*) H = G2
& for H1 being Functor of D1,D
st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds H = H1;
end;
theorem :: CAT_8:45
for C1,C2,A,B being category, P1 be Functor of A,C1, P2 be Functor of A,C2,
Q1 be Functor of B,C1, Q2 be Functor of B,C2
st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant &
A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2
holds A ~= B;
theorem :: CAT_8:46
for C1,C2,D being category, P1 being Functor of D,C1,
P2 being Functor of D,C2
st P1 is covariant & P2 is covariant &
D,P1,P2 is_product_of C1,C2 holds D,P2,P1 is_product_of C2,C1;
notation
let C,C1,C2 be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
synonym F1 [|x|] F2 for [| F1, F2 |];
end;
theorem :: CAT_8:47
for C1,C2 being category holds (C1 ->OrdC1)[|x|](C2 ->OrdC1),
pr1(C1 ->OrdC1,C2 ->OrdC1),pr2(C1 ->OrdC1,C2 ->OrdC1) is_product_of C1,C2;
definition
let C1,C2 be category;
mode categorical_product of C1,C2 -> triple object means
:: CAT_8:def 18
ex D being strict category, P1 being Functor of D,C1,
P2 being Functor of D,C2 st it = [D,P1,P2] &
P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2;
end;
definition
let C1,C2 be category;
func C1 [x] C2 -> strict category equals
:: CAT_8:def 19
(the categorical_product of C1,C2)`1_3;
end;
definition
let C1,C2 be category;
func pr1(C1,C2) -> Functor of C1 [x] C2, C1 equals
:: CAT_8:def 20
(the categorical_product of C1,C2)`2_3;
func pr2(C1,C2) -> Functor of C1 [x] C2, C2 equals
:: CAT_8:def 21
(the categorical_product of C1,C2)`3_3;
end;
theorem :: CAT_8:48
for C1,C2 being category holds
C1 [x] C2,pr1(C1,C2),pr2(C1,C2) is_product_of C1,C2;
registration
let C1,C2 be category;
cluster pr1(C1,C2) -> covariant;
cluster pr2(C1,C2) -> covariant;
end;
theorem :: CAT_8:49
for C1,C2 being category holds
C1 [x] C2 is non empty iff (C1 is non empty & C2 is non empty);
registration
let C1 be empty category;
let C2 be category;
cluster C1 [x] C2 -> empty;
end;
registration
let C1 be category;
let C2 be empty category;
cluster C1 [x] C2 -> empty;
end;
registration
let C1 be non empty category;
let C2 be non empty category;
cluster C1 [x] C2 -> non empty;
end;
definition
let C1,C2,D1,D2 be category;
let F1 be Functor of C1,D1;
let F2 be Functor of C2,D2;
assume
F1 is covariant & F2 is covariant;
func F1 [x] F2 -> Functor of C1 [x] C2,D1 [x] D2 means
:: CAT_8:def 22
it is covariant &
F1(*)pr1(C1,C2) = pr1(D1,D2)(*)it & F2(*)pr2(C1,C2) = pr2(D1,D2)(*)it;
end;
theorem :: CAT_8:50
for A1,A2,B1,B2,C1,C2 being category, F1 being Functor of A1,B1,
F2 being Functor of A2,B2, G1 being Functor of B1,C1,
G2 being Functor of B2,C2
st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant
holds (G1 [x] G2)(*)(F1 [x] F2) = G1(*)F1 [x] G2(*)F2;
theorem :: CAT_8:51
for C1,C2 being category holds id C1 [x] id C2 = id(C1 [x] C2);
notation
let x,y be object;
synonym KuratowskiPair(x,y) for [x,y];
end;
definition
let C1,C2 be category;
let f1 be morphism of C1;
let f2 be morphism of C2;
func [f1,f2] -> morphism of C1 [x] C2 means
:: CAT_8:def 23
pr1(C1,C2).it = f1 & pr2(C1,C2).it = f2 if C1 is not empty & C2 is not empty
otherwise it = the morphism of C1 [x] C2;
end;
theorem :: CAT_8:52
for C1,C2 be category, f being morphism of C1 [x] C2
ex f1 being morphism of C1, f2 being morphism of C2 st f = [f1,f2];
theorem :: CAT_8:53
for C1,C2 being non empty category, f1,g1 being morphism of C1,
f2,g2 being morphism of C2
st [f1,f2] = [g1,g2] holds f1 = g1 & f2 = g2;
theorem :: CAT_8:54
for C1,C2 being category, f1,g1 being morphism of C1,
f2,g2 being morphism of C2
holds [f1,f2] |> [g1,g2] iff f1 |> g1 & f2 |> g2;
theorem :: CAT_8:55
for C1,C2 being category, f1,g1 being morphism of C1,
f2,g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds
[f1,f2](*)[g1,g2] = [f1(*)g1,f2(*)g2];
theorem :: CAT_8:56
for C1,C2 be category, f1 being morphism of C1, f2 being morphism of C2,
f being morphism of C1 [x] C2
st f = [f1,f2] & C1 is non empty & C2 is non empty
holds f is identity iff f1 is identity & f2 is identity;
theorem :: CAT_8:57
for C1,C2 being non empty category, D1,D2 being category,
F1 being Functor of C1,D1, F2 being Functor of C2,D2,
c1 being morphism of C1, c2 being morphism of C2
st F1 is covariant & F2 is covariant holds (F1[x]F2).[c1,c2] = [F1.c1,F2.c2];
begin :: Natural Transformations
definition
let C1,C2 be category;
let F1,F2 be Functor of C1,C2;
let T be Functor of C1,C2;
pred T is_natural_transformation_of F1,F2 means
:: CAT_8:def 24
for f1,f2 being morphism of C1 st f1 |> f2
holds T.f1 |> F1.f2 & F2.f1 |> T.f2 &
T.(f1(*)f2) = (T.f1)(*)(F1.f2) & T.(f1(*)f2) = (F2.f1)(*)(T.f2);
end;
theorem :: CAT_8:58
for C1,C2 being category, F1,F2 being Functor of C1,C2,
T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
T is_natural_transformation_of F1,F2 iff
for f,f1,f2 being morphism of C1 st f1 is identity & f2 is identity &
f1 |> f & f |> f2 holds T.f1 |> F1.f & F2.f |> T.f2 &
T.f = (T.f1)(*)(F1.f) & T.f = (F2.f)(*)(T.f2);
theorem :: CAT_8:59
for C1,C2 being non empty category, F1,F2 being covariant Functor of C1,C2,
T being Function of Ob(C1), Mor(C2) holds
(ex T1 being Functor of C1,C2
st T = T1|Ob(C1) & T1 is_natural_transformation_of F1,F2) iff
(for a being Object of C1 holds T.a in Hom(F1.a,F2.a)) &
(for a1,a2 being Object of C1,f being Morphism of a1,a2 st Hom(a1,a2) <> {}
holds (T.a2)(*)(F1.f) = (F2.f)(*)(T.a1));
theorem :: CAT_8:60
for C,D being Category, F1,F2 being Functor of C,D,
G1,G2,T being Functor of alter(C),alter(D) st F1 = G1 & F2 = G2 &
T is_natural_transformation_of G1,G2
holds (IdMap C)*T is natural_transformation of F1,F2;
definition
let C,D be category;
let F1,F2 be Functor of C,D;
pred F1 is_naturally_transformable_to F2 means
:: CAT_8:def 25
ex T being Functor of C,D st T is_natural_transformation_of F1,F2;
end;
definition
let C,D be category;
let F1,F2 be Functor of C,D;
assume
F1 is_naturally_transformable_to F2;
mode natural_transformation of F1,F2 -> Functor of C,D means
:: CAT_8:def 26
it is_natural_transformation_of F1,F2;
end;
theorem :: CAT_8:61
for C,D being category, F being Functor of C,D
st F is covariant holds F is_natural_transformation_of F,F;
definition
let C,D be category;
let F,F1,F2 be Functor of C,D;
assume that
F1 is_naturally_transformable_to F &
F is_naturally_transformable_to F2 and
F is covariant & F1 is covariant & F2 is covariant;
let T1 be natural_transformation of F1,F;
let T2 be natural_transformation of F,F2;
func T2`*`T1 -> natural_transformation of F1,F2 means
:: CAT_8:def 27
for f,f1,f2 being morphism of C st f1 is identity & f2 is identity &
f |> f1 & f2 |> f holds it.f = (T2.f2)(*)(F.f)(*)(T1.f1);
end;
theorem :: CAT_8:62
for C,D being category, F,F1,F2 being Functor of C,D
st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 &
F is covariant & F1 is covariant & F2 is covariant
holds F1 is_naturally_transformable_to F2;
definition
let C1,C2 be category;
func Functors(C1,C2) -> strict category means
:: CAT_8:def 28
the carrier of it = {[[F1,F2],T] where F1,F2 is Functor of C1,C2,
T is natural_transformation of F1,F2: F1 is covariant & F2 is covariant
& F1 is_naturally_transformable_to F2} &
the composition of it = {[[x2,x1],x3] where x1,x2,x3 is
Element of the carrier of it: ex F1,F2,F3 being Functor of C1,C2,
T1 being natural_transformation of F1,F2,
T2 being natural_transformation of F2,F3 st x1 = [[F1,F2],T1] &
x2 = [[F2,F3],T2] & x3 = [[F1,F3],T2`*`T1]};
end;
registration
let C1 be non empty category;
let C2 be empty category;
cluster Functors(C1,C2) -> empty;
end;
registration
let C1 be empty category;
let C2 be category;
cluster Functors(C1,C2) -> non empty trivial;
end;
registration
let C1 be non empty category;
let C2 be non empty category;
cluster Functors(C1,C2) -> non empty;
end;
theorem :: CAT_8:63
for C1,C2 being non empty category, f1,f2 being morphism of Functors(C1,C2)
holds f1 |> f2 iff ex F,F1,F2 being covariant Functor of C1,C2,
T1 being natural_transformation of F1,F,
T2 being natural_transformation of F,F2 st
f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1(*)f2 = [[F1,F2],T2`*`T1] &
for g1,g2 being morphism of C1 st g2 |> g1 holds T2.g2 |> T1.g1 &
(T2`*`T1).(g2(*)g1) = (T2.g2)(*)(T1.g1);
theorem :: CAT_8:64
for C1,C2 being non empty category, f being morphism of Functors(C1,C2) holds
f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F];
theorem :: CAT_8:65
for C1,C2 being non empty category, f being morphism of Functors(C1,C2) holds
ex F1,F2 being covariant Functor of C1,C2,
T being natural_transformation of F1,F2 st f = [[F1,F2],T] &
dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2];
begin :: Exponential Objects
definition
let C be with_binary_products non empty category;
let a,b,c be Object of C;
let e be Morphism of c [x] a, b such that Hom(c [x] a, b)<>{};
pred c,e is_exponent_of a,b means
:: CAT_8:def 29
for d being Object of C, f being Morphism of d [x] a,b st Hom(d [x] a,b)<>{}
holds Hom(d,c)<>{} & ex h being Morphism of d,c st f = e * (h [x] id- a) &
for h1 being Morphism of d,c st f = e * (h1 [x] id- a) holds h = h1;
end;
theorem :: CAT_8:66
for C being with_binary_products category,
a1,a2,b1,b2,c1,c2 being Object of C, f1 being Morphism of a1,b1,
f2 being Morphism of a2,b2, g1 being Morphism of b1,c1,
g2 being Morphism of b2,c2
st Hom(a1,b1)<>{} & Hom(b1,c1)<>{} & Hom(a2,b2)<>{} & Hom(b2,c2)<>{}
holds (g1 [x] g2) * (f1 [x] f2) = (g1*f1) [x] (g2*f2);
theorem :: CAT_8:67
for C being with_binary_products non empty category, a,b being Object of C
holds id- a [x] id- b = id-(a [x] b);
theorem :: CAT_8:68
for C being with_binary_products non empty category,
a,b,c1,c2 being Object of C,
e1 being Morphism of c1 [x] a, b, e2 being Morphism of c2 [x] a, b
st Hom(c1 [x] a, b)<>{} & Hom(c2 [x] a, b)<>{} & c1,e1 is_exponent_of a,b &
c2,e2 is_exponent_of a,b holds c1,c2 are_isomorphic;
definition
let C be with_binary_products non empty category;
attr C is with_exponential_objects means
:: CAT_8:def 30
for a,b being Object of C holds ex c being Object of C,
e being Morphism of c [x] a,b st Hom(c [x] a, b)<>{} &
c,e is_exponent_of a,b;
end;
registration
cluster OrdC 1 -> with_binary_products;
end;
theorem :: CAT_8:69
OrdC 1 is with_exponential_objects;
registration
cluster with_exponential_objects for with_binary_products non empty category;
end;
definition
let C be with_exponential_objects with_binary_products non empty category;
let a,b be Object of C;
mode categorical_exponent of a,b -> pair object means
:: CAT_8:def 31
ex c being Object of C, e being Morphism of c [x] a,b st it = [c,e] &
Hom(c [x] a, b)<>{} & c,e is_exponent_of a,b;
end;
definition
let C be with_exponential_objects with_binary_products non empty category;
let a,b be Object of C;
func b |^ a -> Object of C equals
:: CAT_8:def 32
(the categorical_exponent of a,b)`1;
end;
definition
let C be with_exponential_objects with_binary_products non empty category;
let a,b be Object of C;
func eval(a,b) -> Morphism of b|^a [x] a, b equals
:: CAT_8:def 33
(the categorical_exponent of a,b)`2;
end;
theorem :: CAT_8:70
for C being with_exponential_objects with_binary_products non empty category,
a,b being Object of C holds Hom(b|^a [x] a, b)<>{} &
b|^a,eval(a,b) is_exponent_of a,b;
theorem :: CAT_8:71
for C being with_exponential_objects with_binary_products non empty category,
a,b,c being Object of C st Hom(c [x] a,b) <> {}
holds
ex L being Function of Hom(c [x] a,b), Hom(c,b|^a) st
(for f being Morphism of c [x] a,b, h being Morphism of c,b|^a st h = L.f
holds eval(a,b) * (h [x] id- a) = f) & L is bijective;
definition
let A,B,C be category;
let E be Functor of C [x] A, B such that E is covariant;
pred C,E is_exponent_of A,B means
:: CAT_8:def 34
for D being category, F being Functor of D [x] A, B st F is covariant holds
ex H being Functor of D,C st H is covariant & F = E (*)(H [x] id A) &
for H1 being Functor of D,C st H1 is covariant & F = E (*)(H1 [x] id A)
holds H = H1;
end;
definition
let C1,C2 be category;
mode categorical_exponent of C1,C2 -> pair object means
:: CAT_8:def 35
ex C being category, E being Functor of C [x] C1,C2 st
it = [C,E] & E is covariant & C,E is_exponent_of C1,C2;
end;
definition
let C1,C2 be category;
func C2 |^ C1 -> category equals
:: CAT_8:def 36
(the categorical_exponent of C1,C2)`1;
end;
definition
let C1,C2 be category;
func eval(C1,C2) -> Functor of C2|^C1 [x] C1, C2 equals
:: CAT_8:def 37
(the categorical_exponent of C1,C2)`2;
end;
theorem :: CAT_8:72
for C1,C2 being category holds C2|^C1,eval(C1,C2) is_exponent_of C1,C2;
theorem :: CAT_8:73
for A,B,C1,C2 being category, E1 being Functor of C1 [x] A,B,
E2 being Functor of C2 [x] A,B st E1 is covariant & E2 is covariant &
C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds C1 ~= C2;
registration
let C1,C2 be category;
cluster eval(C1,C2) -> covariant;
end;
registration
let C1 be non empty category;
let C2 be empty category;
cluster C2|^C1 -> empty;
end;
registration
let C1 be empty category;
let C2 be category;
cluster C2|^C1 -> non empty trivial;
end;
registration
let C1 be non empty category;
let C2 be non empty category;
cluster C2|^C1 -> non empty;
end;
theorem :: CAT_8:74
for C1,C2 being category holds Functors(C1,C2) ~= C2|^C1;