:: Indexed Category
:: by Grzegorz Bancerek
::
:: Received June 8, 1995
:: Copyright (c) 1995-2011 Association of Mizar Users

begin

registration

let A be non empty set ;
cluster Relation-like V3() A -defined Function-like non empty total set ;
existence
not for b₁ being ManySortedSet of A holds b₁ is empty-yielding

proof end;

end;

definition

let C be Categorial Category;
let f be Morphism of C;
:: original: `2
redefine func f `2 -> Functor of f `11 ,f `12 ;
coherence
f `2 is Functor of f `11 ,f `12

proof end;

end;

theorem :: INDEX_1:1

for C being Categorial Category
for f, g being Morphism of C st dom g = cod f holds
g * f = [[(dom f),(cod g)],((g `2) * (f `2))]

proof end;

theorem Th2: :: INDEX_1:2

for C being Category
for 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

proof end;

definition

let IT be Function;
attr IT is Category-yielding means :Def1: :: INDEX_1:def 1
for x being set st x in dom IT holds
IT . x is Category;

end;

:: deftheorem Def1 defines Category-yielding INDEX_1:def 1 :
for IT being Function holds
( IT is Category-yielding iff for x being set st x in dom IT holds
IT . x is Category );

registration

cluster Relation-like Function-like Category-yielding set ;
existence
ex b₁ being Function st b₁ is Category-yielding

proof end;

end;

registration

let X be set ;
cluster Relation-like X -defined Function-like total Category-yielding set ;
existence
ex b₁ being ManySortedSet of X st b₁ is Category-yielding

proof end;

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 carrier of C;
mode ManySortedCategory of C is ManySortedCategory of the carrier of C;

end;

registration

let X be set ;
let x be Category;
cluster X --> x -> Category-yielding ;
coherence
X --> x is Category-yielding

proof end;

end;

registration

let X be non empty set ;
cluster Relation-like X -defined Function-like total -> non empty set ;
coherence
for b₁ being ManySortedSet of X holds not b₁ is empty ;

end;

registration

let f be Category-yielding Function;
cluster proj2 f -> categorial ;
coherence
rng f is categorial

proof end;

end;

definition

let X be non empty set ;
let f be ManySortedCategory of X;
let x be Element of X;
:: original: .
redefine func f . x -> Category;
coherence
f . x is Category

proof end;

end;

registration

let f be Function;
let g be Category-yielding Function;
cluster f * g -> Category-yielding ;
coherence
g * f is Category-yielding

proof end;

end;

definition

let F be Category-yielding Function;
func Objs F -> non-empty Function means :Def2: :: INDEX_1:def 2
( dom it = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
it . x = the carrier of C ) );
existence
ex b₁ being non-empty Function st
( dom b₁ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₁ . x = the carrier of C ) )

proof end;

uniqueness
for b₁, b₂ being non-empty Function st dom b₁ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₁ . x = the carrier of C ) & dom b₂ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₂ . x = the carrier of C ) holds
b₁ = b₂

proof end;

func Mphs F -> non-empty Function means :Def3: :: INDEX_1:def 3
( dom it = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
it . x = the carrier' of C ) );
existence
ex b₁ being non-empty Function st
( dom b₁ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₁ . x = the carrier' of C ) )

proof end;

uniqueness
for b₁, b₂ being non-empty Function st dom b₁ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₁ . x = the carrier' of C ) & dom b₂ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₂ . x = the carrier' of C ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Objs INDEX_1:def 2 :
for F being Category-yielding Function
for b₂ being non-empty Function holds
( b₂ = Objs F iff ( dom b₂ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₂ . x = the carrier of C ) ) );

:: deftheorem Def3 defines Mphs INDEX_1:def 3 :
for F being Category-yielding Function
for b₂ being non-empty Function holds
( b₂ = Mphs F iff ( dom b₂ = dom F & ( for x being set st x in dom F holds
for C being Category st C = F . x holds
b₂ . x = the carrier' of C ) ) );

registration

let A be non empty set ;
let F be ManySortedCategory of A;
cluster Objs F -> non-empty A -defined ;
coherence
Objs F is A -defined

proof end;

cluster Mphs F -> non-empty A -defined ;
coherence
Mphs F is A -defined

proof end;

end;

registration

let A be non empty set ;
let F be ManySortedCategory of A;
cluster Objs F -> non-empty total ;
coherence
Objs F is total

proof end;

cluster Mphs F -> non-empty total ;
coherence
Mphs F is total

proof end;

end;

theorem :: INDEX_1:3

for X being set
for C being Category holds
( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )

proof end;

begin

definition

let A, B be set ;
mode ManySortedSet of A,B -> set means :Def4: :: INDEX_1:def 4
ex f being ManySortedSet of A ex g being ManySortedSet of B st it = [f,g];
existence
ex b₁ being set ex f being ManySortedSet of A ex g being ManySortedSet of B st b₁ = [f,g]

proof end;

end;

:: deftheorem Def4 defines ManySortedSet INDEX_1:def 4 :
for A, B being set
for b₃ being set holds
( b₃ is ManySortedSet of A,B iff ex f being ManySortedSet of A ex g being ManySortedSet of B st b₃ = [f,g] );

definition

let A, B be set ;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
:: original: [
redefine func [f,g] -> ManySortedSet of A,B;
coherence
[f,g] is ManySortedSet of A,B

proof end;

end;

registration

let A, B be set ;
let X be ManySortedSet of A,B;
cluster X `1 -> Relation-like Function-like ;
coherence
( X `1 is Function-like & X `1 is Relation-like )

proof end;

cluster X `2 -> Relation-like Function-like ;
coherence
( X `2 is Function-like & X `2 is Relation-like )

proof end;

end;

registration

let A, B be set ;
let X be ManySortedSet of A,B;
cluster X `1 -> A -defined ;
coherence
X `1 is A -defined

proof end;

cluster X `2 -> B -defined ;
coherence
X `2 is B -defined

proof end;

end;

registration

let A, B be set ;
let X be ManySortedSet of A,B;
cluster X `1 -> A -defined total A -defined Function;
coherence
for b<sub>1</sub> being A -defined Function st b<sub>1</sub> = X `1 holds
b₁ is total

proof end;

cluster X `2 -> B -defined total B -defined Function;
coherence
for b<sub>1</sub> being B -defined Function st b<sub>1</sub> = X `2 holds
b₁ is total

proof end;

end;

definition

let A, B be set ;
let IT be ManySortedSet of A,B;
attr IT is Category-yielding_on_first means :Def5: :: INDEX_1:def 5
IT `1 is Category-yielding ;
attr IT is Function-yielding_on_second means :Def6: :: INDEX_1:def 6
IT `2 is Function-yielding ;

end;

:: deftheorem Def5 defines Category-yielding_on_first INDEX_1:def 5 :
for A, B being set
for IT being ManySortedSet of A,B holds
( IT is Category-yielding_on_first iff IT `1 is Category-yielding );

