:: Introduction to Categories and Functors :: by Czes{\l}aw Byli\'nski :: :: Received October 25, 1989 :: Copyright (c) 1990-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 GRAPH_1, STRUCT_0, FUNCT_1, PARTFUN1, ZFMISC_1, SUBSET_1, XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1, TARSKI, ALGSTR_0, WELLORD1, CAT_1, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, BINOP_1, FUNCOP_1, STRUCT_0, GRAPH_1; constructors PARTFUN1, WELLORD2, BINOP_1, PBOOLE, GRAPH_1, RELSET_1, NUMBERS; registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, RELAT_1, ZFMISC_1; requirements SUBSET, BOOLE; begin :: Structure of a Category definition struct(MultiGraphStruct) CatStr (# carrier,carrier' -> set, Source,Target -> Function of the carrier', the carrier, Comp -> PartFunc of [:the carrier', the carrier' :],the carrier' #); end; reserve C for CatStr; definition let C; mode Object of C is Element of C; mode Morphism of C is Element of the carrier' of C; end; reserve f,g for Morphism of C; :: Domain and codomain of a Morphism registration cluster non void non empty for CatStr; end; definition let C,f,g; assume [g,f] in dom(the Comp of C); func g(*)f -> Morphism of C equals :: CAT_1:def 1 ( the Comp of C ).(g,f); end; definition ::$CD 2 let C be non void non empty CatStr, a,b be Object of C; func Hom(a,b) -> Subset of the carrier' of C equals :: CAT_1:def 4 {f where f is Morphism of C : dom f = a & cod f = b}; end; reserve C for non void non empty CatStr, f,g for Morphism of C, a,b,c,d for Object of C; theorem :: CAT_1:1 f in Hom(a,b) iff dom(f)=a & cod(f)=b; theorem :: CAT_1:2 Hom(dom(f),cod(f)) <> {}; definition let C,a,b; assume Hom(a,b)<>{}; mode Morphism of a,b -> Morphism of C means :: CAT_1:def 5 it in Hom(a,b); end; ::$CT theorem :: CAT_1:4 for f being Morphism of C holds f is Morphism of dom(f),cod(f); theorem :: CAT_1:5 for f being Morphism of a,b st Hom(a,b) <> {} holds dom(f) = a & cod(f) = b; theorem :: CAT_1:6 for f being Morphism of a,b for h being Morphism of c,d st Hom(a,b) <> {} & Hom(c,d) <> {} & f = h holds a = c & b = d; theorem :: CAT_1:7 for f being Morphism of a,b st Hom(a,b) = {f} for g being Morphism of a,b holds f = g; theorem :: CAT_1:8 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_1:9 for f being Morphism of a,b st Hom(a,b),Hom(c,d) are_equipotent & Hom( a,b) = {f} holds ex h being Morphism of c,d st Hom(c,d) = {h}; :: Category definition let C be non empty non void CatStr; attr C is Category-like means :: CAT_1:def 6 for f,g being Morphism of C holds [g,f] in dom(the Comp of C) iff dom g = cod f; attr C is transitive means :: CAT_1:def 7 for f,g being Morphism of C st dom g = cod f holds dom(g(*)f) = dom f & cod(g(*)f) = cod g; attr C is associative means :: CAT_1:def 8 for f,g,h being Morphism of C st dom h = cod g & dom g = cod f holds h(*)(g(*)f) = (h(*)g)(*)f; attr C is reflexive means :: CAT_1:def 9 for b being Element of C holds Hom(b,b) <> {}; attr C is with_identities means :: CAT_1:def 10 for a being Element of C ex i being Morphism of a,a st for b being Element of C holds (Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) & (Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f); end; definition let o,m be object; func 1Cat(o,m) -> strict CatStr equals :: CAT_1:def 11 CatStr(# {o},{m},m:->o,m:->o,(m,m):->m #); end; registration let o,m be object; cluster 1Cat(o,m) -> non empty trivial non void trivial'; end; registration cluster non empty trivial -> transitive reflexive for non empty non void CatStr; end; registration cluster non void trivial' -> associative with_identities for non empty non void CatStr; end; registration let o,m be object; cluster 1Cat(o,m) -> Category-like; end; registration cluster reflexive transitive associative with_identities Category-like non void non empty strict for non empty non void CatStr; end; definition mode Category is reflexive transitive associative with_identities Category-like non void non empty CatStr; end; registration let C be reflexive non void non empty CatStr, a be Object of C; cluster Hom(a,a) -> non empty; end; ::$CT reserve o,m for set; theorem :: CAT_1:11 for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m) holds f in Hom(a,b); theorem :: CAT_1:12 for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m) holds f is Morphism of a,b; theorem :: CAT_1:13 for a,b being Object of 1Cat(o,m) holds Hom(a,b) <> {}; theorem :: CAT_1:14 for a,b,c,d being Object of 1Cat(o,m) for f being Morphism of a,b for g being Morphism of c,d holds f=g; reserve B,C,D for Category; reserve a,b,c,d for Object of C; reserve f,f1,f2,g,g1,g2 for Morphism of C; theorem :: CAT_1:15 dom(g) = cod(f) iff [g,f] in dom(the Comp of C); theorem :: CAT_1:16 dom(g) = cod(f) implies g(*)f = ( the Comp of C ).(g,f); theorem :: CAT_1:17 for f,g being Morphism of C st dom(g) = cod(f) holds dom(g(*)f) = dom(f) & cod(g(*)f) = cod(g); theorem :: CAT_1:18 for f,g,h being Morphism of C st dom(h) = cod(g) & dom(g) = cod( f) holds h(*)(g(*)f) = (h(*)g)(*)f; definition let C be with_identities reflexive non void non empty CatStr, a be Object of C; func id a -> Morphism of a,a means :: CAT_1:def 12 for b being Object of C holds (Hom(a,b) <> {} implies for f being Morphism of a,b holds f(*)it = f) & (Hom(b,a) <> {} implies for f being Morphism of b,a holds it(*)f = f); end; ::$CT 2 theorem :: CAT_1:21 for f being Morphism of C st cod(f) = b holds (id b)(*)f = f; theorem :: CAT_1:22 for g being Morphism of C st dom(g) = b holds g(*)(id b) = g; reserve f,f1,f2 for Morphism of a,b; reserve f9 for Morphism of b,a; reserve g for Morphism of b,c; reserve h,h1,h2 for Morphism of c,d; theorem :: CAT_1:23 Hom(a,b)<>{} & Hom(b,c)<>{} implies g(*)f in Hom(a,c); definition let C,a,b,c,f,g; assume Hom(a,b)<>{} & Hom(b,c)<>{}; func g*f -> Morphism of a,c equals :: CAT_1:def 13 g(*)f; end; theorem :: CAT_1:24 Hom(a,b)<>{} & Hom(b,c)<>{} implies Hom(a,c)<>{}; theorem :: CAT_1:25 Hom(a,b)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} implies (h*g)*f=h*(g* f); ::$CT theorem :: CAT_1:27 id a in Hom(a,a); theorem :: CAT_1:28 Hom(a,b)<>{} implies (id b)*f=f; theorem :: CAT_1:29 Hom(b,c)<>{} implies g*(id b)=g; registration let C,a; let f be Morphism of a,a; reduce f*id a to f; reduce (id a)*f to f; end; theorem :: CAT_1:30 (id a)*(id a) = id a; :: Monics, Epis definition let C be Category, b,c be Object of C, g be Morphism of b,c; attr g is monic means :: CAT_1:def 14 Hom(b,c) <> {} & for a being Object of C st Hom(a,b) <> {} for f1,f2 being Morphism of a,b st g*f1=g*f2 holds f1=f2; end; definition let C be Category, a,b be Object of C, f be Morphism of a,b; attr f is epi means :: CAT_1:def 15 Hom(a,b) <> {} & for c being Object of C st Hom(b,c) <> {} for g1,g2 being Morphism of b,c st g1*f=g2*f holds g1=g2; end; definition let C be Category, a,b be Object of C, f be Morphism of a,b; attr f is invertible means :: CAT_1:def 16 Hom(a,b) <> {} & Hom(b,a) <> {} & ex g being Morphism of b,a st f*g = id b & g*f = id a; end; theorem :: CAT_1:31 Hom(b,c) <> {} implies (g is monic iff for a for f1,f2 being Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2); theorem :: CAT_1:32 g is monic & h is monic implies h*g is monic; theorem :: CAT_1:33 Hom(b,c)<>{} & Hom(c,d)<>{} & h*g is monic implies g is monic; theorem :: CAT_1:34 for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <> {} & Hom(b,a) <> {} & h*g = id b holds g is monic; theorem :: CAT_1:35 id b is monic; theorem :: CAT_1:36 Hom(a,b) <> {} implies (f is epi iff for c for g1,g2 being Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2); theorem :: CAT_1:37 f is epi & g is epi implies g*f is epi; theorem :: CAT_1:38 Hom(a,b)<>{} & Hom(b,c)<>{} & g*f is epi implies g is epi; theorem :: CAT_1:39 for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <> {} & Hom(b,a) <> {} & h*g = id b holds h is epi; theorem :: CAT_1:40 id b is epi; theorem :: CAT_1:41 Hom(a,b) <> {} implies (f is invertible iff Hom(b,a)<>{} & ex g being Morphism of b,a st f*g=id b & g*f=id a); theorem :: CAT_1:42 Hom(a,b) <> {} & Hom(b,a) <> {} implies for g1,g2 being Morphism of b,a st f*g1=id b & g2*f=id a holds g1=g2; definition let C,a,b,f; assume that f is invertible; func f" -> Morphism of b,a means :: CAT_1:def 17 f*it = id b & it*f = id a; end; theorem :: CAT_1:43 f is invertible implies f is monic & f is epi; theorem :: CAT_1:44 id a is invertible; theorem :: CAT_1:45 f is invertible & g is invertible implies g*f is invertible; theorem :: CAT_1:46 f is invertible implies f" is invertible; theorem :: CAT_1:47 f is invertible & g is invertible implies (g*f)" = f"*g"; definition let C,a; attr a is terminal means :: CAT_1:def 18 Hom(b,a)<>{} & ex f being Morphism of b,a st for g being Morphism of b,a holds f=g; attr a is initial means :: CAT_1:def 19 Hom(a,b)<>{} & ex f being Morphism of a,b st for g being Morphism of a,b holds f=g; let b; pred a,b are_isomorphic means :: CAT_1:def 20 ex f st f is invertible; reflexivity; symmetry; end; theorem :: CAT_1:48 a,b are_isomorphic iff Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f9 st f*f9 = id b & f9*f = id a; theorem :: CAT_1:49 a is initial iff for b ex f being Morphism of a,b st Hom(a,b) = {f}; theorem :: CAT_1:50 a is initial implies for h being Morphism of a,a holds id a = h; theorem :: CAT_1:51 a is initial & b is initial implies a,b are_isomorphic; theorem :: CAT_1:52 a is initial & a,b are_isomorphic implies b is initial; theorem :: CAT_1:53 b is terminal iff for a ex f being Morphism of a,b st Hom(a,b) = {f}; theorem :: CAT_1:54 a is terminal implies for h being Morphism of a,a holds id a = h; theorem :: CAT_1:55 a is terminal & b is terminal implies a,b are_isomorphic; theorem :: CAT_1:56 b is terminal & a,b are_isomorphic implies a is terminal; theorem :: CAT_1:57 Hom(a,b) <> {} & a is terminal implies f is monic; registration let C,a; reduce dom id a to a; reduce cod id a to a; end; theorem :: CAT_1:58 dom id a = a & cod id a =a; theorem :: CAT_1:59 id a = id b implies a = b; theorem :: CAT_1:60 a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic; :: Functors (Covariant Functors) definition let C,D; mode Functor of C,D -> Function of the carrier' of C,the carrier' of D means :: CAT_1:def 21 (for c being Element of C ex d being Element of D st it.id c = id d ) & (for f being Element of the carrier' of C holds it.(id dom f) = id dom(it.f) & it.(id cod f) = id cod(it.f)) & for f,g being Element of the carrier' of C st [g,f] in dom(the Comp of C) holds it.(g(*)f) = (it.g)(*)(it.f); end; theorem :: CAT_1:61 for T being Function of the carrier' of C,the carrier' of D st (for c being Object of C ex d being Object of D st T.(id c) = id d) & (for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f)) & (for f,g being Morphism of C st dom g = cod f holds T.(g(*)f) = (T.g)(*)(T.f)) holds T is Functor of C,D; theorem :: CAT_1:62 for T being Functor of C,D for c being Object of C ex d being Object of D st T.(id c) = id d; theorem :: CAT_1:63 for T being Functor of C,D for f being Morphism of C holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f); theorem :: CAT_1:64 for T being Functor of C,D for f,g being Morphism of C st dom g = cod f holds dom(T.g) = cod(T.f) & T.(g(*)f) = (T.g)(*)(T.f); theorem :: CAT_1:65 for T being Function of the carrier' of C,the carrier' of D for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T.(id c) = id(F.c) ) & ( for f being Morphism of C holds F.(dom f) = dom (T.f) & F.(cod f) = cod (T.f) ) & ( for f,g being Morphism of C st dom g = cod f holds T.(g(*)f) = (T.g)(*)(T.f)) holds T is Functor of C,D; :: Object Function of a Functor definition let C,D; let F be Function of the carrier' of C,the carrier' of D; assume for c being Element of C ex d being Element of D st F.id c = id d; func Obj(F) -> Function of the carrier of C,the carrier of D means :: CAT_1:def 22 for c being Element of C for d being Element of D st F.id c = id d holds it.c = d; end; theorem :: CAT_1:66 for T being Function of the carrier' of C,the carrier' of D st for c being Object of C ex d being Object of D st T.(id c) = id d for c being Object of C for d being Object of D st T.(id c) = id d holds (Obj T).c = d; theorem :: CAT_1:67 for T being Functor of C,D for c being Object of C for d being Object of D st T.(id c) = id d holds (Obj T).c = d; theorem :: CAT_1:68 for T being (Functor of C,D),c being Object of C holds T.(id c) = id((Obj T).c); theorem :: CAT_1:69 for T being (Functor of C,D), f being Morphism of C holds (Obj T).(dom f) = dom (T.f) & (Obj T).(cod f) = cod (T.f); definition let C,D be Category; let T be Functor of C,D; let c be Object of C; func T.c -> Object of D equals :: CAT_1:def 23 (Obj T).c; end; theorem :: CAT_1:70 for T being Functor of C,D for c being Object of C for d being Object of D st T.(id c) = id d holds T.c = d; theorem :: CAT_1:71 for T being (Functor of C, D),c being Object of C holds T.(id c) = id( T.c); theorem :: CAT_1:72 for T being (Functor of C, D), f being Morphism of C holds T.(dom f) = dom (T.f) & T.(cod f) = cod (T.f); theorem :: CAT_1:73 for T being Functor of B,C for S being Functor of C,D holds S*T is Functor of B,D; :: Composition of Functors definition let B,C,D; let T be Functor of B,C; let S be Functor of C,D; redefine func S*T -> Functor of B,D; end; theorem :: CAT_1:74 id the carrier' of C is Functor of C,C; theorem :: CAT_1:75 for T being (Functor of B,C),S being (Functor of C,D),b being Object of B holds (Obj (S*T)).b = (Obj S).((Obj T).b); theorem :: CAT_1:76 for T being Functor of B,C for S being Functor of C,D for b being Object of B holds (S*T).b = S.(T.b); :: Identity Functor definition let C; func id C -> Functor of C,C equals :: CAT_1:def 24 id the carrier' of C; end; theorem :: CAT_1:77 for c being Object of C holds (Obj id C).c = c; theorem :: CAT_1:78 Obj id C = id the carrier of C; theorem :: CAT_1:79 for c being Object of C holds (id C).c = c; definition let C,D be Category; let T be Functor of C,D; attr T is isomorphic means :: CAT_1:def 25 T is one-to-one & rng T = the carrier' of D & rng Obj T = the carrier of D; attr T is full means :: CAT_1:def 26 for c,c9 being Object of C st Hom(T.c,T.c9) <> {} for g being Morphism of T.c,T.c9 holds Hom(c,c9) <> {} & ex f being Morphism of c,c9 st g = T.f; attr T is faithful means :: CAT_1:def 27 for c,c9 being Object of C st Hom(c,c9) <> {} for f1,f2 being Morphism of c,c9 holds T.f1 = T.f2 implies f1 = f2; end; theorem :: CAT_1:80 id C is isomorphic; theorem :: CAT_1:81 for T being Functor of C,D for c,c9 being Object of C for f being set st f in Hom(c,c9) holds T.f in Hom(T.c,T.c9); theorem :: CAT_1:82 for T being Functor of C,D for c,c9 being Object of C st Hom(c, c9) <> {} for f being Morphism of c,c9 holds T.f in Hom(T.c,T.c9); theorem :: CAT_1:83 for T being Functor of C,D for c,c9 being Object of C st Hom(c, c9) <> {} for f being Morphism of c,c9 holds T.f is Morphism of T.c,T.c9; theorem :: CAT_1:84 for T being Functor of C,D for c,c9 being Object of C st Hom(c, c9) <> {} holds Hom(T.c,T.c9) <> {}; theorem :: CAT_1:85 for T being Functor of B,C for S being Functor of C,D st T is full & S is full holds S*T is full; theorem :: CAT_1:86 for T being Functor of B,C for S being Functor of C,D st T is faithful & S is faithful holds S*T is faithful; theorem :: CAT_1:87 for T being Functor of C,D for c,c9 being Object of C holds T.: Hom(c,c9) c= Hom(T.c,T.c9); definition let C,D be Category; let T be Functor of C,D; let c,c9 be Object of C; func hom(T,c,c9) -> Function of Hom(c,c9) , Hom(T.c,T.c9) equals :: CAT_1:def 28 T|Hom(c,c9); end; theorem :: CAT_1:88 for T being Functor of C,D for c,c9 being Object of C st Hom(c, c9) <> {} for f being Morphism of c,c9 holds hom(T,c,c9).f = T.f; theorem :: CAT_1:89 for T being Functor of C,D holds T is full iff for c,c9 being Object of C holds rng hom(T,c,c9) = Hom(T.c,T.c9); theorem :: CAT_1:90 for T being Functor of C,D holds T is faithful iff for c,c9 being Object of C holds hom(T,c,c9) is one-to-one; theorem :: CAT_1:91 for a,b being Element of C st Hom(a,b)<>{} ex m being Morphism of a,b st m in Hom(a,b); theorem :: CAT_1:92 the carrier' of C = union the set of all Hom(a,b);