:: Some Isomorphisms Between Functor Categories
:: by Andrzej Trybulec
::
:: Received June 5, 1992
:: Copyright (c) 1992-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, FUNCT_1, FUNCT_2, FUNCT_5, ZFMISC_1, RELAT_1, TARSKI,
SUBSET_1, MCART_1, CAT_1, GRAPH_1, NATTRA_1, STRUCT_0, CAT_2, FINSEQ_2,
PZFMISC1, FUNCOP_1, PARTFUN1, BORSUK_1, ISOCAT_2, MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCOP_1, BINOP_1, FUNCT_3, FUNCT_2, FUNCT_5, STRUCT_0,
GRAPH_1, CAT_1, CAT_2, CAT_3, NATTRA_1, ISOCAT_1;
constructors DOMAIN_1, ISOCAT_1, FUNCOP_1, RELSET_1, CAT_3, RELAT_2, FUNCT_5,
FUNCT_4;
registrations XBOOLE_0, RELSET_1, FUNCT_2, STRUCT_0, CAT_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
definition
let A,B,C be non empty set;
let f be Function of A, Funcs(B,C);
redefine func uncurry f -> Function of [:A,B:],C;
end;
theorem :: ISOCAT_2:1
for A,B,C being non empty set, f being Function of A,Funcs(B,C)
holds curry uncurry f = f;
theorem :: ISOCAT_2:2
for A,B,C being non empty set, f being Function of A, Funcs(B,C)
for a being Element of A, b being Element of B
holds (uncurry f).(a,b) = f.a.b;
::$CT 2
:: Auxiliary category theory facts
reserve A,B,C for Category,
F,F1 for Functor of A,B;
theorem :: ISOCAT_2:5
for f being Morphism of A holds (id cod f)(*)f = f;
theorem :: ISOCAT_2:6
for f being Morphism of A holds f(*)(id dom f) = f;
reserve o,m for set;
reserve t for natural_transformation of F,F1;
theorem :: ISOCAT_2:7
o is Object of Functors(A,B) iff o is Functor of A,B;
theorem :: ISOCAT_2:8
for f being Morphism of Functors(A,B) ex F1,F2 being Functor of A
,B, t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to
F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t];
begin :: The isomorphism between A^1 and A
definition
let A,B;
let a be Object of A;
func a |-> B -> Functor of Functors(A,B), B means
:: ISOCAT_2:def 1
for F1,F2 being Functor of A,B, t being natural_transformation of F1,F2 st F1
is_naturally_transformable_to F2 holds it.[[F1,F2],t] = t.a;
end;
theorem :: ISOCAT_2:9
Functors(1Cat(o,m),A) ~= A;
begin :: The isomorphism between C^(A x B) and C^(A^B)
theorem :: ISOCAT_2:10
for F being Functor of [:A,B:],C, a being Object of A, b being
Object of B holds (F?-a).b = F.[a,b];
theorem :: ISOCAT_2:11
for a1,a2 being Object of A, b1,b2 being Object of B holds Hom(
a1,a2) <> {} & Hom(b1,b2) <> {} iff Hom([a1,b1],[a2,b2]) <> {};
theorem :: ISOCAT_2:12
for a1,a2 being Object of A, b1,b2 being Object of B st Hom([a1,
b1],[a2,b2]) <> {} for f being (Morphism of A), g being Morphism of B holds [f,
g] is Morphism of [a1,b1],[a2,b2] iff f is Morphism of a1,a2 & g is Morphism of
b1,b2;
theorem :: ISOCAT_2:13
for F1,F2 being Functor of [:A,B:],C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2, a
being Object of A holds F1?-a is_naturally_transformable_to F2?-a & (curry t).a
is natural_transformation of F1?-a,F2?-a;
definition
let A,B,C;
let F be Functor of [:A,B:],C;
let f be Morphism of A;
func curry(F,f) -> Function of the carrier' of B,the carrier' of C equals
:: ISOCAT_2:def 2
(
curry F).f;
end;
theorem :: ISOCAT_2:14
for a1,a2 being Object of A, b1,b2 being Object of B, f being (
Morphism of A), g being Morphism of B st f in Hom(a1,a2) & g in Hom(b1,b2)
holds [f,g] in Hom([a1,b1],[a2,b2]);
theorem :: ISOCAT_2:15
for F being Functor of [:A,B:], C for a,b being Object of A st
Hom(a,b) <> {} for f being Morphism of a,b holds F?-a
is_naturally_transformable_to F?-b & curry(F,f)*IdMap B is
natural_transformation of F?-a,F?-b;
definition
let A,B,C;
let F be Functor of [:A,B:],C;
let f be Morphism of A;
func F?-f -> natural_transformation of F?-dom f, F?-cod f equals
:: ISOCAT_2:def 3
curry(F,f)*
IdMap B;
end;
theorem :: ISOCAT_2:16
for F being Functor of [:A,B:],C, g being Morphism of A holds F
?-dom(g) is_naturally_transformable_to F?-cod(g);
theorem :: ISOCAT_2:17
for F being Functor of [:A,B:],C, f being (Morphism of A), b
being Object of B holds (F?-f).b = F.(f, id b);
theorem :: ISOCAT_2:18
for F being Functor of [:A,B:],C, a being Object of A holds id(F
?-a) = F?-id a;
theorem :: ISOCAT_2:19
for F being Functor of [:A,B:],C, g,f being Morphism of A st dom
g = cod f for t being natural_transformation of F?-dom f, F?-dom g st t = F?-f
holds F?-(g(*)f) = (F?-g)`*`t;
definition
let A,B,C;
let F be Functor of [:A,B:],C;
func export F -> Functor of A, Functors(B,C) means
:: ISOCAT_2:def 4
for f being Morphism of A holds it.f =[[F?-dom f,F?-cod f],F?-f];
end;
theorem :: ISOCAT_2:20
for F being Functor of [:A,B:],C, a being Object of A holds (
export F).a = F?-a;
theorem :: ISOCAT_2:21
for F being Functor of [:A,B:],C, a being Object of A holds (
export F).a is Functor of B,C;
theorem :: ISOCAT_2:22
for F1,F2 being Functor of [:A,B:],C holds export F1 = export F2
implies F1 = F2;
theorem :: ISOCAT_2:23
for F1,F2 being Functor of [:A,B:], C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds export F1 is_naturally_transformable_to export F2 & ex G being
natural_transformation of export F1, export F2 st for s being Function of [:the
carrier of A, the carrier of B:], the carrier' of C st t = s for a being Object
of A holds G.a = [[(export F1).a,(export F2).a],(curry s).a];
definition
let A,B,C;
let F1,F2 be Functor of [:A,B:],C such that
F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
func export t -> natural_transformation of export F1, export F2 means
:: ISOCAT_2:def 5
for s being Function of [:the carrier of A, the carrier of B:], the carrier' of
C st t = s for a being Object of A holds it.a = [[(export F1).a,(export F2).a],
(curry s).a];
end;
theorem :: ISOCAT_2:24
for F being Functor of [:A,B:],C holds id export F = export id F;
theorem :: ISOCAT_2:25
for F1,F2,F3 being Functor of [:A,B:],C st F1
is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 for t1
being natural_transformation of F1,F2, t2 being natural_transformation of F2,F3
holds export(t2`*`t1) = (export t2)`*`(export t1);
theorem :: ISOCAT_2:26
for F1,F2 being Functor of [:A,B:],C st F1
is_naturally_transformable_to F2 for t1,t2 being natural_transformation of F1,
F2 holds export t1 = export t2 implies t1 = t2;
theorem :: ISOCAT_2:27
for G being Functor of A, Functors(B,C) ex F being Functor of [:
A,B:],C st G = export F;
theorem :: ISOCAT_2:28
for F1,F2 being Functor of [:A,B:],C st export F1
is_naturally_transformable_to export F2 for t being natural_transformation of
export F1, export F2 holds F1 is_naturally_transformable_to F2 & ex u being
natural_transformation of F1,F2 st t = export u;
definition
let A,B,C;
func export(A,B,C)-> Functor of Functors([:A,B:],C),Functors(A,Functors(B,C)
) means
:: ISOCAT_2:def 6
for F1,F2 being Functor of [:A,B:], C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds it.[[F1,F2],t] = [[export F1, export F2],export t];
end;
registration
let A,B,C;
cluster export(A,B,C) -> isomorphic;
end;
theorem :: ISOCAT_2:29
Functors([:A,B:],C) ~= Functors(A,Functors(B,C));
begin :: The isomorphism between (B x C)^A and B^A x C^A
theorem :: ISOCAT_2:30
for F1,F2 being Functor of A,B, G being Functor of B,C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds G*t = G*(t qua Function);
definition
let A,B,C;
let F be Functor of A,B, G be Functor of A,C;
redefine func <:F,G:> -> Functor of A, [:B,C:];
end;
definition
let A,B,C;
let F be Functor of A, [:B,C:];
func Pr1 F -> Functor of A,B equals
:: ISOCAT_2:def 7
pr1(B,C)*F;
func Pr2 F -> Functor of A,C equals
:: ISOCAT_2:def 8
pr2(B,C)*F;
end;
theorem :: ISOCAT_2:31
for F being Functor of A,B, G being Functor of A,C holds Pr1<:F,
G:> = F & Pr2<:F,G:> = G;
theorem :: ISOCAT_2:32
for F,G being Functor of A, [:B,C:] st Pr1 F = Pr1 G & Pr2 F =
Pr2 G holds F = G;
definition
let A,B,C;
let F1,F2 be Functor of A, [:B,C:];
let t be natural_transformation of F1,F2;
func Pr1 t -> natural_transformation of Pr1 F1, Pr1 F2 equals
:: ISOCAT_2:def 9
pr1(B,C)*t;
func Pr2 t -> natural_transformation of Pr2 F1, Pr2 F2 equals
:: ISOCAT_2:def 10
pr2(B,C)*t;
end;
theorem :: ISOCAT_2:33
for F1,F2,G1,G2 being Functor of A, [:B,C:] st F1
is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 for s
being natural_transformation of F1,F2, t being natural_transformation of G1,G2
st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds s = t;
theorem :: ISOCAT_2:34 :: poprawic na /. !!!
for F being Functor of A,B, G being Functor of A,C for a,b being
Object of A st Hom(a,b) <> {} for f being Morphism of a,b
holds <:F,G:>.f = [F.f,G.f];
theorem :: ISOCAT_2:35
for F being Functor of A,B, G being Functor of A,C for a being
Object of A holds <:F,G:>.a = [F.a,G.a];
theorem :: ISOCAT_2:36
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_transformable_to G1 & F2 is_transformable_to G2 holds <:F1,F2:>
is_transformable_to <:G1,G2:>;
definition
let A,B,C;
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
F1 is_transformable_to G1 & F2 is_transformable_to G2;
let t1 be transformation of F1,G1, t2 be transformation of F2,G2;
func <:t1,t2:> -> transformation of <:F1,F2:>,<:G1,G2:> equals
:: ISOCAT_2:def 11
<:t1,
t2:>;
end;
theorem :: ISOCAT_2:37
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_transformable_to G1 & F2 is_transformable_to G2 for t1 being transformation
of F1,G1, t2 being transformation of F2,G2 for a being Object of A holds <:t1,
t2:>.a = [t1.a,t2.a];
theorem :: ISOCAT_2:38
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds <:
F1,F2:> is_naturally_transformable_to <:G1,G2:>;
definition
let A,B,C;
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2;
let t1 be natural_transformation of F1,G1, t2 be natural_transformation of
F2,G2;
func <:t1,t2:> -> natural_transformation of <:F1,F2:>,<:G1,G2:> equals
:: ISOCAT_2:def 12
<:t1,t2:>;
end;
theorem :: ISOCAT_2:39
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 for t1
being natural_transformation of F1,G1, t2 being natural_transformation of F2,G2
holds Pr1<:t1,t2:> = t1 & Pr2<:t1,t2:> = t2;
definition
let A,B,C;
func distribute(A,B,C) -> Functor of Functors(A,[:B,C:]), [:Functors(A,B),
Functors(A,C):] means
:: ISOCAT_2:def 13
for F1,F2 being Functor of A,[:B,C:] st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds it.[[F1,F2],t] = [[[Pr1 F1, Pr1 F2],Pr1 t],[[Pr2 F1, Pr2 F2],Pr2 t]];
end;
registration
let A,B,C;
cluster distribute(A,B,C) -> isomorphic;
end;
theorem :: ISOCAT_2:40
Functors(A,[:B,C:]) ~= [:Functors(A,B),Functors(A,C):];