Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

The abstract of the Mizar article:

Categorial Categories and Slice Categories

by
Grzegorz Bancerek

Received October 24, 1994

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


environ

 vocabulary COMMACAT, MCART_1, CAT_1, RELAT_1, FUNCT_1, PARTFUN1, CAT_2, BOOLE,
      GROUP_6, TARSKI, SETFAM_1, GRCAT_1, FRAENKEL, FUNCT_3, CAT_5;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, MCART_1, DOMAIN_1,
      RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, FRAENKEL, PARTFUN1, CAT_1, CAT_2,
      COMMACAT;
 constructors NATTRA_1, SETFAM_1, DOMAIN_1, COMMACAT, PARTFUN1, XBOOLE_0;
 clusters FRAENKEL, CAT_1, CAT_2, FUNCT_1, RELSET_1, SUBSET_1, XBOOLE_0,
      ZFMISC_1;
 requirements SUBSET, BOOLE;


begin :: Categories with Triple-like Morphisms

definition let D1,D2,D be non empty set;
 let x be Element of [:[:D1,D2:],D:];
 redefine func x`11 -> Element of D1;
 redefine func x`12 -> Element of D2;
end;

definition let D1,D2 be non empty set;
 let x be Element of [:D1,D2:];
 redefine func x`2 -> Element of D2;
end;

theorem :: CAT_5:1
 for C,D being CatStr st the CatStr of C = the CatStr of D holds
   C is Category-like implies D is Category-like;

definition let IT be CatStr;
 attr IT is with_triple-like_morphisms means
:: CAT_5:def 1
  for f being Morphism of IT ex x being set st f = [[dom f, cod f], x];
end;

definition
 cluster with_triple-like_morphisms (strict Category);
end;

theorem :: CAT_5:2
 for C being with_triple-like_morphisms CatStr, f being Morphism of C holds
  dom f = f`11 & cod f = f`12 & f = [[dom f, cod f], f`2];

definition
 let C be with_triple-like_morphisms CatStr;
 let f be Morphism of C;
 redefine func f`11 -> Object of C;
 redefine func f`12 -> Object of C;
end;

scheme CatEx
 { A, B() -> non empty set, P[set, set, set], F(set,set) -> set }:
 ex C being with_triple-like_morphisms strict Category st
  the Objects of C = A() &
  (for a,b being Element of A(), f being Element of B() st
    P[a,b,f] holds [[a,b],f] is Morphism of C) &
  (for m being Morphism of C
    ex a,b being Element of A(), f being Element of B() st
     m = [[a,b],f] & P[a,b,f]) &
   for m1,m2 being (Morphism of C), a1,a2,a3 being Element of A(),
    f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
    holds m2*m1 = [[a1,a3], F(f2,f1)]
 provided
  for a,b,c being Element of A(), f,g being Element of B() st
      P[a,b,f] & P[b,c,g] holds F(g,f) in B() & P[a,c,F(g,f)] and
  for a being Element of A() ex f being Element of B() st P[a,a,f] &
     for b being Element of A(), g being Element of B() holds
      (P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g) and
  for a,b,c,d being Element of A(), f,g,h being Element of B() st
      P[a,b,f] & P[b,c,g] & P[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f);

scheme CatUniq
 { A, B() -> non empty set, P[set, set, set], F(set,set) -> set }:
for C1, C2 being strict with_triple-like_morphisms Category st
  the Objects of C1 = A() &
  (for a,b being Element of A(), f being Element of B() st
    P[a,b,f] holds [[a,b],f] is Morphism of C1) &
  (for m being Morphism of C1
    ex a,b being Element of A(), f being Element of B() st
     m = [[a,b],f] & P[a,b,f]) &
  (for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of A(),
    f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
    holds m2*m1 = [[a1,a3], F(f2,f1)]) &
  the Objects of C2 = A() &
  (for a,b being Element of A(), f being Element of B() st
    P[a,b,f] holds [[a,b],f] is Morphism of C2) &
  (for m being Morphism of C2
    ex a,b being Element of A(), f being Element of B() st
     m = [[a,b],f] & P[a,b,f]) &
   for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of A(),
    f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
    holds m2*m1 = [[a1,a3], F(f2,f1)]
 holds C1 = C2
 provided
  for a being Element of A() ex f being Element of B() st P[a,a,f] &
     for b being Element of A(), g being Element of B() holds
      (P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g);