:: deftheorem Def6 defines Function-yielding_on_second INDEX_1:def 6 :
for A, B being set
for IT being ManySortedSet of A,B holds
( IT is Function-yielding_on_second iff IT `2 is Function-yielding );

registration

let A, B be set ;
cluster Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;
existence
ex b₁ being ManySortedSet of A,B st
( b₁ is Category-yielding_on_first & b₁ is Function-yielding_on_second )

proof end;

end;

registration

let A, B be set ;
let X be Category-yielding_on_first ManySortedSet of A,B;
cluster X `1 -> Category-yielding ;
coherence
X `1 is Category-yielding by Def5;

end;

registration

let A, B be set ;
let X be Function-yielding_on_second ManySortedSet of A,B;
cluster X `2 -> Function-yielding ;
coherence
X `2 is Function-yielding by Def6;

end;

registration

let f be Function-yielding Function;
cluster proj2 f -> functional ;
coherence
rng f is functional

proof end;

end;

definition

let A, B be set ;
let f be ManySortedCategory of A;
let g be ManySortedFunction of B;
:: original: [
redefine func [f,g] -> Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;
coherence
[f,g] is Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B

proof end;

end;

definition

let A be non empty set ;
let F, G be ManySortedCategory of A;
mode ManySortedFunctor of F,G -> ManySortedFunction of A means :Def7: :: INDEX_1:def 7
for a being Element of A holds it . a is Functor of F . a,G . a;
existence
ex b₁ being ManySortedFunction of A st
for a being Element of A holds b₁ . a is Functor of F . a,G . a

proof end;

end;

:: deftheorem Def7 defines ManySortedFunctor INDEX_1:def 7 :
for A being non empty set
for F, G being ManySortedCategory of A
for b₄ being ManySortedFunction of A holds
( b₄ is ManySortedFunctor of F,G iff for a being Element of A holds b₄ . a is Functor of F . a,G . a );

scheme :: INDEX_1:sch 1
LambdaMSFr{ F₁() -> non empty set , F₂() -> ManySortedCategory of F₁(), F₃() -> ManySortedCategory of F₁(), F₄( set ) -> set } :

ex F being ManySortedFunctor of F₂(),F₃() st
for a being Element of F₁() holds F . a = F₄(a)

provided

A1: for a being Element of F₁() holds F₄(a) is Functor of F₂() . a,F₃() . a

proof end;

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;
:: original: .
redefine func f . a -> Functor of F . a,G . a;
coherence
f . a is Functor of F . a,G . a by Def7;

end;

begin

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 :Def8: :: INDEX_1:def 8
it `2 is ManySortedFunctor of (it `1) * F,(it `1) * G;
existence
ex b<sub>1</sub> being Category-yielding_on_first ManySortedSet of A,B st b<sub>1</sub> `2 is ManySortedFunctor of (b₁ `1) * F,(b<sub>1</sub> `1) * G

proof end;

end;

:: deftheorem Def8 defines Indexing INDEX_1:def 8 :
for A, B being non empty set
for F, G being Function of B,A
for b₅ being Category-yielding_on_first ManySortedSet of A,B holds
( b₅ is Indexing of F,G iff b₅ `2 is ManySortedFunctor of (b<sub>5</sub> `1) * F,(b₅ `1) * G );

