The abstract of the Mizar article:

Subcategories and Products of Categories

by

Czeslaw Bylinski

Received May 31, 1990

MML identifier: CAT_2

[ Mizar article, MML identifier index ]

environ

 vocabulary FRAENKEL, FUNCT_1, FUNCT_5, FUNCT_2, RELAT_1, BOOLE, CAT_1,
      FUNCOP_1, FUNCT_3, TARSKI, PARTFUN1, FUNCT_4, MCART_1, CAT_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
      FUNCT_2, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, FRAENKEL, CAT_1;
 constructors DOMAIN_1, FUNCT_3, FUNCT_4, FUNCT_5, FRAENKEL, CAT_1, MEMBERED,
      PARTFUN1, XBOOLE_0;
 clusters FUNCT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 reserve X for set;
 reserve C,D,E for non empty set;
 reserve c for Element of C, d for Element of D;

:: Auxiliary theorems

definition let D,X,E; let F be FUNCTION_DOMAIN of X,E;
  let f be Function of D,F; let d be Element of D;
  redefine func f.d -> Element of F;
end;

reserve f for Function of [:C,D:],E;

theorem :: CAT_2:1
   curry f is Function of C,Funcs(D,E);

theorem :: CAT_2:2
   curry' f is Function of D,Funcs(C,E);

definition let C,D,E,f;
 redefine func curry f -> Function of C,Funcs(D,E);
  func curry' f -> Function of D,Funcs(C,E);
end;

theorem :: CAT_2:3
   f.[c,d] = ((curry f).c).d;

theorem :: CAT_2:4
   f.[c,d] = ((curry' f).d).c;

reserve B,C,D,C',D' for Category;

:: Auxiliary theorems on Functors

definition let B,C; let c be Object of C;
 func B --> c -> Functor of B,C equals
:: CAT_2:def 1
 (the Morphisms of B) --> (id c);
end;

canceled;

theorem :: CAT_2:6
   for c being Object of C, f being Morphism of B holds (B --> c).f = id c;

theorem :: CAT_2:7
     for c being Object of C, b being Object of B holds (Obj (B --> c)).b = c;

definition let C,D;
 func Funct(C,D) -> set means
:: CAT_2:def 2
 for x being set holds x in it iff x is Functor of C,D;
end;

definition let C,D;
 cluster Funct(C,D) -> non empty;
end;

definition let C,D;
 mode FUNCTOR-DOMAIN of C,D -> non empty set means
:: CAT_2:def 3
 for x being Element of it holds x is Functor of C,D;
end;

definition let C,D; let F be FUNCTOR-DOMAIN of C,D;
 redefine mode Element of F -> Functor of C,D;
end;

definition let A be non empty set; let C,D;
  let F be FUNCTOR-DOMAIN of C,D, T be Function of A,F, x be Element of A;
 redefine func T.x -> Element of F;
end;

definition let C,D;
 redefine func Funct(C,D) -> FUNCTOR-DOMAIN of C,D;
end;

::   Subcategory

definition let C;
 mode Subcategory of C -> Category means
:: CAT_2:def 4

   the Objects of it c= the Objects of C &
    (for a,b being Object of it, a',b' being Object of C
      st a = a' & b = b' holds Hom(a,b) c= Hom(a',b')) &
   the Comp of it <= the Comp of C &
    (for a being Object of it, a' being Object of C st a = a'
     holds id a = id a');
end;

definition let C;
 cluster strict Subcategory of C;
end;

reserve E for Subcategory of C;

canceled 4;

theorem :: CAT_2:12
   for e being Object of E holds e is Object of C;

theorem :: CAT_2:13
   the Morphisms of E c= the Morphisms of C;

theorem :: CAT_2:14
   for f being Morphism of E holds f is Morphism of C;

theorem :: CAT_2:15
   for f being (Morphism of E), f' being Morphism of C st f = f'
    holds dom f = dom f' & cod f = cod f';

theorem :: CAT_2:16
     for a,b being Object of E, a',b' being Object of C,f being Morphism of a,b
    st a = a' & b = b' & Hom(a,b)<>{} holds f is Morphism of a',b';

theorem :: CAT_2:17
   for f,g being (Morphism of E), f',g' being Morphism of C
    st f = f' & g = g' & dom g = cod f holds g*f = g'*f';

theorem :: CAT_2:18
     C is Subcategory of C;

theorem :: CAT_2:19
   id E is Functor of E,C;

definition let C,E;
 func incl(E) -> Functor of E,C equals
:: CAT_2:def 5
 id E;
end;

canceled;

theorem :: CAT_2:21
   for f being Morphism of E holds (incl E).f = f;

theorem :: CAT_2:22
   for a being Object of E holds (Obj incl E).a = a;

theorem :: CAT_2:23
   for a being Object of E holds (incl E).a = a;

theorem :: CAT_2:24
     incl E is faithful;

theorem :: CAT_2:25
   incl E is full iff
    for a,b being Object of E, a',b' being Object of C
      st a = a' & b = b' holds Hom(a,b) = Hom(a',b');

definition let C be CatStr, D;
 pred C is_full_subcategory_of D means
:: CAT_2:def 6
 C is Subcategory of D &
    for a,b being Object of C, a',b' being Object of D
      st a = a' & b = b' holds Hom(a,b) = Hom(a',b');
end;

canceled;

theorem :: CAT_2:27
     E is_full_subcategory_of C iff incl(E) is full;

theorem :: CAT_2:28
   for O being non empty Subset of the Objects of C holds
    union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O}
      is non empty Subset of the Morphisms of C;

theorem :: CAT_2:29
  for O being non empty Subset of the Objects of C, M being non empty set st
   M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O}
    holds (the Dom of C)|M is Function of M,O &
      (the Cod of C)|M is Function of M,O &
      (the Comp of C)|[:M,M:] is PartFunc of [:M,M:],M &
      (the Id of C)|O is Function of O,M;

theorem :: CAT_2:30
   for O being non empty Subset of the Objects of C, M being non empty set,
   d,c being Function of M,O, p being PartFunc of [:M,M:],M,
   i being Function of O,M
  st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
 O}
     & d = (the Dom of C)|M & c = (the Cod of C)|M
     & p = (the Comp of C)|[:M,M:] & i = (the Id of C)|O
   holds CatStr(#O,M,d,c,p,i#) is_full_subcategory_of C;

theorem :: CAT_2:31
     for O being non empty Subset of the Objects of C, M being non empty set,
     d,c being Function of M,O, p being PartFunc of [:M,M:],M,
      i being Function of O,M
    st CatStr(#O,M,d,c,p,i#) is_full_subcategory_of C
   holds
     M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in
 O}
      & d = (the Dom of C)|M & c = (the Cod of C)|M
       & p = (the Comp of C)|[:M,M:] & i = (the Id of C)|O;

:: Product of Categories

definition let X1,X2,Y1,Y2 be non empty set;
 let f1 be Function of X1,Y1; let f2 be Function of X2,Y2;
 redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
end;

definition let A,B be non empty set;
  let f be PartFunc of [:A,A:],A; let g be PartFunc of [:B,B:],B;
 redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];
