:: Examples of Category Structures. Subcategories
:: by Andrzej Trybulec
::
:: Received January 22, 1996
:: Copyright (c) 1996-2019 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 ZFMISC_1, FUNCOP_1, RELAT_1, FUNCT_1, PBOOLE, PZFMISC1, MEMBER_1,
XBOOLE_0, PARTFUN1, SUBSET_1, TARSKI, CAT_1, MCART_1, GRAPH_1, STRUCT_0,
ALTCAT_1, BINOP_1, RELAT_2, REALSET1, ALTCAT_2, MONOID_0, RECDEF_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, XTUPLE_0, MCART_1,
FUNCT_1, PZFMISC1, REALSET1, DOMAIN_1, STRUCT_0, PARTFUN1, FUNCT_2,
BINOP_1, MULTOP_1, FUNCT_3, FUNCT_4, GRAPH_1, CAT_1, PBOOLE, FUNCOP_1,
ALTCAT_1;
constructors FUNCT_3, REALSET1, PZFMISC1, CAT_1, ALTCAT_1, RELSET_1, FUNCT_4,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, PBOOLE, FUNCOP_1,
REALSET1, STRUCT_0, ALTCAT_1, CAT_1, PRALG_1, RELSET_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
reserve e for set;
theorem :: ALTCAT_2:1
for X1,X2 being set, a1,a2 being set holds [:X1 -->a1,X2-->a2:] = [:X1
,X2:] --> [a1,a2];
registration
let I be set;
cluster EmptyMS I -> Function-yielding;
end;
theorem :: ALTCAT_2:2
for f,g being Function holds ~(g*f) = g*~f;
theorem :: ALTCAT_2:3
for f,g,h being Function holds ~(f*[:g,h:]) = ~f*[:h,g:];
registration
let f be Function-yielding Function;
cluster ~f -> Function-yielding;
end;
theorem :: ALTCAT_2:4
for I being set, A,B,C being ManySortedSet of I st A
is_transformable_to B for F being ManySortedFunction of A,B, G being
ManySortedFunction of B,C holds G**F is ManySortedFunction of A,C;
registration
let I be set;
let A be ManySortedSet of [:I,I:];
cluster ~A -> [:I,I:]-defined;
end;
registration
let I be set;
let A be ManySortedSet of [:I,I:];
cluster ~A -> total for [:I,I:]-defined Function;
end;
theorem :: ALTCAT_2:5
for I1 being set, I2 being non empty set, f being Function of I1,I2, B
,C being ManySortedSet of I2, G being ManySortedFunction of B,C holds G*f is
ManySortedFunction of B*f, C*f;
definition
let I be set, A,B be ManySortedSet of [:I,I:], F be ManySortedFunction of A,
B;
redefine func ~F -> ManySortedFunction of ~A,~B;
end;
theorem :: ALTCAT_2:6
for I1,I2 being non empty set, M being ManySortedSet of [:I1,I2:], o1
being Element of I1, o2 being Element of I2 holds (~M).(o2,o1) = M.(o1,o2);
registration
let I1 be set, f,g be ManySortedFunction of I1;
cluster g**f -> I1-defined;
end;
registration
let I1 be set, f,g be ManySortedFunction of I1;
cluster g**f -> total;
end;
begin :: An auxiliary notion
definition
let f,g be Function;
pred f cc= g means
:: ALTCAT_2:def 1
dom f c= dom g & for i being set st i in dom f holds f.i c= g.i;
reflexivity;
end;
definition
let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J;
redefine pred A cc= B means
:: ALTCAT_2:def 2
I c= J & for i being set st i in I holds A.i c= B.i;
end;
theorem :: ALTCAT_2:7
for I,J being set, A being ManySortedSet of I, B being
ManySortedSet of J holds A cc= B & B cc= A implies A = B;
theorem :: ALTCAT_2:8
for I,J,K being set, A being ManySortedSet of I, B being
ManySortedSet of J, C being ManySortedSet of K holds A cc= B & B cc= C implies
A cc= C;
theorem :: ALTCAT_2:9
for I being set, A being ManySortedSet of I, B being ManySortedSet of
I holds A cc= B iff A c= B;
begin :: A bit of lambda calculus
scheme :: ALTCAT_2:sch 1
OnSingletons{X()-> non empty set, F(set)-> set, P[set]}: { [o,F(o)] where o
is Element of X(): P[o] } is Function;
scheme :: ALTCAT_2:sch 2
DomOnSingletons {X()-> non empty set,f()-> Function, F(set)-> set, P[set]}:
dom f() = { o where o is Element of X(): P[o]}
provided
f() = { [o,F(o)] where o is Element of X(): P[o] };
scheme :: ALTCAT_2:sch 3
ValOnSingletons {X()-> non empty set,f()-> Function, x()-> Element of X(), F
(set)-> set, P[set]}: f().x() = F(x())
provided
f() = { [o,F(o)] where o is Element of X(): P[o] } and
P[x()];
begin :: More on old categories
theorem :: ALTCAT_2:10
for C being Category, i,j,k being Object of C holds [:Hom(j,k),
Hom(i,j):] c= dom the Comp of C;
theorem :: ALTCAT_2:11
for C being Category, i,j,k being Object of C holds (the Comp of
C).:[:Hom(j,k),Hom(i,j):] c= Hom(i,k);
definition
let C be non void non empty CatStr;
func the_hom_sets_of C -> ManySortedSet of [:the carrier of C, the carrier
of C:] means
:: ALTCAT_2:def 3
for i,j being Object of C holds it.(i,j) = Hom(i,j);
end;
theorem :: ALTCAT_2:12
for C be Category, i be Object of C holds id i in ( the_hom_sets_of C).(i,i);
definition
let C be Category;
func the_comps_of C -> BinComp of the_hom_sets_of C means
:: ALTCAT_2:def 4
for i,j,k
being Object of C holds it.(i,j,k) = (the Comp of C)| ([:(the_hom_sets_of C).(j
,k),(the_hom_sets_of C).(i,j):] qua set);
end;
theorem :: ALTCAT_2:13
for C being Category, i,j,k being Object of C st Hom(i,j) <> {}
& Hom(j,k) <> {} for f being Morphism of i,j, g being Morphism of j,k holds (
the_comps_of C).(i,j,k).(g,f) = g*f;
theorem :: ALTCAT_2:14
for C being Category holds the_comps_of C is associative;
theorem :: ALTCAT_2:15
for C being Category holds the_comps_of C is with_left_units with_right_units
;
begin :: Transforming an old category into new one
definition
let C be Category;
func Alter C -> strict non empty AltCatStr equals
:: ALTCAT_2:def 5
AltCatStr(#the carrier of
C,the_hom_sets_of C, the_comps_of C#);
end;
theorem :: ALTCAT_2:16
for C being Category holds Alter C is associative;
theorem :: ALTCAT_2:17
for C being Category holds Alter C is with_units;
theorem :: ALTCAT_2:18
for C being Category holds Alter C is transitive;
registration
let C be Category;
cluster Alter C -> transitive associative with_units;
end;
begin :: More on new categories
registration
cluster non empty strict for AltGraph;
end;
definition
let C be AltGraph;
attr C is reflexive means
:: ALTCAT_2:def 6
for x being set st x in the carrier of C holds (the Arrows of C).(x,x) <> {};
end;
definition
let C be non empty AltGraph;
redefine attr C is reflexive means
:: ALTCAT_2:def 7
for o being Object of C holds <^o,o^> <> {};
end;
definition
let C be non empty transitive AltCatStr;
redefine attr C is associative means
:: ALTCAT_2:def 8
for o1,o2,o3,o4 being Object of
C for f being Morphism of o1,o2, g being Morphism of o2,o3, h being Morphism of
o3,o4 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds h*g*f = h*(g
*f);
end;
definition
let C be non empty AltCatStr;
redefine attr C is with_units means
:: ALTCAT_2:def 9
for o being Object of C holds <^o,o^> <>
{} & ex i being Morphism of o,o st for o9 being Object of C, m9 being Morphism
of o9,o, m99 being Morphism of o,o9 holds (<^o9,o^> <> {} implies i*m9 = m9) &
(<^o,o9^> <> {} implies m99*i = m99);
end;
registration
cluster with_units -> reflexive for non empty AltCatStr;
end;
registration
cluster non empty reflexive for AltGraph;
end;
registration
cluster non empty reflexive for AltCatStr;
end;
begin
definition
func the_empty_category -> strict AltCatStr means
:: ALTCAT_2:def 10
the carrier of it is empty;
end;
registration
cluster the_empty_category -> empty;
end;
registration
cluster empty strict for AltCatStr;
end;
theorem :: ALTCAT_2:19
for E being empty strict AltCatStr holds E = the_empty_category;
begin :: Subcategories
:: Semadeni Wiweger 1.6.1 str. 24
definition
let C be AltCatStr;
mode SubCatStr of C -> AltCatStr means
:: ALTCAT_2:def 11
the carrier of it c= the
carrier of C & the Arrows of it cc= the Arrows of C & the Comp of it cc= the
Comp of C;
end;
reserve C,C1,C2,C3 for AltCatStr;
theorem :: ALTCAT_2:20
C is SubCatStr of C;
theorem :: ALTCAT_2:21
C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3;
theorem :: ALTCAT_2:22
for C1,C2 being AltCatStr st C1 is SubCatStr of C2 & C2 is
SubCatStr of C1 holds the AltCatStr of C1 = the AltCatStr of C2;
registration
let C be AltCatStr;
cluster strict for SubCatStr of C;
end;
definition
let C be non empty AltCatStr, o be Object of C;
func ObCat o -> strict SubCatStr of C means
:: ALTCAT_2:def 12
the carrier of it = { o
} & the Arrows of it = (o,o):-> <^o,o^> & the Comp of it = [o,o,o] .--> (the
Comp of C).(o,o,o);
end;
reserve C for non empty AltCatStr,
o for Object of C;
theorem :: ALTCAT_2:23
for o9 being Object of ObCat o holds o9 = o;
registration
let C be non empty AltCatStr, o be Object of C;
cluster ObCat o -> transitive non empty;
end;
registration
let C be non empty AltCatStr;
cluster transitive non empty strict for SubCatStr of C;
end;
theorem :: ALTCAT_2:24
for C being transitive non empty AltCatStr, D1,D2 being
transitive non empty SubCatStr of C st the carrier of D1 c= the carrier of D2 &
the Arrows of D1 cc= the Arrows of D2 holds D1 is SubCatStr of D2;
definition
let C be AltCatStr, D be SubCatStr of C;
attr D is full means
:: ALTCAT_2:def 13
the Arrows of D = (the Arrows of C)||the carrier of D;
end;
definition
let C be with_units non empty AltCatStr, D be SubCatStr of C;
attr D is id-inheriting means
:: ALTCAT_2:def 14
for o being Object of D, o9 being
Object of C st o = o9 holds idm o9 in <^o,o^> if D is non empty otherwise not
contradiction;
end;
registration
let C be AltCatStr;
cluster full strict for SubCatStr of C;
end;
registration
let C be non empty AltCatStr;
cluster full non empty strict for SubCatStr of C;
end;
registration
let C be category, o be Object of C;
cluster ObCat o -> full id-inheriting;
end;
registration
let C be category;
cluster full id-inheriting non empty strict for SubCatStr of C;
end;
reserve C for non empty transitive AltCatStr;
theorem :: ALTCAT_2:25
for D being SubCatStr of C st the carrier of D = the carrier of
C & the Arrows of D = the Arrows of C holds the AltCatStr of D = the AltCatStr
of C;
theorem :: ALTCAT_2:26
for D1,D2 being non empty transitive SubCatStr of C st the
carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 holds
the AltCatStr of D1 = the AltCatStr of D2;
theorem :: ALTCAT_2:27
for D being full SubCatStr of C st the carrier of D = the carrier of C
holds the AltCatStr of D = the AltCatStr of C;
theorem :: ALTCAT_2:28
for C being non empty AltCatStr, D being full non empty
SubCatStr of C, o1,o2 being Object of C, p1,p2 being Object of D st o1 = p1 &
o2 = p2 holds <^o1,o2^> = <^p1,p2^>;
theorem :: ALTCAT_2:29
for C being non empty AltCatStr, D being non empty SubCatStr of
C for o being Object of D holds o is Object of C;
registration
let C be transitive non empty AltCatStr;
cluster full non empty -> transitive for SubCatStr of C;
end;
theorem :: ALTCAT_2:30
for D1,D2 being full non empty SubCatStr of C st the carrier of D1 =
the carrier of D2 holds the AltCatStr of D1 = the AltCatStr of D2;
theorem :: ALTCAT_2:31
for C being non empty AltCatStr, D being non empty SubCatStr of
C, o1,o2 being Object of C, p1,p2 being Object of D st o1 = p1 & o2 = p2 holds
<^p1,p2^> c= <^o1,o2^>;
theorem :: ALTCAT_2:32
for C being non empty transitive AltCatStr, D being non empty
transitive SubCatStr of C, p1,p2,p3 being Object of D st <^p1,p2^> <> {} & <^p2
,p3^> <> {} for o1,o2,o3 being Object of C st o1 = p1 & o2 = p2 & o3 = p3 for f
being Morphism of o1,o2, g being Morphism of o2,o3, ff being Morphism of p1,p2,
gg being Morphism of p2,p3 st f = ff & g = gg holds g*f = gg*ff;
registration
let C be associative transitive non empty AltCatStr;
cluster transitive -> associative for non empty SubCatStr of C;
end;
theorem :: ALTCAT_2:33
for C being non empty AltCatStr, D being non empty SubCatStr of
C, o1,o2 being Object of C, p1,p2 being Object of D st o1 = p1 & o2 = p2 & <^p1
,p2^> <> {} for n being Morphism of p1,p2 holds n is Morphism of o1,o2;
registration
let C be transitive with_units non empty AltCatStr;
cluster id-inheriting transitive -> with_units for
non empty SubCatStr of C;
end;
registration
let C be category;
cluster id-inheriting transitive for non empty SubCatStr of C;
end;
definition
let C be category;
mode subcategory of C is id-inheriting transitive SubCatStr of C;
end;
theorem :: ALTCAT_2:34
for C being category, D being non empty subcategory of C for o being
Object of D, o9 being Object of C st o = o9 holds idm o = idm o9;