theorem Th4: :: INDEX_1:4

for A, B being non empty set
for 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)

proof end;

theorem :: INDEX_1:5

for C being Category
for 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) by Th4;

definition

let A, B be non empty set ;
let F, G be Function of B,A;
let I be Indexing of F,G;
:: original: `2
redefine func I `2 -> ManySortedFunctor of (I `1) * F,(I `1) * G;
coherence
I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G by Def8;

end;

Lm1: now

let A, B be non empty set ; :: thesis: for F, G being Function of B,A
for I being Indexing of F,G ex C being strict Categorial full Category st
( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )
let F, G be Function of B,A; :: thesis: for I being Indexing of F,G ex C being strict Categorial full Category st
( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )
let I be Indexing of F,G; :: thesis: ex C being strict Categorial full Category st
( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )
consider C being strict Categorial full Category such that
A1: the carrier of C = rng (I `1) by CAT_5:20;
take C = C; :: thesis: ( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )
A2: dom (I `1) = A by PARTFUN1:def 4;
hence for a being Element of A holds (I `1) . a is Object of C by A1, FUNCT_1:def 5; :: thesis: for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C
let b be Element of B; :: thesis: [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C
A3: (I `2) . b is Functor of (I `1) . (F . b),(I `1) . (G . b) by Th4;
( (I `1) . (F . b) is Object of C & (I `1) . (G . b) is Object of C ) by A2, A1, FUNCT_1:def 5;
hence [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C by A3, CAT_5:def 8; :: thesis: verum

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 :Def9: :: 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 ) );
existence
ex b₁ being Categorial Category st
( ( for a being Element of A holds (I `1) . a is Object of b<sub>1</sub> ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b₁ ) )

proof end;

end;

:: deftheorem Def9 defines TargetCat INDEX_1:def 9 :
for A, B being non empty set
for F, G being Function of B,A
for I being Indexing of F,G
for b₆ being Categorial Category holds
( b₆ is TargetCat of I iff ( ( for a being Element of A holds (I `1) . a is Object of b<sub>6</sub> ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b₆ ) ) );