end;

definition let C,D;
 func [:C,D:] -> Category equals
:: CAT_2:def 7
  CatStr (# [:the Objects of C,the Objects of D:],
                     [:the Morphisms of C,the Morphisms of D:],
                     [:the Dom of C,the Dom of D:],
                     [:the Cod of C,the Cod of D:],
                     |:the Comp of C, the Comp of D:|,
                     [:the Id of C,the Id of D:]
                   #);
end;

definition let C,D;
 cluster [:C,D:] -> strict;
end;

canceled;

theorem :: CAT_2:33
   the Objects of [:C,D:] = [:the Objects of C,the Objects of D:] &
   the Morphisms of [:C,D:] = [:the Morphisms of C,the Morphisms of D:] &
   the Dom of [:C,D:] = [:the Dom of C,the Dom of D:] &
   the Cod of [:C,D:] = [:the Cod of C,the Cod of D:] &
   the Comp of [:C,D:] = |:the Comp of C, the Comp of D:| &
   the Id of [:C,D:] = [:the Id of C,the Id of D:];

theorem :: CAT_2:34
   for c being Object of C, d being Object of D
    holds [c,d] is Object of [:C,D:];

definition let C,D; let c be Object of C; let d be Object of D;
  redefine func [c,d] -> Object of [:C,D:];
end;

theorem :: CAT_2:35
   for cd being Object of [:C,D:]
    ex c being Object of C, d being Object of D st cd = [c,d];

theorem :: CAT_2:36
   for f being Morphism of C for g being Morphism of D
     holds [f,g] is Morphism of [:C,D:];

definition let C,D; let f be Morphism of C; let g be Morphism of D;
  redefine func [f,g] -> Morphism of [:C,D:];
end;

theorem :: CAT_2:37
   for fg being Morphism of [:C,D:]
    ex f being (Morphism of C), g being Morphism of D st fg = [f,g];

theorem :: CAT_2:38
   for f being Morphism of C for g being Morphism of D
    holds dom [f,g] = [dom f,dom g] & cod [f,g] = [cod f,cod g];

theorem :: CAT_2:39
   for f,f' being Morphism of C for g,g' being Morphism of D
     st dom f' = cod f & dom g' = cod g holds [f',g']*[f,g] = [f'*f,g'*g];

theorem :: CAT_2:40
   for f,f' being Morphism of C for g,g' being Morphism of D
     st dom [f',g'] = cod [f,g] holds [f',g']*[f,g] = [f'*f,g'*g];

theorem :: CAT_2:41
   for c being Object of C, d being Object of D
    holds id [c,d] = [id c,id d];

theorem :: CAT_2:42
     for c,c' being Object of C, d,d' being Object of D
    holds Hom([c,d],[c',d']) = [:Hom(c,c'),Hom(d,d'):];

theorem :: CAT_2:43
     for c,c' being Object of C, f being Morphism of c,c',
       d,d' being Object of D, g being Morphism of d,d'
      st Hom(c,c') <> {} & Hom(d,d') <> {}
     holds [f,g] is Morphism of [c,d],[c',d'];

:: Bifunctors

theorem :: CAT_2:44
   for S being Functor of [:C,C':],D, c being Object of C
     holds (curry S).(id c) is Functor of C',D;

theorem :: CAT_2:45
   for S being Functor of [:C,C':],D, c' being Object of C'
     holds (curry' S).(id c') is Functor of C,D;

:: Partial Functors

definition let C,C',D; let S be Functor of [:C,C':],D, c be Object of C;
 func S?-c -> Functor of C',D equals
:: CAT_2:def 8
 (curry S).(id c);
end;

canceled;

theorem :: CAT_2:47
   for S being Functor of [:C,C':],D, c being Object of C,
       f being Morphism of C' holds (S?-c).f = S.[id c,f];

theorem :: CAT_2:48
     for S being Functor of [:C,C':],D,
      c being Object of C, c' being Object of C'
    holds (Obj S?-c).c' = (Obj S).[c,c'];

definition let C,C',D; let S be Functor of [:C,C':],D, c' be Object of C';
 func S-?c' -> Functor of C,D equals
:: CAT_2:def 9
  (curry' S).(id c');
end;

canceled;

theorem :: CAT_2:50
   for S being Functor of [:C,C':],D, c' being Object of C',
       f being Morphism of C holds (S-?c').f = S.[f,id c'];

theorem :: CAT_2:51
     for S being Functor of [:C,C':],D,
      c being Object of C, c' being Object of C'
    holds (Obj S-?c').c = (Obj S).[c,c'];

theorem :: CAT_2:52
     for L being Function of the Objects of C,Funct(B,D),
       M being Function of the Objects of B,Funct(C,D)
    st ( for c being Object of C,b being Object of B
          holds (M.b).(id c) = (L.c).(id b) ) &
    ( for f being Morphism of B for g being Morphism of C
      holds ((M.(cod f)).g)*((L.(dom g)).f) = ((L.(cod g)).f)*((M.(dom f)).g) )
    ex S being Functor of [:B,C:],D st
     for f being Morphism of B for g being Morphism of C
      holds S.[f,g] = ((L.(cod g)).f)*((M.(dom f)).g);

theorem :: CAT_2:53
     for L being Function of the Objects of C,Funct(B,D),
       M being Function of the Objects of B,Funct(C,D)
    st ex S being Functor of [:B,C:],D st
        for c being Object of C,b being Object of B
         holds S-?c = L.c & S?-b = M.b
    for f being Morphism of B for g being Morphism of C
     holds ((M.(cod f)).g)*((L.(dom g)).f) = ((L.(cod g)).f)*((M.(dom f)).g);

theorem :: CAT_2:54
   pr1(the Morphisms of C,the Morphisms of D) is Functor of [:C,D:],C;

theorem :: CAT_2:55
   pr2(the Morphisms of C,the Morphisms of D) is Functor of [:C,D:],D;

definition let C,D;
 func pr1(C,D) -> Functor of [:C,D:],C equals
:: CAT_2:def 10
  pr1(the Morphisms of C,the Morphisms of D);
 func pr2(C,D) -> Functor of [:C,D:],D equals
:: CAT_2:def 11
  pr2(the Morphisms of C,the Morphisms of D);
end;

canceled 2;

theorem :: CAT_2:58
   for f being (Morphism of C),g being Morphism of D
     holds pr1(C,D).[f,g] = f;

theorem :: CAT_2:59
     for c being Object of C, d being Object of D
    holds (Obj pr1(C,D)).[c,d] = c;

theorem :: CAT_2:60
   for f being (Morphism of C),g being Morphism of D
    holds pr2(C,D).[f,g] = g;

theorem :: CAT_2:61
     for c being Object of C, d being Object of D
    holds (Obj pr2(C,D)).[c,d] = d;

theorem :: CAT_2:62
   for T being Functor of C,D, T' being Functor of C,D'
    holds <:T,T':> is Functor of C,[:D,D':];

definition let C,D,D';
 let T be Functor of C,D, T' be Functor of C,D';
   redefine func <:T,T':> -> Functor of C,[:D,D':];
end;

theorem :: CAT_2:63
     for T being Functor of C,D, T' being Functor of C,D', c being Object of C
    holds (Obj <:T,T':>).c = [(Obj T).c,(Obj T').c];

theorem :: CAT_2:64
   for T being Functor of C,D, T' being Functor of C',D'
    holds [:T,T':] = <:T*pr1(C,C'),T'*pr2(C,C'):>;

theorem :: CAT_2:65
   for T being Functor of C,D, T' being Functor of C',D'
    holds [:T,T':] is Functor of [:C,C':],[:D,D':];

definition let C,C',D,D';
 let T be Functor of C,D, T' be Functor of C',D';
  redefine func [:T,T':] -> Functor of [:C,C':],[:D,D':];
end;

theorem :: CAT_2:66
     for T being Functor of C,D, T' being Functor of C',D',
       c being Object of C, c' being Object of C'
    holds (Obj [:T,T':]).[c,c'] = [(Obj T).c,(Obj T').c'];