:: Some Isomorphisms Between Functor Categories :: by Andrzej Trybulec :: :: Received June 5, 1992 :: Copyright (c) 1992-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 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):];