scheme FunctorEx
 { A,B() -> Category,
   O(set) -> Object of B(),
   F(set) -> set }:
 ex F being Functor of A(),B() st
  for f being Morphism of A() holds F.f = F(f)
 provided
  for f being Morphism of A() holds F(f) is Morphism of B() &
      for g being Morphism of B() st g = F(f) holds
        dom g = O(dom f) & cod g = O(cod f) and
  for a being Object of A() holds F(id a) = id O(a) and
  for f1,f2 being Morphism of A() for g1,g2 being Morphism of B() st
      g1 = F(f1) & g2 = F(f2) & dom f2 = cod f1 holds F(f2*f1) = g2*g1;

theorem :: CAT_5:3
 for C1 being Category, C2 being Subcategory of C1 st C1 is Subcategory of C2
  holds the CatStr of C1 = the CatStr of C2;

theorem :: CAT_5:4
 for C being Category, D being Subcategory of C, E being Subcategory of D
  holds E is Subcategory of C;

definition
 let C1,C2 be Category;
 given C being Category such that
 C1 is Subcategory of C & C2 is Subcategory of C;
 given o1 being Object of C1 such that
 o1 is Object of C2;
 func C1 /\ C2 -> strict Category means
:: CAT_5:def 2

  the Objects of it = (the Objects of C1) /\ the Objects of C2 &
  the Morphisms of it = (the Morphisms of C1) /\ the Morphisms of C2 &
  the Dom of it = (the Dom of C1)|the Morphisms of C2 &
  the Cod of it = (the Cod of C1)|the Morphisms of C2 &
  the Comp of it =
    (the Comp of C1)|([:the Morphisms of C2,the Morphisms of C2:]) &
  the Id of it = (the Id of C1)|the Objects of C2;
end;

reserve C for Category, C1,C2 for Subcategory of C;

theorem :: CAT_5:5
 the Objects of C1 meets the Objects of C2 implies C1 /\ C2 = C2 /\ C1;

theorem :: CAT_5:6
 the Objects of C1 meets the Objects of C2 implies
  C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2;

definition let C,D be Category;
 let F be Functor of C,D;
 func Image F -> strict Subcategory of D means
:: CAT_5:def 3
  the Objects of it = rng Obj F & rng F c= the Morphisms of it &
  for E being Subcategory of D st
    the Objects of E = rng Obj F & rng F c= the Morphisms of E
   holds it is Subcategory of E;
end;

theorem :: CAT_5:7
 for C,D being Category, E be Subcategory of D, F being Functor of C,D st
  rng F c= the Morphisms of E holds F is Functor of C, E;

theorem :: CAT_5:8
   for C,D being Category, F being Functor of C,D holds
  F is Functor of C, Image F;

theorem :: CAT_5:9
 for C,D being Category, E being Subcategory of D, F being Functor of C,E
 for G being Functor of C,D st F = G holds Image F = Image G;

begin :: Categorial Categories

definition let IT be set;
 attr IT is categorial means
:: CAT_5:def 4
  for x being set st x in IT holds x is Category;
end;

definition
 cluster categorial (non empty set);
 let X be non empty set;
 redefine attr X is categorial means
:: CAT_5:def 5

  for x being Element of X holds x is Category;
end;

definition let X be non empty categorial set;
 redefine mode Element of X -> Category;
end;

definition let C be Category;
 attr C is Categorial means
:: CAT_5:def 6
  the Objects of C is categorial &
  (for a being Object of C, A being Category st a = A holds
    id a = [[A,A], id A]) &
  (for m being Morphism of C
    for A,B being Category st A = dom m & B = cod m
     ex F being Functor of A,B st m = [[A,B], F]) &
   for m1,m2 being Morphism of C
    for A,B,C being Category
     for F being Functor of A,B
      for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G]
      holds m2*m1 = [[A,C],G*F];
end;

definition
 cluster Categorial -> with_triple-like_morphisms Category;
end;

theorem :: CAT_5:10
 for C,D being Category st the CatStr of C = the CatStr of D holds
   C is Categorial implies D is Categorial;

