:: Examples of Category Structures. Subcategories
:: by Andrzej Trybulec
::
:: Received January 22, 1996
:: Copyright (c) 1996-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 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;
definitions STRUCT_0, ALTCAT_1, FUNCOP_1, FUNCT_1, RELAT_1, TARSKI, PBOOLE;
equalities ALTCAT_1, FUNCOP_1, PBOOLE, BINOP_1, REALSET1, XTUPLE_0;
expansions RELAT_1, TARSKI, PBOOLE;
theorems MCART_1, ALTCAT_1, PBOOLE, TARSKI, GRFUNC_1, ZFMISC_1, MULTOP_1,
RELAT_1, FUNCT_2, FUNCOP_1, FUNCT_4, FUNCT_1, FUNCT_3, DOMAIN_1,
MSSUBFAM, FUNCT_7, CAT_1, XBOOLE_0, XBOOLE_1, PZFMISC1, PARTFUN1,
XTUPLE_0;
schemes ALTCAT_1, FUNCT_1;
begin :: Preliminaries
reserve e for set;
theorem
for X1,X2 being set, a1,a2 being set holds [:X1 -->a1,X2-->a2:] = [:X1
,X2:] --> [a1,a2]
proof
let X1,X2 be set, a1,a2 be set;
A2: dom([:X1,X2:] --> [a1,a2]) = [:dom(X1 -->a1), dom(X2-->a2):];
now
let x,y be object;
assume
A3: x in dom(X1-->a1) & y in dom(X2-->a2);
then [x,y] in dom([:X1,X2:] --> [a1,a2]) by ZFMISC_1:87;
then
A4: [x,y] in [:X1,X2:];
(X1-->a1).x = a1 & (X2-->a2).y = a2 by A3,FUNCOP_1:7;
hence ([:X1,X2:] --> [a1,a2]).(x,y) = [(X1-->a1).x,(X2-->a2).y] by A4,
FUNCOP_1:7;
end;
hence thesis by A2,FUNCT_3:def 8;
end;
registration
let I be set;
cluster EmptyMS I -> Function-yielding;
coherence;
end;
theorem
for f,g being Function holds ~(g*f) = g*~f
proof
let f,g be Function;
A1: now
let x be object;
hereby
assume
A2: x in dom(g*~f);
then x in dom~f by FUNCT_1:11;
then consider y1,z1 being object such that
A3: x = [z1,y1] and
A4: [y1,z1] in dom f by FUNCT_4:def 2;
take y1,z1;
thus x = [z1,y1] by A3;
~f.(z1,y1) in dom g by A2,A3,FUNCT_1:11;
then f.(y1,z1) in dom g by A4,FUNCT_4:def 2;
hence [y1,z1] in dom(g*f) by A4,FUNCT_1:11;
end;
given y,z being object such that
A5: x = [z,y] and
A6: [y,z] in dom(g*f);
A7: [y,z] in dom f by A6,FUNCT_1:11;
then
A8: x in dom ~f by A5,FUNCT_4:def 2;
f.(y,z) in dom g by A6,FUNCT_1:11;
then ~f.(z,y) in dom g by A7,FUNCT_4:def 2;
hence x in dom(g*~f) by A5,A8,FUNCT_1:11;
end;
now
let y,z be object;
assume
A9: [y,z] in dom(g*f);
then [y,z] in dom f by FUNCT_1:11;
then
A10: [z,y] in dom ~f by FUNCT_4:42;
hence (g*~f).(z,y) = g.(~f.(z,y)) by FUNCT_1:13
.= g.(f.(y,z)) by A10,FUNCT_4:43
.= (g*f).(y,z) by A9,FUNCT_1:12;
end;
hence thesis by A1,FUNCT_4:def 2;
end;
theorem
for f,g,h being Function holds ~(f*[:g,h:]) = ~f*[:h,g:]
proof
let f,g,h be Function;
A1: now
let x be object;
hereby
assume
A2: x in dom(~f*[:h,g:]);
then x in dom[:h,g:] by FUNCT_1:11;
then x in [:dom h, dom g:] by FUNCT_3:def 8;
then consider y1,z1 being object such that
A3: y1 in dom h & z1 in dom g and
A4: x = [y1,z1] by ZFMISC_1:84;
A5: [:h,g:].(y1,z1) = [h.y1,g.z1] & [:g,h:].(z1,y1) = [g.z1,h.y1] by A3,
FUNCT_3:def 8;
[:h,g:].(y1,z1) in dom~f by A2,A4,FUNCT_1:11;
then
A6: [:g,h:].(z1,y1) in dom f by A5,FUNCT_4:42;
take z1,y1;
thus x = [y1,z1] by A4;
dom[:g,h:] = [:dom g,dom h:] by FUNCT_3:def 8;
then [z1,y1] in dom[:g,h:] by A3,ZFMISC_1:87;
hence [z1,y1] in dom(f*[:g,h:]) by A6,FUNCT_1:11;
end;
given y,z being object such that
A7: x = [z,y] and
A8: [y,z] in dom(f*[:g,h:]);
A9: [:g,h:].(y,z) in dom f by A8,FUNCT_1:11;
A10: dom [:g,h:] = [:dom g, dom h:] by FUNCT_3:def 8;
[y,z] in dom [:g,h:] by A8,FUNCT_1:11;
then
A11: y in dom g & z in dom h by A10,ZFMISC_1:87;
then [:g,h:].(y,z) = [g.y,h.z] & [:h,g:].(z,y) = [h.z,g.y] by FUNCT_3:def 8
;
then
A12: [:h,g:].x in dom~f by A7,A9,FUNCT_4:42;
dom[:h,g:] = [:dom h, dom g:] by FUNCT_3:def 8;
then x in dom[:h,g:] by A7,A11,ZFMISC_1:87;
hence x in dom(~f*[:h,g:]) by A12,FUNCT_1:11;
end;
now
let y,z be object;
assume
A13: [y,z] in dom(f*[:g,h:]);
then [y,z] in dom[:g,h:] by FUNCT_1:11;
then [y,z] in [:dom g, dom h:] by FUNCT_3:def 8;
then
A14: y in dom g & z in dom h by ZFMISC_1:87;
[:g,h:].(y,z) in dom f by A13,FUNCT_1:11;
then
A15: [g.y,h.z] in dom f by A14,FUNCT_3:def 8;
[z,y] in [:dom h, dom g:] by A14,ZFMISC_1:87;
then [z,y] in dom[:h,g:] by FUNCT_3:def 8;
hence (~f*[:h,g:]).(z,y) = ~f.([:h,g:].(z,y)) by FUNCT_1:13
.= ~f.(h.z,g.y) by A14,FUNCT_3:def 8
.= f.(g.y,h.z) by A15,FUNCT_4:def 2
.= f.([:g,h:].(y,z)) by A14,FUNCT_3:def 8
.= (f*[:g,h:]).(y,z) by A13,FUNCT_1:12;
end;
hence thesis by A1,FUNCT_4:def 2;
end;
registration
let f be Function-yielding Function;
cluster ~f -> Function-yielding;
coherence
proof
let x be object;
assume x in dom~f;
then consider z,y being object such that
A1: x = [y,z] and
A2: [z,y] in dom f by FUNCT_4:def 2;
f.(z,y) = (~f).(y,z) by A2,FUNCT_4:def 2;
hence thesis by A1;
end;
end;
theorem
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
proof
let I be set, A,B,C be ManySortedSet of I such that
A1: A is_transformable_to B;
let F be ManySortedFunction of A,B, G be ManySortedFunction of B,C;
reconsider GF = G**F as ManySortedFunction of I by MSSUBFAM:15;
GF is ManySortedFunction of A,C
proof
let i be object;
assume
A2: i in I;
then reconsider Gi = G.i as Function of B.i,C.i by PBOOLE:def 15;
reconsider Fi = F.i as Function of A.i,B.i by A2,PBOOLE:def 15;
i in dom GF by A2,PARTFUN1:def 2;
then
A3: (G**F).i = (Gi)*(Fi) by PBOOLE:def 19;
B.i = {} implies A.i = {} by A1,A2,PZFMISC1:def 3;
hence thesis by A3,FUNCT_2:13;
end;
hence thesis;
end;
registration
let I be set;
let A be ManySortedSet of [:I,I:];
cluster ~A -> [:I,I:]-defined;
coherence;
end;
registration
let I be set;
let A be ManySortedSet of [:I,I:];
cluster ~A -> total for [:I,I:]-defined Function;
coherence;
end;
theorem
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
proof
let I1 be set, I2 be non empty set, f be Function of I1,I2, B,C be
ManySortedSet of I2, G be ManySortedFunction of B,C;
let i be object;
assume
A1: i in I1;
then
A2: G.(f.i) is Function of B.(f.i),C.(f.i) by FUNCT_2:5,PBOOLE:def 15;
A3: i in dom f by A1,FUNCT_2:def 1;
then B.(f.i) = (B*f).i & C.(f.i) = (C*f).i by FUNCT_1:13;
hence thesis by A3,A2,FUNCT_1:13;
end;
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; :: redefines ~ (FUNCT_4, definition)
coherence
proof
reconsider G = ~F as ManySortedSet of [:I,I:];
G is ManySortedFunction of ~A,~B
proof
let ii be object;
assume ii in [:I,I:];
then consider i1,i2 being object such that
A1: i1 in I & i2 in I and
A2: ii = [i1,i2] by ZFMISC_1:84;
A3: [i2,i1] in [:I,I:] by A1,ZFMISC_1:87;
dom B = [:I,I:] by PARTFUN1:def 2;
then
A4: B.(i2,i1) = ~B.(i1,i2) by A3,FUNCT_4:def 2;
dom A = [:I,I:] by PARTFUN1:def 2;
then
A5: A.(i2,i1) = ~A.(i1,i2) by A3,FUNCT_4:def 2;
dom F = [:I,I:] by PARTFUN1:def 2;
then F.(i2,i1) = G.(i1,i2) by A3,FUNCT_4:def 2;
hence thesis by A2,A3,A5,A4,PBOOLE:def 15;
end;
hence thesis;
end;
end;
theorem
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)
proof
let I1,I2 be non empty set, M be ManySortedSet of [:I1,I2:], o1 be Element
of I1, o2 be Element of I2;
[o1,o2] in [:I1,I2:];
then [o1,o2] in dom M by PARTFUN1:def 2;
hence thesis by FUNCT_4:def 2;
end;
registration
let I1 be set, f,g be ManySortedFunction of I1;
cluster g**f -> I1-defined;
coherence
proof
A1: dom f = I1 & dom g = I1 by PARTFUN1:def 2;
dom(g**f) = dom g /\ dom f by PBOOLE:def 19
.= I1 by A1;
hence thesis;
end;
end;
registration
let I1 be set, f,g be ManySortedFunction of I1;
cluster g**f -> total;
coherence
proof
A1: dom f = I1 & dom g = I1 by PARTFUN1:def 2;
dom(g**f) = dom g /\ dom f by PBOOLE:def 19
.= I1 by A1;
hence thesis by PARTFUN1:def 2;
end;
end;
begin :: An auxiliary notion
definition
let f,g be Function;
pred f cc= g means
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 :: redefines cc= (ALTCAT_2, definition)
I c= J & for i being set st i in I holds A.i c= B.i;
compatibility
proof
A1: dom A = I by PARTFUN1:def 2;
dom B = J by PARTFUN1:def 2;
hence A cc= B implies I c= J & for i being set st i in I holds A.i c= B.i
by A1;
assume that
A2: I c= J and
A3: for i being set st i in I holds A.i c= B.i;
thus dom A c= dom B by A1,A2,PARTFUN1:def 2;
let i be set;
assume i in dom A;
hence thesis by A1,A3;
end;
end;
theorem Th7:
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
proof
let I,J be set, A be ManySortedSet of I, B be ManySortedSet of J;
assume that
A1: A cc= B and
A2: B cc= A;
A3: I c= J by A1;
J c= I by A2;
then I = J by A3,XBOOLE_0:def 10;
then reconsider B9 = B as ManySortedSet of I;
now
let i be object;
assume i in I;
then A.i c= B.i & B.i c= A.i by A1,A2;
hence A.i = B9.i by XBOOLE_0:def 10;
end;
hence thesis by PBOOLE:3;
end;
theorem Th8:
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
proof
let I,J,K be set, A be ManySortedSet of I, B be ManySortedSet of J, C be
ManySortedSet of K;
assume that
A1: A cc= B and
A2: B cc= C;
A3: I c= J by A1;
J c= K by A2;
hence I c= K by A3;
let i be set;
assume
A4: i in I;
then
A5: A.i c= B.i by A1;
B.i c= C.i by A2,A3,A4;
hence thesis by A5;
end;
theorem
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
OnSingletons{X()-> non empty set, F(set)-> set, P[set]}: { [o,F(o)] where o
is Element of X(): P[o] } is Function proof
set f = { [o,F(o)] where o is Element of X(): P[o] };
A1: f is Function-like
proof
let x,y1,y2 be object;
assume [x,y1] in f;
then consider o1 being Element of X() such that
A2: [x,y1] = [o1,F(o1)] and
P[o1];
A3: o1 = x by A2,XTUPLE_0:1;
assume [x,y2] in f;
then consider o2 being Element of X() such that
A4: [x,y2] = [o2,F(o2)] and
P[o2];
o2 = x by A4,XTUPLE_0:1;
hence thesis by A2,A4,A3,XTUPLE_0:1;
end;
f is Relation-like
proof
let x be object;
assume x in f;
then consider o being Element of X() such that
A5: x = [o,F(o)] and
P[o];
take o,F(o);
thus thesis by A5;
end;
hence thesis by A1;
end;
scheme
DomOnSingletons {X()-> non empty set,f()-> Function, F(set)-> set, P[set]}:
dom f() = { o where o is Element of X(): P[o]}
provided
A1: f() = { [o,F(o)] where o is Element of X(): P[o] }
proof
set A = { o where o is Element of X(): P[o]};
now
let x be object;
hereby
assume x in A;
then consider o being Element of X() such that
A2: x = o & P[o];
reconsider y = F(o) as object;
take y;
thus [x,y] in f() by A1,A2;
end;
given y being object such that
A3: [x,y] in f();
consider o being Element of X() such that
A4: [x,y] = [o,F(o)] and
A5: P[o] by A1,A3;
x = o by A4,XTUPLE_0:1;
hence x in A by A5;
end;
hence thesis by XTUPLE_0:def 12;
end;
scheme
ValOnSingletons {X()-> non empty set,f()-> Function, x()-> Element of X(), F
(set)-> set, P[set]}: f().x() = F(x())
provided
A1: f() = { [o,F(o)] where o is Element of X(): P[o] } and
A2: P[x()]
proof
A3: f() = { [o,F(o)] where o is Element of X(): P[o] } by A1;
dom f() = { o where o is Element of X(): P[o] } from DomOnSingletons( A3
);
then
A4: x() in dom f() by A2;
[x(),F(x())] in { [o,F(o)] where o is Element of X(): P[o] } by A2;
hence thesis by A1,A4,FUNCT_1:def 2;
end;
begin :: More on old categories
theorem Th10:
for C being Category, i,j,k being Object of C holds [:Hom(j,k),
Hom(i,j):] c= dom the Comp of C
proof
let C be Category, i,j,k be Object of C;
let e be object;
assume
A1: e in [:Hom(j,k),Hom(i,j):];
then reconsider y = e`1, x = e`2 as Morphism of C by MCART_1:10;
A2: e`2 in Hom(i,j) by A1,MCART_1:10;
A3: e = [y,x] by A1,MCART_1:21;
e`1 in Hom(j,k) by A1,MCART_1:10;
then dom y = j by CAT_1:1
.= cod x by A2,CAT_1:1;
hence thesis by A3,CAT_1:15;
end;
theorem Th11:
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)
proof
let C be Category, i,j,k be Object of C;
let e be object;
assume e in (the Comp of C).:[:Hom(j,k),Hom(i,j):];
then consider x being object such that
A1: x in dom the Comp of C and
A2: x in [:Hom(j,k),Hom(i,j):] and
A3: e = (the Comp of C).x by FUNCT_1:def 6;
reconsider y = x`1, z = x`2 as Morphism of C by A2,MCART_1:10;
A4: x = [y,z] & e = (the Comp of C).(y,z) by A2,A3,MCART_1:21;
A5: x`2 in Hom(i,j) by A2,MCART_1:10;
then
A6: z is Morphism of i,j by CAT_1:def 5;
A7: x`1 in Hom(j,k) by A2,MCART_1:10;
then y is Morphism of j,k by CAT_1:def 5;
then y(*)z in Hom(i,k) by A7,A5,A6,CAT_1:23;
hence thesis by A1,A4,CAT_1:def 1;
end;
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
:Def3:
for i,j being Object of C holds it.(i,j) = Hom(i,j);
existence
proof
deffunc H(Object of C, Object of C) = Hom($1,$2);
thus ex M being ManySortedSet of [:the carrier of C, the carrier of C:] st
for i,j being Object of C holds M.(i,j) = H(i,j) from ALTCAT_1:sch 2;
end;
uniqueness
proof
let M1,M2 be ManySortedSet of [:the carrier of C, the carrier of C:] such
that
A1: for i,j being Object of C holds M1.(i,j) = Hom(i,j) and
A2: for i,j being Object of C holds M2.(i,j) = Hom(i,j);
now
let i,j be Object of C;
thus M1.(i,j) = Hom(i,j) by A1
.= M2.(i,j) by A2;
end;
hence thesis by ALTCAT_1:7;
end;
end;
theorem Th12:
for C be Category, i be Object of C holds id i in ( the_hom_sets_of C).(i,i)
proof
let C be Category, i be Object of C;
id i in Hom(i,i) by CAT_1:27;
hence thesis by Def3;
end;
definition
let C be Category;
func the_comps_of C -> BinComp of the_hom_sets_of C means
:Def4:
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);
existence
proof
deffunc F(object) =
(the Comp of C)|([:(the_hom_sets_of C).($1`1`2,$1`2), (
the_hom_sets_of C).($1`1`1,$1`1`2):] qua set);
set Ob3 = [:the carrier of C,the carrier of C,the carrier of C:], G =
the_hom_sets_of C;
consider o being Function such that
A1: dom o = Ob3 and
A2: for e being object st e in Ob3 holds o.e = F(e) from FUNCT_1:sch 3;
reconsider o as ManySortedSet of Ob3 by A1,PARTFUN1:def 2,RELAT_1:def 18;
now
let e be object;
assume e in dom o;
then o.e = (the Comp of C)| ([:(the_hom_sets_of C).(e`1`2,e`2),(
the_hom_sets_of C).(e`1`1,e`1`2):] qua set) by A1,A2;
hence o.e is Function;
end;
then reconsider o as ManySortedFunction of Ob3 by FUNCOP_1:def 6;
now
let e be object;
reconsider f = o.e as Function;
assume
A3: e in Ob3;
then consider i,j,k being Object of C such that
A4: e = [i,j,k] by DOMAIN_1:3;
reconsider e9 = e as Element of Ob3 by A3;
A5: [i,j,k] qua set `1`2 = e9`2_3 by A4
.= j by A4,MCART_1:def 6;
A6: [i,j,k] qua set `2 = e9`3_3 by A4
.= k by A4,MCART_1:def 7;
[i,j,k] qua set `1`1 = e9`1_3 by A4
.= i by A4,MCART_1:def 5;
then
A7: f = (the Comp of C)|([:G.(j,k),G.(i,j):] qua set) by A2,A4,A5,A6;
A8: G.(i,j) = Hom(i,j) & G.(j,k) = Hom(j,k) by Def3;
A9: {|G|}.e = {|G|}.(i,j,k) by A4,MULTOP_1:def 1
.= G.(i,k) by ALTCAT_1:def 3
.= Hom(i,k) by Def3;
A10: {|G,G|}.e = {|G,G|}.(i,j,k) by A4,MULTOP_1:def 1
.= [:Hom(j,k),Hom(i,j):] by A8,ALTCAT_1:def 4;
(the Comp of C).:[:Hom(j,k),Hom(i,j):] c= Hom(i,k) by Th11;
then
A11: rng f c= {|G|}.e by A8,A7,A9,RELAT_1:115;
[:Hom(j,k),Hom(i,j):] c= dom the Comp of C by Th10;
then dom f = {|G,G|}.e by A8,A7,A10,RELAT_1:62;
hence o.e is Function of {|G,G|}.e,{|G|}.e by A11,FUNCT_2:2;
end;
then reconsider o as BinComp of G by PBOOLE:def 15;
take o;
let i,j,k be Object of C;
reconsider e = [i,j,k] as Element of Ob3;
A12: [i,j,k] qua set `1`1 = e`1_3
.= i by MCART_1:def 5;
A13: [i,j,k] qua set `1`2 = e`2_3
.= j by MCART_1:def 6;
A14: [i,j,k] qua set `2 = e`3_3
.= k by MCART_1:def 7;
thus o.(i,j,k) = o.[i,j,k] by MULTOP_1:def 1
.= (the Comp of C)| ([:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(
i,j):] qua set) by A2,A12,A13,A14;
end;
uniqueness
proof
let o1,o2 be BinComp of the_hom_sets_of C such that
A15: for i,j,k being Object of C holds o1.(i,j,k) = (the Comp of C)| (
[:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):] qua set) and
A16: for i,j,k being Object of C holds o2.(i,j,k) = (the Comp of C)| (
[:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):] qua set);
now
let a be object;
assume a in [:the carrier of C,the carrier of C,the carrier of C:];
then consider i,j,k being Object of C such that
A17: a = [i,j,k] by DOMAIN_1:3;
thus o1.a = o1.(i,j,k) by A17,MULTOP_1:def 1
.= (the Comp of C)| ([:(the_hom_sets_of C).(j,k),(the_hom_sets_of C)
.(i,j):] qua set) by A15
.= o2.(i,j,k) by A16
.= o2.a by A17,MULTOP_1:def 1;
end;
hence o1 = o2;
end;
end;
theorem Th13:
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
proof
let C be Category, i,j,k be Object of C such that
A1: Hom(i,j) <> {} and
A2: Hom(j,k) <> {};
let f be Morphism of i,j, g be Morphism of j,k;
A3: g in Hom(j,k) by A2,CAT_1:def 5;
then
A4: g in (the_hom_sets_of C).(j,k) by Def3;
A5: f in Hom(i,j) by A1,CAT_1:def 5;
then f in (the_hom_sets_of C).(i,j) by Def3;
then
A6: [g,f] in [:(the_hom_sets_of C).(j,k),(the_hom_sets_of C).(i,j):] by A4,
ZFMISC_1:87;
A7: dom g = j by A3,CAT_1:1
.= cod f by A5,CAT_1:1;
thus (the_comps_of C).(i,j,k).(g,f) = ((the Comp of C)| ([:(the_hom_sets_of
C).(j,k),(the_hom_sets_of C).(i,j):] qua set)) .[g,f] by Def4
.= (the Comp of C).(g,f) by A6,FUNCT_1:49
.= g(*)(f qua Morphism of C) by A7,CAT_1:16
.= g*f by A1,A2,CAT_1:def 13;
end;
theorem Th14:
for C being Category holds the_comps_of C is associative
proof
let C be Category;
let i,j,k,l be Object of C;
let f,g,h be set;
assume f in (the_hom_sets_of C).(i,j);
then
A1: f in Hom(i,j) by Def3;
then reconsider f9 = f as Morphism of i,j by CAT_1:def 5;
assume g in (the_hom_sets_of C).(j,k);
then
A2: g in Hom(j,k) by Def3;
then reconsider g9 = g as Morphism of j,k by CAT_1:def 5;
assume h in (the_hom_sets_of C).(k,l);
then
A3: h in Hom(k,l) by Def3;
then reconsider h9 = h as Morphism of k,l by CAT_1:def 5;
A4: Hom(j,l) <> {} & (the_comps_of C).(j,k,l).(h,g) = h9*g9 by A2,A3,Th13,
CAT_1:24;
Hom(i,k) <> {} & (the_comps_of C).(i,j,k).(g,f) = g9*f9 by A1,A2,Th13,
CAT_1:24;
hence
(the_comps_of C).(i,k,l).(h,(the_comps_of C).(i,j,k).(g,f)) = h9*(g9*f9
) by A3,Th13
.= h9*g9*f9 by A1,A2,A3,CAT_1:25
.= (the_comps_of C).(i,j,l).((the_comps_of C).(j,k,l).(h,g),f) by A1,A4
,Th13;
end;
theorem Th15:
for C being Category holds the_comps_of C is with_left_units with_right_units
proof
let C be Category;
thus the_comps_of C is with_left_units
proof
let i be Object of C;
take id i;
thus id i in (the_hom_sets_of C).(i,i) by Th12;
let j be Object of C, f be set;
assume f in (the_hom_sets_of C).(j,i);
then
A1: f in Hom(j,i) by Def3;
then reconsider m = f as Morphism of j,i by CAT_1:def 5;
Hom(i,i) <> {};
hence (the_comps_of C).(j,i,i).(id i,f) = (id i)*m by A1,Th13
.= f by A1,CAT_1:28;
end;
let j be Object of C;
take id j;
thus id j in (the_hom_sets_of C).(j,j) by Th12;
let i be Object of C, f be set;
assume f in (the_hom_sets_of C).(j,i);
then
A2: f in Hom(j,i) by Def3;
then reconsider m = f as Morphism of j,i by CAT_1:def 5;
Hom(j,j) <> {};
hence (the_comps_of C).(j,j,i).(f,id j) = m*(id j) by A2,Th13
.= f by A2,CAT_1:29;
end;
begin :: Transforming an old category into new one
definition
let C be Category;
func Alter C -> strict non empty AltCatStr equals
AltCatStr(#the carrier of
C,the_hom_sets_of C, the_comps_of C#);
correctness;
end;
theorem Th16:
for C being Category holds Alter C is associative
proof
let C be Category;
thus the Comp of Alter C is associative by Th14;
end;
theorem Th17:
for C being Category holds Alter C is with_units
proof
let C be Category;
thus the Comp of Alter C is with_left_units with_right_units by Th15;
end;
theorem Th18:
for C being Category holds Alter C is transitive
proof
let C be Category;
let o1,o2,o3 be Object of Alter C such that
A1: <^o1,o2^> <> {} & <^o2,o3^> <> {};
reconsider x1 = o1, x2 = o2, x3 = o3 as Object of C;
A2: <^o1,o3^> = Hom(x1,x3) by Def3;
<^o1,o2^> = Hom(x1,x2) & <^o2,o3^> = Hom(x2,x3) by Def3;
hence thesis by A1,A2,CAT_1:24;
end;
registration
let C be Category;
cluster Alter C -> transitive associative with_units;
coherence by Th16,Th17,Th18;
end;
begin :: More on new categories
registration
cluster non empty strict for AltGraph;
existence
proof
set M = the ManySortedSet of [:{{}},{{}}:];
take A = AltGraph(#{{}},M#);
thus the carrier of A is non empty;
thus thesis;
end;
end;
definition
let C be AltGraph;
attr C is reflexive means
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 :: redefines reflexive (ALTCAT_2, definition)
for o being Object of C holds <^o,o^> <> {};
compatibility
proof
thus C is reflexive implies for o be Object of C holds <^o,o^> <> {};
assume
A1: for o being Object of C holds <^o,o^> <> {};
let x be set;
assume x in the carrier of C;
then reconsider o=x as Object of C;
(the Arrows of C).(x,x) = <^o,o^>;
hence thesis by A1;
end;
end;
definition
let C be non empty transitive AltCatStr;
redefine attr C is associative means :: redefines associative (ALTCAT_1, definition)
:Def8:
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);
compatibility
proof
thus C is associative implies 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)
by ALTCAT_1:21;
assume
A1: 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);
let i,j,k,l be Element of C;
reconsider o1=i, o2=j, o3=k, o4=l as Object of C;
let f,g,h be set;
assume
A2: f in (the Arrows of C).(i,j);
then reconsider ff = f as Morphism of o1,o2;
assume
A3: g in (the Arrows of C).(j,k);
then
A4: g in <^o2,o3^>;
f in <^o1,o2^> by A2;
then
A5: <^o1,o3^> <> {} by A4,ALTCAT_1:def 2;
reconsider gg = g as Morphism of o2,o3 by A3;
assume
A6: h in (the Arrows of C).(k,l);
then reconsider hh = h as Morphism of o3,o4;
A7: (the Comp of C).(j,k,l).(h,g) = hh*gg by A3,A6,ALTCAT_1:def 8;
h in <^o3,o4^> by A6;
then
A8: <^o2,o4^> <> {} by A4,ALTCAT_1:def 2;
(the Comp of C).(i,j,k).(g,f) = gg*ff by A2,A3,ALTCAT_1:def 8;
hence
(the Comp of C).(i,k,l).(h,(the Comp of C).(i,j,k).(g,f)) = hh*(gg*ff
) by A6,A5,ALTCAT_1:def 8
.= hh*gg*ff by A1,A2,A3,A6
.= (the Comp of C).(i,j,l).((the Comp of C).(j,k,l).(h,g),f) by A2,A8,A7,
ALTCAT_1:def 8;
end;
end;
definition
let C be non empty AltCatStr;
redefine attr C is with_units means :: redefines with_units (ALTCAT_1, definition)
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);
compatibility
proof
hereby
assume
A1: C is with_units;
then reconsider C9 = C as with_units non empty AltCatStr;
let o be Object of C;
thus <^o,o^> <> {} by A1,ALTCAT_1:18;
reconsider p = o as Object of C9;
reconsider i = idm p as Morphism of o,o;
take i;
let o9 be Object of C, m9 be Morphism of o9,o, m99 be Morphism of o,o9;
thus <^o9,o^> <> {} implies i*m9 = m9 by ALTCAT_1:20;
thus <^o,o9^> <> {} implies m99*i = m99 by ALTCAT_1:def 17;
end;
assume
A2: 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);
hereby
let j be Element of C;
reconsider o = j as Object of C;
consider m being Morphism of o,o such that
A3: for o9 being Object of C, m9 being Morphism of o9,o, m99 being
Morphism of o,o9 holds (<^o9,o^> <> {} implies m*m9 = m9) & (<^o,o9^> <> {}
implies m99*m = m99) by A2;
reconsider e = m as set;
take e;
A4: <^o,o^> <> {} by A2;
hence e in (the Arrows of C).(j,j);
let i be Element of C, f be set such that
A5: f in (the Arrows of C).(i,j);
reconsider o9 = i as Object of C;
reconsider m9 = f as Morphism of o9,o by A5;
thus (the Comp of C).(i,j,j).(e,f) = m*m9 by A4,A5,ALTCAT_1:def 8
.= f by A3,A5;
end;
let i be Element of C;
reconsider o = i as Object of C;
consider m being Morphism of o,o such that
A6: for o9 being Object of C, m9 being Morphism of o9,o, m99 being
Morphism of o,o9 holds (<^o9,o^> <> {} implies m*m9 = m9) & (<^o,o9^> <> {}
implies m99*m = m99) by A2;
take e = m;
A7: <^o,o^> <> {} by A2;
hence e in (the Arrows of C).(i,i);
let j be Element of C, f be set such that
A8: f in (the Arrows of C).(i,j);
reconsider o9 = j as Object of C;
reconsider m9 = f as Morphism of o,o9 by A8;
thus (the Comp of C).(i,i,j).(f,e) = m9*m by A7,A8,ALTCAT_1:def 8
.= f by A6,A8;
end;
end;
registration
cluster with_units -> reflexive for non empty AltCatStr;
coherence;
end;
registration
cluster non empty reflexive for AltGraph;
existence
proof
set C = the with_units non empty AltCatStr;
take C;
thus thesis;
end;
end;
registration
cluster non empty reflexive for AltCatStr;
existence
proof
set C = the category;
take C;
thus thesis;
end;
end;
begin :: The empty category
Lm1: for E1,E2 being strict AltCatStr st the carrier of E1 is empty & the
carrier of E2 is empty holds E1 = E2
proof
let E1,E2 be strict AltCatStr;
set C1 = the carrier of E1, C2 = the carrier of E2;
assume that
A1: C1 is empty and
A2: C2 is empty;
A3: [:C2,C2,C2:] = {} by A2,MCART_1:31;
[:C1,C1,C1:] = {} by A1,MCART_1:31;
then
A4: the Comp of E1 = {}
.= the Comp of E2 by A3;
A5: [:C2,C2:] = {} by A2,ZFMISC_1:90;
[:C1,C1:] = {} by A1,ZFMISC_1:90;
then the Arrows of E1 = {}
.= the Arrows of E2 by A5;
hence thesis by A1,A2,A4;
end;
definition
func the_empty_category -> strict AltCatStr means
:Def10:
the carrier of it is empty;
existence
proof
reconsider a = {} as set;
set m = the ManySortedSet of [:a,a:];
set c = the BinComp of m;
take AltCatStr(#a,m,c#);
thus thesis;
end;
uniqueness by Lm1;
end;
registration
cluster the_empty_category -> empty;
coherence by Def10;
end;
registration
cluster empty strict for AltCatStr;
existence
proof
take the_empty_category;
thus thesis;
end;
end;
theorem
for E being empty strict AltCatStr holds E = the_empty_category by Lm1;
begin :: Subcategories
:: Semadeni Wiweger 1.6.1 str. 24
definition
let C be AltCatStr;
mode SubCatStr of C -> AltCatStr means
:Def11:
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;
existence;
end;
reserve C,C1,C2,C3 for AltCatStr;
theorem Th20:
C is SubCatStr of C
proof
thus the carrier of C c= the carrier of C;
thus thesis;
end;
theorem
C1 is SubCatStr of C2 & C2 is SubCatStr of C3 implies C1 is SubCatStr of C3
proof
assume the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the
Arrows of C2 & the Comp of C1 cc= the Comp of C2 & the carrier of C2 c= the
carrier of C3 & the Arrows of C2 cc= the Arrows of C3 & the Comp of C2 cc= the
Comp of C3;
hence the carrier of C1 c= the carrier of C3 & the Arrows of C1 cc= the
Arrows of C3 & the Comp of C1 cc= the Comp of C3 by Th8;
end;
theorem Th22:
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
proof
let C1,C2 be AltCatStr;
assume that
A1: the carrier of C1 c= the carrier of C2 & the Arrows of C1 cc= the
Arrows of C2 and
A2: the Comp of C1 cc= the Comp of C2 and
A3: the carrier of C2 c= the carrier of C1 & the Arrows of C2 cc= the
Arrows of C1 and
A4: the Comp of C2 cc= the Comp of C1;
the carrier of C1 = the carrier of C2 & the Arrows of C1 = the Arrows of
C2 by A1,A3,Th7,XBOOLE_0:def 10;
hence thesis by A2,A4,Th7;
end;
registration
let C be AltCatStr;
cluster strict for SubCatStr of C;
existence
proof
set D = the AltCatStr of C;
reconsider D as SubCatStr of C by Def11;
take D;
thus thesis;
end;
end;
definition
let C be non empty AltCatStr, o be Object of C;
func ObCat o -> strict SubCatStr of C means
:Def12:
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);
existence
proof
set m = [o,o,o] .--> (the Comp of C).(o,o,o);
dom m = {[o,o,o]}
.= [:{o},{o},{o}:] by MCART_1:35;
then reconsider m as ManySortedSet of [:{o},{o},{o}:];
set a = (o,o):-> <^o,o^>;
dom a = [:{o},{o}:] by FUNCT_2:def 1;
then reconsider a as ManySortedSet of [:{o},{o}:];
A1: a.(o,o) = (the Arrows of C).(o,o) by FUNCT_4:80;
m is ManySortedFunction of {|a,a|},{|a|}
proof
let i be object;
A2: o in {o} by TARSKI:def 1;
assume i in [:{o},{o},{o}:];
then i in {[o,o,o]} by MCART_1:35;
then
A3: i = [o,o,o] by TARSKI:def 1;
then
A4: {|a|}.i = {|a|}.(o,o,o) by MULTOP_1:def 1
.= (the Arrows of C).(o,o) by A1,A2,ALTCAT_1:def 3;
{|a,a|}.i = {|a,a|}.(o,o,o) by A3,MULTOP_1:def 1
.= [:(the Arrows of C).(o,o),(the Arrows of C).(o,o):] by A1,A2,
ALTCAT_1:def 4;
hence thesis by A3,A4,FUNCOP_1:72;
end;
then reconsider m as BinComp of a;
set D = AltCatStr(#{o},a,m#);
D is SubCatStr of C
proof
thus the carrier of D c= the carrier of C;
thus the Arrows of D cc= the Arrows of C
proof
thus [:the carrier of D,the carrier of D:] c= [:the carrier of C,the
carrier of C:];
let i be set;
assume i in [:the carrier of D,the carrier of D:];
then i in {[o,o]} by ZFMISC_1:29;
then i = [o,o] by TARSKI:def 1;
hence thesis by A1;
end;
thus [:the carrier of D,the carrier of D,the carrier of D:] c= [:the
carrier of C,the carrier of C,the carrier of C:];
let i be set;
assume i in [:the carrier of D,the carrier of D,the carrier of D:];
then i in {[o,o,o]} by MCART_1:35;
then
A5: i = [o,o,o] by TARSKI:def 1;
then (the Comp of D).i = (the Comp of C).(o,o,o) by FUNCOP_1:72
.= (the Comp of C).i by A5,MULTOP_1:def 1;
hence thesis;
end;
then reconsider D as strict SubCatStr of C;
take D;
thus thesis;
end;
uniqueness;
end;
reserve C for non empty AltCatStr,
o for Object of C;
theorem Th23:
for o9 being Object of ObCat o holds o9 = o
proof
let o9 be Object of ObCat o;
the carrier of ObCat o = {o} by Def12;
hence thesis by TARSKI:def 1;
end;
registration
let C be non empty AltCatStr, o be Object of C;
cluster ObCat o -> transitive non empty;
coherence
proof
thus ObCat o is transitive
proof
let o1,o2,o3 be Object of ObCat o;
assume that
<^o1,o2^> <> {} and
A1: <^o2,o3^> <> {};
o1 = o by Th23;
hence thesis by A1,Th23;
end;
the carrier of ObCat o = {o} by Def12;
hence the carrier of ObCat o is non empty;
end;
end;
registration
let C be non empty AltCatStr;
cluster transitive non empty strict for SubCatStr of C;
existence
proof
set o = the Object of C;
take ObCat o;
thus thesis;
end;
end;
theorem Th24:
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
proof
let C be transitive non empty AltCatStr, D1,D2 be transitive non empty
SubCatStr of C such that
A1: the carrier of D1 c= the carrier of D2 and
A2: the Arrows of D1 cc= the Arrows of D2;
thus the carrier of D1 c= the carrier of D2 by A1;
thus the Arrows of D1 cc= the Arrows of D2 by A2;
thus [: the carrier of D1, the carrier of D1, the carrier of D1:] c= [: the
carrier of D2, the carrier of D2, the carrier of D2:] by A1,MCART_1:73;
let x be set;
assume
A3: x in [:the carrier of D1,the carrier of D1,the carrier of D1:];
then consider i1,i2,i3 being object such that
A4: i1 in the carrier of D1 & i2 in the carrier of D1 & i3 in the
carrier of D1 and
A5: x = [i1,i2,i3] by MCART_1:68;
reconsider i1,i2,i3 as Object of D1 by A4;
reconsider j1=i1, j2=i2, j3=i3 as Object of D2 by A1;
[i2,i3] in [:the carrier of D1,the carrier of D1:];
then
A6: <^i2,i3^> c= <^j2,j3^> by A2;
reconsider c2 = (the Comp of D2).(j1,j2,j3) as Function of [:<^j2,j3^>,<^j1,
j2^>:],<^j1,j3^>;
reconsider c1 = (the Comp of D1).(i1,i2,i3) as Function of [:<^i2,i3^>,<^i1,
i2^>:],<^i1,i3^>;
<^i1,i3^> = {} implies <^i2,i3^> = {} or <^i1,i2^> = {} by ALTCAT_1:def 2;
then <^i1,i3^> = {} implies [:<^i2,i3^>,<^i1,i2^>:] = {} by ZFMISC_1:90;
then
A7: dom c1 = [:<^i2,i3^>,<^i1,i2^>:] by FUNCT_2:def 1;
<^j1,j3^> = {} implies <^j2,j3^> = {} or <^j1,j2^> = {} by ALTCAT_1:def 2;
then <^j1,j3^> = {} implies [:<^j2,j3^>,<^j1,j2^>:] = {} by ZFMISC_1:90;
then
A8: dom c2 = [:<^j2,j3^>,<^j1,j2^>:] by FUNCT_2:def 1;
[i1,i2] in [:the carrier of D1,the carrier of D1:];
then <^i1,i2^> c= <^j1,j2^> by A2;
then
A9: dom c1 c= dom c2 by A7,A6,A8,ZFMISC_1:96;
A10: now
the carrier of D1 c= the carrier of C by Def11;
then reconsider o1=i1, o2=i2, o3=i3 as Object of C;
reconsider c = (the Comp of C).(o1,o2,o3) as Function of [:<^o2,o3^>,<^o1,
o2^>:],<^o1,o3^>;
let y be object;
A11: c = (the Comp of C).[o1,o2,o3] by MULTOP_1:def 1;
A12: c2 = (the Comp of D2).[o1,o2,o3] by MULTOP_1:def 1;
[o1,o2,o3] in [:the carrier of D2,the carrier of D2,the carrier of D2
:] & the Comp of D2 cc= the Comp of C by A1,A4,Def11,MCART_1:69;
then
A13: c2 c= c by A11,A12;
assume
A14: y in dom c1;
the Comp of D1 cc= the Comp of C & c1 = (the Comp of D1).[o1,o2,o3]
by Def11,MULTOP_1:def 1;
then c1 c= c by A3,A5,A11;
hence c1.y = c.y by A14,GRFUNC_1:2
.= c2.y by A9,A14,A13,GRFUNC_1:2;
end;
c1 = (the Comp of D1).x & c2 = (the Comp of D2).x by A5,MULTOP_1:def 1;
hence thesis by A9,A10,GRFUNC_1:2;
end;
definition
let C be AltCatStr, D be SubCatStr of C;
attr D is full means
:Def13:
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
:Def14:
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;
consistency;
end;
registration
let C be AltCatStr;
cluster full strict for SubCatStr of C;
existence
proof
set D = the AltCatStr of C;
reconsider D as SubCatStr of C by Def11;
take D;
thus the Arrows of D = (the Arrows of C)||the carrier of D;
thus thesis;
end;
end;
registration
let C be non empty AltCatStr;
cluster full non empty strict for SubCatStr of C;
existence
proof
set D = the AltCatStr of C;
reconsider D as SubCatStr of C by Def11;
take D;
thus the Arrows of D = (the Arrows of C)||the carrier of D;
thus the carrier of D is non empty;
thus thesis;
end;
end;
registration
let C be category, o be Object of C;
cluster ObCat o -> full id-inheriting;
coherence
proof
A1: the carrier of ObCat o = {o} by Def12;
the Arrows of ObCat o = (o,o):-> <^o,o^> by Def12
.= (the Arrows of C)||the carrier of ObCat o by A1,FUNCT_7:8;
hence ObCat o is full;
now
let o1 be Object of ObCat o, o2 be Object of C;
assume
A2: o1 = o2;
A3: o1 = o by Th23;
then <^o1,o1^> = ((o,o):-> <^o,o^>).(o,o) by Def12
.= <^o2,o2^> by A3,A2,FUNCT_4:80;
hence idm o2 in <^o1,o1^> by ALTCAT_1:19;
end;
hence thesis by Def14;
end;
end;
registration
let C be category;
cluster full id-inheriting non empty strict for SubCatStr of C;
existence
proof
set o = the Object of C;
take ObCat o;
thus thesis;
end;
end;
reserve C for non empty transitive AltCatStr;
theorem Th25:
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
proof
let D be SubCatStr of C such that
A1: the carrier of D = the carrier of C and
A2: the Arrows of D = the Arrows of C;
A3: D is transitive
proof
let o1,o2,o3 be Object of D;
reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1;
assume
A4: <^o1,o2^> <> {} & <^o2,o3^> <> {};
A5: <^o1,o3^> = <^p1,p3^> by A2;
<^o1,o2^> = <^p1,p2^> & <^o2,o3^> = <^p2,p3^> by A2;
hence thesis by A5,A4,ALTCAT_1:def 2;
end;
A6: C is SubCatStr of C by Th20;
D is non empty by A1;
then C is SubCatStr of D by A1,A2,A3,A6,Th24;
hence thesis by Th22;
end;
theorem Th26:
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
proof
let D1,D2 be non empty transitive SubCatStr of C;
assume
the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2;
then D1 is SubCatStr of D2 & D2 is SubCatStr of D1 by Th24;
hence thesis by Th22;
end;
theorem
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
proof
let D be full SubCatStr of C such that
A1: the carrier of D = the carrier of C;
the Arrows of D = (the Arrows of C)||the carrier of D by Def13
.= the Arrows of C by A1;
hence thesis by A1,Th25;
end;
theorem Th28:
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^>
proof
let C be non empty AltCatStr, D be full non empty SubCatStr of C, o1,o2 be
Object of C, p1,p2 be Object of D such that
A1: o1 = p1 & o2 = p2;
[p1,p2] in [:the carrier of D, the carrier of D:];
hence <^o1,o2^> = ((the Arrows of C)||the carrier of D).(p1,p2) by A1,
FUNCT_1:49
.= <^p1,p2^> by Def13;
end;
theorem Th29:
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
proof
let C be non empty AltCatStr, D be non empty SubCatStr of C;
let o be Object of D;
o in the carrier of D & the carrier of D c= the carrier of C by Def11;
hence thesis;
end;
registration
let C be transitive non empty AltCatStr;
cluster full non empty -> transitive for SubCatStr of C;
coherence
proof
let D be SubCatStr of C;
assume
A1: D is full non empty;
let o1,o2,o3 be Object of D such that
A2: <^o1,o2^> <> {} & <^o2,o3^> <> {};
reconsider p1 = o1, p2 = o2, p3 = o3 as Object of C by A1,Th29;
<^p1,p2^> <> {} & <^p2,p3^> <> {} by A1,A2,Th28;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence thesis by A1,Th28;
end;
end;
theorem
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
proof
let D1,D2 be full non empty SubCatStr of C;
assume
A1: the carrier of D1 = the carrier of D2;
then the Arrows of D1 =(the Arrows of C)||the carrier of D2 by Def13
.= the Arrows of D2 by Def13;
hence thesis by A1,Th26;
end;
theorem Th31:
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^>
proof
let C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be Object
of C, p1,p2 be Object of D such that
A1: o1 = p1 & o2 = p2;
[p1,p2] in [:the carrier of D, the carrier of D:] & the Arrows of D cc=
the Arrows of C by Def11;
hence thesis by A1;
end;
theorem Th32:
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
proof
let C be non empty transitive AltCatStr, D be non empty transitive SubCatStr
of C;
let p1,p2,p3 be Object of D such that
A1: <^p1,p2^> <> {} & <^p2,p3^> <> {};
let o1,o2,o3 be Object of C such that
A2: o1 = p1 & o2 = p2 & o3 = p3;
let f be Morphism of o1,o2, g be Morphism of o2,o3, ff be Morphism of p1,p2,
gg be Morphism of p2,p3 such that
A3: f = ff & g = gg;
<^p1,p3^> <> {} by A1,ALTCAT_1:def 2;
then dom((the Comp of D).(p1,p2,p3)) = [:<^p2,p3^>,<^p1,p2^>:] by
FUNCT_2:def 1;
then
A4: [gg,ff] in dom((the Comp of D).(p1,p2,p3)) by A1,ZFMISC_1:87;
A5: the Comp of D cc= the Comp of C by Def11;
(the Comp of D).(p1,p2,p3) = (the Comp of D).[p1,p2,p3] & (the Comp of C
).( o1,o2,o3) = (the Comp of C).[o1,o2,o3] by MULTOP_1:def 1;
then
A6: (the Comp of D).(p1,p2,p3) c= (the Comp of C).(o1,o2,o3) by A2,A5;
<^o1,o2^> <> {} & <^o2,o3^> <> {} by A1,A2,Th31,XBOOLE_1:3;
hence g*f = (the Comp of C).(o1,o2,o3).(g,f) by ALTCAT_1:def 8
.= (the Comp of D).(p1,p2,p3).(gg,ff) by A3,A4,A6,GRFUNC_1:2
.= gg*ff by A1,ALTCAT_1:def 8;
end;
registration
let C be associative transitive non empty AltCatStr;
cluster transitive -> associative for non empty SubCatStr of C;
coherence
proof
let D be non empty SubCatStr of C;
assume D is transitive;
then reconsider D as transitive non empty SubCatStr of C;
D is associative
proof
let o1,o2,o3,o4 be Object of D;
the carrier of D c= the carrier of C by Def11;
then reconsider p1=o1, p2=o2, p3=o3, p4=o4 as Object of C;
let f be Morphism of o1,o2, g be Morphism of o2,o3, h be Morphism of o3,
o4 such that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} and
A3: <^o3,o4^> <> {};
A4: <^o2,o3^> c= <^p2,p3^> by Th31;
g in <^o2,o3^> by A2;
then reconsider gg = g as Morphism of p2,p3 by A4;
A5: <^o1,o2^> c= <^p1,p2^> by Th31;
f in <^o1,o2^> by A1;
then reconsider ff = f as Morphism of p1,p2 by A5;
A6: <^o1,o3^> <> {} & g*f = gg*ff by A1,A2,Th32,ALTCAT_1:def 2;
A7: <^o3,o4^> c= <^p3,p4^> by Th31;
h in <^o3,o4^> by A3;
then reconsider hh = h as Morphism of p3,p4 by A7;
A8: <^p3,p4^> <> {} by A3,Th31,XBOOLE_1:3;
A9: <^p1,p2^> <> {} & <^p2,p3^> <> {} by A1,A2,Th31,XBOOLE_1:3;
<^o2,o4^> <> {} & h*g = hh* gg by A2,A3,Th32,ALTCAT_1:def 2;
hence h*g*f =hh*gg*ff by A1,Th32
.= hh*(gg*ff) by A9,A8,Def8
.= h*(g*f) by A3,A6,Th32;
end;
hence thesis;
end;
end;
theorem Th33:
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
proof
let C be non empty AltCatStr, D be non empty SubCatStr of C, o1,o2 be Object
of C, p1,p2 be Object of D such that
A1: o1 = p1 & o2 = p2 & <^p1,p2^> <> {};
let n be Morphism of p1,p2;
n in <^p1,p2^> & <^p1,p2^> c= <^o1,o2^> by A1,Th31;
hence thesis;
end;
registration
let C be transitive with_units non empty AltCatStr;
cluster id-inheriting transitive -> with_units for
non empty SubCatStr of C;
coherence
proof
let D be non empty SubCatStr of C such that
A1: D is id-inheriting and
A2: D is transitive;
let o be Object of D;
reconsider p = o as Object of C by Th29;
reconsider i = idm p as Morphism of o,o by A1,Def14;
A3: idm p in <^o,o^> by A1,Def14;
hence <^o,o^> <> {};
take i;
let o9 be Object of D, m9 be Morphism of o9,o, m99 be Morphism of o,o9;
hereby
reconsider p9 = o9 as Object of C by Th29;
assume
A4: <^o9,o^> <> {};
then
A5: <^p9,p^> <> {} by Th31,XBOOLE_1:3;
reconsider n9 = m9 as Morphism of p9,p by A4,Th33;
thus i*m9 = (idm p)*n9 by A2,A3,A4,Th32
.= m9 by A5,ALTCAT_1:20;
end;
reconsider p9 = o9 as Object of C by Th29;
assume
A6: <^o,o9^> <> {};
then
A7: <^p,p9^> <> {} by Th31,XBOOLE_1:3;
reconsider n99 = m99 as Morphism of p,p9 by A6,Th33;
thus m99*i = n99 * idm p by A2,A3,A6,Th32
.= m99 by A7,ALTCAT_1:def 17;
end;
end;
registration
let C be category;
cluster id-inheriting transitive for non empty SubCatStr of C;
existence
proof
set o = the Object of C;
take ObCat o;
thus thesis;
end;
end;
definition
let C be category;
mode subcategory of C is id-inheriting transitive SubCatStr of C;
end;
theorem
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
proof
let C be category, D be non empty subcategory of C;
let o be Object of D, o9 be Object of C;
assume
A1: o = o9;
then reconsider m = idm o9 as Morphism of o,o by Def14;
A2: idm o9 in <^o,o^> by A1,Def14;
now
let p be Object of D such that
A3: <^o,p^> <> {};
reconsider p9 = p as Object of C by Th29;
A4: <^o9,p9^> <> {} by A1,A3,Th31,XBOOLE_1:3;
let a be Morphism of o,p;
reconsider n = a as Morphism of o9,p9 by A1,A3,Th33;
thus a*m = n*(idm o9) by A1,A2,A3,Th32
.= a by A4,ALTCAT_1:def 17;
end;
hence thesis by ALTCAT_1:def 17;
end;