environ vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCOP_1, PARTFUN1, TARSKI, WELLORD1, CAT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1; constructors FUNCOP_1, WELLORD2, MEMBERED, PARTFUN1, XBOOLE_0; clusters FUNCT_1, RELSET_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Auxiliary theorems reserve a,b,c,o,m for set; canceled 3; theorem :: CAT_1:4 for X,Y,Z being set, D being non empty set, f being Function of X,D st Y c= X & f.:Y c= Z holds f|Y is Function of Y,Z; definition let A be non empty set,b; redefine func A --> b -> Function of A,{b}; end; definition let a,b,c; func (a,b).-->c -> PartFunc of [:{a},{b}:],{c} equals :: CAT_1:def 1 {[a,b]} --> c; end; canceled 2; theorem :: CAT_1:7 dom (a,b).-->c = {[a,b]} & dom (a,b).-->c = [:{a},{b}:]; theorem :: CAT_1:8 ((a,b).-->c).[a,b] = c; theorem :: CAT_1:9 for x being Element of {a} for y being Element of {b} holds ((a,b).-->c).[x,y] = c; :: Structure of a Category definition struct CatStr (# Objects,Morphisms -> non empty set, Dom,Cod -> Function of the Morphisms, the Objects, Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms, Id -> Function of the Objects, the Morphisms #); end; reserve C for CatStr; definition let C; mode Object of C is Element of the Objects of C; mode Morphism of C is Element of the Morphisms of C; end; reserve a,b,c,d for Object of C; reserve f,g for Morphism of C; :: Domain and Codomain of a Morphism definition let C,f; func dom(f) -> Object of C equals :: CAT_1:def 2 (the Dom of C).f; func cod(f) -> Object of C equals :: CAT_1:def 3 (the Cod of C).f; 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 4 ( the Comp of C ).[g,f]; end; definition let C,a; func id (a) -> Morphism of C equals :: CAT_1:def 5 ( the Id of C ).a; end; definition let C,a,b; func Hom(a,b) -> Subset of the Morphisms of C equals :: CAT_1:def 6 { f : dom(f)=a & cod(f)=b }; end; canceled 8; theorem :: CAT_1:18 f in Hom(a,b) iff dom(f)=a & cod(f)=b; theorem :: CAT_1:19 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 7 it in Hom(a,b); end; canceled; theorem :: CAT_1:21 for f being set st f in Hom(a,b) holds f is Morphism of a,b; theorem :: CAT_1:22 for f being Morphism of C holds f is Morphism of dom(f),cod(f); theorem :: CAT_1:23 for f being Morphism of a,b st Hom(a,b) <> {} holds dom(f) = a & cod(f) = b; theorem :: CAT_1:24 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:25 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:26 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:27 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 CatStr; attr C is Category-like means :: CAT_1:def 8 (for f,g being Element of the Morphisms of C holds [g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f) & (for f,g being Element of the Morphisms of C st (the Dom of C).g=(the Cod of C).f holds (the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f & (the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g) & (for f,g,h being Element of the Morphisms of C st (the Dom of C).h = (the Cod of C).g & (the Dom of C).g = (the Cod of C).f holds (the Comp of C).[h,(the Comp of C).[g,f]] = (the Comp of C).[(the Comp of C).[h,g],f] ) & (for b being Element of the Objects of C holds (the Dom of C).((the Id of C).b) = b & (the Cod of C).((the Id of C).b) = b & (for f being Element of the Morphisms of C st (the Cod of C).f = b holds (the Comp of C).[(the Id of C).b,f] = f ) & (for g being Element of the Morphisms of C st (the Dom of C).g = b holds (the Comp of C).[g,(the Id of C).b] = g ) ); end; definition cluster Category-like CatStr; end; definition mode Category is Category-like CatStr; end; definition cluster strict Category; end; canceled; theorem :: CAT_1:29 for C being CatStr st ( for f,g being Morphism of C holds [g,f] in dom(the Comp of C) iff dom g = cod f ) & ( for f,g being Morphism of C st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g ) & ( for f,g,h being Morphism of C st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f ) & ( for b being Object of C holds dom id b = b & cod id b = b & (for f being Morphism of C st cod f = b holds (id b)*f = f) & (for g being Morphism of C st dom g = b holds g*(id b) = g) ) holds C is Category-like; definition let o,m; func 1Cat(o,m) -> strict Category equals :: CAT_1:def 9 CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #); end; canceled 2; theorem :: CAT_1:32 o is Object of 1Cat(o,m); theorem :: CAT_1:33 m is Morphism of 1Cat(o,m); theorem :: CAT_1:34 for a being Object of 1Cat(o,m) holds a = o; theorem :: CAT_1:35 for f being Morphism of 1Cat(o,m) holds f = m; theorem :: CAT_1:36 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:37 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:38 for a,b being Object of 1Cat(o,m) holds Hom(a,b) <> {}; theorem :: CAT_1:39 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:40 dom(g) = cod(f) iff [g,f] in dom(the Comp of C); theorem :: CAT_1:41 dom(g) = cod(f) implies g*f = ( the Comp of C ).[g,f]; theorem :: CAT_1:42 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:43 for f,g,h being Morphism of C st dom(h) = cod(g) & dom(g) = cod(f) holds h*(g*f) = (h*g)*f; theorem :: CAT_1:44 dom(id b) = b & cod(id b) = b; theorem :: CAT_1:45 id a = id b implies a = b; theorem :: CAT_1:46 for f being Morphism of C st cod(f) = b holds (id b)*f = f; theorem :: CAT_1:47 for g being Morphism of C st dom(g) = b holds g*(id b) = g; definition let C,g; attr g is monic means :: CAT_1:def 10 for f1,f2 st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g*f1=g*f2 holds f1=f2; end; definition let C,f; attr f is epi means :: CAT_1:def 11 for g1,g2 st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1*f=g2*f holds g1=g2; end; definition let C,f; attr f is invertible means :: CAT_1:def 12 ex g st dom g = cod f & cod g = dom f & f*g = id cod f & g*f = id dom f; end; reserve f,f1,f2 for Morphism of a,b; reserve f' for Morphism of b,a; reserve g for Morphism of b,c; reserve h,h1,h2 for Morphism of c,d; canceled 3; theorem :: CAT_1:51 Hom(a,b)<>{} & Hom(b,c)<>{} implies g*f in Hom(a,c); theorem :: CAT_1:52 Hom(a,b)<>{} & Hom(b,c)<>{} implies 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; canceled; theorem :: CAT_1:54 Hom(a,b)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} implies (h*g)*f=h*(g*f); theorem :: CAT_1:55 id a in Hom(a,a); theorem :: CAT_1:56 Hom(a,a) <> {}; definition let C,a; redefine func id a -> Morphism of a,a; end; theorem :: CAT_1:57 Hom(a,b)<>{} implies (id b)*f=f; theorem :: CAT_1:58 Hom(b,c)<>{} implies g*(id b)=g; theorem :: CAT_1:59 (id a)*(id a) = id a; :: Monics, Epis theorem :: CAT_1:60 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:61 Hom(b,c)<>{} & Hom(c,d)<>{} & g is monic & h is monic implies h*g is monic ; theorem :: CAT_1:62 Hom(b,c)<>{} & Hom(c,d)<>{} & h*g is monic implies g is monic; theorem :: CAT_1:63 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:64 id b is monic; theorem :: CAT_1:65 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:66 Hom(a,b)<>{} & Hom(b,c)<>{} & f is epi & g is epi implies g*f is epi; theorem :: CAT_1:67 Hom(a,b)<>{} & Hom(b,c)<>{} & g*f is epi implies g is epi; theorem :: CAT_1:68 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:69 id b is epi; theorem :: CAT_1:70 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:71 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 Hom(a,b) <> {} and f is invertible; func f" -> Morphism of b,a means :: CAT_1:def 14 f*it = id b & it*f = id a; end; canceled; theorem :: CAT_1:73 Hom(a,b)<>{} & f is invertible implies f is monic & f is epi; theorem :: CAT_1:74 id a is invertible; theorem :: CAT_1:75 Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible implies g*f is invertible; theorem :: CAT_1:76 Hom(a,b)<>{} & f is invertible implies f" is invertible; theorem :: CAT_1:77 Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible implies (g*f)" = f"*g"; definition let C,a; attr a is terminal means :: CAT_1:def 15 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 16 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 17 Hom(a,b)<>{} & ex f st f is invertible; end; canceled 3; theorem :: CAT_1:81 a,b are_isomorphic iff Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f' st f*f' = id b & f'*f = id a; theorem :: CAT_1:82 a is initial iff for b ex f being Morphism of a,b st Hom(a,b) = {f}; theorem :: CAT_1:83 a is initial implies for h being Morphism of a,a holds id a = h; theorem :: CAT_1:84 a is initial & b is initial implies a,b are_isomorphic; theorem :: CAT_1:85 a is initial & a,b are_isomorphic implies b is initial; theorem :: CAT_1:86 b is terminal iff for a ex f being Morphism of a,b st Hom(a,b) = {f}; theorem :: CAT_1:87 a is terminal implies for h being Morphism of a,a holds id a = h; theorem :: CAT_1:88 a is terminal & b is terminal implies a,b are_isomorphic; theorem :: CAT_1:89 b is terminal & a,b are_isomorphic implies a is terminal; theorem :: CAT_1:90 Hom(a,b) <> {} & a is terminal implies f is monic; theorem :: CAT_1:91 a,a are_isomorphic; theorem :: CAT_1:92 a,b are_isomorphic implies b,a are_isomorphic; theorem :: CAT_1:93 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 Morphisms of C,the Morphisms of D means :: CAT_1:def 18 ( for c being Element of the Objects of C ex d being Element of the Objects of D st it.((the Id of C).c) = (the Id of D).d ) & ( for f being Element of the Morphisms of C holds it.((the Id of C).((the Dom of C).f)) = (the Id of D).((the Dom of D).(it.f)) & it.((the Id of C).((the Cod of C).f)) = (the Id of D).((the Cod of D).(it.f)) ) & ( for f,g being Element of the Morphisms of C st [g,f] in dom(the Comp of C) holds it.((the Comp of C).[g,f]) = (the Comp of D).[it.g,it.f] ); end; canceled 2; theorem :: CAT_1:96 for T being Function of the Morphisms of C,the Morphisms 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:97 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:98 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:99 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:100 for T being Function of the Morphisms of C,the Morphisms of D for F being Function of the Objects of C, the Objects 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 Morphisms of C,the Morphisms of D; assume for c being Element of the Objects of C ex d being Element of the Objects of D st F.((the Id of C).c) = (the Id of D).d; func Obj(F) -> Function of the Objects of C,the Objects of D means :: CAT_1:def 19 for c being Element of the Objects of C for d being Element of the Objects of D st F.((the Id of C).c) = (the Id of D).d holds it.c = d; end; canceled; theorem :: CAT_1:102 for T being Function of the Morphisms of C,the Morphisms 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:103 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:104 for T being (Functor of C,D),c being Object of C holds T.(id c) = id((Obj T).c); theorem :: CAT_1:105 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 20 (Obj T).c; end; canceled; theorem :: CAT_1:107 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:108 for T being (Functor of C, D),c being Object of C holds T.(id c) = id(T.c); theorem :: CAT_1:109 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:110 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:111 id the Morphisms of C is Functor of C,C; theorem :: CAT_1:112 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:113 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 21 id the Morphisms of C; end; canceled; theorem :: CAT_1:115 for f being Morphism of C holds (id C).f = f; theorem :: CAT_1:116 for c being Object of C holds (Obj id C).c = c; theorem :: CAT_1:117 Obj id C = id the Objects of C; theorem :: CAT_1:118 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 22 T is one-to-one & rng T = the Morphisms of D & rng Obj T = the Objects of D ; synonym T is_an_isomorphism; attr T is full means :: CAT_1:def 23 for c,c' being Object of C st Hom(T.c,T.c') <> {} for g being Morphism of T.c,T.c' holds Hom(c,c') <> {} & ex f being Morphism of c,c' st g = T.f; attr T is faithful means :: CAT_1:def 24 for c,c' being Object of C st Hom(c,c') <> {} for f1,f2 being Morphism of c,c' holds T.f1 = T.f2 implies f1 = f2; end; canceled 3; theorem :: CAT_1:122 id C is_an_isomorphism; theorem :: CAT_1:123 for T being Functor of C,D for c,c' being Object of C for f being set st f in Hom(c,c') holds T.f in Hom(T.c,T.c'); theorem :: CAT_1:124 for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} for f being Morphism of c,c' holds T.f in Hom(T.c,T.c'); theorem :: CAT_1:125 for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} for f being Morphism of c,c' holds T.f is Morphism of T.c,T.c'; theorem :: CAT_1:126 for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} holds Hom(T.c,T.c') <> {}; theorem :: CAT_1:127 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:128 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:129 for T being Functor of C,D for c,c' being Object of C holds T.:Hom(c,c') c= Hom(T.c,T.c'); definition let C,D be Category; let T be Functor of C,D; let c,c' be Object of C; func hom(T,c,c') -> Function of Hom(c,c') , Hom(T.c,T.c') equals :: CAT_1:def 25 T|Hom(c,c'); end; canceled; theorem :: CAT_1:131 for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {} for f being Morphism of c,c' holds hom(T,c,c').f = T.f; theorem :: CAT_1:132 for T being Functor of C,D holds T is full iff for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c'); theorem :: CAT_1:133 for T being Functor of C,D holds T is faithful iff for c,c' being Object of C holds hom(T,c,c') is one-to-one;