The abstract of the Mizar article:

Indexed Category

by

Grzegorz Bancerek

Received June 8, 1995

MML identifier: INDEX_1

[ Mizar article, MML identifier index ]

environ

 vocabulary MATRIX_1, PBOOLE, ZF_REFLE, FUNCT_1, CAT_5, CAT_1, MCART_1,
      COMMACAT, GRCAT_1, RELAT_1, BOOLE, FUNCOP_1, PRALG_1, FRAENKEL, PARTFUN1,
      OPPCAT_1, GROUP_6, CAT_2, FUNCT_3, INDEX_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1,
      FUNCT_2, PARTFUN1, PBOOLE, FRAENKEL, MSUALG_1, PRALG_1, DTCONSTR, CAT_1,
      CAT_2, OPPCAT_1, COMMACAT, PRE_CIRC, CAT_5;
 constructors MSUALG_3, PRE_CIRC, OPPCAT_1, CAT_5, ISOCAT_1, DOMAIN_1;
 clusters FUNCT_1, RELSET_1, PRVECT_1, CAT_2, PBOOLE, PRALG_1, CAT_5, FUNCOP_1,
      CIRCCOMB, RELAT_1;
 requirements SUBSET, BOOLE;


begin :: Category Yielding Functions

definition let A be non empty set;
 cluster non empty-yielding ManySortedSet of A;
end;

definition let A be non empty set;
 cluster non-empty -> non empty-yielding ManySortedSet of A;
end;

definition
 let C be Categorial Category;
 let f be Morphism of C;
 redefine func f`2 -> Functor of f`11, f`12;
end;

theorem :: INDEX_1:1
   for C being Categorial Category, f,g being Morphism of C st
   dom g = cod f holds g*f = [[dom f, cod g], g`2*f`2];

theorem :: INDEX_1:2
 for C being Category, D,E being Categorial Category
 for F being Functor of C,D for G being Functor of C,E
   st F = G holds Obj F = Obj G;

definition let IT be Function;
 attr IT is Category-yielding means
:: INDEX_1:def 1

  for x being set st x in dom IT holds IT.x is Category;
end;

definition
 cluster Category-yielding Function;
end;

definition let X be set;
 cluster Category-yielding ManySortedSet of X;
end;

definition let A be set;
 mode ManySortedCategory of A is Category-yielding ManySortedSet of A;
end;

definition let C be Category;
 mode ManySortedSet of C is ManySortedSet of the Objects of C;
 mode ManySortedCategory of C is ManySortedCategory of the Objects of C;
end;

definition let X be set, x be Category;
 cluster X --> x -> Category-yielding;
end;

definition let X be non empty set;
 cluster -> non empty ManySortedSet of X;
end;

definition
 let f be Category-yielding Function;
 cluster rng f -> categorial;
end;

definition let X be non empty set;
 let f be ManySortedCategory of X;
 let x be Element of X;
 redefine func f.x -> Category;
end;

definition
 let f be Function;
 let g be Category-yielding Function;
 cluster g*f -> Category-yielding;
end;

:: Objects and Morphisms

definition let F be Category-yielding Function;
 func Objs F -> non-empty Function means
:: INDEX_1:def 2

  dom it = dom F &
  for x being set st x in dom F
   for C being Category st C = F.x holds it.x = the Objects of C;

 func Mphs F -> non-empty Function means
:: INDEX_1:def 3

  dom it = dom F &
  for x being set st x in dom F
   for C being Category st C = F.x holds it.x = the Morphisms of C;
end;

definition let A be non empty set;
 let F be ManySortedCategory of A;
 redefine
  func Objs F -> non-empty ManySortedSet of A;
  func Mphs F -> non-empty ManySortedSet of A;
end;

theorem :: INDEX_1:3
   for X being set, C being Category holds
  Objs (X --> C) = X --> the Objects of C &
  Mphs (X --> C) = X --> the Morphisms of C;

begin :: Pairs of Many Sorted Sets

definition let A,B be set;
 mode ManySortedSet of A,B means
:: INDEX_1:def 4

  ex f being (ManySortedSet of A), g being ManySortedSet of B st it = [f,g];
end;

definition let A,B be set;
 let f be ManySortedSet of A;
 let g be ManySortedSet of B;
 redefine func [f,g] -> ManySortedSet of A,B;
end;

definition let A, B be set;
 let X be ManySortedSet of A,B;
 redefine
  func X`1 -> ManySortedSet of A;
  func X`2 -> ManySortedSet of B;
end;

definition let A,B be set;
 let IT be ManySortedSet of A,B;
 attr IT is Category-yielding_on_first means
:: INDEX_1:def 5

  IT`1 is Category-yielding;
 attr IT is Function-yielding_on_second means
