Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### 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);

```

Back to top