:: Indexed Category
:: by Grzegorz Bancerek
::
:: Received June 8, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, RELAT_1, PBOOLE, SUBSET_1, CAT_5, CAT_1, MCART_1,
GRCAT_1, GRAPH_1, STRUCT_0, FUNCT_1, FUNCOP_1, PARTFUN1, ZFMISC_1,
ARYTM_0, TARSKI, GROUP_6, CAT_2, FUNCT_3, INDEX_1, MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1,
RELAT_1, FUNCT_1, BINOP_1, PARTFUN1, PBOOLE, FUNCOP_1, FUNCT_2, FUNCT_4,
STRUCT_0, GRAPH_1, CAT_1, CAT_2, OPPCAT_1, CAT_5, ISOCAT_1;
constructors DOMAIN_1, OPPCAT_1, CAT_5, RELSET_1, PBOOLE, XTUPLE_0, ISOCAT_1,
REALSET1, XFAMILY, FUNCT_4;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, PBOOLE, CAT_2, CAT_5,
STRUCT_0, RELSET_1, CAT_1, XTUPLE_0, OPPCAT_1;
requirements SUBSET, BOOLE;
begin :: Category Yielding Functions
registration
let A be non empty set;
cluster non empty-yielding for ManySortedSet of A;
end;
definition
let C be Categorial Category;
let f be Morphism of C;
redefine func f`2 -> Functor of f`11, f`12;
end;
theorem :: INDEX_1:1
for C being Categorial Category, f,g being Morphism of C st dom g =
cod f holds g(*)f = [[dom f, cod g], g`2*f`2];
theorem :: INDEX_1:2
for C being Category, D,E being Categorial Category for F being
Functor of C,D for G being Functor of C,E st F = G holds Obj F = Obj G;
definition
let IT be Function;
attr IT is Category-yielding means
:: INDEX_1:def 1
for x being set st x in dom IT holds IT.x is Category;
end;
registration
cluster Category-yielding for Function;
end;
registration
let X be set;
cluster Category-yielding for ManySortedSet of X;
end;
definition
let A be set;
mode ManySortedCategory of A is Category-yielding ManySortedSet of A;
end;
definition
let C be Category;
mode ManySortedCategory of C is ManySortedCategory of the carrier of C;
end;
registration
let X be set, x be Category;
cluster X --> x -> Category-yielding;
end;
registration
let X be non empty set;
cluster -> non empty for ManySortedSet of X;
end;
registration
let f be Category-yielding Function;
cluster rng f -> categorial;
end;
definition
let X be non empty set;
let f be ManySortedCategory of X;
let x be Element of X;
redefine func f.x -> Category;
end;
registration
let f be Function;
let g be Category-yielding Function;
cluster g*f -> Category-yielding;
end;
:: carrier and Morphisms
definition
let F be Category-yielding Function;
func Objs F -> non-empty Function means
:: INDEX_1:def 2
dom it = dom F &
for x being object st x in dom F
for C being Category st C = F.x holds it.x = the carrier of C;
func Mphs F -> non-empty Function means
:: INDEX_1:def 3
dom it = dom F & for x being object st x in dom F
for C being Category st C = F.x holds it.x = the carrier' of
C;
end;
registration
let A be non empty set;
let F be ManySortedCategory of A;
cluster Objs F -> A-defined;
cluster Mphs F -> A-defined;
end;
registration
let A be non empty set;
let F be ManySortedCategory of A;
cluster Objs F -> total;
cluster Mphs F -> total;
end;
theorem :: INDEX_1:3
for X being set, C being Category holds Objs (X --> C) = X --> the
carrier of C & Mphs (X --> C) = X --> the carrier' of C;
begin :: Pairs of Many Sorted Sets
definition
let A,B be set;
mode ManySortedSet of A,B -> object means
:: INDEX_1:def 4
ex f being (ManySortedSet of A), g being ManySortedSet of B st it = [f,g];
end;
definition
let A,B be set;
let f be ManySortedSet of A;
let g be ManySortedSet of B;
redefine func [f,g] -> ManySortedSet of A,B;
end;
registration
let A, B be set;
let X be ManySortedSet of A,B;
cluster X`1 -> Function-like Relation-like for set;
cluster X`2 -> Function-like Relation-like for set;
end;
registration
let A, B be set;
let X be ManySortedSet of A,B;
cluster X`1 -> A-defined for Relation;
cluster X`2 -> B-defined for Relation;
end;
registration
let A, B be set;
let X be ManySortedSet of A,B;
cluster X`1 -> total for A-defined Function;
cluster X`2 -> total for B-defined Function;
end;
definition
let A,B be set;
let IT be ManySortedSet of A,B;
attr IT is Category-yielding_on_first means
:: INDEX_1:def 5
IT`1 is Category-yielding;
attr IT is Function-yielding_on_second means
:: INDEX_1:def 6
IT`2 is Function-yielding;
end;
registration
let A,B be set;
cluster Category-yielding_on_first Function-yielding_on_second for
ManySortedSet
of A,B;
end;
registration
let A, B be set;
let X be Category-yielding_on_first ManySortedSet of A,B;
cluster X`1 -> Category-yielding for Function;
end;
registration
let A, B be set;
let X be Function-yielding_on_second ManySortedSet of A,B;
cluster X`2 -> Function-yielding for Function;
end;
registration
let f be Function-yielding Function;
cluster rng f -> functional;
end;
definition
let A,B be set;
let f be ManySortedCategory of A;
let g be ManySortedFunction of B;
redefine func [f,g] -> Category-yielding_on_first
Function-yielding_on_second ManySortedSet of A,B;
end;
definition
let A be non empty set;
let F,G be ManySortedCategory of A;
mode ManySortedFunctor of F,G -> ManySortedFunction of A means
:: INDEX_1:def 7
for a being Element of A holds it.a is Functor of F.a, G.a;
end;
scheme :: INDEX_1:sch 1
LambdaMSFr {A() -> non empty set, C1, C2() -> ManySortedCategory of A(), F(
object) -> set}:
ex F being ManySortedFunctor of C1(), C2() st for a being Element
of A() holds F.a = F(a)
provided
for a being Element of A() holds F(a) is Functor of C1().a, C2().a;
definition
let A be non empty set;
let F,G be ManySortedCategory of A;
let f be ManySortedFunctor of F,G;
let a be Element of A;
redefine func f.a -> Functor of F.a, G.a;
end;
begin :: Indexing
definition
let A,B be non empty set;
let F,G be Function of B,A;
mode Indexing of F,G -> Category-yielding_on_first ManySortedSet of A,B
means
:: INDEX_1:def 8
it`2 is ManySortedFunctor of it`1*F, it`1*G;
end;
theorem :: INDEX_1:4
for A,B being non empty set, F,G being Function of B,A for I
being Indexing of F,G for m being Element of B holds I`2.m is Functor of I`1.(F
.m), I`1.(G.m);
theorem :: INDEX_1:5
for C being Category, I being Indexing of the Source of C, the Target
of C for m being Morphism of C holds I`2.m is Functor of I`1.dom m, I`1.cod m
;
definition
let A,B be non empty set;
let F,G be Function of B,A;
let I be Indexing of F,G;
redefine func I`2 -> ManySortedFunctor of I`1*F,I`1*G;
end;
definition
let A,B be non empty set;
let F,G be Function of B,A;
let I be Indexing of F,G;
mode TargetCat of I -> Categorial Category means
:: INDEX_1:def 9
(for a being
Element of A holds I`1.a is Object of it) & for b being Element of B holds [[I
`1.(F.b),I`1.(G.b)],I`2.b] is Morphism of it;
end;
registration
let A,B be non empty set;
let F,G be Function of B,A;
let I be Indexing of F,G;
cluster full strict for TargetCat of I;
end;
definition
:: This is very technical definition made for having the indexing and
:: coindexing as the same mode.
let A,B be non empty set;
let F,G be Function of B,A;
let c be PartFunc of [:B,B:], B;
let i be Function of A,B;
given C being Category such that
C = CatStr(#A, B, F, G, c#);
mode Indexing of F, G, c, i -> Indexing of F,G means
:: INDEX_1:def 10
(for a being
Element of A holds it`2.(i.a) = id (it`1.a)) & for m1, m2 being Element of B st
F.m2 = G.m1 holds it`2.(c.[m2,m1]) = (it`2.m2)*(it`2.m1);
end;
definition
let C be Category;
mode Indexing of C is Indexing of the Source of C, the Target of C, the Comp
of C, IdMap C;
mode coIndexing of C is
Indexing of the Target of C, the Source of C, ~(the Comp of C), IdMap C;
end;
theorem :: INDEX_1:6
for C being Category, I being Indexing of the Source of C, the
Target of C holds I is Indexing of C iff (for a being Object of C holds I`2.id
a = id (I`1.a)) & for m1, m2 being Morphism of C st dom m2 = cod m1 holds I`2.(
m2(*)m1) = (I`2.m2)*(I`2.m1);
theorem :: INDEX_1:7
for C being Category, I being Indexing of the Target of C, the
Source of C holds I is coIndexing of C iff (for a being Object of C holds I`2.
id a = id (I`1.a)) & for m1, m2 being Morphism of C st dom m2 = cod m1 holds I
`2.(m2(*)m1) = (I`2.m1)*(I`2.m2);
theorem :: INDEX_1:8
for C being Category, x be set holds x is coIndexing of C iff x is
Indexing of C opp;
theorem :: INDEX_1:9
for C being Category, I being Indexing of C for c1,c2 being Object of
C st Hom(c1,c2) is non empty for m being Morphism of c1,c2 holds I`2.m is
Functor of I`1.c1, I`1.c2;
theorem :: INDEX_1:10
for C being Category, I being coIndexing of C for c1,c2 being Object
of C st Hom(c1,c2) is non empty for m being Morphism of c1,c2 holds I`2.m is
Functor of I`1.c2, I`1.c1;
definition
let C be Category;
let I be Indexing of C;
let T be TargetCat of I;
func I-functor(C,T) -> Functor of C,T means
:: INDEX_1:def 11
for f being Morphism of C holds it.f = [[I`1.dom f, I`1.cod f], I`2.f];
end;
theorem :: INDEX_1:11
for C being Category, I being Indexing of C for T1,T2 being
TargetCat of I holds I-functor(C,T1) = I-functor(C,T2) & Obj (I-functor(C,T1))
= Obj (I-functor(C,T2));
theorem :: INDEX_1:12
for C being Category, I being Indexing of C for T being TargetCat of I
holds Obj (I-functor(C,T)) = I`1;
theorem :: INDEX_1:13
for C being Category, I being Indexing of C for T being TargetCat of I
, x being Object of C holds (I-functor(C,T)).x = I`1.x;
definition
let C be Category;
let I be Indexing of C;
func rng I -> strict TargetCat of I means
:: INDEX_1:def 12
for T being TargetCat of I holds it = Image (I-functor(C,T));
end;
theorem :: INDEX_1:14
for C being Category, I be Indexing of C for D being Categorial
Category holds rng I is Subcategory of D iff D is TargetCat of I;
definition
let C be Category;
let I be Indexing of C;
let m be Morphism of C;
func I.m -> Functor of I`1.dom m, I`1.cod m equals
:: INDEX_1:def 13
I`2.m;
end;
definition
let C be Category;
let I be coIndexing of C;
let m be Morphism of C;
func I.m -> Functor of I`1.cod m, I`1.dom m equals
:: INDEX_1:def 14
I`2.m;
end;
theorem :: INDEX_1:15
for C,D being Category holds [(the carrier of C) --> D, (the carrier'
of C) --> id D] is Indexing of C & [(the carrier of C) --> D, (the carrier' of
C) --> id D] is coIndexing of C;
begin :: Indexing vs Functor into Categorial Categories
registration
let C be Category, D be Categorial Category;
let F be Functor of C,D;
cluster Obj F -> Category-yielding;
end;
theorem :: INDEX_1:16
for C being Category, D being Categorial Category, F being
Functor of C,D holds [Obj F, pr2 F] is Indexing of C;
definition
let C be Category;
let D be Categorial Category;
let F be Functor of C,D;
func F-indexing_of C -> Indexing of C equals
:: INDEX_1:def 15
[Obj F, pr2 F];
end;
theorem :: INDEX_1:17
for C being Category, D being Categorial Category, F being Functor of
C,D holds D is TargetCat of F-indexing_of C;
theorem :: INDEX_1:18
for C being Category, D being Categorial Category, F being
Functor of C,D for T being TargetCat of F-indexing_of C holds F = (F
-indexing_of C)-functor(C,T);
theorem :: INDEX_1:19
for C being Category, D,E being Categorial Category for F being
Functor of C,D for G being Functor of C,E st F = G holds F-indexing_of C = G
-indexing_of C;
theorem :: INDEX_1:20
for C being Category, I being (Indexing of C), T being TargetCat
of I holds pr2 (I-functor(C,T)) = I`2;
theorem :: INDEX_1:21
for C being Category, I being (Indexing of C), T being TargetCat of I
holds (I-functor(C,T))-indexing_of C = I;
begin
definition
let C,D,E be Category;
let F be Functor of C,D;
let I be Indexing of E;
assume
Image F is Subcategory of E;
func I*F -> Indexing of C means
:: INDEX_1:def 16
for F9 being Functor of C,E st F9 =
F holds it = (I-functor(E,rng I)*F9)-indexing_of C;
end;
theorem :: INDEX_1:22
for C,D1,D2,E being Category, I being Indexing of E for F being
Functor of C,D1 for G being Functor of C,D2 st Image F is Subcategory of E &
Image G is Subcategory of E & F = G holds I*F = I*G;
theorem :: INDEX_1:23
for C,D being Category, F being Functor of C,D, I being Indexing
of D for T being TargetCat of I holds I*F = ((I-functor(D,T))*F)-indexing_of C;
theorem :: INDEX_1:24
for C,D being Category, F being Functor of C,D, I being Indexing
of D for T being TargetCat of I holds T is TargetCat of I*F;
theorem :: INDEX_1:25
for C,D being Category, F being Functor of C,D, I being Indexing of D
for T being TargetCat of I holds rng (I*F) is Subcategory of T;
theorem :: INDEX_1:26
for C,D,E being Category, F being Functor of C,D for G being
Functor of D,E, I being Indexing of E holds (I*G)*F = I*(G*F);
definition
let C be Category;
let I be Indexing of C;
let D be Categorial Category such that
D is TargetCat of I;
let E be Categorial Category;
let F be Functor of D,E;
func F*I -> Indexing of C means
:: INDEX_1:def 17
for T being TargetCat of I, G being
Functor of T,E st T = D & G = F holds it = (G*(I-functor(C,T)))-indexing_of C;
end;
theorem :: INDEX_1:27
for C being Category, I being Indexing of C for T being
TargetCat of I, D,E being Categorial Category for F being Functor of T,D for G
being Functor of T,E st F = G holds F*I = G*I;
theorem :: INDEX_1:28
for C being Category, I being Indexing of C for T being
TargetCat of I, D being Categorial Category for F being Functor of T,D holds
Image F is TargetCat of F*I;
theorem :: INDEX_1:29
for C being Category, I being Indexing of C for T being
TargetCat of I, D being Categorial Category for F being Functor of T,D holds D
is TargetCat of F*I;
theorem :: INDEX_1:30
for C being Category, I being Indexing of C for T being TargetCat of I
, D being Categorial Category for F being Functor of T,D holds rng (F*I) is
Subcategory of Image F;
theorem :: INDEX_1:31
for C be Category, I being Indexing of C for T being TargetCat of I
for D,E being Categorial Category, F being Functor of T,D for G being Functor
of D,E holds (G*F)*I = G*(F*I);
definition
let C,D be Category;
let I1 be Indexing of C;
let I2 be Indexing of D;
func I2*I1 -> Indexing of C equals
:: INDEX_1:def 18
I2*(I1-functor(C,rng I1));
end;
theorem :: INDEX_1:32
for C being Category, D being Categorial Category, I1 being
Indexing of C for I2 being Indexing of D for T being TargetCat of I1 st D is
TargetCat of I1 holds I2*I1 = I2*(I1-functor(C,T));
theorem :: INDEX_1:33
for C being Category, D being Categorial Category, I1 being Indexing
of C for I2 being Indexing of D for T being TargetCat of I2 st D is TargetCat
of I1 holds I2*I1 = (I2-functor(D,T))*I1;
theorem :: INDEX_1:34
for C,D being Category, F being Functor of C,D, I being Indexing
of D for T being TargetCat of I, E being Categorial Category for G being
Functor of T,E holds (G*I)*F = G*(I*F);
theorem :: INDEX_1:35
for C being Category, I being Indexing of C for T being TargetCat of I
, D being Categorial Category for F being Functor of T,D, J being Indexing of D
holds (J*F)*I = J*(F*I);
theorem :: INDEX_1:36
for C being Category, I being Indexing of C for T1 being TargetCat of
I, J being Indexing of T1 for T2 being TargetCat of J for D being Categorial
Category, F being Functor of T2,D holds (F*J)*I = F*(J*I);
theorem :: INDEX_1:37
for C,D being Category, F being Functor of C,D, I being Indexing
of D for T being TargetCat of I, J being Indexing of T holds (J*I)*F = J*(I*F);
theorem :: INDEX_1:38
for C being Category, I being Indexing of C for D being TargetCat of I
, J being Indexing of D for E being TargetCat of J, K being Indexing of E holds
(K*J)*I = K*(J*I);
theorem :: INDEX_1:39
for C being Category holds IdMap C = IdMap(C opp);