theorem :: CAT_5:11
 for C being Category holds 1Cat(C, [[C,C], id C]) is Categorial;

definition
 cluster Categorial (strict Category);
end;

theorem :: CAT_5:12
 for C being Categorial Category, a being Object of C holds a is Category;

theorem :: CAT_5:13
 for C being Categorial Category, f being Morphism of C holds
  dom f = f`11 & cod f = f`12;

definition let C be Categorial Category;
 let m be Morphism of C;
 redefine func m`11 -> Category;
 redefine func m`12 -> Category;
end;

theorem :: CAT_5:14
 for C1, C2 being Categorial Category st
   the Objects of C1 = the Objects of C2 &
   the Morphisms of C1 = the Morphisms of C2
  holds the CatStr of C1 = the CatStr of C2;

definition let C be Categorial Category;
 cluster -> Categorial Subcategory of C;
end;

theorem :: CAT_5:15
 for C,D being Categorial Category st the Morphisms of C c= the Morphisms of D
  holds C is Subcategory of D;

definition
 let a be set such that
   a is Category;
 func cat a -> Category equals
:: CAT_5:def 7

   a;
end;

theorem :: CAT_5:16
 for C being Categorial Category, c being Object of C holds cat c = c;

definition let C be Categorial Category;
 let m be Morphism of C;
 redefine func m`2 -> Functor of cat dom m, cat cod m;
end;

theorem :: CAT_5:17
 for X being categorial non empty set, Y being non empty set st
   (for A,B,C being Element of X
     for F being Functor of A,B, G being Functor of B,C st
      F in Y & G in Y holds G*F in Y) &
   (for A being Element of X holds id A in Y)
 ex C being strict Categorial Category st
  the Objects of C = X &
  for A,B being Element of X, F being Functor of A,B holds
   [[A,B],F] is Morphism of C iff F in Y;

theorem :: CAT_5:18
 for X being categorial non empty set, Y being non empty set
 for C1, C2 being strict Categorial Category st
  the Objects of C1 = X &
  (for A,B being Element of X, F being Functor of A,B holds
   [[A,B],F] is Morphism of C1 iff F in Y) &
  the Objects of C2 = X &
  (for A,B being Element of X, F being Functor of A,B holds
   [[A,B],F] is Morphism of C2 iff F in Y)
 holds C1 = C2;

definition let IT be Categorial Category;
 attr IT is full means
:: CAT_5:def 8

  for a,b being Category st a is Object of IT & b is Object of IT
   for F being Functor of a, b holds [[a,b],F] is Morphism of IT;
end;

definition
 cluster full (Categorial strict Category);
end;

theorem :: CAT_5:19
   for C1,C2 being full (Categorial Category) st
  the Objects of C1 = the Objects of C2 holds
  the CatStr of C1 = the CatStr of C2;

theorem :: CAT_5:20
 for A being categorial non empty set
  ex C being full (Categorial strict Category) st the Objects of C = A;

theorem :: CAT_5:21
 for C being Categorial Category, D being full (Categorial Category) st
  the Objects of C c= the Objects of D holds C is Subcategory of D;

theorem :: CAT_5:22
   for C being Category, D1,D2 being Categorial Category
 for F1 being Functor of C,D1 for F2 being Functor of C,D2 st
  F1 = F2 holds Image F1 = Image F2;

begin :: Slice category

definition
 let C be Category;
 let o be Object of C;
 func Hom o -> Subset of the Morphisms of C equals
:: CAT_5:def 9

   (the Cod of C)"{o};
 func o Hom -> Subset of the Morphisms of C equals
:: CAT_5:def 10

   (the Dom of C)"{o};
end;

definition
 let C be Category;
 let o be Object of C;
 cluster Hom o -> non empty;
 cluster o Hom -> non empty;
end;

theorem :: CAT_5:23
 for C being Category, a being Object of C, f being Morphism of C holds
  f in Hom a iff cod f = a;

theorem :: CAT_5:24
 for C being Category, a being Object of C, f being Morphism of C holds
  f in a Hom iff dom f = a;

theorem :: CAT_5:25
   for C being Category, a,b being Object of C holds
  Hom(a,b) = (a Hom) /\ (Hom b);

theorem :: CAT_5:26
   for C being Category, f being Morphism of C holds
  f in (dom f) Hom & f in Hom (cod f);

theorem :: CAT_5:27
 for C being Category, f being (Morphism of C),
     g being Element of Hom dom f
 holds f*g in Hom cod f;

theorem :: CAT_5:28
 for C being Category, f being (Morphism of C),
     g being Element of (cod f) Hom
 holds g*f in (dom f) Hom;

definition
 let C be Category, o be Object of C;

 func C-SliceCat(o) -> strict with_triple-like_morphisms Category means
:: CAT_5:def 11

  the Objects of it = Hom o &
  (for a,b being Element of Hom o, f being Morphism of C st
    dom b = cod f & a = b*f holds [[a,b],f] is Morphism of it) &
  (for m being Morphism of it
    ex a,b being Element of Hom o, f being Morphism of C st
     m = [[a,b],f] & dom b = cod f & a = b*f) &
   for m1,m2 being (Morphism of it), a1,a2,a3 being Element of Hom o,
    f1,f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
    holds m2*m1 = [[a1,a3], f2*f1];

 func o-SliceCat(C) -> strict with_triple-like_morphisms Category means
:: CAT_5:def 12

  the Objects of it = o Hom &
  (for a,b being Element of o Hom, f being Morphism of C st
    dom f = cod a & f*a = b holds [[a,b],f] is Morphism of it) &
  (for m being Morphism of it
    ex a,b being Element of o Hom, f being Morphism of C st
     m = [[a,b],f] & dom f = cod a & f*a = b) &
   for m1,m2 being (Morphism of it), a1,a2,a3 being Element of o Hom,
    f1,f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
    holds m2*m1 = [[a1,a3], f2*f1];
end;

definition
 let C be Category;
 let o be Object of C;
 let m be Morphism of C-SliceCat(o);
 redefine func m`2 -> Morphism of C;
 redefine func m`11 -> Element of Hom o;
 redefine func m`12 -> Element of Hom o;
