:: Indexed Category
::  by Grzegorz Bancerek
::
:: Received June 8, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, RELAT_1, PBOOLE, SUBSET_1, CAT_5, CAT_1, MCART_1,
      GRCAT_1, GRAPH_1, STRUCT_0, FUNCT_1, FUNCOP_1, PARTFUN1, ZFMISC_1,
      ARYTM_0, TARSKI, GROUP_6, CAT_2, FUNCT_3, INDEX_1, MONOID_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1,
      RELAT_1, FUNCT_1, BINOP_1, PARTFUN1, PBOOLE, FUNCOP_1, FUNCT_2, FUNCT_4,
      STRUCT_0, GRAPH_1, CAT_1, CAT_2, OPPCAT_1, CAT_5, ISOCAT_1;
 constructors DOMAIN_1, OPPCAT_1, CAT_5, RELSET_1, PBOOLE, XTUPLE_0, ISOCAT_1,
      REALSET1, XFAMILY, FUNCT_4;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, PBOOLE, CAT_2, CAT_5,
      STRUCT_0, RELSET_1, CAT_1, XTUPLE_0, OPPCAT_1;
 requirements SUBSET, BOOLE;


begin :: Category Yielding Functions

registration
  let A be non empty set;
  cluster non empty-yielding for 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;

registration
  cluster Category-yielding for Function;
end;

registration
  let X be set;
  cluster Category-yielding for 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 ManySortedCategory of C is ManySortedCategory of the carrier of C;
end;

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

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

registration
  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;

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

:: carrier 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 object st x in dom F
  for C being Category st C = F.x holds it.x = the carrier of C;
  func Mphs F -> non-empty Function means
:: INDEX_1:def 3

  dom it = dom F & for x being object st x in dom F
  for C being Category st C = F.x holds it.x = the carrier' of
  C;
end;

registration
  let A be non empty set;
  let F be ManySortedCategory of A;
  cluster Objs F -> A-defined;
  cluster Mphs F -> A-defined;
end;

registration
  let A be non empty set;
  let F be ManySortedCategory of A;
  cluster Objs F -> total;
  cluster Mphs F -> total;
end;

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

begin :: Pairs of Many Sorted Sets

definition
  let A,B be set;
  mode ManySortedSet of A,B -> object 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;

registration
  let A, B be set;
  let X be ManySortedSet of A,B;
  cluster X`1 -> Function-like Relation-like for set;
  cluster X`2 -> Function-like Relation-like for set;
end;

registration
  let A, B be set;
  let X be ManySortedSet of A,B;
  cluster X`1 -> A-defined for Relation;
  cluster X`2 -> B-defined for Relation;
end;

registration
  let A, B be set;
  let X be ManySortedSet of A,B;
  cluster X`1 -> total for A-defined Function;
  cluster X`2 -> total for B-defined Function;
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;

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

registration
  let A, B be set;
  let X be Category-yielding_on_first ManySortedSet of A,B;
  cluster X`1 -> Category-yielding for Function;
end;

registration
  let A, B be set;
  let X be Function-yielding_on_second ManySortedSet of A,B;
  cluster X`2 ->  Function-yielding for Function;
end;

registration
  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 :: INDEX_1:sch 1
  LambdaMSFr {A() -> non empty set, C1, C2() -> ManySortedCategory of A(), F(
object) -> 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 Source of C, the Target
  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;

registration
  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 for 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#);
  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 Source of C, the Target of C, the Comp
    of C, IdMap C;
  mode coIndexing of C is
    Indexing of the Target of C, the Source of C, ~(the Comp of C), IdMap C;
end;

theorem :: INDEX_1:6
  for C being Category, I being Indexing of the Source of C, the
Target 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 Target of C, the
Source 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 carrier of C) --> D, (the carrier'
of C) --> id D] is Indexing of C & [(the carrier of C) --> D, (the carrier' of
  C) --> id D] is coIndexing of C;

begin :: Indexing vs Functor into Categorial Categories

registration
  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 F9 being Functor of C,E st F9 =
  F holds it = (I-functor(E,rng I)*F9)-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);

theorem :: INDEX_1:39
 for C being Category holds IdMap C = IdMap(C opp);