:: Indexed Category
:: by Grzegorz Bancerek
::
:: Received June 8, 1995
:: Copyright (c) 1995-2026 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;
definitions TARSKI, FUNCT_1, PBOOLE, CAT_5, FUNCOP_1, FUNCT_2;
equalities CAT_1, BINOP_1, GRAPH_1, OPPCAT_1;
expansions FUNCT_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;
begin :: Category Yielding Functions
registration
let A be non empty set;
cluster non empty-yielding for ManySortedSet of A;
existence
proof
take the non-empty ManySortedSet of A;
take the Element of A;
thus thesis;
end;
end;
definition
let C be Categorial Category;
let f be Morphism of C;
redefine func f`2 -> Functor of f`11, f`12; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
A1: dom f = f`11 by CAT_5:2;
f`11 = cat f`11 & f`12 = cat f`12 by CAT_5:def 7;
hence f`2 is Functor of f`11, f`12 by A1,CAT_5:2;
end;
end;
theorem
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]
proof
let C be Categorial Category;
let f,g be Morphism of C;
A1: g`11 = dom g by CAT_5:13;
A2: f`11 = dom f by CAT_5:13;
assume
A3: dom g = cod f;
then consider ff being Functor of f`11, g`11 such that
A4: f = [[dom f, cod f], ff] by A1,A2,CAT_5:def 6;
A5: g`12 = cod g by CAT_5:13;
then consider gg being Functor of g`11, g`12 such that
A6: g = [[dom g, cod g], gg] by A1,CAT_5:def 6;
thus g(*)f = [[dom f, cod g], gg*ff] by A3,A1,A5,A2,A6,A4,CAT_5:def 6
.= [[dom f, cod g], gg*f`2] by A4
.= [[dom f, cod g], g`2*f`2] by A6;
end;
theorem Th2:
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
proof
let C be Category, D,E be Categorial Category;
let F be Functor of C,D;
let G be Functor of C,E such that
A1: F = G;
A2: now
let x be object;
assume x in the carrier of C;
then reconsider a = x as Object of C;
A3: a = dom id a;
hence (Obj F).x = dom (F.(id a qua Morphism of C)) by CAT_1:69
.= (F.(id a qua Morphism of C))`11 by CAT_5:13
.= dom (G.(id a qua Morphism of C)) by A1,CAT_5:13
.= (Obj G).x by A3,CAT_1:69;
end;
thus thesis by A2;
end;
definition
let IT be Function;
attr IT is Category-yielding means
: Def1:
for x being set st x in dom IT holds IT.x is Category;
end;
registration
cluster Category-yielding for Function;
existence
proof
take f = {} --> 1Cat({},{{}});
let x be set;
assume x in dom f;
hence thesis;
end;
end;
registration
let X be set;
cluster Category-yielding for ManySortedSet of X;
existence
proof
take f = X --> 1Cat({},{{}});
let x be set;
assume x in dom f;
then x in X;
hence thesis by FUNCOP_1:7;
end;
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;
coherence by FUNCOP_1:7;
end;
registration
let f be Category-yielding Function;
cluster rng f -> categorial;
coherence
proof
let x be set;
assume x in rng f;
then ex y being object st y in dom f & x = f.y by FUNCT_1:def 3;
hence thesis by Def1;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
dom f = X by PARTFUN1:def 2;
hence thesis by Def1;
end;
end;
registration
let f be Function;
let g be Category-yielding Function;
cluster g*f -> Category-yielding;
coherence
proof
let x be set;
assume x in dom (g*f);
then (g*f).x = g.(f.x) & f.x in dom g by FUNCT_1:11,12;
hence thesis by Def1;
end;
end;
:: carrier and Morphisms
definition
let F be Category-yielding Function;
func Objs F -> non-empty Function means
: Def2:
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;
existence
proof
defpred P[object,object] means
for C being Category st C = F.$1 holds $2 = the carrier of C;
A1: now
let x be object;
assume x in dom F;
then reconsider C = F.x as Category by Def1;
reconsider y = the carrier of C as object;
take y;
thus P[x,y];
end;
consider f being Function such that
A2: dom f = dom F & for x being object st x in dom F holds P[x,f.x] from
CLASSES1:sch 1(A1);
f is non-empty
proof
let x be object;
assume
A3: x in dom f;
then reconsider C = F.x as Category by A2,Def1;
f.x = the carrier of C by A2,A3;
hence thesis;
end;
hence thesis by A2;
end;
uniqueness
proof
let f1, f2 be non-empty Function such that
A4: dom f1 = dom F and
A5: for x being object st x in dom F for C being Category st C = F.x
holds f1.x = the carrier of C and
A6: dom f2 = dom F and
A7: for x being object st x in dom F for C being Category st C = F.x
holds f2.x = the carrier of C;
now
let x be object;
assume
A8: x in dom F;
then reconsider C = F.x as Category by Def1;
thus f1.x = the carrier of C by A5,A8
.= f2.x by A7,A8;
end;
hence thesis by A4,A6;
end;
func Mphs F -> non-empty Function means
:Def3:
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;
existence
proof
defpred P[object,object] means
for C being Category st C = F.$1 holds $2 = the carrier' of C;
A9: now
let x be object;
assume x in dom F;
then reconsider C = F.x as Category by Def1;
reconsider y = the carrier' of C as object;
take y;
thus P[x,y];
end;
consider f being Function such that
A10: dom f = dom F & for x being object st x in dom F holds P[x,f.x] from
CLASSES1:sch 1(A9);
f is non-empty
proof
let x be object;
assume
A11: x in dom f;
then reconsider C = F.x as Category by A10,Def1;
f.x = the carrier' of C by A10,A11;
hence thesis;
end;
hence thesis by A10;
end;
uniqueness
proof
let f1, f2 be non-empty Function such that
A12: dom f1 = dom F and
A13: for x being object st x in dom F for C being Category st C = F.x
holds f1.x = the carrier' of C and
A14: dom f2 = dom F and
A15: for x being object st x in dom F for C being Category st C = F.x
holds f2.x = the carrier' of C;
now
let x be object;
assume
A16: x in dom F;
then reconsider C = F.x as Category by Def1;
thus f1.x = the carrier' of C by A13,A16
.= f2.x by A15,A16;
end;
hence thesis by A12,A14;
end;
end;
registration
let A be non empty set;
let F be ManySortedCategory of A;
cluster Objs F -> A-defined;
coherence
proof
dom Objs F = dom F by Def2
.= A by PARTFUN1:def 2;
hence thesis by RELAT_1:def 18;
end;
cluster Mphs F -> A-defined;
coherence
proof
dom Mphs F = dom F by Def3
.= A by PARTFUN1:def 2;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let A be non empty set;
let F be ManySortedCategory of A;
cluster Objs F -> total;
coherence
proof
dom Objs F = dom F by Def2
.= A by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
cluster Mphs F -> total;
coherence
proof
dom Mphs F = dom F by Def3
.= A by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem
for X being set, C being Category holds Objs (X --> C) = X --> the
carrier of C & Mphs (X --> C) = X --> the carrier' of C
proof
let X be set, C be Category;
A2: dom Objs (X --> C) = dom (X --> C) by Def2;
now
let a be object;
assume
A3: a in dom Objs (X --> C);
then (X --> C).a = C by A2,FUNCOP_1:7;
hence (Objs (X --> C)).a = the carrier of C by A2,A3,Def2;
end;
hence Objs (X --> C) = X --> the carrier of C by A2,FUNCOP_1:11;
A4: dom Mphs (X --> C) = dom (X --> C) by Def3;
now
let a be object;
assume
A5: a in dom Mphs (X --> C);
then (X --> C).a = C by A4,FUNCOP_1:7;
hence (Mphs (X --> C)).a = the carrier' of C by A4,A5,Def3;
end;
hence thesis by A4,FUNCOP_1:11;
end;
begin :: Pairs of Many Sorted Sets
definition
let A,B be set;
mode ManySortedSet of A,B -> object means
: Def4:
ex f being (ManySortedSet of A), g being ManySortedSet of B st it = [f,g];
existence
proof
set f = the (ManySortedSet of A),g = the ManySortedSet of B;
take [f,g], f, g;
thus thesis;
end;
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; :: redefines [ (TARSKI, definition)
coherence
proof
take f,g;
thus thesis;
end;
end;
registration
let A, B be set;
let X be ManySortedSet of A,B;
cluster X`1 -> Function-like Relation-like for set;
coherence
proof
ex f being (ManySortedSet of A), g being ManySortedSet of B st ( X = [f
,g]) by Def4;
hence thesis;
end;
cluster X`2 -> Function-like Relation-like for set;
coherence
proof
ex f being (ManySortedSet of A), g being ManySortedSet of B st ( X = [f
,g]) by Def4;
hence thesis;
end;
end;
registration
let A, B be set;
let X be ManySortedSet of A,B;
cluster X`1 -> A-defined for Relation;
coherence
proof
ex f being (ManySortedSet of A), g being ManySortedSet of B st ( X = [f
,g]) by Def4;
hence thesis;
end;
cluster X`2 -> B-defined for Relation;
coherence
proof
ex f being (ManySortedSet of A), g being ManySortedSet of B st ( X = [f
,g]) by Def4;
hence thesis;
end;
end;
registration
let A, B be set;
let X be ManySortedSet of A,B;
cluster X`1 -> total for A-defined Function;
coherence
proof
ex f being (ManySortedSet of A), g being ManySortedSet of B st ( X = [f
,g]) by Def4;
hence thesis;
end;
cluster X`2 -> total for B-defined Function;
coherence
proof
ex f being (ManySortedSet of A), g being ManySortedSet of B st ( X = [f
,g]) by Def4;
hence thesis;
end;
end;
definition
let A,B be set;
let IT be ManySortedSet of A,B;
attr IT is Category-yielding_on_first means
: Def5:
IT`1 is Category-yielding;
attr IT is Function-yielding_on_second means
: Def6:
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;
existence
proof
set g = the ManySortedFunction of B;
set f = the ManySortedCategory of A;
reconsider X = [f,g] as ManySortedSet of A,B;
take X;
thus X`1 is Category-yielding & X`2 is Function-yielding;
end;
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;
coherence 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 for Function;
coherence by Def6;
end;
registration
let f be Function-yielding Function;
cluster rng f -> functional;
coherence
proof
let x be object;
assume x in rng f;
then ex y being object st y in dom f & x = f.y by FUNCT_1:def 3;
hence thesis;
end;
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 :: redefines [ (TARSKI, definition)
Function-yielding_on_second ManySortedSet of A,B;
coherence
proof
[f,g]`1 = f & [f,g]`2 = g;
hence thesis by Def5,Def6;
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:
for a being Element of A holds it.a is Functor of F.a, G.a;
existence
proof
defpred P[object,object] means
ex a9 being Element of A, t being Functor of F.a9
, G.a9 st $1 = a9 & $2 = t;
A1: now
let a be object;
assume a in A;
then reconsider a9 = a as Element of A;
set f = the Functor of F.a9, G.a9;
reconsider f as object;
take f;
thus P[a,f];
end;
consider f being Function such that
A2: dom f = A & for a being object st a in A holds P[a,f.a] from CLASSES1
:sch 1(A1);
f is Function-yielding
proof
let a be object;
assume a in dom f;
then
ex a9 being Element of A, t being Functor of F.a9, G.a9 st a = a9 &
f.a = t by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of A by A2,PARTFUN1:def 2
,RELAT_1:def 18;
take f;
let a be Element of A;
ex a9 being Element of A, t being Functor of F.a9, G.a9 st a = a9 & f.
a = t by A2;
hence thesis;
end;
end;
scheme
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
A1: for a being Element of A() holds F(a) is Functor of C1().a, C2().a
proof
consider f being ManySortedSet of A() such that
A2: for a being object st a in A() holds f.a = F(a) from PBOOLE:sch 4;
f is Function-yielding
proof
let a be object;
assume a in dom f;
then reconsider a as Element of A() by PARTFUN1:def 2;
f.a = F(a) by A2;
hence thesis by A1;
end;
then reconsider f as ManySortedFunction of A();
f is ManySortedFunctor of C1(), C2()
proof
let a be Element of A();
f.a = F(a) by A2;
hence thesis by A1;
end;
then reconsider f as ManySortedFunctor of C1(), C2();
take f;
thus thesis by A2;
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;
redefine func f.a -> Functor of F.a, G.a; :: redefines . (FUNCT_1, definition)
coherence by Def7;
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
: Def8:
it`2 is ManySortedFunctor of it`1*F, it`1*G;
existence
proof
set g = the ManySortedCategory of A;
set f = the ManySortedFunctor of g*F, g*G;
take I = [g,f];
thus thesis;
end;
end;
theorem Th4:
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)
proof
let A,B be non empty set, F,G be Function of B,A;
let I be Indexing of F,G;
reconsider H = I`2 as ManySortedFunctor of I`1*F, I`1*G by Def8;
let m be Element of B;
dom (I`1*F) = B by PARTFUN1:def 2;
then
A1: (I`1*F).m = I`1.(F.m) by FUNCT_1:12;
H.m is Functor of (I`1*F).m, (I`1*G).m & dom (I`1*G) = B by PARTFUN1:def 2;
hence thesis by A1,FUNCT_1:12;
end;
theorem
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
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;
redefine func I`2 -> ManySortedFunctor of I`1*F,I`1*G; :: redefines `2 (XTUPLE_0, definition)
coherence by Def8;
end;
Lm1: now
let A,B be non empty set;
let F,G be Function of B,A;
let I be Indexing of F,G;
consider C being full strict Categorial Category such that
A1: the carrier of C = rng I`1 by CAT_5:20;
take C;
A2: dom I`1 = A by PARTFUN1:def 2;
hence for a be Element of A holds I`1.a is Object of C by A1,FUNCT_1:def 3;
let b be Element of B;
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 3;
hence [[I`1.(F.b),I`1.(G.b)],I`2.b] is Morphism of C by A3,CAT_5:def 8;
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:
(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
proof
ex C being full strict Categorial 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) by Lm1;
hence thesis;
end;
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;
existence
proof
consider C being full strict Categorial Category such that
A1: ( 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 by Lm1;
C is TargetCat of I by A1,Def9;
hence thesis;
end;
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
A1: C = CatStr(#A, B, F, G, c#);
mode Indexing of F, G, c, i -> Indexing of F,G means
: Def10:
(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
proof
set I2 = B --> id C;
set I1 = A --> C;
A2: [I1,I2]`1 = I1;
A3: [I1,I2]`2 = I2;
I2 is ManySortedFunctor of I1*F, I1*G
proof
let a be Element of B;
I1.(F.a) = C & dom (I1*F) = B by PARTFUN1:def 2;
then
A4: I2.a = id C & (I1*F).a = C by FUNCT_1:12;
I1.(G.a) = C & dom (I1*G) = B by PARTFUN1:def 2;
hence thesis by A4,FUNCT_1:12;
end;
then reconsider I = [I1,I2] as Indexing of F,G by A2,A3,Def8;
take I;
thus for a be Element of A holds I`2.(i.a) = id (I`1.a);
let m1, m2 be Element of B;
reconsider mm1=m1, mm2=m2 as Morphism of C by A1;
assume F.m2 = G.m1;
then cod mm1 = dom mm2 by A1;
then [m2,m1] in dom c by A1,CAT_1:def 6;
then
A5: I`2.(c.[m2,m1]) = id C by FUNCOP_1:7,PARTFUN1:4;
thus thesis by A5,FUNCT_2:17;
end;
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 Th6:
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)
proof
let C be Category;
reconsider D = the CatStr of C as Category by CAT_5:1;
let I be Indexing of the Source of C, the Target of C;
A1: D = CatStr(# the carrier of C, the carrier' of C, the Source of C, the
Target of C, the Comp of C#);
hereby
assume
A2: I is Indexing of C;
thus for a being Object of C holds I`2.id a = id (I`1.a)
proof let a be Object of C;
id a = (IdMap C).a by ISOCAT_1:def 12;
hence thesis by A1,Def10,A2;
end;
let m1, m2 be Morphism of C;
assume
A3: dom m2 = cod m1;
then I`2.((the Comp of C).(m2,m1)) = (I`2.m2)*(I`2.m1) by A1,A2,Def10;
hence I`2.(m2(*)m1) = (I`2.m2)*(I`2.m1) by A3,CAT_1:16;
end;
assume that
A4: for a being Object of C holds I`2.id a = id (I`1.a) and
A5: for m1, m2 being Morphism of C st dom m2 = cod m1 holds I`2.(m2(*)m1)
= (I`2.m2)*(I`2.m1);
thus ex D being Category st D = CatStr(# the carrier of C, the carrier' of C
, the Source of C, the Target of C, the Comp of C#) by A1;
hereby
let a be Object of C;
id a = (IdMap C).a by ISOCAT_1:def 12;
hence I`2.((IdMap C).a) = I`2.id a .= id (I`1.a) by A4;
end;
let m1, m2 be Morphism of C;
assume (the Source of C).m2 = (the Target of C).m1;
then
A6: dom m2 = cod m1;
then
A7: I`2.(m2(*)m1) = (I`2.m2)*(I`2.m1) by A5;
thus I`2.((the Comp of C).[m2,m1]) = I`2.((the Comp of C).(m2,m1))
.= (I`2.m2)*(I`2.m1) by A6,A7,CAT_1:16;
end;
theorem Th7:
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)
proof
let C be Category;
let I be Indexing of the Target of C, the Source of C;
A1: C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C,
the Source of C, ~the Comp of C#);
hereby
assume
A2: I is coIndexing of C;
thus for a be Object of C holds I`2.id a = id (I`1.a)
proof let a be Object of C;
id a = (IdMap C).a by ISOCAT_1:def 12;
hence thesis by A1,Def10,A2;
end;
let m1, m2 be Morphism of C;
assume
A3: dom m2 = cod m1;
then
A4: [m2,m1] in dom the Comp of C by CAT_1:15;
I`2.((~the Comp of C).(m1,m2)) = (I`2.m1)*(I`2.m2) by A1,A2,A3,Def10;
then I`2.((the Comp of C).(m2,m1)) = (I`2.m1)*(I`2.m2) by A4,FUNCT_4:def 2;
hence I`2.(m2(*)m1) = (I`2.m1)*(I`2.m2) by A3,CAT_1:16;
end;
assume that
A5: for a being Object of C holds I`2.id a = id (I`1.a) and
A6: for m1, m2 being Morphism of C st dom m2 = cod m1 holds I`2.(m2(*)m1)
= (I`2.m1)*(I`2.m2);
thus ex D being Category st D = CatStr(# the carrier of C, the carrier' of C
, the Target of C, the Source of C, ~the Comp of C#) by A1;
hereby
let a be Object of C;
id a = (IdMap C).a by ISOCAT_1:def 12;
hence I`2.((IdMap C).a) = I`2.id a .= id (I`1.a) by A5;
end;
let m1, m2 be Morphism of C;
assume (the Target of C).m2 = (the Source of C).m1;
then
A7: dom m1 = cod m2;
then I`2.(m1(*)m2) = (I`2.m2)*(I`2.m1) by A6;
then
A8: I`2.((the Comp of C).(m1,m2)) = (I`2.m2)*(I`2.m1) by A7,CAT_1:16;
A9: [m1,m2] in dom the Comp of C by A7,CAT_1:15;
thus I`2.((~the Comp of C).[m2,m1]) = I`2.((~the Comp of C).(m2,m1))
.= (I`2.m2)*(I`2.m1) by A8,A9,FUNCT_4:def 2;
end;
Lm2: for C being Category holds IdMap C = IdMap(C opp)
proof let C be Category;
thus the carrier of C = the carrier of C opp;
let o be Element of the carrier of C;
thus (IdMap C).o = id o by ISOCAT_1:def 12
.= id(o opp) by OPPCAT_1:71
.= (IdMap(C opp)).(o opp) by ISOCAT_1:def 12
.= (IdMap(C opp)).o;
end;
theorem
for C being Category, x be set holds x is coIndexing of C iff x is
Indexing of C opp
by Lm2;
theorem
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
proof
let C be Category, I be Indexing of C;
let c1,c2 be Object of C such that
A1: Hom(c1,c2) is non empty;
let m be Morphism of c1,c2;
dom (I`1*(the Source of C)) = the carrier' of C by PARTFUN1:def 2;
then
A2: dom (I`1*(the Target of C)) = the carrier' of C & (I`1*(the Source of C)
).m = I`1.((the Source of C).m) by FUNCT_1:12,PARTFUN1:def 2;
dom m = c1 & cod m = c2 by A1,CAT_1:5;
hence thesis by A2,FUNCT_1:12;
end;
theorem
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
proof
let C be Category, I be coIndexing of C;
let c1,c2 be Object of C such that
A1: Hom(c1,c2) is non empty;
let m be Morphism of c1,c2;
dom (I`1*(the Source of C)) = the carrier' of C by PARTFUN1:def 2;
then
A2: dom (I`1*(the Target of C)) = the carrier' of C & (I`1*(the Source of C)
).m = I`1.((the Source of C).m) by FUNCT_1:12,PARTFUN1:def 2;
dom m = c1 & cod m = c2 by A1,CAT_1:5;
hence thesis by A2,FUNCT_1:12;
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:
for f being Morphism of C holds it.f = [[I`1.dom f, I`1.cod f], I`2.f];
existence
proof
A1: rng I`1 c= the carrier of T
proof
let x be object;
assume x in rng I`1;
then consider a being object such that
A2: a in dom I`1 and
A3: x = I`1.a by FUNCT_1:def 3;
reconsider a as Object of C by A2,PARTFUN1:def 2;
I`1.a is Object of T by Def9;
hence thesis by A3;
end;
dom I`1 = the carrier of C by PARTFUN1:def 2;
then reconsider
I1 = I`1 as Function of the carrier of C, the carrier of T by A1,
FUNCT_2:def 1,RELSET_1:4;
deffunc O(Object of C) = I1.$1;
deffunc F(Morphism of C) = [[I`1.dom $1, I`1.cod $1], I`2.$1];
A4: now
let f be Morphism of C;
thus F(f) is Morphism of T by Def9;
let g be Morphism of T;
assume
A5: g = F(f);
hence dom g = F(f)`11 by CAT_5:13
.= O(dom f) by MCART_1:85;
thus cod g = F(f)`12 by A5,CAT_5:13
.= O(cod f) by MCART_1:85;
end;
A6: now
let f1,f2 be Morphism of C;
let g1,g2 be Morphism of T;
assume that
A7: g1 = F(f1) & g2 = F(f2) and
A8: dom f2 = cod f1;
A9: dom (f2(*)f1) = dom f1 & cod (f2(*)f1) = cod f2 by A8,CAT_1:17;
A10: I`2.f1 is Functor of I`1.dom f1, I`1.cod f1 & I`2.f2 is Functor of
I`1.dom f2, I`1.cod f2 by Th4;
I`2.(f2(*)f1) = (I`2.f2)*(I`2.f1) by A8,Th6;
hence F(f2(*)f1) = g2(*)g1 by A7,A8,A10,A9,CAT_5:def 6;
end;
A11: now
let a be Object of C;
thus F(id a) = [[I1.a, I1.a], id (I`1.a)] by Th6
.= id O(a) by CAT_5:def 6;
end;
thus ex F being Functor of C,T st for f being Morphism of C holds F.f = F(
f) from CAT_5:sch 3(A4,A11,A6 );
end;
uniqueness
proof
let F1, F2 be Functor of C,T such that
A12: for f being Morphism of C holds F1.f = [[I`1.dom f, I`1.cod f], I
`2.f] and
A13: for f being Morphism of C holds F2.f = [[I`1.dom f, I`1.cod f], I `2.f];
now
let f be Morphism of C;
thus F1.f = [[I`1.dom f, I`1.cod f], I`2.f] by A12
.= F2.f by A13;
end;
hence thesis;
end;
end;
Lm3: for C being Category, I being Indexing of C for T being TargetCat of I
holds Obj (I-functor(C,T)) = I`1
proof
let C be Category, I be Indexing of C;
let T be TargetCat of I;
A1: now
let x be object;
assume x in the carrier of C;
then reconsider a = x as Object of C;
A2: dom id a = a & cod id a = a;
(Obj (I-functor(C,T))).a = dom id ((Obj (I-functor(C,T))).a)
.= dom ((I-functor(C,T)).(id a qua Morphism of C)) by CAT_1:68
.= ((I-functor(C,T) qua Function).id a)`11 by CAT_5:2
.= [[I`1.a, I`1.a], I`2.id a]`11 by A2,Def11;
hence (Obj (I-functor(C,T))).x = I`1.x by MCART_1:85;
end;
dom Obj (I-functor(C,T)) = the carrier of C & dom I`1 = the carrier of C
by FUNCT_2:def 1,PARTFUN1:def 2;
hence thesis by A1;
end;
theorem Th11:
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))
proof
let C be Category, I be Indexing of C;
let T1,T2 be TargetCat of I;
A1: now
let x be object;
assume x in the carrier' of C;
then reconsider f = x as Morphism of C;
thus (I-functor(C,T1)).x = [[I`1.dom f, I`1.cod f], I`2.f] by Def11
.= (I-functor(C,T2)).x by Def11;
end;
thus I-functor(C,T1) = I-functor(C,T2) by A1;
A2: now
let x be object;
assume x in the carrier of C;
then reconsider a = x as Object of C;
thus (Obj (I-functor(C,T1))).x = I`1.a by Lm3
.= (Obj (I-functor(C,T2))).x by Lm3;
end;
thus thesis by A2;
end;
theorem
for C being Category, I being Indexing of C for T being TargetCat of I
holds Obj (I-functor(C,T)) = I`1 by Lm3;
theorem
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 by Lm3;
definition
let C be Category;
let I be Indexing of C;
func rng I -> strict TargetCat of I means
: Def12:
for T being TargetCat of I holds it = Image (I-functor(C,T));
uniqueness
proof
set T = the TargetCat of I;
let T1,T2 be strict TargetCat of I such that
A1: for T being TargetCat of I holds T1 = Image (I-functor(C,T)) and
A2: for T being TargetCat of I holds T2 = Image (I-functor(C,T));
thus T1 = Image (I-functor(C,T)) by A1
.= T2 by A2;
end;
existence
proof
set S = the TargetCat of I;
reconsider T = Image (I-functor(C,S)) as strict Subcategory of S;
reconsider F = I-functor(C,S) as Functor of C,T by CAT_5:8;
T is TargetCat of I
proof
the carrier of T = rng Obj (I-functor(C,S)) by CAT_5:def 3;
then
A3: the carrier of T = rng I`1 by Lm3;
dom I`1 = the carrier of C by PARTFUN1:def 2;
hence for a being Object of C holds I`1.a is Object of T by A3,
FUNCT_1:def 3;
let b be Morphism of C;
F.b = [[I`1.dom b, I`1.cod b], I`2.b] by Def11;
hence thesis;
end;
then reconsider T as strict TargetCat of I;
take T;
let T9 be TargetCat of I;
thus thesis by Th11,CAT_5:22;
end;
end;
theorem Th14:
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
proof
let C be Category, I be Indexing of C;
let D be Categorial Category;
hereby
assume
A1: rng I is Subcategory of D;
thus D is TargetCat of I
proof
hereby
let a be Object of C;
I`1.a is Object of rng I by Def9;
hence I`1.a is Object of D by A1,CAT_2:6;
end;
let b be Morphism of C;
[[I`1.((the Source of C).b),I`1.((the Target of C).b)],I`2.b] is
Morphism of rng I by Def9;
hence thesis by A1,CAT_2:8;
end;
end;
assume D is TargetCat of I;
then reconsider T = D as TargetCat of I;
rng I = Image (I-functor(C,T)) by Def12;
hence thesis;
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
I`2.m;
coherence
proof
dom (I`1*(the Source of C)) = the carrier' of C by PARTFUN1:def 2;
then
dom (I`1*(the Target of C)) = the carrier' of C & (I`1*(the Source of
C)).m = I`1.((the Source of C).m) by FUNCT_1:12,PARTFUN1:def 2;
hence thesis by FUNCT_1:12;
end;
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
I`2.m;
coherence
proof
dom (I`1*(the Source of C)) = the carrier' of C by PARTFUN1:def 2;
then
dom (I`1*(the Target of C)) = the carrier' of C & (I`1*(the Source of
C)).m = I`1.((the Source of C).m) by FUNCT_1:12,PARTFUN1:def 2;
hence thesis by FUNCT_1:12;
end;
end;
Lm4: now
let C,D be Category;
set F = (the carrier of C) --> D, G = (the carrier' of C) --> id D;
set H = [F,G];
let m be Morphism of C;
dom (H`1*(the Source of C)) = the carrier' of C by PARTFUN1:def 2;
then
A1: (H`1*(the Source of C)).m = H`1.((the Source of C).m) by FUNCT_1:12
.= F.((the Source of C).m)
.= D;
dom (H`1*(the Target of C)) = the carrier' of C by PARTFUN1:def 2;
then
A2: (H`1*(the Target of C)).m = H`1.((the Target of C).m) by FUNCT_1:12
.= F.((the Target of C).m)
.= D;
thus
H`2.m is Functor of (H`1*(the Source of C)).m, (H`1*(the Target of C)).
m by A1,A2;
end;
Lm5: now
let C,D be Category;
set F = (the carrier of C) --> D, G = (the carrier' of C) --> id D;
set H = [F,G];
let m be Morphism of C;
dom (H`1*(the Source of C)) = the carrier' of C by PARTFUN1:def 2;
then
A1: (H`1*(the Source of C)).m = H`1.((the Source of C).m) by FUNCT_1:12
.= F.((the Source of C).m)
.= D;
dom (H`1*(the Target of C)) = the carrier' of C by PARTFUN1:def 2;
then
A2: (H`1*(the Target of C)).m = H`1.((the Target of C).m) by FUNCT_1:12
.= F.((the Target of C).m)
.= D;
thus
H`2.m is Functor of (H`1*(the Target of C)).m, (H`1*(the Source of C)).
m by A1,A2;
end;
theorem
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
let C,D be Category;
set H = [(the carrier of C) --> D, (the carrier' of C) --> id D], I = H;
A1: for a be Object of C holds H`2.id a = id (H`1.a);
for m being Morphism of C holds H`2.m is Functor of (H`1*(the Source of
C)).m, (H`1*(the Target of C)).m by Lm4;
then
H`2 is ManySortedFunctor of H`1*(the Source of C), H`1*(the Target of C)
by Def7;
then reconsider H as Indexing of the Source of C, the Target of C by Def8;
for m1, m2 be Morphism of C st dom m2 = cod m1 holds
H`2.(m2(*)m1) = (H`2.m2)*(H`2.m1) by FUNCT_2:17;
hence I is Indexing of C by A1,Th6;
for m being Morphism of C holds H`2.m is Functor of (H`1*(the Target of
C)).m, (H`1*(the Source of C)).m by Lm5;
then
H`2 is ManySortedFunctor of H`1*(the Target of C), H`1*(the Source of C
) by Def7;
then reconsider H as Indexing of the Target of C, the Source of C by Def8;
for m1, m2 be Morphism of C st dom m2 = cod m1 holds
H`2.(m2(*)m1) = (H`2.m1)*(H`2.m2) by FUNCT_2:17;
hence thesis by A1,Th7;
end;
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;
coherence
proof
let x be set;
assume x in dom Obj F;
then rng Obj F c= the carrier of D & (Obj F).x in rng Obj F by
FUNCT_1:def 3,RELAT_1:def 19;
hence thesis by CAT_5:12;
end;
end;
theorem Th16:
for C being Category, D being Categorial Category, F being
Functor of C,D holds [Obj F, pr2 F] is Indexing of C
proof
let C be Category, D be Categorial Category, F be Functor of C,D;
set I = [Obj F, pr2 F];
A1: dom F = the carrier' of C by FUNCT_2:def 1;
dom Obj F = the carrier of C by FUNCT_2:def 1;
then
A2: Obj F is ManySortedSet of the carrier of C by PARTFUN1:def 2;
A3: I`2 = pr2 F;
A4: dom pr2 F = dom F by MCART_1:def 13;
then pr2 F is ManySortedSet of the carrier' of C by A1,PARTFUN1:def 2
,RELAT_1:def 18;
then reconsider
I as ManySortedSet of the carrier of C, the carrier' of C by A2,Def4;
pr2 F is Function-yielding
proof
let x be object;
assume x in dom pr2 F;
then reconsider x as Morphism of C by A1,MCART_1:def 13;
reconsider m = F.x as Morphism of D;
(pr2 F).x = m`2 by A1,MCART_1:def 13;
hence thesis;
end;
then reconsider
FF = pr2 F as ManySortedFunction of the carrier' of C by A4,A1,PARTFUN1:def 2
,RELAT_1:def 18;
I`1 is Category-yielding;
then reconsider
I as Category-yielding_on_first ManySortedSet of the carrier of C
, the carrier' of C by Def5;
FF is ManySortedFunctor of I`1*the Source of C, I`1*the Target of C
proof
let m be Morphism of C;
reconsider x = F.m as Morphism of D;
A5: x`11 = dom (F.m) by CAT_5:13;
x`12 = cod (F.m) by CAT_5:13;
then consider f being Functor of x`11, x`12 such that
A6: F.m = [[x`11, x`12], f] by A5,CAT_5:def 6;
A7: ((Obj F)*the Source of C).m = (Obj F).dom m by FUNCT_2:15
.= dom (F.m) by CAT_1:69;
A8: ((Obj F)*the Target of C).m = (Obj F).cod m by FUNCT_2:15
.= cod (F.m) by CAT_1:69;
FF.m = x`2 by A1,MCART_1:def 13
.= f by A6;
hence thesis by A5,A7,A8,CAT_5:13;
end;
then reconsider I as Indexing of the Source of C, the Target of C by A3,Def8;
A9: dom F = the carrier' of C by FUNCT_2:def 1;
A10: now
let m1, m2 be Morphism of C;
assume
A11: dom m2 = cod m1;
set h1 = F.m1, h2 = F.m2;
A12: dom h2 = F.dom m2 by CAT_1:72
.= cod h1 by A11,CAT_1:72;
A13: dom h2 = h2`11 by CAT_5:13;
cod h2 = h2`12 by CAT_5:13;
then consider f2 being Functor of h2`11, h2`12 such that
A14: h2 = [[h2`11, h2`12], f2] by A13,CAT_5:def 6;
A15: cod h1 = h1`12 by CAT_5:13;
dom h1 = h1`11 by CAT_5:13;
then consider f1 being Functor of h1`11, h1`12 such that
A16: h1 = [[h1`11, h1`12], f1] by A15,CAT_5:def 6;
thus I`2.(m2(*)m1) = (F.(m2(*)m1))`2 by A9,MCART_1:def 13
.= (h2(*)h1)`2 by A11,CAT_1:64
.= [[h1`11, h2`12], f2*f1]`2 by A13,A15,A14,A16,A12,CAT_5:def 6
.= f2*f1
.= h2`2*f1 by A14
.= h2`2*h1`2 by A16
.= (I`2.m2)*h1`2 by A9,MCART_1:def 13
.= (I`2.m2)*(I`2.m1) by A9,MCART_1:def 13;
end;
now
let a be Object of C;
reconsider i = (Obj F).a as Object of D;
thus I`2.id a = (F.(id a qua Morphism of C))`2 by A9,MCART_1:def 13
.= (id i qua Morphism of D)`2 by CAT_1:68
.= [[I`1.a, I`1.a], id (I`1.a)]`2 by CAT_5:def 6
.= id (I`1.a);
end;
hence thesis by A10,Th6;
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
[Obj F, pr2 F];
coherence by Th16;
end;
theorem
for C being Category, D being Categorial Category, F being Functor of
C,D holds D is TargetCat of F-indexing_of C
proof
let C be Category, D be Categorial Category, F be Functor of C,D;
set I = F-indexing_of C;
thus for a being Object of C holds I`1.a is Object of D by FUNCT_2:5;
let b be Morphism of C;
set h = F.b;
A1: dom h = h`11 by CAT_5:13;
cod h = h`12 by CAT_5:13;
then consider f being Functor of h`11, h`12 such that
A2: h = [[h`11, h`12], f] by A1,CAT_5:def 6;
A3: cod h = (Obj F).cod b by CAT_1:69
.= (Obj F).((the Target of C).b);
A4: dom h = (Obj F).dom b by CAT_1:69
.= (Obj F).((the Source of C).b);
I`2 = pr2 F & dom F = the carrier' of C by FUNCT_2:def 1;
then I`2.b = h`2 by MCART_1:def 13
.= f by A2;
hence thesis by A1,A2,A4,A3,CAT_5:13;
end;
theorem Th18:
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)
proof
let C be Category, D be Categorial Category, F be Functor of C,D;
set I = F-indexing_of C;
let T be TargetCat of I;
A1: dom F = the carrier' of C by FUNCT_2:def 1;
A2: now
let x be object;
assume x in the carrier' of C;
then reconsider f = x as Morphism of C;
set h = F.f;
A3: dom h = (Obj F).dom f & cod h = (Obj F).cod f by CAT_1:69;
A4: dom h = h`11 & cod h = h`12 by CAT_5:13;
then consider g being Functor of h`11, h`12 such that
A5: h = [[h`11, h`12], g] by CAT_5:def 6;
I`2.f = h`2 by A1,MCART_1:def 13
.= g by A5;
hence F.x = (I-functor(C,T)).x by A4,A5,A3,Def11;
end;
thus thesis by A2;
end;
theorem
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 by Th2;
theorem Th20:
for C being Category, I being (Indexing of C), T being TargetCat
of I holds pr2 (I-functor(C,T)) = I`2
proof
let C be Category, I be Indexing of C;
let T be TargetCat of I;
A1: dom (I-functor(C,T)) = the carrier' of C by FUNCT_2:def 1;
A2: now
let x be object;
assume x in the carrier' of C;
then reconsider f = x as Morphism of C;
(I-functor(C,T)).f = [[I`1.dom f, I`1.cod f], I`2.f] by Def11;
then ((I-functor(C,T)).x)`2 = I`2.f;
hence (pr2 (I-functor(C,T))).x = I`2.x by A1,MCART_1:def 13;
end;
dom pr2 (I-functor(C,T)) = dom (I-functor(C,T)) & dom I`2 = the carrier'
of C by MCART_1:def 13,PARTFUN1:def 2;
hence thesis by A1,A2;
end;
theorem
for C being Category, I being (Indexing of C), T being TargetCat of I
holds (I-functor(C,T))-indexing_of C = I
proof
let C be Category, I be Indexing of C;
let T be TargetCat of I;
set F = I-functor(C,T);
A1: ex f being (ManySortedSet of the carrier of C), g being ManySortedSet of
the carrier' of C st I = [f,g] by Def4;
thus F-indexing_of C = [I`1, pr2 F] by Lm3
.= [I`1, I`2] by Th20
.= I by A1;
end;
begin :: Composing Indexings and Functors
Lm6: now
let c,d be Category, e be Subcategory of d;
let f be Functor of c,e;
(incl e)*f = (id e)*f by CAT_2:def 5
.= f by FUNCT_2:17;
hence f is Functor of c,d;
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:
for F9 being Functor of C,E st F9 =
F holds it = (I-functor(E,rng I)*F9)-indexing_of C;
existence
proof
reconsider A = Image F as Subcategory of E by A1;
reconsider G = F as Functor of C, A by CAT_5:8;
reconsider G as Functor of C, E by Lm6;
take (I-functor(E,rng I)*G)-indexing_of C;
thus thesis;
end;
uniqueness
proof
reconsider A = Image F as Subcategory of E by A1;
reconsider G = F as Functor of C, A by CAT_5:8;
let J1, J2 be Indexing of C such that
A2: for F9 being Functor of C,E st F9 = F holds J1 = (I-functor(E,rng
I)*F9)-indexing_of C and
A3: for F9 being Functor of C,E st F9 = F holds J2 = (I-functor(E,rng
I)*F9)-indexing_of C;
reconsider G as Functor of C, E by Lm6;
thus J1 = (I-functor(E,rng I)*G)-indexing_of C by A2
.= J2 by A3;
end;
end;
theorem Th22:
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
proof
let C,D1,D2,E be Category, I be Indexing of E;
let F be Functor of C,D1, G be Functor of C,D2;
assume that
A1: Image F is Subcategory of E and
A2: Image G is Subcategory of E and
A3: F = G;
reconsider F9 = F as Functor of C, Image F by CAT_5:8;
reconsider F9 as Functor of C,E by A1,Lm6;
I*F = (I-functor(E,rng I)*F9)-indexing_of C by A1,Def16;
hence thesis by A2,A3,Def16;
end;
theorem Th23:
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
proof
let C,D be Category;
let F be Functor of C,D;
let I be Indexing of D;
let T be TargetCat of I;
Image F is Subcategory of D;
then
A1: I*F = (I-functor(D,rng I)*F)-indexing_of C by Def16;
(I-functor(D,rng I))*F = (I-functor(D,T))*F by Th11;
hence thesis by A1,Th2;
end;
theorem Th24:
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
proof
let C,D be Category;
let F be Functor of C,D;
let I be Indexing of D;
let T be TargetCat of I;
set T9 = the TargetCat of I*F;
rng (I*F) = Image ((I*F)-functor(C,T9)) & I*F = ((I-functor(D,T))*F)
-indexing_of C by Def12,Th23;
then rng (I*F) = Image ((I-functor(D,T))*F) by Th18,CAT_5:22;
hence thesis by Th14;
end;
theorem
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
proof
let C,D be Category;
let F be Functor of C,D;
let I be Indexing of D;
let T be TargetCat of I;
T is TargetCat of I*F by Th24;
hence thesis by Th14;
end;
theorem Th26:
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)
proof
let C,D,E be Category;
let F be Functor of C,D;
let G be Functor of D,E;
let I be Indexing of E;
set T = rng I;
reconsider T9 = T as TargetCat of I*G by Th24;
I*G = ((I-functor(E,T))*G)-indexing_of D by Th23;
then (I*G)-functor(D,T9) = (I-functor(E,T))*G by Th18;
hence (I*G)*F = ((I-functor(E,T))*G*F)-indexing_of C by Th23
.= ((I-functor(E,T))*(G*F))-indexing_of C by RELAT_1:36
.= I*(G*F) by Th23;
end;
definition
let C be Category;
let I be Indexing of C;
let D be Categorial Category such that
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:
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;
existence
proof
reconsider T = D as TargetCat of I by A1;
reconsider G = F as Functor of T,E;
take (G*(I-functor(C,T)))-indexing_of C;
thus thesis;
end;
uniqueness
proof
reconsider T = D as TargetCat of I by A1;
reconsider G = F as Functor of T,E;
let J1, J2 be Indexing of C;
assume
A2: not thesis;
then J1 = (G*(I-functor(C,T)))-indexing_of C;
hence thesis by A2;
end;
end;
theorem Th27:
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
proof
let C be Category;
let I be Indexing of C;
let T be TargetCat of I, D,E be Categorial Category;
let F be Functor of T,D;
let G be Functor of T,E;
assume
A1: F = G;
thus F*I = (F*(I-functor(C,T)))-indexing_of C by Def17
.= (G*(I-functor(C,T)))-indexing_of C by A1,Th2
.= G*I by Def17;
end;
theorem Th28:
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
proof
let C be Category;
let I be Indexing of C;
let T be TargetCat of I, D be Categorial Category;
let F be Functor of T,D;
reconsider F9 = F as Functor of T, Image F by CAT_5:8;
set T9 = the TargetCat of F*I;
A1: rng (F*I) = Image ((F*I)-functor(C,T9)) by Def12;
F*I = F9*I by Th27
.= (F9*(I-functor(C,T)))-indexing_of C by Def17;
then rng (F*I) = Image (F9*(I-functor(C,T))) by A1,Th18,CAT_5:22;
hence thesis by Th14;
end;
theorem Th29:
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
proof
let C be Category;
let I be Indexing of C;
let T be TargetCat of I, D be Categorial Category;
let F be Functor of T,D;
Image F is TargetCat of F*I by Th28;
then rng (F*I) is Subcategory of Image F by Th14;
then rng (F*I) is Subcategory of D by CAT_5:4;
hence thesis by Th14;
end;
theorem
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
proof
let C be Category;
let I be Indexing of C;
let T be TargetCat of I, D be Categorial Category;
let F be Functor of T,D;
Image F is TargetCat of F*I by Th28;
hence thesis by Th14;
end;
theorem
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)
proof
let C be Category;
let I be Indexing of C;
let T be TargetCat of I;
let D,E be Categorial Category;
let F be Functor of T,D;
reconsider D9 = D as TargetCat of F*I by Th29;
let G be Functor of D,E;
reconsider G9 = G as Functor of D9, E;
F*I = (F*(I-functor(C,T)))-indexing_of C by Def17;
then
A1: (F*I)-functor(C,D9) = F*(I-functor(C,T)) by Th18;
thus (G*F)*I = ((G*F)*(I-functor(C,T)))-indexing_of C by Def17
.= (G9*((F*I)-functor(C,D9)))-indexing_of C by A1,RELAT_1:36
.= G*(F*I) by Def17;
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
I2*(I1-functor(C,rng I1));
correctness;
end;
theorem Th32:
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))
proof
let C be Category, D be Categorial Category;
let I1 be Indexing of C;
let I2 be Indexing of D;
let T be TargetCat of I1;
assume D is TargetCat of I1;
then reconsider D9 = D as TargetCat of I1;
A1: Image (I1-functor(C,rng I1)) = rng I1 by Def12;
Image (I1-functor(C,D9)) = rng I1 & Image (I1-functor(C,T)) = rng I1 by Def12
;
hence thesis by A1,Th11,Th22;
end;
theorem
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
proof
let C be Category, D be Categorial Category;
let I1 be Indexing of C;
let I2 be Indexing of D;
let T be TargetCat of I2;
assume D is TargetCat of I1;
then reconsider D9 = D as TargetCat of I1;
reconsider I29 = I2 as Indexing of D9;
reconsider T9 = T as TargetCat of I29;
Image (I1-functor(C,D9)) = rng I1 & Image (I1-functor(C,rng I1)) = rng
I1 by Def12;
hence I2*I1 = I2*(I1-functor(C,D9)) by Th11,Th22
.= (I29-functor(D9,T9)*(I1-functor(C,D9)))-indexing_of C by Th23
.= (I2-functor(D,T))*I1 by Def17;
end;
theorem Th34:
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)
proof
let C,D be Category, F be Functor of C,D, I be Indexing of D;
let T be TargetCat of I;
reconsider T9 = T as TargetCat of I*F by Th24;
let E be Categorial Category, G be Functor of T,E;
reconsider G9 = G as Functor of T9, E;
reconsider GI = rng (G*I) as TargetCat of (G*(I-functor(D,T)))-indexing_of D
by Def17;
A1: I*F = ((I-functor(D,T))*F)-indexing_of C by Th23;
A2: ((G*(I-functor(D,T)))-indexing_of D)-functor(D,GI) = G*(I-functor(D,T))
by Th18;
G*I = (G*(I-functor(D,T)))-indexing_of D & Image F is Subcategory of D
by Def17;
hence (G*I)*F = (((G*(I-functor(D,T)))-indexing_of D)-functor(D,GI)*F)
-indexing_of C by Def16
.= ((G*(I-functor(D,T))) * F) -indexing_of C by A2,Th2
.= (G * ((I-functor(D,T))*F)) -indexing_of C by RELAT_1:36
.= (G9*((I*F)-functor(C,T9)))-indexing_of C by A1,Th18
.= G*(I*F) by Def17;
end;
theorem
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)
proof
let C be Category, I be Indexing of C;
let T be TargetCat of I;
let D be Categorial Category, F be Functor of T,D;
let J be Indexing of D;
A1: F*I = (F*(I-functor(C,T)))-indexing_of C & Image (F*(I-functor(C,T))) is
Subcategory of D by Def17;
D is TargetCat of F*I by Th29;
then rng (F*I) is Subcategory of D by Th14;
then
A2: Image ((F*I)-functor(C, rng (F*I))) is Subcategory of D by CAT_5:4;
thus (J*F)*I = (J*F)*(I-functor(C,T)) by Th32
.= J*(F*(I-functor(C,T))) by Th26
.= J*(F*I) by A1,A2,Th18,Th22;
end;
theorem
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)
proof
let C be Category, I be Indexing of C;
let T1 be TargetCat of I;
let J be Indexing of T1;
let T2 be TargetCat of J;
let D be Categorial Category, F be Functor of T2,D;
thus (F*J)*I = (F*J)*(I-functor(C,T1)) by Th32
.= F*(J*(I-functor(C,T1))) by Th34
.= F*(J*I) by Th32;
end;
theorem Th37:
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)
proof
let C,D be Category, F be Functor of C,D, I be Indexing of D;
let T be TargetCat of I, J be Indexing of T;
A1: I*F = ((I-functor(D,T))*F)-indexing_of C & Image ((I-functor(D,T))*F) is
Subcategory of T by Th23;
T is TargetCat of I*F by Th24;
then rng (I*F) is Subcategory of T by Th14;
then
A2: Image ((I*F)-functor(C, rng (I*F))) is Subcategory of T by CAT_5:4;
thus (J*I)*F = (J*(I-functor(D,T)))*F by Th32
.= J*((I-functor(D,T))*F) by Th26
.= J*(I*F) by A1,A2,Th18,Th22;
end;
theorem
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)
proof
let C be Category, I be Indexing of C;
let D be TargetCat of I, J be Indexing of D;
let E be TargetCat of J, K be Indexing of E;
thus (K*J)*I = (K*J)*(I-functor(C,D)) by Th32
.= K*(J*(I-functor(C,D))) by Th37
.= K*(J*I) by Th32;
end;
theorem
for C being Category holds IdMap C = IdMap(C opp) by Lm2;