end;

theorem :: CAT_5:29
 for C being Category, a being Object of C, m being Morphism of C-SliceCat a
 holds m = [[m`11,m`12],m`2] & dom m`12 = cod m`2 & m`11 = m`12*m`2 &
   dom m = m`11 & cod m = m`12;

theorem :: CAT_5:30
 for C being Category, o being Object of C, f being Element of Hom o
 for a being Object of C-SliceCat o st a = f holds
  id a = [[a,a], id dom f];

definition
 let C be Category;
 let o be Object of C;
 let m be Morphism of o-SliceCat(C);
 redefine func m`2 -> Morphism of C;
 redefine func m`11 -> Element of o Hom;
 redefine func m`12 -> Element of o Hom;
end;

theorem :: CAT_5:31
 for C being Category, a being Object of C, m being Morphism of a-SliceCat C
 holds m = [[m`11,m`12],m`2] & dom m`2 = cod m`11 & m`2*m`11 = m`12 &
   dom m = m`11 & cod m = m`12;

theorem :: CAT_5:32
 for C being Category, o being Object of C, f being Element of o Hom
 for a being Object of o-SliceCat C st a = f holds
  id a = [[a,a], id cod f];

begin :: Functors Between Slice Categories

definition
 let C be Category, f be Morphism of C;
 func SliceFunctor f -> Functor of C-SliceCat dom f, C-SliceCat cod f means
:: CAT_5:def 13

  for m being Morphism of C-SliceCat dom f holds
   it.m = [[f*m`11, f*m`12], m`2];
 func SliceContraFunctor f ->
      Functor of (cod f)-SliceCat C, (dom f)-SliceCat C means
:: CAT_5:def 14

  for m being Morphism of (cod f)-SliceCat C holds
   it.m = [[m`11*f, m`12*f], m`2];
end;

theorem :: CAT_5:33
   for C being Category, f,g being Morphism of C st dom g = cod f holds
  SliceFunctor (g*f) = (SliceFunctor g)*(SliceFunctor f);

theorem :: CAT_5:34
   for C being Category, f,g being Morphism of C st dom g = cod f holds
  SliceContraFunctor (g*f) = (SliceContraFunctor f)*(SliceContraFunctor g);


Back to top