registration

let A, B be non empty set ;
let F, G be Function of B,A;
let I be Indexing of F,G;
cluster non empty non void strict Category-like with_triple-like_morphisms Categorial full TargetCat of I;
existence
ex b₁ being TargetCat of I st
( b₁ is full & b₁ is strict )

proof end;

end;

definition

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 A1: C = CatStr(# A,B,F,G,c,i #) ;
mode Indexing of F,G,c,i -> Indexing of F,G means :Def10: :: 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) ) );
existence
ex b<sub>1</sub> being Indexing of F,G st
( ( for a being Element of A holds (b<sub>1</sub> `2) . (i . a) = id ((b₁ `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b<sub>1</sub> `2) . (c . [m2,m1]) = ((b₁ `2) . m2) * ((b<sub>1</sub> `2) . m1) ) )

proof end;

end;

:: deftheorem Def10 defines Indexing INDEX_1:def 10 :
for A, B being non empty set
for F, G being Function of B,A
for c being PartFunc of [:B,B:],B
for i being Function of A,B st ex C being Category st C = CatStr(# A,B,F,G,c,i #) holds
for b₇ being Indexing of F,G holds
( b₇ is Indexing of F,G,c,i iff ( ( for a being Element of A holds (b₇ `2) . (i . a) = id ((b<sub>7</sub> `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b₇ `2) . (c . [m2,m1]) = ((b<sub>7</sub> `2) . m2) * ((b₇ `2) . m1) ) ) );

definition

let C be Category;
mode Indexing of C is Indexing of the Source of C, the Target of C, the Comp of C, the Id of C;
mode coIndexing of C is Indexing of the Target of C, the Source of C, ~ the Comp of C, the Id of C;

end;

theorem Th6: :: INDEX_1:6

for C being Category
for 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) ) ) )

proof end;

theorem Th7: :: INDEX_1:7

for C being Category
for 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) ) ) )

proof end;

theorem :: INDEX_1:8

for C being Category
for x being set holds
( x is coIndexing of C iff x is Indexing of (C opp) )

proof end;

theorem :: INDEX_1:9

for C being Category
for I being Indexing of C
for c1, c2 being Object of C st not Hom (c1,c2) is empty holds
for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c1,(I `1) . c2

proof end;

theorem :: INDEX_1:10

for C being Category
for I being coIndexing of C
for c1, c2 being Object of C st not Hom (c1,c2) is empty holds
for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c2,(I `1) . c1

proof end;

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 :Def11: :: INDEX_1:def 11
for f being Morphism of C holds it . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)];
existence
ex b<sub>1</sub> being Functor of C,T st
for f being Morphism of C holds b<sub>1</sub> . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)]

proof end;

uniqueness
for b₁, b₂ being Functor of C,T st ( for f being Morphism of C holds b₁ . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) & ( for f being Morphism of C holds b<sub>2</sub> . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines -functor INDEX_1:def 11 :
for C being Category
for I being Indexing of C
for T being TargetCat of I
for b₄ being Functor of C,T holds
( b₄ = I -functor (C,T) iff for f being Morphism of C holds b₄ . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] );

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

proof end;

theorem Th11: :: INDEX_1:11

for C being Category
for 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)) )

proof end;

theorem :: INDEX_1:12

for C being Category
for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1 by Lm2;

theorem :: INDEX_1:13