:: INDEX_1:def 6

  IT`2 is Function-yielding;
end;

definition let A,B be set;
 cluster Category-yielding_on_first Function-yielding_on_second
         ManySortedSet of A,B;
end;

definition let A, B be set;
 let X be Category-yielding_on_first ManySortedSet of A,B;
 redefine func X`1 -> ManySortedCategory of A;
end;

definition let A, B be set;
 let X be Function-yielding_on_second ManySortedSet of A,B;
 redefine func X`2 -> ManySortedFunction of B;
end;

definition let f be Function-yielding Function;
 cluster rng f -> functional;
end;

definition let A,B be set;
 let f be ManySortedCategory of A;
 let g be ManySortedFunction of B;
 redefine func [f,g] ->
  Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;
end;

definition
 let A be non empty set;
 let F,G be ManySortedCategory of A;
 mode ManySortedFunctor of F,G -> ManySortedFunction of A means
:: INDEX_1:def 7

  for a being Element of A holds it.a is Functor of F.a, G.a;
end;

scheme LambdaMSFr
 {A() -> non empty set, C1, C2() -> ManySortedCategory of A(),
  F(set) -> set}:
 ex F being ManySortedFunctor of C1(), C2() st
  for a being Element of A() holds F.a = F(a)
 provided
  for a being Element of A() holds F(a) is Functor of C1().a, C2().a;

definition
 let A be non empty set;
 let F,G be ManySortedCategory of A;
 let f be ManySortedFunctor of F,G;
 let a be Element of A;
 redefine func f.a -> Functor of F.a, G.a;
end;

begin :: Indexing

definition
 let A,B be non empty set;
 let F,G be Function of B,A;
 mode Indexing of F,G -> Category-yielding_on_first ManySortedSet of A,B
  means
:: INDEX_1:def 8

   it`2 is ManySortedFunctor of it`1*F, it`1*G;
end;

theorem :: INDEX_1:4
 for A,B being non empty set, F,G being Function of B,A
  for I being Indexing of F,G
   for m being Element of B holds I`2.m is Functor of I`1.(F.m), I`1.(G.m);

theorem :: INDEX_1:5
 for C being Category, I being Indexing of the Dom of C, the Cod of C
  for m being Morphism of C holds I`2.m is Functor of I`1.dom m, I`1.cod m;

