environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, FUNCT_1, PBOOLE, CAT_5, FUNCOP_1, FUNCT_2;
theorems MCART_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PARTFUN1, FUNCT_4, CAT_1, CAT_2, OPPCAT_1, CAT_5, RELSET_1, ISOCAT_1;
schemes CLASSES1, PBOOLE, CAT_5;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, PBOOLE, CAT_2, CAT_5, STRUCT_0, RELSET_1, CAT_1, XTUPLE_0, OPPCAT_1;
constructors HIDDEN, DOMAIN_1, OPPCAT_1, CAT_5, RELSET_1, PBOOLE, XTUPLE_0, ISOCAT_1, REALSET1, XFAMILY, FUNCT_4;
requirements HIDDEN, SUBSET, BOOLE;
equalities CAT_1, BINOP_1, GRAPH_1, OPPCAT_1;
expansions FUNCT_1, FUNCT_2;
Lm1:
now for A, B being non empty set
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 A,
B be non
empty set ;
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;
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;
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;
( ( 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 2;
hence
for
a being
Element of
A holds
(I `1) . a is
Object of
C
by A1, FUNCT_1:def 3;
for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of Clet b be
Element of
B;
[[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of CA3:
(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 3;
hence
[[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is
Morphism of
C
by A3, CAT_5:def 8;
verum
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 #)
;
existence
ex b1 being Indexing of F,G st
( ( for a being Element of A holds (b1 `2) . (i . a) = id ((b1 `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b1 `2) . (c . [m2,m1]) = ((b1 `2) . m2) * ((b1 `2) . m1) ) )
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 #) holds
for b7 being Indexing of F,G holds
( b7 is Indexing of F,G,c,i iff ( ( for a being Element of A holds (b7 `2) . (i . a) = id ((b7 `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b7 `2) . (c . [m2,m1]) = ((b7 `2) . m2) * ((b7 `2) . m1) ) ) );
Lm2:
for C being Category holds IdMap C = IdMap (C opp)
Lm3:
for C being Category
for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1
Lm4:
now for C, D being Category
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
let C,
D be
Category;
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) . mset 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;
([( 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 2;
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:12
.=
( the carrier of C --> D) . ( the Source of C . m)
.=
D
by FUNCOP_1:7
;
dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the
carrier' of
C
by PARTFUN1:def 2;
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:12
.=
( the carrier of C --> D) . ( the Target of C . m)
.=
D
by FUNCOP_1:7
;
([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m =
( the carrier' of C --> (id D)) . m
.=
id D
by FUNCOP_1:7
;
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;
verum
end;
Lm5:
now for C, D being Category
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
let C,
D be
Category;
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) . mset 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;
([( 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 2;
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:12
.=
( the carrier of C --> D) . ( the Source of C . m)
.=
D
by FUNCOP_1:7
;
dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the
carrier' of
C
by PARTFUN1:def 2;
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:12
.=
( the carrier of C --> D) . ( the Target of C . m)
.=
D
by FUNCOP_1:7
;
([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m =
( the carrier' of C --> (id D)) . m
.=
id D
by FUNCOP_1:7
;
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;
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
;
existence
ex b1 being Indexing of C st
for F9 being Functor of C,E st F9 = F holds
b1 = ((I -functor (E,(rng I))) * F9) -indexing_of C
uniqueness
for b1, b2 being Indexing of C st ( for F9 being Functor of C,E st F9 = F holds
b1 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) & ( for F9 being Functor of C,E st F9 = F holds
b2 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) holds
b1 = b2
end;