for C being Category
for I being Indexing of C
for T being TargetCat of I
for x being Object of C holds (I -functor (C,T)) . x = (I `1) . x by Lm2;

definition

let C be Category;
let I be Indexing of C;
func rng I -> strict TargetCat of I means :Def12: :: INDEX_1:def 12
for T being TargetCat of I holds it = Image (I -functor (C,T));
uniqueness
for b₁, b₂ being strict TargetCat of I st ( for T being TargetCat of I holds b₁ = Image (I -functor (C,T)) ) & ( for T being TargetCat of I holds b₂ = Image (I -functor (C,T)) ) holds
b₁ = b₂

proof end;

existence
ex b₁ being strict TargetCat of I st
for T being TargetCat of I holds b₁ = Image (I -functor (C,T))

proof end;

end;

:: deftheorem Def12 defines rng INDEX_1:def 12 :
for C being Category
for I being Indexing of C
for b₃ being strict TargetCat of I holds
( b₃ = rng I iff for T being TargetCat of I holds b₃ = Image (I -functor (C,T)) );

theorem Th14: :: INDEX_1:14

for C being Category
for I being Indexing of C
for D being Categorial Category holds
( rng I is Subcategory of D iff D is TargetCat of I )

proof end;

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;
coherence
(I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m)

proof end;

end;

:: deftheorem defines . INDEX_1:def 13 :
for C being Category
for I being Indexing of C
for m being Morphism of C holds I . m = (I `2) . m;

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;
coherence
(I `2) . m is Functor of (I `1) . (cod m),(I `1) . (dom m)

proof end;

end;

:: deftheorem defines . INDEX_1:def 14 :
for C being Category
for I being coIndexing of C
for m being Morphism of C holds I . m = (I `2) . m;

Lm3: now

let C, D be Category; :: thesis: for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m
set F = the carrier of C --> D;
set G = the carrier' of C --> (id D);
set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];
let m be Morphism of C; :: thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m
dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def 4;
then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:22
.= ( the carrier of C --> D) . ( the Source of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def 4;
then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:22
.= ( the carrier of C --> D) . ( the Target of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m by MCART_1:7
.= id D by FUNCOP_1:13 ;
hence ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m by A1, A2; :: thesis: verum

end;

Lm4: now

let C, D be Category; :: thesis: for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m
set F = the carrier of C --> D;
set G = the carrier' of C --> (id D);
set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];
let m be Morphism of C; :: thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m
dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def 4;
then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:22
.= ( the carrier of C --> D) . ( the Source of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def 4;
then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:22
.= ( the carrier of C --> D) . ( the Target of C . m) by MCART_1:7
.= D by FUNCOP_1:13 ;
([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m by MCART_1:7
.= id D by FUNCOP_1:13 ;
hence ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m by A1, A2; :: thesis: verum

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 )

proof end;

begin

registration

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

proof end;

end;

theorem Th16: :: INDEX_1:16

for C being Category
for D being Categorial Category
for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C

proof end;

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)];
coherence
[(Obj F),(pr2 F)] is Indexing of C by Th16;

end;

:: deftheorem defines -indexing_of INDEX_1:def 15 :
for C being Category
for D being Categorial Category
for F being Functor of C,D holds F -indexing_of C = [(Obj F),(pr2 F)];

theorem :: INDEX_1:17

for C being Category
for D being Categorial Category
for F being Functor of C,D holds D is TargetCat of F -indexing_of C

proof end;

theorem Th18: :: INDEX_1:18

for C being Category
for D being Categorial Category
for F being Functor of C,D
for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)

proof end;

theorem :: INDEX_1:19

for C being Category
for 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 by Th2;

theorem Th20: :: INDEX_1:20

for C being Category
for I being Indexing of C
for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2

proof end;

theorem :: INDEX_1:21

for C being Category
for I being Indexing of C
for T being TargetCat of I holds (I -functor (C,T)) -indexing_of C = I

proof end;

begin

Lm5: now

let c, d be Category; :: thesis: for e being Subcategory of d
for f being Functor of c,e holds f is Functor of c,d
let e be Subcategory of d; :: thesis: for f being Functor of c,e holds f is Functor of c,d
let f be Functor of c,e; :: thesis: f is Functor of c,d
(incl e) * f = (id e) * f by CAT_2:def 5
.= f by FUNCT_2:23 ;
hence f is Functor of c,d ; :: thesis: verum

end;

definition

let C, D, E be Category;
let F be Functor of C,D;
let I be Indexing of E;
assume A1: Image F is Subcategory of E ;
func I * F -> Indexing of C means :Def16: :: 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;
existence
ex b₁ being Indexing of C st
for F9 being Functor of C,E st F9 = F holds
b₁ = ((I -functor (E,(rng I))) * F9) -indexing_of C

