:: Natural Transformations. Discrete Categories :: by Andrzej Trybulec :: :: Received May 15, 1991 :: Copyright (c) 1991-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, SUBSET_1, RELAT_1, ZFMISC_1, PARTFUN1, FUNCT_4, REALSET1, TARSKI, CAT_1, GRAPH_1, STRUCT_0, CAT_2, MCART_1, PZFMISC1, ALGSTR_0, FUNCT_2, NATTRA_1, MONOID_0, RELAT_2, BINOP_1, ALTCAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, REALSET1, PARTFUN1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_4, STRUCT_0, GRAPH_1, CAT_1, CAT_2, CAT_3; constructors PARTFUN1, REALSET1, CAT_2, FUNCOP_1, RELSET_1, CAT_3, XTUPLE_0, FUNCT_4; registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, CAT_2, STRUCT_0, ZFMISC_1, RELAT_1, XTUPLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries reserve A,B,C for Category, F,F1,F2,F3 for Functor of A,B, G for Functor of B, C; reserve m,o for set; ::$CT 4 theorem :: NATTRA_1:5 for a being Object of A holds [[id a,id a],id a] in the Comp of A; theorem :: NATTRA_1:6 the Comp of 1Cat(o,m) = {[[m,m],m]}; theorem :: NATTRA_1:7 for a being Object of A holds 1Cat(a,id a) is Subcategory of A; theorem :: NATTRA_1:8 for C being Subcategory of A holds the Source of C = (the Source of A)|the carrier' of C & the Target of C = (the Target of A)|the carrier' of C & the Comp of C = (the Comp of A)||the carrier' of C; theorem :: NATTRA_1:9 for O being non empty Subset of the carrier of A, M being non empty Subset of the carrier' of A st for o being Element of A st o in O holds id o in M for DOM,COD being Function of M,O st DOM = (the Source of A) |M & COD = (the Target of A)|M for COMP being PartFunc of [:M,M qua non empty set:], M st COMP = (the Comp of A)||M holds CatStr(#O,M,DOM,COD,COMP#) is Subcategory of A; theorem :: NATTRA_1:10 for C being strict Category, A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds A = C; begin :: Application of a functor to a morphism definition ::$CD end; theorem :: NATTRA_1:11 for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a, b holds (G*F)/.f = G/.(F/.f); :: The following theorems are analogues of theorems from CAT_1, with :: the new concept of the application of a functor to a morphism theorem :: NATTRA_1:12 for F1,F2 being Functor of A,B st for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,b holds F1.f = F2.f holds F1 = F2; theorem :: NATTRA_1:13 for a,b,c being Object of A st Hom(a,b) <> {} & Hom(b,c) <> {} for f being Morphism of a,b, g being Morphism of b,c holds F/.(g*f) = (F/.g)*(F/.f); theorem :: NATTRA_1:14 for c being Object of A, d being Object of B st F/.(id c) = id d holds F.c = d; theorem :: NATTRA_1:15 for a being Object of A holds F/.id a = id (F.a); theorem :: NATTRA_1:16 for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a, b holds (id A)/.f = f; theorem :: NATTRA_1:17 for a,b,c,d being Object of A st Hom(a,b) meets Hom(c,d) holds a = c & b = d; begin :: Transformations definition let A,B,F1,F2; pred F1 is_transformable_to F2 means :: NATTRA_1:def 2 for a being Object of A holds Hom(F1.a,F2.a) <> {}; reflexivity; end; theorem :: NATTRA_1:18 F is_transformable_to F1 & F1 is_transformable_to F2 implies F is_transformable_to F2; definition let A,B,F1,F2; assume F1 is_transformable_to F2; mode transformation of F1,F2 -> Function of the carrier of A, the carrier' of B means :: NATTRA_1:def 3 for a being Object of A holds it.a is Morphism of F1.a,F2.a; end; definition let A,B; let F be Functor of A,B; func id F ->transformation of F,F means :: NATTRA_1:def 4 for a being Object of A holds it.a = id (F.a); end; definition let A,B,F1,F2; assume F1 is_transformable_to F2; let t be transformation of F1,F2; let a be Object of A; func t.a -> Morphism of F1.a, F2.a equals :: NATTRA_1:def 5 t.a; end; definition let A,B,F,F1,F2; assume that F is_transformable_to F1 and F1 is_transformable_to F2; let t1 be transformation of F,F1; let t2 be transformation of F1,F2; func t2`*`t1 -> transformation of F,F2 means :: NATTRA_1:def 6 for a being Object of A holds it.a = (t2.a)*(t1.a); end; theorem :: NATTRA_1:19 F1 is_transformable_to F2 implies for t1,t2 being transformation of F1,F2 st for a being Object of A holds t1.a = t2.a holds t1 = t2; theorem :: NATTRA_1:20 for a being Object of A holds id F.a = id(F.a); theorem :: NATTRA_1:21 F1 is_transformable_to F2 implies for t being transformation of F1,F2 holds (id F2)`*`t = t & t`*`(id F1) = t; theorem :: NATTRA_1:22 F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1, t2 being transformation of F1,F2, t3 being transformation of F2,F3 holds t3`*`t2`*`t1 = t3`*`(t2`*`t1); begin definition let A,B,F1,F2; pred F1 is_naturally_transformable_to F2 means :: NATTRA_1:def 7 F1 is_transformable_to F2 & ex t being transformation of F1,F2 st for a,b being Object of A st Hom(a,b ) <> {} for f being Morphism of a,b holds t.b*F1/.f = F2/.f*t.a; reflexivity; end; theorem :: NATTRA_1:23 F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2; definition let A,B,F1,F2; assume F1 is_naturally_transformable_to F2; mode natural_transformation of F1,F2 -> transformation of F1,F2 means :: NATTRA_1:def 8 for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,b holds it.b*F1/.f = F2/.f*it.a; end; definition let A,B,F; redefine func id F -> natural_transformation of F,F; end; definition let A,B,F,F1,F2 such that F is_naturally_transformable_to F1 and F1 is_naturally_transformable_to F2; let t1 be natural_transformation of F,F1; let t2 be natural_transformation of F1,F2; func t2`*`t1 -> natural_transformation of F,F2 equals :: NATTRA_1:def 9 t2`*`t1; end; theorem :: NATTRA_1:24 F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds (id F2)`*`t = t & t`*`(id F1) = t; reserve t for natural_transformation of F,F1, t1 for natural_transformation of F1,F2; theorem :: NATTRA_1:25 F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies for t1 being natural_transformation of F,F1 for t2 being natural_transformation of F1,F2 for a being Object of A holds (t2`*`t1).a = (t2.a)*(t1.a); theorem :: NATTRA_1:26 F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds t3`*`t1`*`t = t3`*`(t1`*`t); :: Natural equivalences definition let A,B,F1,F2; let IT be transformation of F1,F2; attr IT is invertible means :: NATTRA_1:def 10 for a being Object of A holds IT.a is invertible; end; definition let A,B,F1,F2; pred F1,F2 are_naturally_equivalent means :: NATTRA_1:def 11 F1 is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2 st t is invertible; reflexivity; end; notation let A,B,F1,F2; synonym F1 ~= F2 for F1,F2 are_naturally_equivalent; end; definition let A,B,F1,F2 such that F1 is_transformable_to F2; let t1 be transformation of F1,F2 such that t1 is invertible; func t1" -> transformation of F2,F1 means :: NATTRA_1:def 12 for a being Object of A holds it.a = (t1.a)"; end; definition let A,B,F1,F2,t1 such that F1 is_naturally_transformable_to F2 and t1 is invertible; func t1" -> natural_transformation of F2,F1 equals :: NATTRA_1:def 13 (t1 qua transformation of F1,F2)"; end; theorem :: NATTRA_1:27 for A,B,F1,F2,t1 st F1 is_naturally_transformable_to F2 & t1 is invertible for a being Object of A holds t1".a = (t1.a)"; theorem :: NATTRA_1:28 F1 ~= F2 implies F2 ~= F1; theorem :: NATTRA_1:29 F1 ~= F2 & F2 ~= F3 implies F1 ~= F3; definition let A,B,F1,F2; assume F1,F2 are_naturally_equivalent; mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means :: NATTRA_1:def 14 it is invertible; end; theorem :: NATTRA_1:30 id F is natural_equivalence of F,F; theorem :: NATTRA_1:31 F1 ~= F2 & F2 ~= F3 implies for t being natural_equivalence of F1,F2, t9 being natural_equivalence of F2,F3 holds t9`*`t is natural_equivalence of F1 ,F3; begin :: Functor category definition let A,B; mode NatTrans-DOMAIN of A,B -> non empty set means :: NATTRA_1:def 15 for x being set holds x in it implies ex F1,F2 being Functor of A,B, t being natural_transformation of F1,F2 st x = [[F1,F2],t] & F1 is_naturally_transformable_to F2; end; definition let A,B; func NatTrans(A,B) -> NatTrans-DOMAIN of A,B means :: NATTRA_1:def 16 for x being set holds x in it iff ex F1,F2 being Functor of A,B, t being natural_transformation of F1,F2 st x = [[F1,F2],t] & F1 is_naturally_transformable_to F2; end; theorem :: NATTRA_1:32 F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B); definition let A,B; func Functors(A,B) -> strict Category means :: NATTRA_1:def 17 the carrier of it = Funct(A,B) & the carrier' of it = NatTrans(A,B) & (for f being Morphism of it holds dom f = f`1`1 & cod f = f`1`2) & (for f,g being Morphism of it st dom g = cod f holds [g,f] in dom the Comp of it) & (for f,g being Morphism of it st [g, f] in dom (the Comp of it) ex F,F1,F2,t,t1 st f = [[F,F1],t] & g = [[F1,F2],t1] & (the Comp of it).[g,f] = [[F,F2],t1`*`t]) & for a being Object of it, F st F = a holds id a = [[F,F],id F]; end; :: As immediate consequences of the definition we get theorem :: NATTRA_1:33 for f being Morphism of Functors(A,B) st f = [[F,F1],t] holds dom f = F & cod f = F1; theorem :: NATTRA_1:34 for a,b being Object of Functors(A,B), f being Morphism of a,b st Hom( a,b) <> {} ex F,F1,t st a = F & b = F1 & f = [[F,F1],t]; theorem :: NATTRA_1:35 for t9 being natural_transformation of F2,F3 for f,g being Morphism of Functors(A,B) st f = [[F,F1],t] & g = [[F2,F3],t9] holds [g,f] in dom the Comp of Functors(A,B) iff F1 = F2; theorem :: NATTRA_1:36 for f,g being Morphism of Functors(A,B) st f = [[F,F1],t] & g = [[F1, F2],t1] holds g(*)f = [[F,F2],t1`*`t]; begin :: Discrete categories definition let C be Category; attr C is quasi-discrete means :: NATTRA_1:def 18 for a,b being Element of C st Hom(a,b)<>{} holds a=b; attr C is pseudo-discrete means :: NATTRA_1:def 19 for a being Element of C holds Hom(a,a) is trivial; end; reserve a,b for Element of C; definition let C be Category; attr C is discrete means :: NATTRA_1:def 20 C is quasi-discrete pseudo-discrete; end; registration cluster discrete -> quasi-discrete pseudo-discrete for Category; cluster quasi-discrete pseudo-discrete -> discrete for Category; end; registration let o,m be set; cluster 1Cat(o,m) -> discrete; end; registration cluster discrete for Category; end; registration let C be discrete Category; let a be Element of C; cluster Hom(a,a) -> trivial; end; theorem :: NATTRA_1:37 for A being discrete Category, a being Object of A holds Hom(a,a ) = { id a}; registration let A be discrete Category; cluster -> discrete for Subcategory of A; end; registration let A,B be discrete Category; cluster [:A,B:] -> discrete; end; ::$CT 3 theorem :: NATTRA_1:41 for A being discrete Category, B being Category, F1,F2 being Functor of B,A st F1 is_transformable_to F2 holds F1 = F2; theorem :: NATTRA_1:42 for A being discrete Category, B being Category, F being Functor of B,A, t being transformation of F,F holds t = id F; registration let B be Category, A be discrete Category; cluster Functors(B,A) -> discrete; end; registration let C be Category; cluster strict discrete for Subcategory of C; end; definition let C; func IdCat(C) -> strict Subcategory of C means :: NATTRA_1:def 21 the carrier of it = the carrier of C & the carrier' of it = the set of all id a where a is Object of C; end; registration let C; cluster IdCat C -> discrete; end; registration cluster strict discrete for Category; end; registration let C be strict discrete Category; reduce IdCat C to C; end; ::$CT 4 theorem :: NATTRA_1:47 IdCat([:A,B:]) = [:IdCat(A), IdCat(B):];