definition
 let A,B be non empty set;
 let F,G be Function of B,A;
 let I be Indexing of F,G;
 redefine func I`2 -> ManySortedFunctor of I`1*F,I`1*G;
end;

definition
 let A,B be non empty set;
 let F,G be Function of B,A;
 let I be Indexing of F,G;
 mode TargetCat of I -> Categorial Category means
:: INDEX_1:def 9

  (for a being Element of A holds I`1.a is Object of it) &
  (for b being Element of B holds
       [[I`1.(F.b),I`1.(G.b)],I`2.b] is Morphism of it);
end;

definition
 let A,B be non empty set;
 let F,G be Function of B,A;
 let I be Indexing of F,G;
 cluster full strict TargetCat of I;
end;

definition
    :: This is very technical definition made for having the indexing and
    :: coindexing as the same mode.
 let A,B be non empty set;
 let F,G be Function of B,A;
 let c be PartFunc of [:B,B:], B;
 let i be Function of A,B;
 given C being Category such that
 C = CatStr(#A, B, F, G, c, i#);

 mode Indexing of F, G, c, i -> Indexing of F,G means
:: INDEX_1:def 10

  (for a being Element of A holds it`2.(i.a) = id (it`1.a)) &
  for m1, m2 being Element of B st F.m2 = G.m1 holds
   it`2.(c.[m2,m1]) = (it`2.m2)*(it`2.m1);
end;

definition let C be Category;
 mode Indexing of C is
   Indexing of the Dom of C, the Cod of C, the Comp of C, the Id of C;
 mode coIndexing of C is
   Indexing of the Cod of C, the Dom of C, ~(the Comp of C), the Id of C;
end;

theorem :: INDEX_1:6
 for C being Category, I being Indexing of the Dom of C, the Cod of C holds
  I is Indexing of C iff
   (for a being Object of C holds I`2.id a = id (I`1.a)) &
   for m1, m2 being Morphism of C st dom m2 = cod m1 holds
    I`2.(m2*m1) = (I`2.m2)*(I`2.m1);

theorem :: INDEX_1:7
 for C being Category, I being Indexing of the Cod of C, the Dom of C holds
  I is coIndexing of C iff
   (for a being Object of C holds I`2.id a = id (I`1.a)) &
   for m1, m2 being Morphism of C st dom m2 = cod m1 holds
    I`2.(m2*m1) = (I`2.m1)*(I`2.m2);

theorem :: INDEX_1:8
   for C being Category, x be set holds
  x is coIndexing of C iff x is Indexing of C opp;


theorem :: INDEX_1:9
   for C being Category, I being Indexing of C
  for c1,c2 being Object of C st Hom(c1,c2) is non empty
   for m being Morphism of c1,c2 holds I`2.m is Functor of I`1.c1, I`1.c2;

theorem :: INDEX_1:10
   for C being Category, I being coIndexing of C
  for c1,c2 being Object of C st Hom(c1,c2) is non empty
   for m being Morphism of c1,c2 holds I`2.m is Functor of I`1.c2, I`1.c1;

definition let C be Category;
 let I be Indexing of C;
 let T be TargetCat of I;
 func I-functor(C,T) -> Functor of C,T means
:: INDEX_1:def 11

  for f being Morphism of C holds it.f = [[I`1.dom f, I`1.cod f], I`2.f];
end;

theorem :: INDEX_1:11
 for C being Category, I being Indexing of C
  for T1,T2 being TargetCat of I holds
   I-functor(C,T1) = I-functor(C,T2) &
   Obj (I-functor(C,T1)) = Obj (I-functor(C,T2));

theorem :: INDEX_1:12
  for C being Category, I being Indexing of C
  for T being TargetCat of I holds Obj (I-functor(C,T)) = I`1;

theorem :: INDEX_1:13
   for C being Category, I being Indexing of C
  for T being TargetCat of I, x being Object of C holds
   (I-functor(C,T)).x = I`1.x;

definition let C be Category;
 let I be Indexing of C;
 func rng I -> strict TargetCat of I means
:: INDEX_1:def 12

  for T being TargetCat of I holds it = Image (I-functor(C,T));
end;

theorem :: INDEX_1:14
 for C being Category, I be Indexing of C
  for D being Categorial Category holds
   rng I is Subcategory of D iff D is TargetCat of I;

definition
 let C be Category;
 let I be Indexing of C;
 let m be Morphism of C;
 func I.m -> Functor of I`1.dom m, I`1.cod m equals
:: INDEX_1:def 13
     I`2.m;
end;

definition
 let C be Category;
 let I be coIndexing of C;
 let m be Morphism of C;
 func I.m -> Functor of I`1.cod m, I`1.dom m equals
:: INDEX_1:def 14
     I`2.m;
end;

theorem :: INDEX_1:15
   for C,D being Category holds
 [(the Objects of C) --> D, (the Morphisms of C) --> id D] is Indexing of C &
 [(the Objects of C) --> D, (the Morphisms of C) --> id D] is coIndexing of C;

begin :: Indexing vs Functor into Categorial Categories

definition let C be Category, D be Categorial Category;
 let F be Functor of C,D;
 cluster Obj F -> Category-yielding;
end;

theorem :: INDEX_1:16
 for C being Category, D being Categorial Category, F being Functor of C,D
 holds [Obj F, pr2 F] is Indexing of C;

definition let C be Category;
 let D be Categorial Category;
 let F be Functor of C,D;
 func F-indexing_of C -> Indexing of C equals
:: INDEX_1:def 15

   [Obj F, pr2 F];
end;

theorem :: INDEX_1:17
   for C being Category, D being Categorial Category, F being Functor of C,D
   holds D is TargetCat of F-indexing_of C;


theorem :: INDEX_1:18
 for C being Category, D being Categorial Category, F being Functor of C,D
 for T being TargetCat of F-indexing_of C holds
     F = (F-indexing_of C)-functor(C,T);

theorem :: INDEX_1:19
 for C being Category, D,E being Categorial Category
 for F being Functor of C,D for G being Functor of C,E st F = G
   holds F-indexing_of C = G-indexing_of C;


theorem :: INDEX_1:20
 for C being Category, I being (Indexing of C), T being TargetCat of I holds
    pr2 (I-functor(C,T)) = I`2;

theorem :: INDEX_1:21
   for C being Category, I being (Indexing of C), T being TargetCat of I holds
  (I-functor(C,T))-indexing_of C = I;

begin

definition
 let C,D,E be Category;
 let F be Functor of C,D;
 let I be Indexing of E; assume
     Image F is Subcategory of E;
 func I*F -> Indexing of C means
:: INDEX_1:def 16

 for F' being Functor of C,E st F' = F holds
  it = (I-functor(E,rng I)*F')-indexing_of C;
end;

theorem :: INDEX_1:22
 for C,D1,D2,E being Category, I being Indexing of E
 for F being Functor of C,D1 for G being Functor of C,D2
  st Image F is Subcategory of E & Image G is Subcategory of E & F = G
  holds I*F = I*G;

theorem :: INDEX_1:23
 for C,D being Category, F being Functor of C,D, I being Indexing of D
 for T being TargetCat of I holds
   I*F = ((I-functor(D,T))*F)-indexing_of C;

theorem :: INDEX_1:24
 for C,D being Category, F being Functor of C,D, I being Indexing of D
 for T being TargetCat of I holds
   T is TargetCat of I*F;

theorem :: INDEX_1:25
   for C,D being Category, F being Functor of C,D, I being Indexing of D
 for T being TargetCat of I holds
   rng (I*F) is Subcategory of T;

theorem :: INDEX_1:26
 for C,D,E being Category, F being Functor of C,D
 for G being Functor of D,E, I being Indexing of E holds
  (I*G)*F = I*(G*F);

definition
 let C be Category;
 let I be Indexing of C;
 let D be Categorial Category such that
   D is TargetCat of I;
 let E be Categorial Category;
 let F be Functor of D,E;
 func F*I -> Indexing of C means
:: INDEX_1:def 17

 for T being TargetCat of I, G being Functor of T,E st T = D & G = F holds
  it = (G*(I-functor(C,T)))-indexing_of C;
end;

theorem :: INDEX_1:27
 for C being Category, I being Indexing of C
 for T being TargetCat of I, D,E being Categorial Category
 for F being Functor of T,D for G being Functor of T,E
  st F = G holds F*I = G*I;

theorem :: INDEX_1:28
 for C being Category, I being Indexing of C
 for T being TargetCat of I, D being Categorial Category
 for F being Functor of T,D holds
   Image F is TargetCat of F*I;

theorem :: INDEX_1:29
 for C being Category, I being Indexing of C
 for T being TargetCat of I, D being Categorial Category
 for F being Functor of T,D holds
   D is TargetCat of F*I;


theorem :: INDEX_1:30
   for C being Category, I being Indexing of C
 for T being TargetCat of I, D being Categorial Category
 for F being Functor of T,D holds
   rng (F*I) is Subcategory of Image F;

theorem :: INDEX_1:31
   for C be Category, I being Indexing of C for T being TargetCat of I
 for D,E being Categorial Category, F being Functor of T,D
 for G being Functor of D,E holds
  (G*F)*I = G*(F*I);

definition
 let C,D be Category;
 let I1 be Indexing of C;
 let I2 be Indexing of D;
 func I2*I1 -> Indexing of C equals
:: INDEX_1:def 18

   I2*(I1-functor(C,rng I1));
end;

theorem :: INDEX_1:32
 for C being Category, D being Categorial Category, I1 being Indexing of C
 for I2 being Indexing of D for T being TargetCat of I1
   st D is TargetCat of I1 holds I2*I1 = I2*(I1-functor(C,T));

theorem :: INDEX_1:33
   for C being Category, D being Categorial Category, I1 being Indexing of C
 for I2 being Indexing of D for T being TargetCat of I2
   st D is TargetCat of I1 holds I2*I1 = (I2-functor(D,T))*I1;

theorem :: INDEX_1:34
 for C,D being Category, F being Functor of C,D, I being Indexing of D
 for T being TargetCat of I, E being Categorial Category
 for G being Functor of T,E holds
  (G*I)*F = G*(I*F);

theorem :: INDEX_1:35
   for C being Category, I being Indexing of C
 for T being TargetCat of I, D being Categorial Category
 for F being Functor of T,D, J being Indexing of D holds
  (J*F)*I = J*(F*I);

theorem :: INDEX_1:36
   for C being Category, I being Indexing of C
 for T1 being TargetCat of I, J being Indexing of T1
 for T2 being TargetCat of J
 for D being Categorial Category, F being Functor of T2,D holds
  (F*J)*I = F*(J*I);

theorem :: INDEX_1:37
 for C,D being Category, F being Functor of C,D, I being Indexing of D
 for T being TargetCat of I, J being Indexing of T holds
  (J*I)*F = J*(I*F);

theorem :: INDEX_1:38
   for C being Category, I being Indexing of C
 for D being TargetCat of I, J being Indexing of D
 for E being TargetCat of J, K being Indexing of E holds
  (K*J)*I = K*(J*I);