proof end;

uniqueness
for b₁, b₂ being Indexing of C st ( for F9 being Functor of C,E st F9 = F holds
b₁ = ((I -functor (E,(rng I))) * F9) -indexing_of C ) & ( for F9 being Functor of C,E st F9 = F holds
b₂ = ((I -functor (E,(rng I))) * F9) -indexing_of C ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines * INDEX_1:def 16 :
for C, D, E being Category
for F being Functor of C,D
for I being Indexing of E st Image F is Subcategory of E holds
for b₆ being Indexing of C holds
( b₆ = I * F iff for F9 being Functor of C,E st F9 = F holds
b₆ = ((I -functor (E,(rng I))) * F9) -indexing_of C );

theorem Th22: :: INDEX_1:22

for C, D1, D2, E being Category
for 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

proof end;

theorem Th23: :: INDEX_1:23

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

proof end;

theorem Th24: :: INDEX_1:24

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I holds T is TargetCat of I * F

proof end;

theorem :: INDEX_1:25

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

proof end;

theorem Th26: :: INDEX_1:26

for C, D, E being Category
for F being Functor of C,D
for G being Functor of D,E
for I being Indexing of E holds (I * G) * F = I * (G * F)

proof end;

definition

let C be Category;
let I be Indexing of C;
let D be Categorial Category;
assume A1: D is TargetCat of I ;
let E be Categorial Category;
let F be Functor of D,E;
func F * I -> Indexing of C means :Def17: :: INDEX_1:def 17
for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
it = (G * (I -functor (C,T))) -indexing_of C;
existence
ex b₁ being Indexing of C st
for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b₁ = (G * (I -functor (C,T))) -indexing_of C

proof end;

uniqueness
for b₁, b₂ being Indexing of C st ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b₁ = (G * (I -functor (C,T))) -indexing_of C ) & ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b₂ = (G * (I -functor (C,T))) -indexing_of C ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines * INDEX_1:def 17 :
for C being Category
for I being Indexing of C
for D being Categorial Category st D is TargetCat of I holds
for E being Categorial Category
for F being Functor of D,E
for b₆ being Indexing of C holds
( b₆ = F * I iff for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b₆ = (G * (I -functor (C,T))) -indexing_of C );

theorem Th27: :: INDEX_1:27

for C being Category
for I being Indexing of C
for T being TargetCat of I
for 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

proof end;

theorem Th28: :: INDEX_1:28

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D holds Image F is TargetCat of F * I

proof end;

theorem Th29: :: INDEX_1:29

for C being Category
for I being Indexing of C
for T being TargetCat of I
for D being Categorial Category
for F being Functor of T,D holds D is TargetCat of F * I

proof end;

theorem :: INDEX_1:30

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

proof end;

theorem :: INDEX_1:31

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

proof end;

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)));
correctness
coherence
I2 * (I1 -functor (C,(rng I1))) is Indexing of C;
;

end;

:: deftheorem defines * INDEX_1:def 18 :
for C, D being Category
for I1 being Indexing of C
for I2 being Indexing of D holds I2 * I1 = I2 * (I1 -functor (C,(rng I1)));

theorem Th32: :: INDEX_1:32

for C being Category
for D being Categorial Category
for 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))

proof end;

theorem :: INDEX_1:33

for C being Category
for D being Categorial Category
for 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

proof end;

theorem Th34: :: INDEX_1:34

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

proof end;

theorem :: INDEX_1:35

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

proof end;

theorem :: INDEX_1:36

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

proof end;

theorem Th37: :: INDEX_1:37

for C, D being Category
for F being Functor of C,D
for I being Indexing of D
for T being TargetCat of I
for J being Indexing of T holds (J * I) * F = J * (I * F)

proof end;

theorem :: INDEX_1:38

for C being Category
for I being Indexing of C
for D being TargetCat of I
for J being Indexing of D
for E being TargetCat of J
for K being Indexing of E holds (K * J) * I = K * (J * I)

proof end;