The abstract of the Mizar article:

Natural transformations. Discrete categories

by

Andrzej Trybulec

Received May 15, 1991

MML identifier: NATTRA_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, PARTFUN1, FUNCT_4, BOOLE, CAT_1, CAT_2, MCART_1,
      FUNCT_2, FINSET_1, CARD_1, NATTRA_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, FINSET_1, PARTFUN1,
      RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, CARD_1, CAT_1, CAT_2;
 constructors MCART_1, CARD_1, CAT_2, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, FINSET_1, CAT_1, CAT_2, RELSET_1, SUBSET_1, MEMBERED,
      ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

:: Preliminaries

reserve A1,A2,B1,B2 for non empty set,
        f for Function of A1,B1,
        g for Function of A2,B2,
        Y1 for non empty Subset of A1,
        Y2 for non empty Subset of A2;

definition let A1 be set, B1 be non empty set,
               f be Function of A1, B1,
               Y1 be Subset of A1;
 redefine func f|Y1 -> Function of Y1,B1;
end;

theorem :: NATTRA_1:1
 [:f,g:]|[:Y1,Y2:] = [:f|Y1,g|Y2:];

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

theorem :: NATTRA_1:2
 for f being PartFunc of [:A1,A1:],A1, g being PartFunc of [:A2,A2:],A2
 for F being PartFunc of [:Y1,Y1:],Y1 st F = f|([:Y1,Y1:] qua set)
 for G being PartFunc of [:Y2,Y2:],Y2 st G = g|([:Y2,Y2:] qua set)
 holds |:F,G:| = |:f,g:| |([:[:Y1,Y2:],[:Y1,Y2:]:] qua set);

 reserve A,B,C for Category,
         F,F1,F2,F3 for Functor of A,B,
         G for Functor of B,C;

scheme M_Choice{A()-> non empty set, B()-> non empty set,
                  F(set) -> set}:
ex t being Function of A(),B() st
  for a being Element of A() holds t.a in F(a)
provided
 for a being Element of A() holds B() meets F(a);

theorem :: NATTRA_1:3
 for a being Object of A, m being Morphism of a,a holds m in Hom(a,a);

reserve m,o for set;

theorem :: NATTRA_1:4
 for f,g being Morphism of 1Cat(o,m) holds f = g;

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 Dom of C = (the Dom of A)|the Morphisms of C &
   the Cod of C = (the Cod of A)|the Morphisms of C &
   the Comp of C = (the Comp of A)|[:the Morphisms of C, the Morphisms of C:] &
   the Id of C = (the Id of A)|the Objects of C;

theorem :: NATTRA_1:9
 for O being non empty Subset of the Objects of A,
     M being non empty Subset of the Morphisms of A
 for DOM,COD being Function of M,O st
   DOM = (the Dom of A) |M & COD = (the Cod of A)|M
 for COMP being PartFunc of [:M,M qua non empty set:], M st
   COMP = (the Comp of A)|([:M,M:] qua set)
 for ID being Function of O,M st ID = (the Id of A)|O
  holds CatStr(#O,M,DOM,COD,COMP,ID#) is Subcategory of A;

theorem :: NATTRA_1:10
 for C being strict Category, A being strict Subcategory of C st
  the Objects of A = the Objects of C & the Morphisms of A = the Morphisms of C
 holds A = C;

begin :: Application of a functor to a morphism

definition let A,B,F; let a,b be Object of A such that
 Hom(a,b) <> {};
 let f be Morphism of a,b;
  func F.f -> Morphism of F.a, F.b equals
:: NATTRA_1:def 1
  F.f;
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.MIZ, with
:: the new concept of the application of a functor to a morphism

theorem :: NATTRA_1:12 :: CAT_1:95
     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  :: CAT_1:99
 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 :: CAT_1:107
    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  :: CAT_1:108
 for a being Object of A holds F.id a = id (F.a);

theorem :: NATTRA_1:16 :: CAT_1:115
   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;

canceled;

theorem :: NATTRA_1:19
 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 Objects of A, the Morphisms 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:20
 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:21
 for a being Object of A holds id F.a = id(F.a);

theorem :: NATTRA_1:22
 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:23
 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;

canceled;

theorem :: NATTRA_1:25
 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:26
 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:27
 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:28
 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;
 synonym F1 ~= F2;
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;

canceled;

theorem :: NATTRA_1:30
 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:31
   F1 ~= F2 implies F2 ~= F1;

theorem :: NATTRA_1:32
 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:33
   id F is natural_equivalence of F,F;

theorem :: NATTRA_1:34
   F1 ~= F2 & F2 ~= F3 implies
  for t being natural_equivalence of F1,F2,
      t' being natural_equivalence of F2,F3 holds
   t'`*`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;

definition let A1,B1,A2,B2 be non empty set,
     f1 be Function of A1,B1,
     f2 be Function of A2,B2;
 redefine pred f1 = f2 means
:: NATTRA_1:def 17
     A1 = A2 & for a being Element of A1 holds f1.a = f2.a;
end;

theorem :: NATTRA_1:35
 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 18
 the Objects of it = Funct(A,B) &
   the Morphisms 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

canceled 3;

theorem :: NATTRA_1:39
 for f being Morphism of Functors(A,B) st f = [[F,F1],t] holds
   dom f = F & cod f = F1;

theorem :: NATTRA_1:40
   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:41
 for t' being natural_transformation of F2,F3
 for f,g being Morphism of Functors(A,B) st
  f = [[F,F1],t] & g = [[F2,F3],t'] holds
  [g,f] in dom the Comp of Functors(A,B) iff F1 = F2;

theorem :: NATTRA_1:42
   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 discrete means
:: NATTRA_1:def 19
 for f being Morphism of C ex a being Object of C st f = id a;
end;

definition
 cluster discrete Category;
end;

canceled;

theorem :: NATTRA_1:44
 for A being discrete Category, a being Object of A holds Hom(a,a) = { id a};

theorem :: NATTRA_1:45
 A is discrete iff
  (for a being Object of A
   ex B being finite set st B = Hom(a,a) & card B = 1) &
  for a,b being Object of A st a <> b holds Hom(a,b) = {};

theorem :: NATTRA_1:46
 1Cat(o,m) is discrete;

theorem :: NATTRA_1:47
   for A being discrete Category, C being Subcategory of A holds C is discrete;

theorem :: NATTRA_1:48
   A is discrete & B is discrete implies [:A,B:] is discrete;

theorem :: NATTRA_1:49
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:50
for A being discrete Category, B being Category, F being Functor of B,A,
   t being transformation of F,F holds t = id F;

theorem :: NATTRA_1:51
   A is discrete implies Functors(B,A) is discrete;

definition let C be Category;
 cluster strict discrete Subcategory of C;
end;

definition let C;
 func IdCat(C) -> strict discrete Subcategory of C means
:: NATTRA_1:def 20
 the Objects of it = the Objects of C &
  the Morphisms of it = { id a where a is Object of C: not contradiction};
end;

theorem :: NATTRA_1:52
 for C being strict Category holds C is discrete implies IdCat(C) = C;

theorem :: NATTRA_1:53
   IdCat(IdCat(C)) = IdCat(C);

theorem :: NATTRA_1:54
   IdCat(1Cat(o,m)) = 1Cat(o,m);

theorem :: NATTRA_1:55
   IdCat([:A,B:]) = [:IdCat(A), IdCat(B):];