Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### Indexed Category

**by****Grzegorz Bancerek**- Received June 8, 1995
- MML identifier: INDEX_1

- [ Mizar article, MML identifier index ]

environ vocabulary MATRIX_1, PBOOLE, ZF_REFLE, FUNCT_1, CAT_5, CAT_1, MCART_1, COMMACAT, GRCAT_1, RELAT_1, BOOLE, FUNCOP_1, PRALG_1, FRAENKEL, PARTFUN1, OPPCAT_1, GROUP_6, CAT_2, FUNCT_3, INDEX_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, PBOOLE, FRAENKEL, MSUALG_1, PRALG_1, DTCONSTR, CAT_1, CAT_2, OPPCAT_1, COMMACAT, PRE_CIRC, CAT_5; constructors MSUALG_3, PRE_CIRC, OPPCAT_1, CAT_5, ISOCAT_1, DOMAIN_1; clusters FUNCT_1, RELSET_1, PRVECT_1, CAT_2, PBOOLE, PRALG_1, CAT_5, FUNCOP_1, CIRCCOMB, RELAT_1; requirements SUBSET, BOOLE; begin :: Category Yielding Functions definition let A be non empty set; cluster non empty-yielding ManySortedSet of A; end; definition let A be non empty set; cluster non-empty -> non empty-yielding ManySortedSet of A; end; definition let C be Categorial Category; let f be Morphism of C; redefine func f`2 -> Functor of f`11, f`12; end; theorem :: INDEX_1:1 for C being Categorial Category, f,g being Morphism of C st dom g = cod f holds g*f = [[dom f, cod g], g`2*f`2]; theorem :: INDEX_1:2 for C being Category, D,E being Categorial Category for F being Functor of C,D for G being Functor of C,E st F = G holds Obj F = Obj G; definition let IT be Function; attr IT is Category-yielding means :: INDEX_1:def 1 for x being set st x in dom IT holds IT.x is Category; end; definition cluster Category-yielding Function; end; definition let X be set; cluster Category-yielding ManySortedSet of X; end; definition let A be set; mode ManySortedCategory of A is Category-yielding ManySortedSet of A; end; definition let C be Category; mode ManySortedSet of C is ManySortedSet of the Objects of C; mode ManySortedCategory of C is ManySortedCategory of the Objects of C; end; definition let X be set, x be Category; cluster X --> x -> Category-yielding; end; definition let X be non empty set; cluster -> non empty ManySortedSet of X; end; definition let f be Category-yielding Function; cluster rng f -> categorial; end; definition let X be non empty set; let f be ManySortedCategory of X; let x be Element of X; redefine func f.x -> Category; end; definition let f be Function; let g be Category-yielding Function; cluster g*f -> Category-yielding; end; :: Objects and Morphisms definition let F be Category-yielding Function; func Objs F -> non-empty Function means :: INDEX_1:def 2 dom it = dom F & for x being set st x in dom F for C being Category st C = F.x holds it.x = the Objects of C; func Mphs F -> non-empty Function means :: INDEX_1:def 3 dom it = dom F & for x being set st x in dom F for C being Category st C = F.x holds it.x = the Morphisms of C; end; definition let A be non empty set; let F be ManySortedCategory of A; redefine func Objs F -> non-empty ManySortedSet of A; func Mphs F -> non-empty ManySortedSet of A; end; theorem :: INDEX_1:3 for X being set, C being Category holds Objs (X --> C) = X --> the Objects of C & Mphs (X --> C) = X --> the Morphisms of C; begin :: Pairs of Many Sorted Sets definition let A,B be set; mode ManySortedSet of A,B means :: INDEX_1:def 4 ex f being (ManySortedSet of A), g being ManySortedSet of B st it = [f,g]; end; definition let A,B be set; let f be ManySortedSet of A; let g be ManySortedSet of B; redefine func [f,g] -> ManySortedSet of A,B; end; definition let A, B be set; let X be ManySortedSet of A,B; redefine func X`1 -> ManySortedSet of A; func X`2 -> ManySortedSet of B; end; definition let A,B be set; let IT be ManySortedSet of A,B; attr IT is Category-yielding_on_first means :: INDEX_1:def 5 IT`1 is Category-yielding; attr IT is Function-yielding_on_second means :: INDEX_1:def 6 IT`2 is Function-yielding; end; definition let A,B be set; cluster Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B; end; definition let A, B be set; let X be Category-yielding_on_first ManySortedSet of A,B; redefine func X`1 -> ManySortedCategory of A; end; definition let A, B be set; let X be Function-yielding_on_second ManySortedSet of A,B; redefine func X`2 -> ManySortedFunction of B; end; definition let f be Function-yielding Function; cluster rng f -> functional; end; definition let A,B be set; let f be ManySortedCategory of A; let g be ManySortedFunction of B; redefine func [f,g] -> Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B; end; definition let A be non empty set; let F,G be ManySortedCategory of A; mode ManySortedFunctor of F,G -> ManySortedFunction of A means :: INDEX_1:def 7 for a being Element of A holds it.a is Functor of F.a, G.a; end; scheme LambdaMSFr {A() -> non empty set, C1, C2() -> ManySortedCategory of A(), F(set) -> set}: ex F being ManySortedFunctor of C1(), C2() st for a being Element of A() holds F.a = F(a) provided for a being Element of A() holds F(a) is Functor of C1().a, C2().a; definition let A be non empty set; let F,G be ManySortedCategory of A; let f be ManySortedFunctor of F,G; let a be Element of A; redefine func f.a -> Functor of F.a, G.a; end; begin :: Indexing definition let A,B be non empty set; let F,G be Function of B,A; mode Indexing of F,G -> Category-yielding_on_first ManySortedSet of A,B means :: INDEX_1:def 8 it`2 is ManySortedFunctor of it`1*F, it`1*G; end; theorem :: INDEX_1:4 for A,B being non empty set, F,G being Function of B,A for I being Indexing of F,G for m being Element of B holds I`2.m is Functor of I`1.(F.m), I`1.(G.m); theorem :: INDEX_1:5 for C being Category, I being Indexing of the Dom of C, the Cod of C for m being Morphism of C holds I`2.m is Functor of I`1.dom m, I`1.cod m; definition let A,B be non empty set; let F,G be Function of B,A; let I be Indexing of F,G; redefine func I`2 -> ManySortedFunctor of I`1*F,I`1*G; end; definition let A,B be non empty set; let F,G be Function of B,A; let I be Indexing of F,G; mode TargetCat of I -> Categorial Category means :: INDEX_1:def 9 (for a being Element of A holds I`1.a is Object of it) & (for b being Element of B holds [[I`1.(F.b),I`1.(G.b)],I`2.b] is Morphism of it); end; definition let A,B be non empty set; let F,G be Function of B,A; let I be Indexing of F,G; cluster full strict TargetCat of I; end; definition :: This is very technical definition made for having the indexing and :: coindexing as the same mode. let A,B be non empty set; let F,G be Function of B,A; let c be PartFunc of [:B,B:], B; let i be Function of A,B; given C being Category such that C = CatStr(#A, B, F, G, c, i#); mode Indexing of F, G, c, i -> Indexing of F,G means :: INDEX_1:def 10 (for a being Element of A holds it`2.(i.a) = id (it`1.a)) & for m1, m2 being Element of B st F.m2 = G.m1 holds it`2.(c.[m2,m1]) = (it`2.m2)*(it`2.m1); end; definition let C be Category; mode Indexing of C is Indexing of the Dom of C, the Cod of C, the Comp of C, the Id of C; mode coIndexing of C is Indexing of the Cod of C, the Dom of C, ~(the Comp of C), the Id of C; end; theorem :: INDEX_1:6 for C being Category, I being Indexing of the Dom of C, the Cod of C holds I is Indexing of C iff (for a being Object of C holds I`2.id a = id (I`1.a)) & for m1, m2 being Morphism of C st dom m2 = cod m1 holds I`2.(m2*m1) = (I`2.m2)*(I`2.m1); theorem :: INDEX_1:7 for C being Category, I being Indexing of the Cod of C, the Dom of C holds I is coIndexing of C iff (for a being Object of C holds I`2.id a = id (I`1.a)) & for m1, m2 being Morphism of C st dom m2 = cod m1 holds I`2.(m2*m1) = (I`2.m1)*(I`2.m2); theorem :: INDEX_1:8 for C being Category, x be set holds x is coIndexing of C iff x is Indexing of C opp; theorem :: INDEX_1:9 for C being Category, I being Indexing of C for c1,c2 being Object of C st Hom(c1,c2) is non empty for m being Morphism of c1,c2 holds I`2.m is Functor of I`1.c1, I`1.c2; theorem :: INDEX_1:10 for C being Category, I being coIndexing of C for c1,c2 being Object of C st Hom(c1,c2) is non empty for m being Morphism of c1,c2 holds I`2.m is Functor of I`1.c2, I`1.c1; definition let C be Category; let I be Indexing of C; let T be TargetCat of I; func I-functor(C,T) -> Functor of C,T means :: INDEX_1:def 11 for f being Morphism of C holds it.f = [[I`1.dom f, I`1.cod f], I`2.f]; end; theorem :: INDEX_1:11 for C being Category, I being Indexing of C for T1,T2 being TargetCat of I holds I-functor(C,T1) = I-functor(C,T2) & Obj (I-functor(C,T1)) = Obj (I-functor(C,T2)); theorem :: INDEX_1:12 for C being Category, I being Indexing of C for T being TargetCat of I holds Obj (I-functor(C,T)) = I`1; theorem :: INDEX_1:13 for C being Category, I being Indexing of C for T being TargetCat of I, x being Object of C holds (I-functor(C,T)).x = I`1.x; definition let C be Category; let I be Indexing of C; func rng I -> strict TargetCat of I means :: INDEX_1:def 12 for T being TargetCat of I holds it = Image (I-functor(C,T)); end; theorem :: INDEX_1:14 for C being Category, I be Indexing of C for D being Categorial Category holds rng I is Subcategory of D iff D is TargetCat of I; definition let C be Category; let I be Indexing of C; let m be Morphism of C; func I.m -> Functor of I`1.dom m, I`1.cod m equals :: INDEX_1:def 13 I`2.m; end; definition let C be Category; let I be coIndexing of C; let m be Morphism of C; func I.m -> Functor of I`1.cod m, I`1.dom m equals :: INDEX_1:def 14 I`2.m; end; theorem :: INDEX_1:15 for C,D being Category holds [(the Objects of C) --> D, (the Morphisms of C) --> id D] is Indexing of C & [(the Objects of C) --> D, (the Morphisms of C) --> id D] is coIndexing of C; begin :: Indexing vs Functor into Categorial Categories definition let C be Category, D be Categorial Category; let F be Functor of C,D; cluster Obj F -> Category-yielding; end; theorem :: INDEX_1:16 for C being Category, D being Categorial Category, F being Functor of C,D holds [Obj F, pr2 F] is Indexing of C; definition let C be Category; let D be Categorial Category; let F be Functor of C,D; func F-indexing_of C -> Indexing of C equals :: INDEX_1:def 15 [Obj F, pr2 F]; end; theorem :: INDEX_1:17 for C being Category, D being Categorial Category, F being Functor of C,D holds D is TargetCat of F-indexing_of C; theorem :: INDEX_1:18 for C being Category, D being Categorial Category, F being Functor of C,D for T being TargetCat of F-indexing_of C holds F = (F-indexing_of C)-functor(C,T); theorem :: INDEX_1:19 for C being Category, D,E being Categorial Category for F being Functor of C,D for G being Functor of C,E st F = G holds F-indexing_of C = G-indexing_of C; theorem :: INDEX_1:20 for C being Category, I being (Indexing of C), T being TargetCat of I holds pr2 (I-functor(C,T)) = I`2; theorem :: INDEX_1:21 for C being Category, I being (Indexing of C), T being TargetCat of I holds (I-functor(C,T))-indexing_of C = I; begin definition let C,D,E be Category; let F be Functor of C,D; let I be Indexing of E; assume Image F is Subcategory of E; func I*F -> Indexing of C means :: INDEX_1:def 16 for F' being Functor of C,E st F' = F holds it = (I-functor(E,rng I)*F')-indexing_of C; end; theorem :: INDEX_1:22 for C,D1,D2,E being Category, I being Indexing of E for F being Functor of C,D1 for G being Functor of C,D2 st Image F is Subcategory of E & Image G is Subcategory of E & F = G holds I*F = I*G; theorem :: INDEX_1:23 for C,D being Category, F being Functor of C,D, I being Indexing of D for T being TargetCat of I holds I*F = ((I-functor(D,T))*F)-indexing_of C; theorem :: INDEX_1:24 for C,D being Category, F being Functor of C,D, I being Indexing of D for T being TargetCat of I holds T is TargetCat of I*F; theorem :: INDEX_1:25 for C,D being Category, F being Functor of C,D, I being Indexing of D for T being TargetCat of I holds rng (I*F) is Subcategory of T; theorem :: INDEX_1:26 for C,D,E being Category, F being Functor of C,D for G being Functor of D,E, I being Indexing of E holds (I*G)*F = I*(G*F); definition let C be Category; let I be Indexing of C; let D be Categorial Category such that D is TargetCat of I; let E be Categorial Category; let F be Functor of D,E; func F*I -> Indexing of C means :: INDEX_1:def 17 for T being TargetCat of I, G being Functor of T,E st T = D & G = F holds it = (G*(I-functor(C,T)))-indexing_of C; end; theorem :: INDEX_1:27 for C being Category, I being Indexing of C for T being TargetCat of I, D,E being Categorial Category for F being Functor of T,D for G being Functor of T,E st F = G holds F*I = G*I; theorem :: INDEX_1:28 for C being Category, I being Indexing of C for T being TargetCat of I, D being Categorial Category for F being Functor of T,D holds Image F is TargetCat of F*I; theorem :: INDEX_1:29 for C being Category, I being Indexing of C for T being TargetCat of I, D being Categorial Category for F being Functor of T,D holds D is TargetCat of F*I; theorem :: INDEX_1:30 for C being Category, I being Indexing of C for T being TargetCat of I, D being Categorial Category for F being Functor of T,D holds rng (F*I) is Subcategory of Image F; theorem :: INDEX_1:31 for C be Category, I being Indexing of C for T being TargetCat of I for D,E being Categorial Category, F being Functor of T,D for G being Functor of D,E holds (G*F)*I = G*(F*I); definition let C,D be Category; let I1 be Indexing of C; let I2 be Indexing of D; func I2*I1 -> Indexing of C equals :: INDEX_1:def 18 I2*(I1-functor(C,rng I1)); end; theorem :: INDEX_1:32 for C being Category, D being Categorial Category, I1 being Indexing of C for I2 being Indexing of D for T being TargetCat of I1 st D is TargetCat of I1 holds I2*I1 = I2*(I1-functor(C,T)); theorem :: INDEX_1:33 for C being Category, D being Categorial Category, I1 being Indexing of C for I2 being Indexing of D for T being TargetCat of I2 st D is TargetCat of I1 holds I2*I1 = (I2-functor(D,T))*I1; theorem :: INDEX_1:34 for C,D being Category, F being Functor of C,D, I being Indexing of D for T being TargetCat of I, E being Categorial Category for G being Functor of T,E holds (G*I)*F = G*(I*F); theorem :: INDEX_1:35 for C being Category, I being Indexing of C for T being TargetCat of I, D being Categorial Category for F being Functor of T,D, J being Indexing of D holds (J*F)*I = J*(F*I); theorem :: INDEX_1:36 for C being Category, I being Indexing of C for T1 being TargetCat of I, J being Indexing of T1 for T2 being TargetCat of J for D being Categorial Category, F being Functor of T2,D holds (F*J)*I = F*(J*I); theorem :: INDEX_1:37 for C,D being Category, F being Functor of C,D, I being Indexing of D for T being TargetCat of I, J being Indexing of T holds (J*I)*F = J*(I*F); theorem :: INDEX_1:38 for C being Category, I being Indexing of C for D being TargetCat of I, J being Indexing of D for E being TargetCat of J, K being Indexing of E holds (K*J)*I = K*(J*I);

Back to top