Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

The abstract of the Mizar article:

Introduction to Categories and Functors

by
Czeslaw Bylinski

Received October 25, 1989

MML identifier: CAT_1
[ Mizar article, MML identifier index ]


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;

Back to top