:: On the Categories Without Uniqueness of { \bf cod } and { \bf
:: dom } . Some Properties of the Morphisms and the Functors
:: by Artur Korni{\l}owicz
::
:: Received October 3, 1997
:: Copyright (c) 1997-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 ALTCAT_1, XBOOLE_0, CAT_1, RELAT_1, ALTCAT_3, CAT_3, RELAT_2,
FUNCTOR0, FUNCT_1, FUNCT_2, ZFMISC_1, STRUCT_0, PBOOLE, MSUALG_3,
MSUALG_6, ALTCAT_2, TARSKI, ALTCAT_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, MULTOP_1, PBOOLE, STRUCT_0, MSUALG_3, ALTCAT_1,
ALTCAT_2, ALTCAT_3, FUNCTOR0;
constructors REALSET1, MSUALG_3, FUNCTOR0, ALTCAT_3, RELSET_1, XTUPLE_0;
registrations SUBSET_1, RELSET_1, FUNCOP_1, STRUCT_0, FUNCT_1, RELAT_1,
ALTCAT_1, ALTCAT_2, FUNCTOR0, FUNCTOR2, PBOOLE;
requirements SUBSET, BOOLE;
definitions ALTCAT_1, ALTCAT_3, FUNCTOR0, MSUALG_3, TARSKI, FUNCT_2, XBOOLE_0,
PBOOLE, ALTCAT_2;
equalities ALTCAT_1, FUNCTOR0, XBOOLE_0, BINOP_1, REALSET1;
expansions ALTCAT_3, FUNCTOR0, MSUALG_3, TARSKI, FUNCT_2, ALTCAT_2;
theorems ALTCAT_1, ALTCAT_2, ALTCAT_3, FUNCT_1, FUNCT_2, FUNCTOR0, MCART_1,
MULTOP_1, FUNCTOR1, FUNCTOR2, PBOOLE, RELAT_1, ZFMISC_1, XBOOLE_0,
XBOOLE_1, PARTFUN1, XTUPLE_0;
schemes PBOOLE, XBOOLE_0;
begin :: Preliminaries
reserve C for category,
o1, o2, o3 for Object of C;
registration
let C be with_units non empty AltCatStr, o be Object of C;
cluster <^o,o^> -> non empty;
coherence by ALTCAT_1:19;
end;
theorem Th1:
for v being Morphism of o1, o2, u being Morphism of o1, o3 for f
being Morphism of o2, o3 st u = f * v & f" * f = idm o2 & <^o1,o2^> <> {} & <^
o2,o3^> <> {} & <^o3,o2^> <> {} holds v = f" * u
proof
let v be Morphism of o1, o2, u be Morphism of o1, o3, f be Morphism of o2,
o3 such that
A1: u = f * v and
A2: f" * f = idm o2 and
A3: <^o1,o2^> <> {} and
A4: <^o2,o3^> <> {} & <^o3,o2^> <> {};
thus f" * u = f" * f * v by A1,A3,A4,ALTCAT_1:21
.= v by A2,A3,ALTCAT_1:20;
end;
theorem Th2:
for v being Morphism of o2, o3, u being Morphism of o1, o3 for f
being Morphism of o1, o2 st u = v * f & f * f" = idm o2 & <^o1,o2^> <> {} & <^
o2,o1^> <> {} & <^o2,o3^> <> {} holds v = u * f"
proof
let v be Morphism of o2, o3, u be Morphism of o1, o3, f be Morphism of o1,
o2 such that
A1: u = v * f and
A2: f * f" = idm o2 and
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A4: <^o2,o3^> <> {};
thus u * f" = v * (f * f") by A1,A3,A4,ALTCAT_1:21
.= v by A2,A4,ALTCAT_1:def 17;
end;
theorem Th3:
for m being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <>
{} & m is iso holds m" is iso
proof
let m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
assume m is iso;
then
A2: m is retraction coretraction by ALTCAT_3:5;
hence m"*(m")" = m" * m by A1,ALTCAT_3:3
.= idm o1 by A1,A2,ALTCAT_3:2;
thus (m")"*m" = m * m" by A1,A2,ALTCAT_3:3
.= idm o2 by A1,A2,ALTCAT_3:2;
end;
theorem Th4:
for C being with_units non empty AltCatStr, o being Object of C
holds idm o is epi mono
proof
let C be with_units non empty AltCatStr, o be Object of C;
thus idm o is epi
proof
let o1 be Object of C such that
A1: <^o,o1^> <> {};
let B, C be Morphism of o, o1 such that
A2: B * idm o = C * idm o;
thus B = B * idm o by A1,ALTCAT_1:def 17
.= C by A1,A2,ALTCAT_1:def 17;
end;
let o1 be Object of C such that
A3: <^o1,o^> <> {};
let B, C be Morphism of o1, o such that
A4: idm o * B = idm o * C;
thus B = idm o * B by A3,ALTCAT_1:20
.= C by A3,A4,ALTCAT_1:20;
end;
registration
let C be with_units non empty AltCatStr, o be Object of C;
cluster idm o -> epi mono retraction coretraction;
coherence by Th4,ALTCAT_3:1;
end;
registration
let C be category, o be Object of C;
cluster idm o -> iso;
coherence by ALTCAT_3:6;
end;
theorem
for f being Morphism of o1, o2, g, h being Morphism of o2, o1 st h * f
= idm o1 & f * g = idm o2 & <^o1,o2^> <> {} & <^o2,o1^> <> {} holds g = h
proof
let f be Morphism of o1, o2, g, h be Morphism of o2, o1 such that
A1: h * f = idm o1 and
A2: f * g = idm o2 & <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
thus g = h * f * g by A1,A3,ALTCAT_1:20
.= h * idm o2 by A2,A3,ALTCAT_1:21
.= h by A3,ALTCAT_1:def 17;
end;
theorem
(for o1, o2 being Object of C, f being Morphism of o1, o2 holds f is
coretraction) implies for a, b being Object of C, g being Morphism of a, b st
<^a,b^> <> {} & <^b,a^> <> {} holds g is iso
proof
assume
A1: for o1, o2 being Object of C, f being Morphism of o1, o2 holds f is
coretraction;
let a, b be Object of C, g be Morphism of a, b such that
A2: <^a,b^> <> {} and
A3: <^b,a^> <> {};
A4: g is coretraction by A1;
g is retraction
proof
consider f be Morphism of b, a such that
A5: f is_left_inverse_of g by A4;
take f;
A6: f is mono by A1,A2,A3,ALTCAT_3:16;
f * (g * f) = f * g * f by A2,A3,ALTCAT_1:21
.= idm a * f by A5
.= f by A3,ALTCAT_1:20
.= f * idm b by A3,ALTCAT_1:def 17;
hence g * f = idm b by A6;
end;
hence thesis by A2,A3,A4,ALTCAT_3:6;
end;
begin :: Some properties of the initial and terminal objects
theorem
for m, m9 being Morphism of o1, o2 st m is _zero & m9 is _zero & ex O
being Object of C st O is _zero holds m = m9
proof
let m, m9 be Morphism of o1, o2 such that
A1: m is _zero and
A2: m9 is _zero;
given O being Object of C such that
A3: O is _zero;
set n = the Morphism of O, O;
set b = the Morphism of O, o2;
set a = the Morphism of o1, O;
thus m = b * (n" * n) * a by A1,A3
.= m9 by A2,A3;
end;
theorem
for C being non empty AltCatStr, O, A being Object of C for M being
Morphism of O, A st O is terminal holds M is mono
proof
let C be non empty AltCatStr, O, A be Object of C, M be Morphism of O, A
such that
A1: O is terminal;
let o be Object of C such that
A2: <^o,O^> <> {};
let a, b be Morphism of o, O such that
M * a = M * b;
consider N being Morphism of o, O such that
N in <^o,O^> and
A3: for M1 being Morphism of o, O st M1 in <^o,O^> holds N = M1 by A1,
ALTCAT_3:27;
thus a = N by A2,A3
.= b by A2,A3;
end;
theorem
for C being non empty AltCatStr, O, A being Object of C for M being
Morphism of A, O st O is initial holds M is epi
proof
let C be non empty AltCatStr, O, A be Object of C, M be Morphism of A, O
such that
A1: O is initial;
let o be Object of C such that
A2: <^O,o^> <> {};
let a, b be Morphism of O, o such that
a * M = b * M;
consider N being Morphism of O, o such that
N in <^O,o^> and
A3: for M1 being Morphism of O, o st M1 in <^O,o^> holds N = M1 by A1,
ALTCAT_3:25;
thus a = N by A2,A3
.= b by A2,A3;
end;
theorem
o2 is terminal & o1, o2 are_iso implies o1 is terminal
proof
assume that
A1: o2 is terminal and
A2: o1, o2 are_iso;
for o3 being Object of C holds ex M being Morphism of o3, o1 st M in <^
o3,o1^> & for v being Morphism of o3, o1 st v in <^o3,o1^> holds M = v
proof
consider f being Morphism of o1, o2 such that
A3: f is iso by A2;
A4: f" * f = idm o1 by A3;
let o3 be Object of C;
consider u being Morphism of o3, o2 such that
A5: u in <^o3,o2^> and
A6: for M1 being Morphism of o3, o2 st M1 in <^o3,o2^> holds u = M1 by A1,
ALTCAT_3:27;
take f" * u;
A7: <^o2,o1^> <> {} by A2;
then
A8: <^o3,o1^> <> {} by A5,ALTCAT_1:def 2;
hence f" * u in <^o3,o1^>;
A9: <^o1,o2^> <> {} by A2;
let v be Morphism of o3, o1 such that
v in <^o3,o1^>;
f * v = u by A5,A6;
hence thesis by A4,A9,A7,A8,Th1;
end;
hence thesis by ALTCAT_3:27;
end;
theorem
o1 is initial & o1, o2 are_iso implies o2 is initial
proof
assume that
A1: o1 is initial and
A2: o1, o2 are_iso;
for o3 being Object of C holds ex M being Morphism of o2, o3 st M in <^
o2,o3^> & for v being Morphism of o2, o3 st v in <^o2,o3^> holds M = v
proof
consider f being Morphism of o1, o2 such that
A3: f is iso by A2;
A4: f * f" = idm o2 by A3;
let o3 be Object of C;
consider u being Morphism of o1, o3 such that
A5: u in <^o1,o3^> and
A6: for M1 being Morphism of o1, o3 st M1 in <^o1,o3^> holds u = M1 by A1,
ALTCAT_3:25;
take u * f";
A7: <^o2,o1^> <> {} by A2;
then
A8: <^o2,o3^> <> {} by A5,ALTCAT_1:def 2;
hence u * f" in <^o2,o3^>;
A9: <^o1,o2^> <> {} by A2;
let v be Morphism of o2, o3 such that
v in <^o2,o3^>;
v * f = u by A5,A6;
hence thesis by A4,A9,A7,A8,Th2;
end;
hence thesis by ALTCAT_3:25;
end;
theorem
o1 is initial & o2 is terminal & <^o2,o1^> <> {} implies o2 is initial
& o1 is terminal
proof
assume that
A1: o1 is initial and
A2: o2 is terminal;
consider l being Morphism of o1, o2 such that
A3: l in <^o1,o2^> and
for M1 being Morphism of o1, o2 st M1 in <^o1,o2^> holds l = M1 by A1,
ALTCAT_3:25;
assume <^o2,o1^> <> {};
then consider m being object such that
A4: m in <^o2,o1^> by XBOOLE_0:def 1;
reconsider m as Morphism of o2, o1 by A4;
for o3 being Object of C holds ex M being Morphism of o2, o3 st M in <^
o2,o3^> & for M1 being Morphism of o2, o3 st M1 in <^o2,o3^> holds M = M1
proof
let o3 be Object of C;
consider M being Morphism of o1, o3 such that
A5: M in <^o1,o3^> and
A6: for M1 being Morphism of o1, o3 st M1 in <^o1,o3^> holds M = M1 by A1,
ALTCAT_3:25;
take M * m;
<^o2,o3^> <> {} by A4,A5,ALTCAT_1:def 2;
hence M * m in <^o2,o3^>;
let M1 be Morphism of o2, o3 such that
A7: M1 in <^o2,o3^>;
consider i2 being Morphism of o2, o2 such that
i2 in <^o2,o2^> and
A8: for M1 being Morphism of o2, o2 st M1 in <^o2,o2^> holds i2 = M1
by A2,ALTCAT_3:27;
thus M * m = M1 * l * m by A5,A6
.= M1 * (l * m) by A4,A3,A7,ALTCAT_1:21
.= M1 * i2 by A8
.= M1 * idm o2 by A8
.= M1 by A7,ALTCAT_1:def 17;
end;
hence o2 is initial by ALTCAT_3:25;
for o3 being Object of C holds ex M being Morphism of o3, o1 st M in <^
o3,o1^> & for M1 being Morphism of o3, o1 st M1 in <^o3,o1^> holds M = M1
proof
let o3 be Object of C;
consider M being Morphism of o3, o2 such that
A9: M in <^o3,o2^> and
A10: for M1 being Morphism of o3, o2 st M1 in <^o3,o2^> holds M = M1
by A2,ALTCAT_3:27;
take m * M;
<^o3,o1^> <> {} by A4,A9,ALTCAT_1:def 2;
hence m * M in <^o3,o1^>;
let M1 be Morphism of o3, o1 such that
A11: M1 in <^o3,o1^>;
consider i1 being Morphism of o1, o1 such that
i1 in <^o1,o1^> and
A12: for M1 being Morphism of o1, o1 st M1 in <^o1,o1^> holds i1 = M1
by A1,ALTCAT_3:25;
thus m * M = m * (l * M1) by A9,A10
.= m * l * M1 by A4,A3,A11,ALTCAT_1:21
.= i1 * M1 by A12
.= idm o1 * M1 by A12
.= M1 by A11,ALTCAT_1:20;
end;
hence thesis by ALTCAT_3:27;
end;
begin :: The properties of the functors
theorem Th13:
for A, B being transitive with_units non empty AltCatStr for F
being contravariant Functor of A, B for a being Object of A holds F.idm a = idm
(F.a)
proof
let A, B be transitive with_units non empty AltCatStr, F be contravariant
Functor of A, B;
let a be Object of A;
thus F.idm a = Morph-Map(F,a,a).idm a by FUNCTOR0:def 16
.= idm (F.a) by FUNCTOR0:def 20;
end;
theorem Th14:
for C1, C2 being non empty AltCatStr for F being Contravariant
FunctorStr over C1, C2 holds F is full iff for o1, o2 being Object of C1 holds
Morph-Map(F,o2,o1) is onto
proof
let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1, C2;
set I = [:the carrier of C1, the carrier of C1:];
hereby
assume
A1: F is full;
let o1, o2 be Object of C1;
thus Morph-Map(F,o2,o1) is onto
proof
A2: [o2,o1] in I by ZFMISC_1:87;
then
A3: [o2,o1] in dom(the ObjectMap of F) by FUNCT_2:def 1;
consider f being ManySortedFunction of the Arrows of C1, (the Arrows of
C2)*the ObjectMap of F such that
A4: f = the MorphMap of F and
A5: f is "onto" by A1;
rng(f.[o2,o1]) = ((the Arrows of C2)*the ObjectMap of F).[o2,o1] by A5,A2
;
hence
rng(Morph-Map(F,o2,o1)) = (the Arrows of C2).((the ObjectMap of F).
(o2,o1)) by A4,A3,FUNCT_1:13
.= <^F.o1,F.o2^> by FUNCTOR0:23;
end;
end;
assume
A6: for o1,o2 being Object of C1 holds Morph-Map(F,o2,o1) is onto;
ex I29 being non empty set, B9 being ManySortedSet of I29, f9 being
Function of I, I29 st the ObjectMap of F = f9 & the Arrows of C2 = B9 & the
MorphMap of F is ManySortedFunction of the Arrows of C1, B9*f9 by
FUNCTOR0:def 3;
then reconsider
f = the MorphMap of F as ManySortedFunction of the Arrows of C1,
(the Arrows of C2)*the ObjectMap of F;
take f;
thus f = the MorphMap of F;
let i be set;
assume i in I;
then consider o2, o1 being object such that
A7: o2 in the carrier of C1 & o1 in the carrier of C1 and
A8: i = [o2,o1] by ZFMISC_1:84;
reconsider o1, o2 as Object of C1 by A7;
[o2,o1] in I by ZFMISC_1:87;
then
A9: [o2,o1] in dom(the ObjectMap of F) by FUNCT_2:def 1;
Morph-Map(F,o2,o1) is onto by A6;
then rng(Morph-Map(F,o2,o1)) = (the Arrows of C2).(F.o1,F.o2)
.= (the Arrows of C2).((the ObjectMap of F).(o2,o1)) by FUNCTOR0:23
.= ((the Arrows of C2)*the ObjectMap of F).[o2,o1] by A9,FUNCT_1:13;
hence thesis by A8;
end;
theorem Th15:
for C1, C2 being non empty AltCatStr for F being Contravariant
FunctorStr over C1, C2 holds F is faithful iff for o1, o2 being Object of C1
holds Morph-Map(F,o2,o1) is one-to-one
proof
let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1,C2;
set I = [:the carrier of C1, the carrier of C1:];
hereby
assume F is faithful;
then
A1: (the MorphMap of F) is "1-1";
let o1, o2 be Object of C1;
[o2,o1] in I & dom(the MorphMap of F) = I by PARTFUN1:def 2,ZFMISC_1:87;
hence Morph-Map(F,o2,o1) is one-to-one by A1;
end;
assume
A2: for o1, o2 being Object of C1 holds Morph-Map(F,o2,o1) is one-to-one;
let i be set, f be Function such that
A3: i in dom(the MorphMap of F) and
A4: (the MorphMap of F).i = f;
dom(the MorphMap of F) = I by PARTFUN1:def 2;
then consider o1, o2 being object such that
A5: o1 in the carrier of C1 & o2 in the carrier of C1 and
A6: i = [o1,o2] by A3,ZFMISC_1:84;
reconsider o1, o2 as Object of C1 by A5;
(the MorphMap of F).(o1,o2) = Morph-Map(F,o1,o2);
hence thesis by A2,A4,A6;
end;
theorem Th16:
for C1, C2 being non empty AltCatStr for F being Covariant
FunctorStr over C1, C2 for o1, o2 being Object of C1, Fm being Morphism of F.o1
, F.o2 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st
Fm = F.m
proof
let C1, C2 be non empty AltCatStr, F be Covariant FunctorStr over C1, C2, o1
, o2 be Object of C1, Fm be Morphism of F.o1, F.o2 such that
A1: <^o1,o2^> <> {};
assume F is full;
then Morph-Map(F,o1,o2) is onto by FUNCTOR1:15;
then
A2: rng Morph-Map(F,o1,o2) = <^F.o1,F.o2^>;
assume F is feasible;
then
A3: <^F.o1,F.o2^> <> {} by A1;
then consider m being object such that
A4: m in dom Morph-Map(F,o1,o2) and
A5: Fm = Morph-Map(F,o1,o2).m by A2,FUNCT_1:def 3;
reconsider m as Morphism of o1, o2 by A3,A4,FUNCT_2:def 1;
take m;
thus thesis by A1,A3,A5,FUNCTOR0:def 15;
end;
theorem Th17:
for C1, C2 being non empty AltCatStr for F being Contravariant
FunctorStr over C1, C2 for o1, o2 being Object of C1, Fm being Morphism of F.o2
, F.o1 st <^o1,o2^> <> {} & F is full feasible ex m being Morphism of o1, o2 st
Fm = F.m
proof
let C1, C2 be non empty AltCatStr, F be Contravariant FunctorStr over C1, C2
, o1, o2 be Object of C1, Fm be Morphism of F.o2, F.o1 such that
A1: <^o1,o2^> <> {};
assume F is full;
then Morph-Map(F,o1,o2) is onto by Th14;
then
A2: rng Morph-Map(F,o1,o2) = <^F.o2,F.o1^>;
assume F is feasible;
then
A3: <^F.o2,F.o1^> <> {} by A1;
then consider m being object such that
A4: m in dom Morph-Map(F,o1,o2) and
A5: Fm = Morph-Map(F,o1,o2).m by A2,FUNCT_1:def 3;
reconsider m as Morphism of o1, o2 by A3,A4,FUNCT_2:def 1;
take m;
thus thesis by A1,A3,A5,FUNCTOR0:def 16;
end;
theorem Th18:
for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being Object of A, a being Morphism
of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds F.a is
retraction
proof
let A, B be transitive with_units non empty AltCatStr, F be covariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
assume a is retraction;
then consider b being Morphism of o2, o1 such that
A2: b is_right_inverse_of a;
take F.b;
a * b = idm o2 by A2;
hence (F.a) * (F.b) = F.idm o2 by A1,FUNCTOR0:def 23
.= idm F.o2 by FUNCTOR2:1;
end;
theorem Th19:
for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being Object of A, a being Morphism
of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction holds F.a is
coretraction
proof
let A, B be transitive with_units non empty AltCatStr, F be covariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
assume a is coretraction;
then consider b being Morphism of o2, o1 such that
A2: a is_right_inverse_of b;
take F.b;
b * a = idm o1 by A2;
hence (F.b) * (F.a) = F.idm o1 by A1,FUNCTOR0:def 23
.= idm F.o1 by FUNCTOR2:1;
end;
theorem Th20:
for A, B being category, F being covariant Functor of A, B for
o1, o2 being Object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,
o1^> <> {} & a is iso holds F.a is iso
proof
let A, B be category, F be covariant Functor of A, B, o1, o2 be Object of A,
a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A2: a is iso;
a is retraction coretraction by A1,A2,ALTCAT_3:6;
then
A3: F.a is retraction coretraction by A1,Th18,Th19;
<^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 18;
hence thesis by A3,ALTCAT_3:6;
end;
theorem
for A, B being category, F being covariant Functor of A, B for o1, o2
being Object of A st o1, o2 are_iso holds F.o1, F.o2 are_iso
proof
let A, B be category, F be covariant Functor of A, B, o1, o2 be Object of A;
assume
A1: o1, o2 are_iso;
then consider a being Morphism of o1, o2 such that
A2: a is iso;
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A1;
hence <^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by FUNCTOR0:def 18;
take F.a;
thus thesis by A3,A2,Th20;
end;
theorem Th22:
for A, B being transitive with_units non empty AltCatStr for F
being contravariant Functor of A, B for o1, o2 being Object of A, a being
Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is retraction holds
F.a is coretraction
proof
let A, B be transitive with_units non empty AltCatStr, F be contravariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
assume a is retraction;
then consider b being Morphism of o2, o1 such that
A2: b is_right_inverse_of a;
take F.b;
a * b = idm o2 by A2;
hence (F.b) * (F.a) = F.idm o2 by A1,FUNCTOR0:def 24
.= idm F.o2 by Th13;
end;
theorem Th23:
for A, B being transitive with_units non empty AltCatStr for F
being contravariant Functor of A, B for o1, o2 being Object of A, a being
Morphism of o1, o2 st <^o1,o2^> <> {} & <^o2,o1^> <> {} & a is coretraction
holds F.a is retraction
proof
let A, B be transitive with_units non empty AltCatStr, F be contravariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {};
assume a is coretraction;
then consider b being Morphism of o2, o1 such that
A2: a is_right_inverse_of b;
take F.b;
b * a = idm o1 by A2;
hence (F.a) * (F.b) = F.idm o1 by A1,FUNCTOR0:def 24
.= idm F.o1 by Th13;
end;
theorem Th24:
for A, B being category, F being contravariant Functor of A, B
for o1, o2 being Object of A, a being Morphism of o1, o2 st <^o1,o2^> <> {} &
<^o2,o1^> <> {} & a is iso holds F.a is iso
proof
let A, B be category, F be contravariant Functor of A, B, o1, o2 be Object
of A, a be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A2: a is iso;
a is retraction coretraction by A1,A2,ALTCAT_3:6;
then
A3: F.a is retraction coretraction by A1,Th22,Th23;
<^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A1,FUNCTOR0:def 19;
hence thesis by A3,ALTCAT_3:6;
end;
theorem
for A, B being category, F being contravariant Functor of A, B for o1,
o2 being Object of A st o1, o2 are_iso holds F.o2, F.o1 are_iso
proof
let A, B be category, F be contravariant Functor of A, B, o1, o2 be Object
of A;
assume
A1: o1, o2 are_iso;
then consider a being Morphism of o1, o2 such that
A2: a is iso;
A3: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A1;
hence <^F.o2,F.o1^> <> {} & <^F.o1,F.o2^> <> {} by FUNCTOR0:def 19;
take F.a;
thus thesis by A3,A2,Th24;
end;
theorem Th26:
for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being Object of A, a being Morphism
of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is
retraction holds a is retraction
proof
let A, B be transitive with_units non empty AltCatStr, F be covariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o2,F.o1^> <> {} by A3,FUNCTOR0:def 18;
assume F.a is retraction;
then consider b being Morphism of F.o2, F.o1 such that
A5: b is_right_inverse_of F.a;
Morph-Map(F,o2,o1) is onto by A1,FUNCTOR1:15;
then rng Morph-Map(F,o2,o1) = <^F.o2,F.o1^>;
then consider a9 being object such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
take a9;
A8: (F.a) * b = idm F.o2 by A5;
A9: dom Morph-Map(F,o2,o2) = <^o2,o2^> & Morph-Map(F,o2,o2) is one-to-one
by A1,FUNCTOR1:16,FUNCT_2:def 1;
Morph-Map(F,o2,o2).idm o2 = F.(idm o2) by FUNCTOR0:def 15
.= idm F.o2 by FUNCTOR2:1
.= (F.a) * F.a9 by A3,A8,A4,A7,FUNCTOR0:def 15
.= F.(a * a9) by A2,A3,FUNCTOR0:def 23
.= Morph-Map(F,o2,o2).(a * a9) by FUNCTOR0:def 15;
hence a * a9 = idm o2 by A9,FUNCT_1:def 4;
end;
theorem Th27:
for A, B being transitive with_units non empty AltCatStr for F
being covariant Functor of A, B for o1, o2 being Object of A, a being Morphism
of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is
coretraction holds a is coretraction
proof
let A, B be transitive with_units non empty AltCatStr, F be covariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o2,F.o1^> <> {} by A3,FUNCTOR0:def 18;
assume F.a is coretraction;
then consider b being Morphism of F.o2, F.o1 such that
A5: F.a is_right_inverse_of b;
Morph-Map(F,o2,o1) is onto by A1,FUNCTOR1:15;
then rng Morph-Map(F,o2,o1) = <^F.o2,F.o1^>;
then consider a9 being object such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
take a9;
A8: b * (F.a) = idm F.o1 by A5;
A9: dom Morph-Map(F,o1,o1) = <^o1,o1^> & Morph-Map(F,o1,o1) is one-to-one
by A1,FUNCTOR1:16,FUNCT_2:def 1;
Morph-Map(F,o1,o1).idm o1 = F.(idm o1) by FUNCTOR0:def 15
.= idm F.o1 by FUNCTOR2:1
.= (F.a9) * F.a by A3,A8,A4,A7,FUNCTOR0:def 15
.= F.(a9 * a) by A2,A3,FUNCTOR0:def 23
.= Morph-Map(F,o1,o1).(a9 * a) by FUNCTOR0:def 15;
hence a9 * a = idm o1 by A9,FUNCT_1:def 4;
end;
theorem Th28:
for A, B being category, F being covariant Functor of A, B for
o1, o2 being Object of A, a being Morphism of o1, o2 st F is full faithful & <^
o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso
proof
let A, B be category, F be covariant Functor of A, B, o1, o2 be Object of A,
a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A3: F.a is iso;
<^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A2,FUNCTOR0:def 18;
then F.a is retraction coretraction by A3,ALTCAT_3:6;
then a is retraction coretraction by A1,A2,Th26,Th27;
hence thesis by A2,ALTCAT_3:6;
end;
theorem
for A, B being category, F being covariant Functor of A, B for o1, o2
being Object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F
.o1, F.o2 are_iso holds o1, o2 are_iso
proof
let A, B be category, F be covariant Functor of A, B, o1, o2 be Object of A
such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {} and
A4: F.o1, F.o2 are_iso;
consider Fa being Morphism of F.o1, F.o2 such that
A5: Fa is iso by A4;
consider a being Morphism of o1, o2 such that
A6: Fa = F.a by A1,A2,Th16;
thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2,A3;
take a;
thus thesis by A1,A2,A3,A5,A6,Th28;
end;
theorem Th30:
for A, B being transitive with_units non empty AltCatStr for F
being contravariant Functor of A, B for o1, o2 being Object of A, a being
Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} &
F.a is retraction holds a is coretraction
proof
let A, B be transitive with_units non empty AltCatStr, F be contravariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o1,F.o2^> <> {} by A3,FUNCTOR0:def 19;
assume F.a is retraction;
then consider b being Morphism of F.o1, F.o2 such that
A5: b is_right_inverse_of F.a;
Morph-Map(F,o2,o1) is onto by A1,Th14;
then rng Morph-Map(F,o2,o1) = <^F.o1,F.o2^>;
then consider a9 being object such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
take a9;
A8: (F.a) * b = idm F.o1 by A5;
A9: dom Morph-Map(F,o1,o1) = <^o1,o1^> & Morph-Map(F,o1,o1) is one-to-one
by A1,Th15,FUNCT_2:def 1;
Morph-Map(F,o1,o1).idm o1 = F.(idm o1) by FUNCTOR0:def 16
.= idm F.o1 by Th13
.= (F.a) * F.a9 by A3,A8,A4,A7,FUNCTOR0:def 16
.= F.(a9 * a) by A2,A3,FUNCTOR0:def 24
.= Morph-Map(F,o1,o1).(a9 * a) by FUNCTOR0:def 16;
hence a9 * a = idm o1 by A9,FUNCT_1:def 4;
end;
theorem Th31:
for A, B being transitive with_units non empty AltCatStr for F
being contravariant Functor of A, B for o1, o2 being Object of A, a being
Morphism of o1, o2 st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} &
F.a is coretraction holds a is retraction
proof
let A, B be transitive with_units non empty AltCatStr, F be contravariant
Functor of A, B, o1, o2 be Object of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {};
A4: <^F.o1,F.o2^> <> {} by A3,FUNCTOR0:def 19;
assume F.a is coretraction;
then consider b being Morphism of F.o1, F.o2 such that
A5: F.a is_right_inverse_of b;
Morph-Map(F,o2,o1) is onto by A1,Th14;
then rng Morph-Map(F,o2,o1) = <^F.o1,F.o2^>;
then consider a9 being object such that
A6: a9 in dom Morph-Map(F,o2,o1) and
A7: b = Morph-Map(F,o2,o1).a9 by A4,FUNCT_1:def 3;
reconsider a9 as Morphism of o2, o1 by A4,A6,FUNCT_2:def 1;
take a9;
A8: b * (F.a) = idm F.o2 by A5;
A9: dom Morph-Map(F,o2,o2) = <^o2,o2^> & Morph-Map(F,o2,o2) is one-to-one
by A1,Th15,FUNCT_2:def 1;
Morph-Map(F,o2,o2).idm o2 = F.(idm o2) by FUNCTOR0:def 16
.= idm F.o2 by Th13
.= (F.a9) * F.a by A3,A8,A4,A7,FUNCTOR0:def 16
.= F.(a * a9) by A2,A3,FUNCTOR0:def 24
.= Morph-Map(F,o2,o2).(a * a9) by FUNCTOR0:def 16;
hence a * a9 = idm o2 by A9,FUNCT_1:def 4;
end;
theorem Th32:
for A, B being category, F being contravariant Functor of A, B
for o1, o2 being Object of A, a being Morphism of o1, o2 st F is full faithful
& <^o1,o2^> <> {} & <^o2,o1^> <> {} & F.a is iso holds a is iso
proof
let A, B be category, F be contravariant Functor of A, B, o1, o2 be Object
of A, a be Morphism of o1, o2 such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} & <^o2,o1^> <> {} and
A3: F.a is iso;
<^F.o1,F.o2^> <> {} & <^F.o2,F.o1^> <> {} by A2,FUNCTOR0:def 19;
then F.a is retraction coretraction by A3,ALTCAT_3:6;
then a is retraction coretraction by A1,A2,Th30,Th31;
hence thesis by A2,ALTCAT_3:6;
end;
theorem
for A, B being category, F being contravariant Functor of A, B for o1,
o2 being Object of A st F is full faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {}
& F.o2, F.o1 are_iso holds o1, o2 are_iso
proof
let A, B be category, F be contravariant Functor of A, B, o1, o2 be Object
of A such that
A1: F is full faithful and
A2: <^o1,o2^> <> {} and
A3: <^o2,o1^> <> {} and
A4: F.o2, F.o1 are_iso;
consider Fa being Morphism of F.o2, F.o1 such that
A5: Fa is iso by A4;
consider a being Morphism of o1, o2 such that
A6: Fa = F.a by A1,A2,Th17;
thus <^o1,o2^> <> {} & <^o2,o1^> <> {} by A2,A3;
take a;
thus thesis by A1,A2,A3,A5,A6,Th32;
end;
Lm1: now
let C be non empty transitive AltCatStr, p1, p2, p3 be Object of C such that
A1: (the Arrows of C).(p1,p3) = {};
thus [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] = {}
proof
assume [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] <> {};
then consider k being object such that
A2: k in [:(the Arrows of C).(p2,p3),(the Arrows of C).(p1,p2):] by
XBOOLE_0:def 1;
consider u1, u2 being object such that
A3: u1 in (the Arrows of C).(p2,p3) & u2 in (the Arrows of C).(p1,p2) and
k = [u1,u2] by A2,ZFMISC_1:def 2;
u1 in <^p2,p3^> & u2 in <^p1,p2^> by A3;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence contradiction by A1;
end;
end;
begin :: The subcategories of the morphisms
theorem Th34:
for C being AltCatStr, D being SubCatStr of C st the carrier of
C = the carrier of D & the Arrows of C = the Arrows of D holds D is full;
theorem Th35:
for C being with_units non empty AltCatStr, D being SubCatStr
of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D
holds D is id-inheriting
proof
let C be with_units non empty AltCatStr, D be SubCatStr of C;
assume
the carrier of C = the carrier of D & the Arrows of C = the Arrows of D;
then reconsider D as full non empty SubCatStr of C by Th34;
now
let o be Object of D, o9 be Object of C;
assume o = o9;
then <^o9,o9^> = <^o,o^> by ALTCAT_2:28;
hence idm o9 in <^o,o^>;
end;
hence thesis by ALTCAT_2:def 14;
end;
registration
let C be category;
cluster full non empty strict for subcategory of C;
existence
proof
reconsider D = the AltCatStr of C as SubCatStr of C by ALTCAT_2:def 11;
reconsider D as full non empty id-inheriting SubCatStr of C by Th34,Th35;
take D;
thus thesis;
end;
end;
theorem Th36:
for B being non empty subcategory of C for A being non empty
subcategory of B holds A is non empty subcategory of C
proof
let B be non empty subcategory of C, A be non empty subcategory of B;
reconsider D = A as with_units non empty SubCatStr of C by ALTCAT_2:21;
now
let o be Object of D, o1 be Object of C such that
A1: o = o1;
o in the carrier of D & the carrier of D c= the carrier of B by
ALTCAT_2:def 11;
then reconsider oo = o as Object of B;
idm o = idm oo by ALTCAT_2:34
.= idm o1 by A1,ALTCAT_2:34;
hence idm o1 in <^o,o^>;
end;
hence thesis by ALTCAT_2:def 14;
end;
theorem Th37:
for C being non empty transitive AltCatStr for D being non empty
transitive SubCatStr of C for o1, o2 being Object of C, p1, p2 being Object of
D for m being Morphism of o1, o2, n being Morphism of p1, p2 st p1 = o1 & p2 =
o2 & m = n & <^p1,p2^> <> {} holds (m is mono implies n is mono) & (m is epi
implies n is epi)
proof
let C be non empty transitive AltCatStr, D be non empty transitive SubCatStr
of C, o1, o2 be Object of C, p1, p2 be Object of D, m be Morphism of o1, o2, n
be Morphism of p1, p2 such that
A1: p1 = o1 and
A2: p2 = o2 and
A3: m = n & <^p1,p2^> <> {};
thus m is mono implies n is mono
proof
assume
A4: m is mono;
let p3 be Object of D such that
A5: <^p3,p1^> <> {};
reconsider o3 = p3 as Object of C by ALTCAT_2:29;
A6: <^o3,o1^> <> {} by A1,A5,ALTCAT_2:31,XBOOLE_1:3;
let f, g be Morphism of p3, p1 such that
A7: n * f = n * g;
reconsider f1 = f, g1 = g as Morphism of o3, o1 by A1,A5,ALTCAT_2:33;
m * f1 = n * f by A1,A2,A3,A5,ALTCAT_2:32
.= m * g1 by A1,A2,A3,A5,A7,ALTCAT_2:32;
hence thesis by A4,A6;
end;
assume
A8: m is epi;
let p3 be Object of D such that
A9: <^p2,p3^> <> {};
reconsider o3 = p3 as Object of C by ALTCAT_2:29;
A10: <^o2,o3^> <> {} by A2,A9,ALTCAT_2:31,XBOOLE_1:3;
let f, g be Morphism of p2, p3 such that
A11: f * n = g * n;
reconsider f1 = f, g1 = g as Morphism of o2, o3 by A2,A9,ALTCAT_2:33;
f1 * m = f * n by A1,A2,A3,A9,ALTCAT_2:32
.= g1 * m by A1,A2,A3,A9,A11,ALTCAT_2:32;
hence thesis by A8,A10;
end;
theorem Th38:
for D being non empty subcategory of C for o1, o2 being Object
of C, p1, p2 being Object of D for m being Morphism of o1, o2, m1 being
Morphism of o2, o1 for n being Morphism of p1, p2, n1 being Morphism of p2, p1
st p1 = o1 & p2 = o2 & m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {}
holds (m is_left_inverse_of m1 iff n is_left_inverse_of n1) & (m
is_right_inverse_of m1 iff n is_right_inverse_of n1)
proof
let D be non empty subcategory of C, o1, o2 be Object of C, p1, p2 be Object
of D, m be Morphism of o1, o2, m1 be Morphism of o2, o1, n be Morphism of p1,
p2, n1 be Morphism of p2, p1 such that
A1: p1 = o1 and
A2: p2 = o2 and
A3: m = n & m1 = n1 & <^p1,p2^> <> {} & <^p2,p1^> <> {};
thus m is_left_inverse_of m1 iff n is_left_inverse_of n1
proof
thus m is_left_inverse_of m1 implies n is_left_inverse_of n1
proof
assume
A4: m is_left_inverse_of m1;
thus n * n1 = m * m1 by A1,A2,A3,ALTCAT_2:32
.= idm o2 by A4
.= idm p2 by A2,ALTCAT_2:34;
end;
assume
A5: n is_left_inverse_of n1;
thus m * m1 = n * n1 by A1,A2,A3,ALTCAT_2:32
.= idm p2 by A5
.= idm o2 by A2,ALTCAT_2:34;
end;
thus m is_right_inverse_of m1 implies n is_right_inverse_of n1
proof
assume
A6: m is_right_inverse_of m1;
thus n1 * n = m1 * m by A1,A2,A3,ALTCAT_2:32
.= idm o1 by A6
.= idm p1 by A1,ALTCAT_2:34;
end;
assume
A7: n is_right_inverse_of n1;
thus m1 * m = n1 * n by A1,A2,A3,ALTCAT_2:32
.= idm p1 by A7
.= idm o1 by A1,ALTCAT_2:34;
end;
theorem
for D being full non empty subcategory of C for o1, o2 being Object of
C, p1, p2 being Object of D for m being Morphism of o1, o2, n being Morphism of
p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {} holds (
m is retraction implies n is retraction) & (m is coretraction implies n is
coretraction) & (m is iso implies n is iso)
proof
let D be full non empty subcategory of C, o1, o2 be Object of C, p1, p2 be
Object of D, m be Morphism of o1, o2, n be Morphism of p1, p2;
assume that
A1: p1 = o1 & p2 = o2 and
A2: m = n and
A3: <^p1,p2^> <> {} & <^p2,p1^> <> {};
thus
A4: m is retraction implies n is retraction
proof
assume m is retraction;
then consider B being Morphism of o2, o1 such that
A5: B is_right_inverse_of m;
reconsider B1 = B as Morphism of p2, p1 by A1,ALTCAT_2:28;
take B1;
thus thesis by A1,A2,A3,A5,Th38;
end;
thus
A6: m is coretraction implies n is coretraction
proof
assume m is coretraction;
then consider B being Morphism of o2, o1 such that
A7: B is_left_inverse_of m;
reconsider B1 = B as Morphism of p2, p1 by A1,ALTCAT_2:28;
take B1;
thus thesis by A1,A2,A3,A7,Th38;
end;
assume m is iso;
hence thesis by A3,A4,A6,ALTCAT_3:5,6;
end;
theorem Th40:
for D being non empty subcategory of C for o1, o2 being Object
of C, p1, p2 being Object of D for m being Morphism of o1, o2, n being Morphism
of p1, p2 st p1 = o1 & p2 = o2 & m = n & <^p1,p2^> <> {} & <^p2,p1^> <> {}
holds (n is retraction implies m is retraction) & (n is coretraction implies m
is coretraction) & (n is iso implies m is iso)
proof
let D be non empty subcategory of C, o1, o2 be Object of C, p1, p2 be Object
of D, m be Morphism of o1, o2, n be Morphism of p1, p2 such that
A1: p1 = o1 & p2 = o2 and
A2: m = n and
A3: <^p1,p2^> <> {} and
A4: <^p2,p1^> <> {};
A5: <^o1,o2^> <> {} & <^o2,o1^> <> {} by A1,A3,A4,ALTCAT_2:31,XBOOLE_1:3;
thus
A6: n is retraction implies m is retraction
proof
assume n is retraction;
then consider B being Morphism of p2, p1 such that
A7: B is_right_inverse_of n;
reconsider B1 = B as Morphism of o2, o1 by A1,A4,ALTCAT_2:33;
take B1;
thus thesis by A1,A2,A3,A4,A7,Th38;
end;
thus
A8: n is coretraction implies m is coretraction
proof
assume n is coretraction;
then consider B being Morphism of p2, p1 such that
A9: B is_left_inverse_of n;
reconsider B1 = B as Morphism of o2, o1 by A1,A4,ALTCAT_2:33;
take B1;
thus thesis by A1,A2,A3,A4,A9,Th38;
end;
assume n is iso;
hence thesis by A6,A8,A5,ALTCAT_3:5,6;
end;
definition
let C be category;
func AllMono C -> strict non empty transitive SubCatStr of C means
:Def1:
the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C &
for o1, o2 being Object of C, m being Morphism of o1, o2 holds m in (the Arrows
of it).(o1,o2) iff <^o1,o2^> <> {} & m is mono;
existence
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for x being set holds x in D2 iff ex o1, o2 being
Object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & x =
m & m is mono;
set I = the carrier of C;
A1: for i being object st i in [:I,I:] ex X being object st P[i,X]
proof
let i be object;
assume i in [:I,I:];
then consider o1, o2 being object such that
A2: o1 in I & o2 in I and
A3: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A2;
defpred P[object] means
ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
m = $1 & m is mono;
consider X being set such that
A4: for x being object holds x in X iff x in (the Arrows of C).(o1,o2)
& P[x] from XBOOLE_0:sch 1;
take X,X;
thus X = X;
let x be set;
thus x in X implies ex o1, o2 being Object of C, m being Morphism of o1,
o2 st i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is mono
proof
assume x in X;
then consider m being Morphism of o1, o2 such that
A5: <^o1,o2^> <> {} & m = x & m is mono by A4;
take o1, o2, m;
thus thesis by A3,A5;
end;
given p1, p2 being Object of C, m being Morphism of p1, p2 such that
A6: i = [p1,p2] and
A7: <^p1,p2^> <> {} & x = m & m is mono;
o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
hence thesis by A4,A7;
end;
consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being object st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
(A1);
defpred R[object,object] means
ex p1, p2, p3 being Object of C st $1 = [p1,p2,p3
] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being object st i in [:I,I,I:] ex j being object st R[i,j]
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being object such that
A10: p1 in I & p2 in I & p3 in I and
A11: i = [p1,p2,p3] by MCART_1:68;
reconsider p1, p2, p3 as Object of C by A10;
take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
take p1, p2, p3;
thus i = [p1,p2,p3] by A11;
thus thesis;
end;
consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being object st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
3 (A9 );
A13: Ar cc= the Arrows of C
proof
thus [:I,I:] c= [:the carrier of C,the carrier of C:];
let i be set;
assume
A14: i in [:I,I:];
let q be object;
assume
A15: q in Ar.i;
P[i,Ar.i] by A8,A14;
then ex p1, p2 being Object of C, m being Morphism of p1, p2 st i = [p1,
p2] & <^p1,p2^> <> {} & q = m & m is mono by A15;
hence thesis;
end;
Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being Object of C such that
A16: i = [p1,p2,p3] and
A17: Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A18: [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then
A19: Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13;
A20: [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13;
then
A21: [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
Arrows of C).(p1,p2):] by A19,ZFMISC_1:96;
(the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
(the Arrows of C).(p1,p2):] = {} by Lm1;
then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
Arrows of C).(p1,p3) by A17,A21,FUNCT_2:32;
A22: Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A18;
A23: Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A20;
A24: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
proof
assume
A25: (the Arrows of C).(p1,p3) = {};
assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
then consider k being object such that
A26: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
consider u1, u2 being object such that
A27: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
k = [u1,u2] by A26,ZFMISC_1:def 2;
u1 in <^p2,p3^> & u2 in <^p1,p2^> by A23,A22,A27;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence contradiction by A25;
end;
A28: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A29: rng f c= {|Ar|}.i
proof
let q be object;
assume q in rng f;
then consider x being object such that
A30: x in dom f and
A31: q = f.x by FUNCT_1:def 3;
A32: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A24,FUNCT_2:def 1;
then consider m1, m2 being object such that
A33: m1 in Ar.(p2,p3) and
A34: m2 in Ar.(p1,p2) and
A35: x = [m1,m2] by A30,ZFMISC_1:84;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such
that
A36: [p2,p3] = [q2,q3] and
A37: <^q2,q3^> <> {} and
A38: m1 = qq and
A39: qq is mono by A33;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such
that
A40: [p1,p2] = [r1,r2] and
A41: <^r1,r2^> <> {} and
A42: m2 = rr and
A43: rr is mono by A34;
A44: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3
] = [o1,o3] & <^o1,o3^> <> {} & q = m & m is mono
proof
A45: p2 = q2 by A36,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A40,XTUPLE_0:1;
take r1, q3, mm * rr;
A46: p1 = r1 by A40,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A36,XTUPLE_0:1;
A47: r2 = p2 by A40,XTUPLE_0:1;
hence <^r1,q3^> <> {} by A37,A41,A45,ALTCAT_1:def 2;
A48: p3 = q3 by A36,XTUPLE_0:1;
thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A17,A30,A31,A32,A35
,A38,A42,FUNCT_1:49
.= mm * rr by A36,A37,A41,A47,A46,A48,ALTCAT_1:def 8;
thus thesis by A37,A39,A41,A43,A47,A45,ALTCAT_3:9;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
then q in Ar.[p1,p3] by A44;
hence thesis by A16,A28,MULTOP_1:def 1;
end;
{|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A16,MULTOP_1:def 1;
hence thesis by A24,A29,FUNCT_2:6;
end;
then reconsider Co as BinComp of Ar;
set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
IT is SubCatStr of C
proof
thus the carrier of IT c= the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
thus [:J,J,J:] c= [:I,I,I:];
let i be set;
assume i in [:J,J,J:];
then consider p1, p2, p3 being Object of C such that
A49: i = [p1,p2,p3] and
A50: Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A51: ((the Comp of C).(p1,p2,p3)) qua Relation |([:Ar.(p2,p3),Ar.(p1,p2)
:] qua set) c= (the Comp of C).(p1,p2,p3) by RELAT_1:59;
let q be object;
assume q in (the Comp of IT).i;
then q in (the Comp of C).(p1,p2,p3) by A50,A51;
hence thesis by A49,MULTOP_1:def 1;
end;
then reconsider IT as strict non empty SubCatStr of C;
IT is transitive
proof
let p1, p2, p3 be Object of IT;
assume that
A52: <^p1,p2^> <> {} and
A53: <^p2,p3^> <> {};
consider m2 being object such that
A54: m2 in <^p1,p2^> by A52,XBOOLE_0:def 1;
consider m1 being object such that
A55: m1 in <^p2,p3^> by A53,XBOOLE_0:def 1;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such that
A56: [p2,p3] = [q2,q3] and
A57: <^q2,q3^> <> {} and
m1 = qq and
A58: qq is mono by A55;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such that
A59: [p1,p2] = [r1,r2] and
A60: <^r1,r2^> <> {} and
m2 = rr and
A61: rr is mono by A54;
A62: p2 = q2 by A56,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A59,XTUPLE_0:1;
A63: r2 = p2 by A59,XTUPLE_0:1;
A64: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3]
= [o1,o3] & <^o1,o3^> <> {} & mm * rr = m & m is mono
proof
take r1, q3, mm * rr;
p1 = r1 by A59,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A56,XTUPLE_0:1;
thus <^r1,q3^> <> {} by A57,A60,A63,A62,ALTCAT_1:def 2;
thus mm * rr = mm * rr;
thus thesis by A57,A58,A60,A61,A63,A62,ALTCAT_3:9;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
hence thesis by A64;
end;
then reconsider IT as strict non empty transitive SubCatStr of C;
take IT;
thus the carrier of IT = the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
let o1, o2 be Object of C, m be Morphism of o1, o2;
A65: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & m is mono
proof
assume
A66: m in (the Arrows of IT).(o1,o2);
P[[o1,o2],Ar.[o1,o2]] by A8,A65;
then consider
p1, p2 being Object of C, n being Morphism of p1, p2 such that
A67: [o1,o2] = [p1,p2] and
A68: <^p1,p2^> <> {} & m = n & n is mono by A66;
o1 = p1 & o2 = p2 by A67,XTUPLE_0:1;
hence thesis by A68;
end;
assume
A69: <^o1,o2^> <> {} & m is mono;
P[[o1,o2],Ar.[o1,o2]] by A8,A65;
hence thesis by A69;
end;
uniqueness
proof
let S1, S2 be strict non empty transitive SubCatStr of C such that
A70: the carrier of S1 = the carrier of C and
A71: the Arrows of S1 cc= the Arrows of C and
A72: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & m is mono and
A73: the carrier of S2 = the carrier of C and
A74: the Arrows of S2 cc= the Arrows of C and
A75: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & m is mono;
now
let i be object;
assume
A76: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A77: o1 in the carrier of C & o2 in the carrier of C and
A78: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A77;
thus (the Arrows of S1).i = (the Arrows of S2).i
proof
thus (the Arrows of S1).i c= (the Arrows of S2).i
proof
let n be object such that
A79: n in (the Arrows of S1).i;
(the Arrows of S1).i c= (the Arrows of C).i by A70,A71,A76;
then reconsider m = n as Morphism of o1, o2 by A78,A79;
m in (the Arrows of S1).(o1,o2) by A78,A79;
then <^o1,o2^> <> {} & m is mono by A72;
then m in (the Arrows of S2).(o1,o2) by A75;
hence thesis by A78;
end;
let n be object such that
A80: n in (the Arrows of S2).i;
(the Arrows of S2).i c= (the Arrows of C).i by A73,A74,A76;
then reconsider m = n as Morphism of o1, o2 by A78,A80;
m in (the Arrows of S2).(o1,o2) by A78,A80;
then <^o1,o2^> <> {} & m is mono by A75;
then m in (the Arrows of S1).(o1,o2) by A72;
hence thesis by A78;
end;
end;
hence thesis by A70,A73,ALTCAT_2:26,PBOOLE:3;
end;
end;
registration
let C be category;
cluster AllMono C -> id-inheriting;
coherence
proof
for o be Object of AllMono C, o9 be Object of C st o = o9 holds idm o9
in <^o,o^> by Def1;
hence thesis by ALTCAT_2:def 14;
end;
end;
definition
let C be category;
func AllEpi C -> strict non empty transitive SubCatStr of C means
:Def2:
the
carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for
o1, o2 being Object of C, m being Morphism of o1, o2 holds m in (the Arrows of
it).(o1,o2) iff <^o1,o2^> <> {} & m is epi;
existence
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for x being set holds x in D2 iff ex o1, o2 being
Object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & x =
m & m is epi;
set I = the carrier of C;
A1: for i being object st i in [:I,I:] ex X being object st P[i,X]
proof
let i be object;
assume i in [:I,I:];
then consider o1, o2 being object such that
A2: o1 in I & o2 in I and
A3: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A2;
defpred P[object] means
ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
m = $1 & m is epi;
consider X being set such that
A4: for x being object holds x in X iff x in (the Arrows of C).(o1,o2)
& P[x] from XBOOLE_0:sch 1;
take X,X;
thus X=X;
let x be set;
thus x in X implies ex o1, o2 being Object of C, m being Morphism of o1,
o2 st i = [o1,o2] & <^o1,o2^> <> {} & x = m & m is epi
proof
assume x in X;
then consider m being Morphism of o1, o2 such that
A5: <^o1,o2^> <> {} & m = x & m is epi by A4;
take o1, o2, m;
thus thesis by A3,A5;
end;
given p1, p2 being Object of C, m being Morphism of p1, p2 such that
A6: i = [p1,p2] and
A7: <^p1,p2^> <> {} & x = m & m is epi;
o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
hence thesis by A4,A7;
end;
consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being object st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
(A1);
defpred R[object,object] means
ex p1, p2, p3 being Object of C st $1 = [p1,p2,p3
] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being object st i in [:I,I,I:] ex j being object st R[i,j]
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being object such that
A10: p1 in I & p2 in I & p3 in I and
A11: i = [p1,p2,p3] by MCART_1:68;
reconsider p1, p2, p3 as Object of C by A10;
take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
take p1, p2, p3;
thus i = [p1,p2,p3] by A11;
thus thesis;
end;
consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being object st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
3 (A9 );
A13: Ar cc= the Arrows of C
proof
thus [:I,I:] c= [:the carrier of C,the carrier of C:];
let i be set;
assume
A14: i in [:I,I:];
let q be object;
assume
A15: q in Ar.i;
P[i,Ar.i] by A8,A14;
then ex p1, p2 being Object of C, m being Morphism of p1, p2 st i = [p1,
p2] & <^p1,p2^> <> {} & q = m & m is epi by A15;
hence thesis;
end;
Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being Object of C such that
A16: i = [p1,p2,p3] and
A17: Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A18: [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then
A19: Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13;
A20: [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13;
then
A21: [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
Arrows of C).(p1,p2):] by A19,ZFMISC_1:96;
(the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
(the Arrows of C).(p1,p2):] = {} by Lm1;
then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
Arrows of C).(p1,p3) by A17,A21,FUNCT_2:32;
A22: Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A18;
A23: Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A20;
A24: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
proof
assume
A25: (the Arrows of C).(p1,p3) = {};
assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
then consider k being object such that
A26: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
consider u1, u2 being object such that
A27: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
k = [u1,u2] by A26,ZFMISC_1:def 2;
u1 in <^p2,p3^> & u2 in <^p1,p2^> by A23,A22,A27;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence contradiction by A25;
end;
A28: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A29: rng f c= {|Ar|}.i
proof
let q be object;
assume q in rng f;
then consider x being object such that
A30: x in dom f and
A31: q = f.x by FUNCT_1:def 3;
A32: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A24,FUNCT_2:def 1;
then consider m1, m2 being object such that
A33: m1 in Ar.(p2,p3) and
A34: m2 in Ar.(p1,p2) and
A35: x = [m1,m2] by A30,ZFMISC_1:84;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such
that
A36: [p2,p3] = [q2,q3] and
A37: <^q2,q3^> <> {} and
A38: m1 = qq and
A39: qq is epi by A33;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such
that
A40: [p1,p2] = [r1,r2] and
A41: <^r1,r2^> <> {} and
A42: m2 = rr and
A43: rr is epi by A34;
A44: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3
] = [o1,o3] & <^o1,o3^> <> {} & q = m & m is epi
proof
A45: p2 = q2 by A36,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A40,XTUPLE_0:1;
take r1, q3, mm * rr;
A46: p1 = r1 by A40,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A36,XTUPLE_0:1;
A47: r2 = p2 by A40,XTUPLE_0:1;
hence <^r1,q3^> <> {} by A37,A41,A45,ALTCAT_1:def 2;
A48: p3 = q3 by A36,XTUPLE_0:1;
thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A17,A30,A31,A32,A35
,A38,A42,FUNCT_1:49
.= mm * rr by A36,A37,A41,A47,A46,A48,ALTCAT_1:def 8;
thus thesis by A37,A39,A41,A43,A47,A45,ALTCAT_3:10;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
then q in Ar.[p1,p3] by A44;
hence thesis by A16,A28,MULTOP_1:def 1;
end;
{|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A16,MULTOP_1:def 1;
hence thesis by A24,A29,FUNCT_2:6;
end;
then reconsider Co as BinComp of Ar;
set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
IT is SubCatStr of C
proof
thus the carrier of IT c= the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
thus [:J,J,J:] c= [:I,I,I:];
let i be set;
assume i in [:J,J,J:];
then consider p1, p2, p3 being Object of C such that
A49: i = [p1,p2,p3] and
A50: Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A51: ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):] qua set)
c= (the Comp of C).(p1,p2,p3) by RELAT_1:59;
let q be object;
assume q in (the Comp of IT).i;
then q in (the Comp of C).(p1,p2,p3) by A50,A51;
hence thesis by A49,MULTOP_1:def 1;
end;
then reconsider IT as strict non empty SubCatStr of C;
IT is transitive
proof
let p1, p2, p3 be Object of IT;
assume that
A52: <^p1,p2^> <> {} and
A53: <^p2,p3^> <> {};
consider m2 being object such that
A54: m2 in <^p1,p2^> by A52,XBOOLE_0:def 1;
consider m1 being object such that
A55: m1 in <^p2,p3^> by A53,XBOOLE_0:def 1;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such that
A56: [p2,p3] = [q2,q3] and
A57: <^q2,q3^> <> {} and
m1 = qq and
A58: qq is epi by A55;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such that
A59: [p1,p2] = [r1,r2] and
A60: <^r1,r2^> <> {} and
m2 = rr and
A61: rr is epi by A54;
A62: p2 = q2 by A56,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A59,XTUPLE_0:1;
A63: r2 = p2 by A59,XTUPLE_0:1;
A64: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3]
= [o1,o3] & <^o1,o3^> <> {} & mm * rr = m & m is epi
proof
take r1, q3, mm * rr;
p1 = r1 by A59,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A56,XTUPLE_0:1;
thus <^r1,q3^> <> {} by A57,A60,A63,A62,ALTCAT_1:def 2;
thus mm * rr = mm * rr;
thus thesis by A57,A58,A60,A61,A63,A62,ALTCAT_3:10;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
hence thesis by A64;
end;
then reconsider IT as strict non empty transitive SubCatStr of C;
take IT;
thus the carrier of IT = the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
let o1, o2 be Object of C, m be Morphism of o1, o2;
A65: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & m is epi
proof
assume
A66: m in (the Arrows of IT).(o1,o2);
P[[o1,o2],Ar.[o1,o2]] by A8,A65;
then consider
p1, p2 being Object of C, n being Morphism of p1, p2 such that
A67: [o1,o2] = [p1,p2] and
A68: <^p1,p2^> <> {} & m = n & n is epi by A66;
o1 = p1 & o2 = p2 by A67,XTUPLE_0:1;
hence thesis by A68;
end;
assume
A69: <^o1,o2^> <> {} & m is epi;
P[[o1,o2],Ar.[o1,o2]] by A8,A65;
hence thesis by A69;
end;
uniqueness
proof
let S1, S2 be strict non empty transitive SubCatStr of C such that
A70: the carrier of S1 = the carrier of C and
A71: the Arrows of S1 cc= the Arrows of C and
A72: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & m is epi and
A73: the carrier of S2 = the carrier of C and
A74: the Arrows of S2 cc= the Arrows of C and
A75: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & m is epi;
now
let i be object;
assume
A76: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A77: o1 in the carrier of C & o2 in the carrier of C and
A78: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A77;
thus (the Arrows of S1).i = (the Arrows of S2).i
proof
thus (the Arrows of S1).i c= (the Arrows of S2).i
proof
let n be object such that
A79: n in (the Arrows of S1).i;
(the Arrows of S1).i c= (the Arrows of C).i by A70,A71,A76;
then reconsider m = n as Morphism of o1, o2 by A78,A79;
m in (the Arrows of S1).(o1,o2) by A78,A79;
then <^o1,o2^> <> {} & m is epi by A72;
then m in (the Arrows of S2).(o1,o2) by A75;
hence thesis by A78;
end;
let n be object such that
A80: n in (the Arrows of S2).i;
(the Arrows of S2).i c= (the Arrows of C).i by A73,A74,A76;
then reconsider m = n as Morphism of o1, o2 by A78,A80;
m in (the Arrows of S2).(o1,o2) by A78,A80;
then <^o1,o2^> <> {} & m is epi by A75;
then m in (the Arrows of S1).(o1,o2) by A72;
hence thesis by A78;
end;
end;
hence thesis by A70,A73,ALTCAT_2:26,PBOOLE:3;
end;
end;
registration
let C be category;
cluster AllEpi C -> id-inheriting;
coherence
proof
for o be Object of AllEpi C, o9 be Object of C st o = o9 holds idm o9
in <^o,o^> by Def2;
hence thesis by ALTCAT_2:def 14;
end;
end;
definition
let C be category;
func AllRetr C -> strict non empty transitive SubCatStr of C means
:Def3:
the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C &
for o1, o2 being Object of C, m being Morphism of o1, o2 holds m in (the Arrows
of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction;
existence
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for x being set holds x in D2 iff ex o1, o2 being
Object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^
o2,o1^> <> {} & x = m & m is retraction;
set I = the carrier of C;
A1: for i being object st i in [:I,I:] ex X being object st P[i,X]
proof
let i be object;
assume i in [:I,I:];
then consider o1, o2 being object such that
A2: o1 in I & o2 in I and
A3: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A2;
defpred P[object]
means ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
<^o2,o1^> <> {} & m = $1 & m is retraction;
consider X being set such that
A4: for x being object holds x in X iff x in (the Arrows of C).(o1,o2)
& P[x] from XBOOLE_0:sch 1;
take X,X;
thus X=X;
let x be set;
thus x in X implies ex o1, o2 being Object of C, m being Morphism of o1,
o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is retraction
proof
assume x in X;
then consider m being Morphism of o1, o2 such that
A5: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is retraction by A4;
take o1, o2, m;
thus thesis by A3,A5;
end;
given p1, p2 being Object of C, m being Morphism of p1, p2 such that
A6: i = [p1,p2] and
A7: <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is retraction;
o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
hence thesis by A4,A7;
end;
consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being object st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
(A1);
defpred R[object,object] means
ex p1, p2, p3 being Object of C st $1 = [p1,p2,p3
] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being object st i in [:I,I,I:] ex j being object st R[i,j]
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being object such that
A10: p1 in I & p2 in I & p3 in I and
A11: i = [p1,p2,p3] by MCART_1:68;
reconsider p1, p2, p3 as Object of C by A10;
take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
take p1, p2, p3;
thus i = [p1,p2,p3] by A11;
thus thesis;
end;
consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being object st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
3 (A9 );
A13: Ar cc= the Arrows of C
proof
thus [:I,I:] c= [:the carrier of C,the carrier of C:];
let i be set;
assume
A14: i in [:I,I:];
let q be object;
assume
A15: q in Ar.i;
P[i,Ar.i] by A8,A14;
then ex p1, p2 being Object of C, m being Morphism of p1, p2 st i = [p1,
p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is retraction
by A15;
hence thesis;
end;
Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being Object of C such that
A16: i = [p1,p2,p3] and
A17: Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A18: [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then
A19: Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13;
A20: [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13;
then
A21: [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
Arrows of C).(p1,p2):] by A19,ZFMISC_1:96;
(the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
(the Arrows of C).(p1,p2):] = {} by Lm1;
then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
Arrows of C).(p1,p3) by A17,A21,FUNCT_2:32;
A22: Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A18;
A23: Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A20;
A24: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
proof
assume
A25: (the Arrows of C).(p1,p3) = {};
assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
then consider k being object such that
A26: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
consider u1, u2 being object such that
A27: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
k = [u1,u2] by A26,ZFMISC_1:def 2;
u1 in <^p2,p3^> & u2 in <^p1,p2^> by A23,A22,A27;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence contradiction by A25;
end;
A28: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A29: rng f c= {|Ar|}.i
proof
let q be object;
assume q in rng f;
then consider x being object such that
A30: x in dom f and
A31: q = f.x by FUNCT_1:def 3;
A32: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A24,FUNCT_2:def 1;
then consider m1, m2 being object such that
A33: m1 in Ar.(p2,p3) and
A34: m2 in Ar.(p1,p2) and
A35: x = [m1,m2] by A30,ZFMISC_1:84;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such
that
A36: [p2,p3] = [q2,q3] and
A37: <^q2,q3^> <> {} and
A38: <^q3,q2^> <> {} and
A39: m1 = qq and
A40: qq is retraction by A33;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such
that
A41: [p1,p2] = [r1,r2] and
A42: <^r1,r2^> <> {} and
A43: <^r2,r1^> <> {} and
A44: m2 = rr and
A45: rr is retraction by A34;
A46: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3
] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is retraction
proof
A47: p2 = q2 by A36,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A41,XTUPLE_0:1;
take r1, q3, mm * rr;
A48: p1 = r1 by A41,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A36,XTUPLE_0:1;
A49: r2 = p2 by A41,XTUPLE_0:1;
hence
A50: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A37,A38,A42,A43,A47,
ALTCAT_1:def 2;
A51: p3 = q3 by A36,XTUPLE_0:1;
thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A17,A30,A31,A32,A35
,A39,A44,FUNCT_1:49
.= mm * rr by A36,A37,A42,A49,A48,A51,ALTCAT_1:def 8;
thus thesis by A37,A40,A42,A45,A49,A47,A50,ALTCAT_3:18;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
then q in Ar.[p1,p3] by A46;
hence thesis by A16,A28,MULTOP_1:def 1;
end;
{|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A16,MULTOP_1:def 1;
hence thesis by A24,A29,FUNCT_2:6;
end;
then reconsider Co as BinComp of Ar;
set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
IT is SubCatStr of C
proof
thus the carrier of IT c= the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
thus [:J,J,J:] c= [:I,I,I:];
let i be set;
assume i in [:J,J,J:];
then consider p1, p2, p3 being Object of C such that
A52: i = [p1,p2,p3] and
A53: Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A54: ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set) c=
(the Comp of C).(p1,p2,p3) by RELAT_1:59;
let q be object;
assume q in (the Comp of IT).i;
then q in (the Comp of C).(p1,p2,p3) by A53,A54;
hence thesis by A52,MULTOP_1:def 1;
end;
then reconsider IT as strict non empty SubCatStr of C;
IT is transitive
proof
let p1, p2, p3 be Object of IT;
assume that
A55: <^p1,p2^> <> {} and
A56: <^p2,p3^> <> {};
consider m2 being object such that
A57: m2 in <^p1,p2^> by A55,XBOOLE_0:def 1;
consider m1 being object such that
A58: m1 in <^p2,p3^> by A56,XBOOLE_0:def 1;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such that
A59: [p2,p3] = [q2,q3] and
A60: <^q2,q3^> <> {} and
A61: <^q3,q2^> <> {} and
m1 = qq and
A62: qq is retraction by A58;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such that
A63: [p1,p2] = [r1,r2] and
A64: <^r1,r2^> <> {} and
A65: <^r2,r1^> <> {} and
m2 = rr and
A66: rr is retraction by A57;
A67: p2 = q2 by A59,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A63,XTUPLE_0:1;
A68: r2 = p2 by A63,XTUPLE_0:1;
A69: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3]
= [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is retraction
proof
take r1, q3, mm * rr;
p1 = r1 by A63,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A59,XTUPLE_0:1;
thus
A70: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A60,A61,A64,A65,A68,A67,
ALTCAT_1:def 2;
thus mm * rr = mm * rr;
thus thesis by A60,A62,A64,A66,A68,A67,A70,ALTCAT_3:18;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
hence thesis by A69;
end;
then reconsider IT as strict non empty transitive SubCatStr of C;
take IT;
thus the carrier of IT = the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
let o1, o2 be Object of C, m be Morphism of o1, o2;
A71: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^>
<> {} & m is retraction
proof
assume
A72: m in (the Arrows of IT).(o1,o2);
P[[o1,o2],Ar.[o1,o2]] by A8,A71;
then consider
p1, p2 being Object of C, n being Morphism of p1, p2 such that
A73: [o1,o2] = [p1,p2] and
A74: <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is retraction by A72;
o1 = p1 & o2 = p2 by A73,XTUPLE_0:1;
hence thesis by A74;
end;
assume
A75: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction;
P[[o1,o2],Ar.[o1,o2]] by A8,A71;
hence thesis by A75;
end;
uniqueness
proof
let S1, S2 be strict non empty transitive SubCatStr of C such that
A76: the carrier of S1 = the carrier of C and
A77: the Arrows of S1 cc= the Arrows of C and
A78: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
retraction and
A79: the carrier of S2 = the carrier of C and
A80: the Arrows of S2 cc= the Arrows of C and
A81: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
retraction;
now
let i be object;
assume
A82: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A83: o1 in the carrier of C & o2 in the carrier of C and
A84: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A83;
thus (the Arrows of S1).i = (the Arrows of S2).i
proof
thus (the Arrows of S1).i c= (the Arrows of S2).i
proof
let n be object such that
A85: n in (the Arrows of S1).i;
(the Arrows of S1).i c= (the Arrows of C).i by A76,A77,A82;
then reconsider m = n as Morphism of o1, o2 by A84,A85;
A86: m in (the Arrows of S1).(o1,o2) by A84,A85;
then
A87: m is retraction by A78;
<^o1,o2^> <> {} & <^o2,o1^> <> {} by A78,A86;
then m in (the Arrows of S2).(o1,o2) by A81,A87;
hence thesis by A84;
end;
let n be object such that
A88: n in (the Arrows of S2).i;
(the Arrows of S2).i c= (the Arrows of C).i by A79,A80,A82;
then reconsider m = n as Morphism of o1, o2 by A84,A88;
A89: m in (the Arrows of S2).(o1,o2) by A84,A88;
then
A90: m is retraction by A81;
<^o1,o2^> <> {} & <^o2,o1^> <> {} by A81,A89;
then m in (the Arrows of S1).(o1,o2) by A78,A90;
hence thesis by A84;
end;
end;
hence thesis by A76,A79,ALTCAT_2:26,PBOOLE:3;
end;
end;
registration
let C be category;
cluster AllRetr C -> id-inheriting;
coherence
proof
for o be Object of AllRetr C, o9 be Object of C st o = o9 holds idm o9
in <^o,o^> by Def3;
hence thesis by ALTCAT_2:def 14;
end;
end;
definition
let C be category;
func AllCoretr C -> strict non empty transitive SubCatStr of C means
:Def4:
the carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C &
for o1, o2 being Object of C, m being Morphism of o1, o2 holds m in (the Arrows
of it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction;
existence
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for x being set holds x in D2 iff ex o1, o2 being
Object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^
o2,o1^> <> {} & x = m & m is coretraction;
set I = the carrier of C;
A1: for i being object st i in [:I,I:] ex X being object st P[i,X]
proof
let i be object;
assume i in [:I,I:];
then consider o1, o2 being object such that
A2: o1 in I & o2 in I and
A3: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A2;
defpred P[object] means
ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
<^o2,o1^> <> {} & m = $1 & m is coretraction;
consider X being set such that
A4: for x being object holds x in X iff x in (the Arrows of C).(o1,o2)
& P[x] from XBOOLE_0:sch 1;
take X,X;
thus X=X;
let x be set;
thus x in X implies ex o1, o2 being Object of C, m being Morphism of o1,
o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is
coretraction
proof
assume x in X;
then consider m being Morphism of o1, o2 such that
A5: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is coretraction by A4;
take o1, o2, m;
thus thesis by A3,A5;
end;
given p1, p2 being Object of C, m being Morphism of p1, p2 such that
A6: i = [p1,p2] and
A7: <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is coretraction;
o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
hence thesis by A4,A7;
end;
consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being object st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
(A1);
defpred R[object,object] means
ex p1, p2, p3 being Object of C st $1 = [p1,p2,p3
] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being object st i in [:I,I,I:] ex j being object st R[i,j]
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being object such that
A10: p1 in I & p2 in I & p3 in I and
A11: i = [p1,p2,p3] by MCART_1:68;
reconsider p1, p2, p3 as Object of C by A10;
take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
take p1, p2, p3;
thus i = [p1,p2,p3] by A11;
thus thesis;
end;
consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being object st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
3 (A9 );
A13: Ar cc= the Arrows of C
proof
thus [:I,I:] c= [:the carrier of C,the carrier of C:];
let i be set;
assume
A14: i in [:I,I:];
let q be object;
assume
A15: q in Ar.i;
P[i,Ar.i] by A8,A14;
then ex p1, p2 being Object of C, m being Morphism of p1, p2 st i = [p1,
p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is coretraction
by A15;
hence thesis;
end;
Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being Object of C such that
A16: i = [p1,p2,p3] and
A17: Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A18: [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then
A19: Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13;
A20: [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13;
then
A21: [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
Arrows of C).(p1,p2):] by A19,ZFMISC_1:96;
(the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
(the Arrows of C).(p1,p2):] = {} by Lm1;
then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
Arrows of C).(p1,p3) by A17,A21,FUNCT_2:32;
A22: Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A18;
A23: Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A20;
A24: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
proof
assume
A25: (the Arrows of C).(p1,p3) = {};
assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
then consider k being object such that
A26: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
consider u1, u2 being object such that
A27: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
k = [u1,u2] by A26,ZFMISC_1:def 2;
u1 in <^p2,p3^> & u2 in <^p1,p2^> by A23,A22,A27;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence contradiction by A25;
end;
A28: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A29: rng f c= {|Ar|}.i
proof
let q be object;
assume q in rng f;
then consider x being object such that
A30: x in dom f and
A31: q = f.x by FUNCT_1:def 3;
A32: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A24,FUNCT_2:def 1;
then consider m1, m2 being object such that
A33: m1 in Ar.(p2,p3) and
A34: m2 in Ar.(p1,p2) and
A35: x = [m1,m2] by A30,ZFMISC_1:84;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such
that
A36: [p2,p3] = [q2,q3] and
A37: <^q2,q3^> <> {} and
A38: <^q3,q2^> <> {} and
A39: m1 = qq and
A40: qq is coretraction by A33;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such
that
A41: [p1,p2] = [r1,r2] and
A42: <^r1,r2^> <> {} and
A43: <^r2,r1^> <> {} and
A44: m2 = rr and
A45: rr is coretraction by A34;
A46: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3
] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is coretraction
proof
A47: p2 = q2 by A36,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A41,XTUPLE_0:1;
take r1, q3, mm * rr;
A48: p1 = r1 by A41,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A36,XTUPLE_0:1;
A49: r2 = p2 by A41,XTUPLE_0:1;
hence
A50: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A37,A38,A42,A43,A47,
ALTCAT_1:def 2;
A51: p3 = q3 by A36,XTUPLE_0:1;
thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A17,A30,A31,A32,A35
,A39,A44,FUNCT_1:49
.= mm * rr by A36,A37,A42,A49,A48,A51,ALTCAT_1:def 8;
thus thesis by A37,A40,A42,A45,A49,A47,A50,ALTCAT_3:19;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
then q in Ar.[p1,p3] by A46;
hence thesis by A16,A28,MULTOP_1:def 1;
end;
{|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A16,MULTOP_1:def 1;
hence thesis by A24,A29,FUNCT_2:6;
end;
then reconsider Co as BinComp of Ar;
set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
IT is SubCatStr of C
proof
thus the carrier of IT c= the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
thus [:J,J,J:] c= [:I,I,I:];
let i be set;
assume i in [:J,J,J:];
then consider p1, p2, p3 being Object of C such that
A52: i = [p1,p2,p3] and
A53: Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A54: ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set) c=
(the Comp of C).(p1,p2,p3) by RELAT_1:59;
let q be object;
assume q in (the Comp of IT).i;
then q in (the Comp of C).(p1,p2,p3) by A53,A54;
hence thesis by A52,MULTOP_1:def 1;
end;
then reconsider IT as strict non empty SubCatStr of C;
IT is transitive
proof
let p1, p2, p3 be Object of IT;
assume that
A55: <^p1,p2^> <> {} and
A56: <^p2,p3^> <> {};
consider m2 being object such that
A57: m2 in <^p1,p2^> by A55,XBOOLE_0:def 1;
consider m1 being object such that
A58: m1 in <^p2,p3^> by A56,XBOOLE_0:def 1;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such that
A59: [p2,p3] = [q2,q3] and
A60: <^q2,q3^> <> {} and
A61: <^q3,q2^> <> {} and
m1 = qq and
A62: qq is coretraction by A58;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such that
A63: [p1,p2] = [r1,r2] and
A64: <^r1,r2^> <> {} and
A65: <^r2,r1^> <> {} and
m2 = rr and
A66: rr is coretraction by A57;
A67: p2 = q2 by A59,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A63,XTUPLE_0:1;
A68: r2 = p2 by A63,XTUPLE_0:1;
A69: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3]
= [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is coretraction
proof
take r1, q3, mm * rr;
p1 = r1 by A63,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A59,XTUPLE_0:1;
thus
A70: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A60,A61,A64,A65,A68,A67,
ALTCAT_1:def 2;
thus mm * rr = mm * rr;
thus thesis by A60,A62,A64,A66,A68,A67,A70,ALTCAT_3:19;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
hence thesis by A69;
end;
then reconsider IT as strict non empty transitive SubCatStr of C;
take IT;
thus the carrier of IT = the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
let o1, o2 be Object of C, m be Morphism of o1, o2;
A71: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^>
<> {} & m is coretraction
proof
assume
A72: m in (the Arrows of IT).(o1,o2);
P[[o1,o2],Ar.[o1,o2]] by A8,A71;
then consider
p1, p2 being Object of C, n being Morphism of p1, p2 such that
A73: [o1,o2] = [p1,p2] and
A74: <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is coretraction
by A72;
o1 = p1 & o2 = p2 by A73,XTUPLE_0:1;
hence thesis by A74;
end;
assume
A75: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction;
P[[o1,o2],Ar.[o1,o2]] by A8,A71;
hence thesis by A75;
end;
uniqueness
proof
let S1, S2 be strict non empty transitive SubCatStr of C such that
A76: the carrier of S1 = the carrier of C and
A77: the Arrows of S1 cc= the Arrows of C and
A78: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
coretraction and
A79: the carrier of S2 = the carrier of C and
A80: the Arrows of S2 cc= the Arrows of C and
A81: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is
coretraction;
now
let i be object;
assume
A82: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A83: o1 in the carrier of C & o2 in the carrier of C and
A84: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A83;
thus (the Arrows of S1).i = (the Arrows of S2).i
proof
thus (the Arrows of S1).i c= (the Arrows of S2).i
proof
let n be object such that
A85: n in (the Arrows of S1).i;
(the Arrows of S1).i c= (the Arrows of C).i by A76,A77,A82;
then reconsider m = n as Morphism of o1, o2 by A84,A85;
A86: m in (the Arrows of S1).(o1,o2) by A84,A85;
then
A87: m is coretraction by A78;
<^o1,o2^> <> {} & <^o2,o1^> <> {} by A78,A86;
then m in (the Arrows of S2).(o1,o2) by A81,A87;
hence thesis by A84;
end;
let n be object such that
A88: n in (the Arrows of S2).i;
(the Arrows of S2).i c= (the Arrows of C).i by A79,A80,A82;
then reconsider m = n as Morphism of o1, o2 by A84,A88;
A89: m in (the Arrows of S2).(o1,o2) by A84,A88;
then
A90: m is coretraction by A81;
<^o1,o2^> <> {} & <^o2,o1^> <> {} by A81,A89;
then m in (the Arrows of S1).(o1,o2) by A78,A90;
hence thesis by A84;
end;
end;
hence thesis by A76,A79,ALTCAT_2:26,PBOOLE:3;
end;
end;
registration
let C be category;
cluster AllCoretr C -> id-inheriting;
coherence
proof
for o be Object of AllCoretr C, o9 be Object of C st o = o9 holds idm
o9 in <^o,o^> by Def4;
hence thesis by ALTCAT_2:def 14;
end;
end;
definition
let C be category;
func AllIso C -> strict non empty transitive SubCatStr of C means
:Def5:
the
carrier of it = the carrier of C & the Arrows of it cc= the Arrows of C & for
o1, o2 being Object of C, m being Morphism of o1, o2 holds m in (the Arrows of
it).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso;
existence
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for x being set holds x in D2 iff ex o1, o2 being
Object of C, m being Morphism of o1, o2 st $1 = [o1,o2] & <^o1,o2^> <> {} & <^
o2,o1^> <> {} & x = m & m is iso;
set I = the carrier of C;
A1: for i being object st i in [:I,I:] ex X being object st P[i,X]
proof
let i be object;
assume i in [:I,I:];
then consider o1, o2 being object such that
A2: o1 in I & o2 in I and
A3: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A2;
defpred P[object] means
ex m being Morphism of o1, o2 st <^o1,o2^> <> {} &
<^o2,o1^> <> {} & m = $1 & m is iso;
consider X being set such that
A4: for x being object holds x in X iff x in (the Arrows of C).(o1,o2)
& P[x] from XBOOLE_0:sch 1;
take X,X;
thus X = X;
let x be set;
thus x in X implies ex o1, o2 being Object of C, m being Morphism of o1,
o2 st i = [o1,o2] & <^o1,o2^> <> {} & <^o2,o1^> <> {} & x = m & m is iso
proof
assume x in X;
then consider m being Morphism of o1, o2 such that
A5: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m = x & m is iso by A4;
take o1, o2, m;
thus thesis by A3,A5;
end;
given p1, p2 being Object of C, m being Morphism of p1, p2 such that
A6: i = [p1,p2] and
A7: <^p1,p2^> <> {} & <^p2,p1^> <> {} & x = m & m is iso;
o1 = p1 & o2 = p2 by A3,A6,XTUPLE_0:1;
hence thesis by A4,A7;
end;
consider Ar being ManySortedSet of [:I,I:] such that
A8: for i being object st i in [:I,I:] holds P[i,Ar.i] from PBOOLE:sch 3
(A1);
defpred R[object,object] means
ex p1, p2, p3 being Object of C st $1 = [p1,p2,p3
] & $2 = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
A9: for i being object st i in [:I,I,I:] ex j being object st R[i,j]
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being object such that
A10: p1 in I & p2 in I & p3 in I and
A11: i = [p1,p2,p3] by MCART_1:68;
reconsider p1, p2, p3 as Object of C by A10;
take ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set);
take p1, p2, p3;
thus i = [p1,p2,p3] by A11;
thus thesis;
end;
consider Co being ManySortedSet of [:I,I,I:] such that
A12: for i being object st i in [:I,I,I:] holds R[i,Co.i] from PBOOLE:sch
3 (A9 );
A13: Ar cc= the Arrows of C
proof
thus [:I,I:] c= [:the carrier of C,the carrier of C:];
let i be set;
assume
A14: i in [:I,I:];
let q be object;
assume
A15: q in Ar.i;
P[i,Ar.i] by A8,A14;
then ex p1, p2 being Object of C, m being Morphism of p1, p2 st i = [p1,
p2] & <^p1,p2^> <> {} & <^p2,p1^> <> {} & q = m & m is iso
by A15;
hence thesis;
end;
Co is ManySortedFunction of {|Ar,Ar|}, {|Ar|}
proof
let i be object;
assume i in [:I,I,I:];
then consider p1, p2, p3 being Object of C such that
A16: i = [p1,p2,p3] and
A17: Co.i = ((the Comp of C).(p1,p2,p3))| ([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A18: [p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then
A19: Ar.[p1,p2] c= (the Arrows of C).(p1,p2) by A13;
A20: [p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then Ar.[p2,p3] c= (the Arrows of C).(p2,p3) by A13;
then
A21: [:Ar.(p2,p3),Ar.(p1,p2):] c= [:(the Arrows of C).(p2,p3),(the
Arrows of C).(p1,p2):] by A19,ZFMISC_1:96;
(the Arrows of C).(p1,p3) = {} implies [:(the Arrows of C).(p2,p3),
(the Arrows of C).(p1,p2):] = {} by Lm1;
then reconsider f = Co.i as Function of [:Ar.(p2,p3),Ar.(p1,p2):], (the
Arrows of C).(p1,p3) by A17,A21,FUNCT_2:32;
A22: Ar.[p1,p2] c= (the Arrows of C).[p1,p2] by A13,A18;
A23: Ar.[p2,p3] c= (the Arrows of C).[p2,p3] by A13,A20;
A24: (the Arrows of C).(p1,p3) = {} implies [:Ar.(p2,p3),Ar.(p1,p2):] = {}
proof
assume
A25: (the Arrows of C).(p1,p3) = {};
assume [:Ar.(p2,p3),Ar.(p1,p2):] <> {};
then consider k being object such that
A26: k in [:Ar.(p2,p3),Ar.(p1,p2):] by XBOOLE_0:def 1;
consider u1, u2 being object such that
A27: u1 in Ar.(p2,p3) & u2 in Ar.(p1,p2) and
k = [u1,u2] by A26,ZFMISC_1:def 2;
u1 in <^p2,p3^> & u2 in <^p1,p2^> by A23,A22,A27;
then <^p1,p3^> <> {} by ALTCAT_1:def 2;
hence contradiction by A25;
end;
A28: {|Ar|}.(p1,p2,p3) = Ar.(p1,p3) by ALTCAT_1:def 3;
A29: rng f c= {|Ar|}.i
proof
let q be object;
assume q in rng f;
then consider x being object such that
A30: x in dom f and
A31: q = f.x by FUNCT_1:def 3;
A32: dom f = [:Ar.(p2,p3),Ar.(p1,p2):] by A24,FUNCT_2:def 1;
then consider m1, m2 being object such that
A33: m1 in Ar.(p2,p3) and
A34: m2 in Ar.(p1,p2) and
A35: x = [m1,m2] by A30,ZFMISC_1:84;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such
that
A36: [p2,p3] = [q2,q3] and
A37: <^q2,q3^> <> {} and
A38: <^q3,q2^> <> {} and
A39: m1 = qq and
A40: qq is iso by A33;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such
that
A41: [p1,p2] = [r1,r2] and
A42: <^r1,r2^> <> {} and
A43: <^r2,r1^> <> {} and
A44: m2 = rr and
A45: rr is iso by A34;
A46: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3
] = [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & q = m & m is iso
proof
A47: p2 = q2 by A36,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A41,XTUPLE_0:1;
take r1, q3, mm * rr;
A48: p1 = r1 by A41,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A36,XTUPLE_0:1;
A49: r2 = p2 by A41,XTUPLE_0:1;
hence
A50: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A37,A38,A42,A43,A47,
ALTCAT_1:def 2;
A51: p3 = q3 by A36,XTUPLE_0:1;
thus q = (the Comp of C).(p1,p2,p3).(mm,rr) by A17,A30,A31,A32,A35
,A39,A44,FUNCT_1:49
.= mm * rr by A36,A37,A42,A49,A48,A51,ALTCAT_1:def 8;
thus thesis by A37,A40,A42,A45,A49,A47,A50,ALTCAT_3:7;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
then q in Ar.[p1,p3] by A46;
hence thesis by A16,A28,MULTOP_1:def 1;
end;
{|Ar,Ar|}.(p1,p2,p3) = [:Ar.(p2,p3),Ar.(p1,p2):] by ALTCAT_1:def 4;
then [:Ar.(p2,p3),Ar.(p1,p2):] = {|Ar,Ar|}.i by A16,MULTOP_1:def 1;
hence thesis by A24,A29,FUNCT_2:6;
end;
then reconsider Co as BinComp of Ar;
set IT = AltCatStr (#I, Ar, Co#), J = the carrier of IT;
IT is SubCatStr of C
proof
thus the carrier of IT c= the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
thus [:J,J,J:] c= [:I,I,I:];
let i be set;
assume i in [:J,J,J:];
then consider p1, p2, p3 being Object of C such that
A52: i = [p1,p2,p3] and
A53: Co.i = ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):]
qua set) by A12;
A54: ((the Comp of C).(p1,p2,p3))|([:Ar.(p2,p3),Ar.(p1,p2):] qua set) c=
(the Comp of C).(p1,p2,p3) by RELAT_1:59;
let q be object;
assume q in (the Comp of IT).i;
then q in (the Comp of C).(p1,p2,p3) by A53,A54;
hence thesis by A52,MULTOP_1:def 1;
end;
then reconsider IT as strict non empty SubCatStr of C;
IT is transitive
proof
let p1, p2, p3 be Object of IT;
assume that
A55: <^p1,p2^> <> {} and
A56: <^p2,p3^> <> {};
consider m2 being object such that
A57: m2 in <^p1,p2^> by A55,XBOOLE_0:def 1;
consider m1 being object such that
A58: m1 in <^p2,p3^> by A56,XBOOLE_0:def 1;
[p2,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p2,p3],Ar.[p2,p3]] by A8;
then consider
q2, q3 being Object of C, qq being Morphism of q2, q3 such that
A59: [p2,p3] = [q2,q3] and
A60: <^q2,q3^> <> {} and
A61: <^q3,q2^> <> {} and
m1 = qq and
A62: qq is iso by A58;
[p1,p2] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p2],Ar.[p1,p2]] by A8;
then consider
r1, r2 being Object of C, rr being Morphism of r1, r2 such that
A63: [p1,p2] = [r1,r2] and
A64: <^r1,r2^> <> {} and
A65: <^r2,r1^> <> {} and
m2 = rr and
A66: rr is iso by A57;
A67: p2 = q2 by A59,XTUPLE_0:1;
then reconsider mm = qq as Morphism of r2, q3 by A63,XTUPLE_0:1;
A68: r2 = p2 by A63,XTUPLE_0:1;
A69: ex o1, o3 being Object of C, m being Morphism of o1, o3 st [p1,p3]
= [o1,o3] & <^o1,o3^> <> {} & <^o3,o1^> <> {} & mm * rr = m & m is iso
proof
take r1, q3, mm * rr;
p1 = r1 by A63,XTUPLE_0:1;
hence [p1,p3] = [r1,q3] by A59,XTUPLE_0:1;
thus
A70: <^r1,q3^> <> {} & <^q3,r1^> <> {} by A60,A61,A64,A65,A68,A67,
ALTCAT_1:def 2;
thus mm * rr = mm * rr;
thus thesis by A60,A62,A64,A66,A68,A67,A70,ALTCAT_3:7;
end;
[p1,p3] in [:I,I:] by ZFMISC_1:def 2;
then P[[p1,p3],Ar.[p1,p3]] by A8;
hence thesis by A69;
end;
then reconsider IT as strict non empty transitive SubCatStr of C;
take IT;
thus the carrier of IT = the carrier of C;
thus the Arrows of IT cc= the Arrows of C by A13;
let o1, o2 be Object of C, m be Morphism of o1, o2;
A71: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
thus m in (the Arrows of IT).(o1,o2) implies <^o1,o2^> <> {} & <^o2,o1^>
<> {} & m is iso
proof
assume
A72: m in (the Arrows of IT).(o1,o2);
P[[o1,o2],Ar.[o1,o2]] by A8,A71;
then consider
p1, p2 being Object of C, n being Morphism of p1, p2 such that
A73: [o1,o2] = [p1,p2] and
A74: <^p1,p2^> <> {} & <^p2,p1^> <> {} & m = n & n is iso by A72;
o1 = p1 & o2 = p2 by A73,XTUPLE_0:1;
hence thesis by A74;
end;
assume
A75: <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso;
P[[o1,o2],Ar.[o1,o2]] by A8,A71;
hence thesis by A75;
end;
uniqueness
proof
let S1, S2 be strict non empty transitive SubCatStr of C such that
A76: the carrier of S1 = the carrier of C and
A77: the Arrows of S1 cc= the Arrows of C and
A78: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S1).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso
and
A79: the carrier of S2 = the carrier of C and
A80: the Arrows of S2 cc= the Arrows of C and
A81: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m
in (the Arrows of S2).(o1,o2) iff <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso;
now
let i be object;
assume
A82: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A83: o1 in the carrier of C & o2 in the carrier of C and
A84: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A83;
thus (the Arrows of S1).i = (the Arrows of S2).i
proof
thus (the Arrows of S1).i c= (the Arrows of S2).i
proof
let n be object such that
A85: n in (the Arrows of S1).i;
(the Arrows of S1).i c= (the Arrows of C).i by A76,A77,A82;
then reconsider m = n as Morphism of o1, o2 by A84,A85;
A86: m in (the Arrows of S1).(o1,o2) by A84,A85;
then
A87: m is iso by A78;
<^o1,o2^> <> {} & <^o2,o1^> <> {} by A78,A86;
then m in (the Arrows of S2).(o1,o2) by A81,A87;
hence thesis by A84;
end;
let n be object such that
A88: n in (the Arrows of S2).i;
(the Arrows of S2).i c= (the Arrows of C).i by A79,A80,A82;
then reconsider m = n as Morphism of o1, o2 by A84,A88;
A89: m in (the Arrows of S2).(o1,o2) by A84,A88;
then
A90: m is iso by A81;
<^o1,o2^> <> {} & <^o2,o1^> <> {} by A81,A89;
then m in (the Arrows of S1).(o1,o2) by A78,A90;
hence thesis by A84;
end;
end;
hence thesis by A76,A79,ALTCAT_2:26,PBOOLE:3;
end;
end;
registration
let C be category;
cluster AllIso C -> id-inheriting;
coherence
proof
for o be Object of AllIso C, o9 be Object of C st o = o9 holds idm o9
in <^o,o^> by Def5;
hence thesis by ALTCAT_2:def 14;
end;
end;
theorem Th41:
AllIso C is non empty subcategory of AllRetr C
proof
the carrier of AllIso C = the carrier of C by Def5;
then
A1: the carrier of AllIso C c= the carrier of AllRetr C by Def3;
the Arrows of AllIso C cc= the Arrows of AllRetr C
proof
thus [:the carrier of AllIso C,the carrier of AllIso C:] c= [:the carrier
of AllRetr C,the carrier of AllRetr C:] by A1,ZFMISC_1:96;
let i be set;
assume
A2: i in [:the carrier of AllIso C,the carrier of AllIso C:];
then consider o1, o2 being object such that
A3: o1 in the carrier of AllIso C & o2 in the carrier of AllIso C and
A4: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A3,Def5;
let m be object;
assume
A5: m in (the Arrows of AllIso C).i;
the Arrows of AllIso C cc= the Arrows of C by Def5;
then
(the Arrows of AllIso C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2,A4;
then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
m in (the Arrows of AllIso C).(o1,o2) by A4,A5;
then m1 is iso by Def5;
then
A6: m1 is retraction by ALTCAT_3:5;
m1 in (the Arrows of AllIso C).(o1,o2) by A4,A5;
then <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def5;
then m in (the Arrows of AllRetr C).(o1,o2) by A6,Def3;
hence thesis by A4;
end;
then reconsider
A = AllIso C as with_units non empty SubCatStr of AllRetr C by A1,ALTCAT_2:24
;
now
let o be Object of A, o1 be Object of AllRetr C such that
A7: o = o1;
reconsider oo = o as Object of C by Def5;
idm o = idm oo by ALTCAT_2:34
.= idm o1 by A7,ALTCAT_2:34;
hence idm o1 in <^o,o^>;
end;
hence thesis by ALTCAT_2:def 14;
end;
theorem Th42:
AllIso C is non empty subcategory of AllCoretr C
proof
the carrier of AllIso C = the carrier of C by Def5;
then
A1: the carrier of AllIso C c= the carrier of AllCoretr C by Def4;
the Arrows of AllIso C cc= the Arrows of AllCoretr C
proof
thus [:the carrier of AllIso C,the carrier of AllIso C:] c= [:the carrier
of AllCoretr C,the carrier of AllCoretr C:] by A1,ZFMISC_1:96;
let i be set;
assume
A2: i in [:the carrier of AllIso C,the carrier of AllIso C:];
then consider o1, o2 being object such that
A3: o1 in the carrier of AllIso C & o2 in the carrier of AllIso C and
A4: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A3,Def5;
let m be object;
assume
A5: m in (the Arrows of AllIso C).i;
the Arrows of AllIso C cc= the Arrows of C by Def5;
then
(the Arrows of AllIso C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2,A4;
then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
m in (the Arrows of AllIso C).(o1,o2) by A4,A5;
then m1 is iso by Def5;
then
A6: m1 is coretraction by ALTCAT_3:5;
m1 in (the Arrows of AllIso C).(o1,o2) by A4,A5;
then <^o1,o2^> <> {} & <^o2,o1^> <> {} by Def5;
then m in (the Arrows of AllCoretr C).(o1,o2) by A6,Def4;
hence thesis by A4;
end;
then reconsider
A = AllIso C as with_units non empty SubCatStr of AllCoretr C
by A1,ALTCAT_2:24;
now
let o be Object of A, o1 be Object of AllCoretr C such that
A7: o = o1;
reconsider oo = o as Object of C by Def5;
idm o = idm oo by ALTCAT_2:34
.= idm o1 by A7,ALTCAT_2:34;
hence idm o1 in <^o,o^>;
end;
hence thesis by ALTCAT_2:def 14;
end;
theorem Th43:
AllCoretr C is non empty subcategory of AllMono C
proof
the carrier of AllCoretr C = the carrier of C by Def4;
then
A1: the carrier of AllCoretr C c= the carrier of AllMono C by Def1;
the Arrows of AllCoretr C cc= the Arrows of AllMono C
proof
thus [:the carrier of AllCoretr C,the carrier of AllCoretr C:] c= [:the
carrier of AllMono C,the carrier of AllMono C:] by A1,ZFMISC_1:96;
let i be set;
assume
A2: i in [:the carrier of AllCoretr C,the carrier of AllCoretr C:];
then consider o1, o2 being object such that
A3: o1 in the carrier of AllCoretr C & o2 in the carrier of AllCoretr C and
A4: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A3,Def4;
let m be object;
assume
A5: m in (the Arrows of AllCoretr C).i;
the Arrows of AllCoretr C cc= the Arrows of C by Def4;
then (the Arrows of AllCoretr C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2
,A4;
then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
m in (the Arrows of AllCoretr C).(o1,o2) by A4,A5;
then
A6: m1 is coretraction by Def4;
A7: m1 in (the Arrows of AllCoretr C).(o1,o2) by A4,A5;
then
A8: <^o1,o2^> <> {} by Def4;
<^o2,o1^> <> {} by A7,Def4;
then m1 is mono by A8,A6,ALTCAT_3:16;
then m in (the Arrows of AllMono C).(o1,o2) by A8,Def1;
hence thesis by A4;
end;
then reconsider
A = AllCoretr C as with_units non empty SubCatStr of AllMono C
by A1,ALTCAT_2:24;
now
let o be Object of A, o1 be Object of AllMono C such that
A9: o = o1;
reconsider oo = o as Object of C by Def4;
idm o = idm oo by ALTCAT_2:34
.= idm o1 by A9,ALTCAT_2:34;
hence idm o1 in <^o,o^>;
end;
hence thesis by ALTCAT_2:def 14;
end;
theorem Th44:
AllRetr C is non empty subcategory of AllEpi C
proof
the carrier of AllRetr C = the carrier of C by Def3;
then
A1: the carrier of AllRetr C c= the carrier of AllEpi C by Def2;
the Arrows of AllRetr C cc= the Arrows of AllEpi C
proof
thus [:the carrier of AllRetr C,the carrier of AllRetr C:] c= [:the
carrier of AllEpi C,the carrier of AllEpi C:] by A1,ZFMISC_1:96;
let i be set;
assume
A2: i in [:the carrier of AllRetr C,the carrier of AllRetr C:];
then consider o1, o2 being object such that
A3: o1 in the carrier of AllRetr C & o2 in the carrier of AllRetr C and
A4: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A3,Def3;
let m be object;
assume
A5: m in (the Arrows of AllRetr C).i;
the Arrows of AllRetr C cc= the Arrows of C by Def3;
then (the Arrows of AllRetr C).[o1,o2] c= (the Arrows of C).(o1,o2) by A2
,A4;
then reconsider m1 = m as Morphism of o1, o2 by A4,A5;
m in (the Arrows of AllRetr C).(o1,o2) by A4,A5;
then
A6: m1 is retraction by Def3;
A7: m1 in (the Arrows of AllRetr C).(o1,o2) by A4,A5;
then
A8: <^o1,o2^> <> {} by Def3;
<^o2,o1^> <> {} by A7,Def3;
then m1 is epi by A8,A6,ALTCAT_3:15;
then m in (the Arrows of AllEpi C).(o1,o2) by A8,Def2;
hence thesis by A4;
end;
then reconsider
A = AllRetr C as with_units non empty SubCatStr of AllEpi C by A1,ALTCAT_2:24
;
now
let o be Object of A, o1 be Object of AllEpi C such that
A9: o = o1;
reconsider oo = o as Object of C by Def3;
idm o = idm oo by ALTCAT_2:34
.= idm o1 by A9,ALTCAT_2:34;
hence idm o1 in <^o,o^>;
end;
hence thesis by ALTCAT_2:def 14;
end;
theorem
(for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
mono ) implies the AltCatStr of C = AllMono C
proof
assume
A1: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is mono;
A2: the carrier of AllMono C = the carrier of the AltCatStr of C by Def1;
A3: the Arrows of AllMono C cc= the Arrows of C by Def1;
now
let i be object;
assume
A4: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A5;
thus (the Arrows of AllMono C).i = (the Arrows of C).i
proof
thus (the Arrows of AllMono C).i c= (the Arrows of C).i by A2,A3,A4;
let n be object;
assume
A7: n in (the Arrows of C).i;
then reconsider n1 = n as Morphism of o1, o2 by A6;
n1 is mono by A1;
then n in (the Arrows of AllMono C).(o1,o2) by A6,A7,Def1;
hence thesis by A6;
end;
end;
hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;
theorem
(for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
epi ) implies the AltCatStr of C = AllEpi C
proof
assume
A1: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is epi;
A2: the carrier of AllEpi C = the carrier of the AltCatStr of C by Def2;
A3: the Arrows of AllEpi C cc= the Arrows of C by Def2;
now
let i be object;
assume
A4: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A5;
thus (the Arrows of AllEpi C).i = (the Arrows of C).i
proof
thus (the Arrows of AllEpi C).i c= (the Arrows of C).i by A2,A3,A4;
let n be object;
assume
A7: n in (the Arrows of C).i;
then reconsider n1 = n as Morphism of o1, o2 by A6;
n1 is epi by A1;
then n in (the Arrows of AllEpi C).(o1,o2) by A6,A7,Def2;
hence thesis by A6;
end;
end;
hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;
theorem
(for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
retraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllRetr C
proof
assume
A1: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
retraction & <^o2,o1^> <> {};
A2: the carrier of AllRetr C = the carrier of the AltCatStr of C by Def3;
A3: the Arrows of AllRetr C cc= the Arrows of C by Def3;
now
let i be object;
assume
A4: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A5;
thus (the Arrows of AllRetr C).i = (the Arrows of C).i
proof
thus (the Arrows of AllRetr C).i c= (the Arrows of C).i by A2,A3,A4;
let n be object;
assume
A7: n in (the Arrows of C).i;
then reconsider n1 = n as Morphism of o1, o2 by A6;
<^o2,o1^> <> {} & n1 is retraction by A1;
then n in (the Arrows of AllRetr C).(o1,o2) by A6,A7,Def3;
hence thesis by A6;
end;
end;
hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;
theorem
(for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
coretraction & <^o2,o1^> <> {}) implies the AltCatStr of C = AllCoretr C
proof
assume
A1: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
coretraction & <^o2,o1^> <> {};
A2: the carrier of AllCoretr C = the carrier of the AltCatStr of C by Def4;
A3: the Arrows of AllCoretr C cc= the Arrows of C by Def4;
now
let i be object;
assume
A4: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A5;
thus (the Arrows of AllCoretr C).i = (the Arrows of C).i
proof
thus (the Arrows of AllCoretr C).i c= (the Arrows of C).i by A2,A3,A4;
let n be object;
assume
A7: n in (the Arrows of C).i;
then reconsider n1 = n as Morphism of o1, o2 by A6;
<^o2,o1^> <> {} & n1 is coretraction by A1;
then n in (the Arrows of AllCoretr C).(o1,o2) by A6,A7,Def4;
hence thesis by A6;
end;
end;
hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;
theorem
(for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
iso & <^o2,o1^> <> {}) implies the AltCatStr of C = AllIso C
proof
assume
A1: for o1, o2 being Object of C, m being Morphism of o1, o2 holds m is
iso & <^o2,o1^> <> {};
A2: the carrier of AllIso C = the carrier of the AltCatStr of C by Def5;
A3: the Arrows of AllIso C cc= the Arrows of C by Def5;
now
let i be object;
assume
A4: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A5: o1 in the carrier of C & o2 in the carrier of C and
A6: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of C by A5;
thus (the Arrows of AllIso C).i = (the Arrows of C).i
proof
thus (the Arrows of AllIso C).i c= (the Arrows of C).i by A2,A3,A4;
let n be object;
assume
A7: n in (the Arrows of C).i;
then reconsider n1 = n as Morphism of o1, o2 by A6;
<^o2,o1^> <> {} & n1 is iso by A1;
then n in (the Arrows of AllIso C).(o1,o2) by A6,A7,Def5;
hence thesis by A6;
end;
end;
hence thesis by A2,ALTCAT_2:25,PBOOLE:3;
end;
theorem Th50:
for o1, o2 being Object of AllMono C for m being Morphism of o1,
o2 st <^o1,o2^> <> {} holds m is mono
proof
let o1, o2 be Object of AllMono C, m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {};
reconsider p1 = o1, p2 = o2 as Object of C by Def1;
reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:33;
p is mono by A1,Def1;
hence thesis by A1,Th37;
end;
theorem Th51:
for o1, o2 being Object of AllEpi C for m being Morphism of o1,
o2 st <^o1,o2^> <> {} holds m is epi
proof
let o1, o2 be Object of AllEpi C, m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {};
reconsider p1 = o1, p2 = o2 as Object of C by Def2;
reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:33;
p is epi by A1,Def2;
hence thesis by A1,Th37;
end;
theorem Th52:
for o1, o2 being Object of AllIso C for m being Morphism of o1,
o2 st <^o1,o2^> <> {} holds m is iso & m" in <^o2,o1^>
proof
let o1, o2 be Object of AllIso C, m be Morphism of o1, o2 such that
A1: <^o1,o2^> <> {};
reconsider p1 = o1, p2 = o2 as Object of C by Def5;
reconsider p = m as Morphism of p1, p2 by A1,ALTCAT_2:33;
p in (the Arrows of AllIso C).(o1,o2) by A1;
then
A2: <^p1,p2^> <> {} & <^p2,p1^> <> {} by Def5;
A3: p is iso by A1,Def5;
then
A4: p" is iso by A2,Th3;
then
A5: p" in (the Arrows of AllIso C).(p2,p1) by A2,Def5;
reconsider m1 = p" as Morphism of o2, o1 by A2,A4,Def5;
A6: m is retraction
proof
take m1;
thus m * m1 = p * p" by A1,A5,ALTCAT_2:32
.= idm p2 by A3
.= idm o2 by ALTCAT_2:34;
end;
A7: m is coretraction
proof
take m1;
thus m1 * m = p" * p by A1,A5,ALTCAT_2:32
.= idm p1 by A3
.= idm o1 by ALTCAT_2:34;
end;
p" in <^o2,o1^> by A2,A4,Def5;
hence m is iso by A1,A6,A7,ALTCAT_3:6;
thus thesis by A5;
end;
theorem
AllMono AllMono C = AllMono C
proof
A1: the carrier of AllMono AllMono C = the carrier of AllMono C & the
carrier of AllMono C = the carrier of C by Def1;
A2: the Arrows of AllMono AllMono C cc= the Arrows of AllMono C by Def1;
now
let i be object;
assume
A3: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A4: o1 in the carrier of C & o2 in the carrier of C and
A5: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of AllMono C by A4,Def1;
thus (the Arrows of AllMono AllMono C).i = (the Arrows of AllMono C).i
proof
thus (the Arrows of AllMono AllMono C).i c= (the Arrows of AllMono C).i
by A1,A2,A3;
let n be object;
assume
A6: n in (the Arrows of AllMono C).i;
then reconsider n1 = n as Morphism of o1, o2 by A5;
n1 is mono by A5,A6,Th50;
then n in (the Arrows of AllMono AllMono C).(o1,o2) by A5,A6,Def1;
hence thesis by A5;
end;
end;
hence thesis by A1,ALTCAT_2:25,PBOOLE:3;
end;
theorem
AllEpi AllEpi C = AllEpi C
proof
A1: the carrier of AllEpi AllEpi C = the carrier of AllEpi C & the carrier
of AllEpi C = the carrier of C by Def2;
A2: the Arrows of AllEpi AllEpi C cc= the Arrows of AllEpi C by Def2;
now
let i be object;
assume
A3: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A4: o1 in the carrier of C & o2 in the carrier of C and
A5: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of AllEpi C by A4,Def2;
thus (the Arrows of AllEpi AllEpi C).i = (the Arrows of AllEpi C).i
proof
thus (the Arrows of AllEpi AllEpi C).i c= (the Arrows of AllEpi C).i by
A1,A2,A3;
let n be object;
assume
A6: n in (the Arrows of AllEpi C).i;
then reconsider n1 = n as Morphism of o1, o2 by A5;
n1 is epi by A5,A6,Th51;
then n in (the Arrows of AllEpi AllEpi C).(o1,o2) by A5,A6,Def2;
hence thesis by A5;
end;
end;
hence thesis by A1,ALTCAT_2:25,PBOOLE:3;
end;
theorem
AllIso AllIso C = AllIso C
proof
A1: the carrier of AllIso AllIso C = the carrier of AllIso C & the carrier
of AllIso C = the carrier of C by Def5;
A2: the Arrows of AllIso AllIso C cc= the Arrows of AllIso C by Def5;
now
let i be object;
assume
A3: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A4: o1 in the carrier of C & o2 in the carrier of C and
A5: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of AllIso C by A4,Def5;
thus (the Arrows of AllIso AllIso C).i = (the Arrows of AllIso C).i
proof
thus (the Arrows of AllIso AllIso C).i c= (the Arrows of AllIso C).i by
A1,A2,A3;
let n be object;
assume
A6: n in (the Arrows of AllIso C).i;
then reconsider n1 = n as Morphism of o1, o2 by A5;
n1" in <^o2,o1^> & n1 is iso by A5,A6,Th52;
then n in (the Arrows of AllIso AllIso C).(o1,o2) by A5,A6,Def5;
hence thesis by A5;
end;
end;
hence thesis by A1,ALTCAT_2:25,PBOOLE:3;
end;
theorem
AllIso AllMono C = AllIso C
proof
A1: AllIso AllMono C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllMono C = the carrier of AllMono C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllMono C = the carrier of C by Def1;
AllIso C is non empty subcategory of AllCoretr C & AllCoretr C is non
empty subcategory of AllMono C by Th42,Th43;
then
A5: AllIso C is non empty subcategory of AllMono C by Th36;
A6: now
let i be object;
assume
A7: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of AllMono C by A8,Def1;
thus (the Arrows of AllIso AllMono C).i = (the Arrows of AllIso C).i
proof
thus (the Arrows of AllIso AllMono C).i c= (the Arrows of AllIso C).i
proof
reconsider r1 = o1, r2 = o2 as Object of C by Def1;
reconsider q1 = o1, q2 = o2 as Object of AllIso AllMono C by Def5;
A10: <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
let n be object such that
A11: n in (the Arrows of AllIso AllMono C).i;
n in <^q1,q2^> by A9,A11;
then
A12: <^o2,o1^> <> {} by A10,Th52;
then
A13: <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14: <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15: <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
<^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
then <^q1,q2^> c= <^r1,r2^> by A14;
then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
n in (the Arrows of AllIso AllMono C).(q1,q2) by A9,A11;
then n2 is iso by Def5;
then n1 is iso by A9,A11,A14,A12,Th40;
then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
hence thesis by A9;
end;
reconsider p1 = o1, p2 = o2 as Object of AllIso C by A4,Def5;
A16: <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
let n be object such that
A17: n in (the Arrows of AllIso C).i;
reconsider n2 = n as Morphism of p1, p2 by A9,A17;
the Arrows of AllIso C cc= the Arrows of AllMono C by A5,ALTCAT_2:def 11;
then
A18: (the Arrows of AllIso C).i c= (the Arrows of AllMono C).i by A3,A7;
then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19: n2" in <^p2,p1^> by A9,A17,Th52;
n2 is iso by A9,A17,Th52;
then n1 is iso by A5,A9,A17,A19,Th40;
then
n in (the Arrows of AllIso AllMono C).(o1,o2) by A9,A17,A18,A19,A16,Def5;
hence thesis by A9;
end;
end;
then the Arrows of AllIso AllMono C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
then AllIso AllMono C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;
theorem
AllIso AllEpi C = AllIso C
proof
A1: AllIso AllEpi C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllEpi C = the carrier of AllEpi C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllEpi C = the carrier of C by Def2;
AllIso C is non empty subcategory of AllRetr C & AllRetr C is non empty
subcategory of AllEpi C by Th41,Th44;
then
A5: AllIso C is non empty subcategory of AllEpi C by Th36;
A6: now
let i be object;
assume
A7: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of AllEpi C by A8,Def2;
thus (the Arrows of AllIso AllEpi C).i = (the Arrows of AllIso C).i
proof
thus (the Arrows of AllIso AllEpi C).i c= (the Arrows of AllIso C).i
proof
reconsider r1 = o1, r2 = o2 as Object of C by Def2;
reconsider q1 = o1, q2 = o2 as Object of AllIso AllEpi C by Def5;
A10: <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
let n be object such that
A11: n in (the Arrows of AllIso AllEpi C).i;
n in <^q1,q2^> by A9,A11;
then
A12: <^o2,o1^> <> {} by A10,Th52;
then
A13: <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14: <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15: <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
<^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
then <^q1,q2^> c= <^r1,r2^> by A14;
then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
n in (the Arrows of AllIso AllEpi C).(q1,q2) by A9,A11;
then n2 is iso by Def5;
then n1 is iso by A9,A11,A14,A12,Th40;
then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
hence thesis by A9;
end;
reconsider p1 = o1, p2 = o2 as Object of AllIso C by A4,Def5;
A16: <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
let n be object such that
A17: n in (the Arrows of AllIso C).i;
reconsider n2 = n as Morphism of p1, p2 by A9,A17;
the Arrows of AllIso C cc= the Arrows of AllEpi C by A5,ALTCAT_2:def 11;
then
A18: (the Arrows of AllIso C).i c= (the Arrows of AllEpi C).i by A3,A7;
then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19: n2" in <^p2,p1^> by A9,A17,Th52;
n2 is iso by A9,A17,Th52;
then n1 is iso by A5,A9,A17,A19,Th40;
then n in (the Arrows of AllIso AllEpi C).(o1,o2) by A9,A17,A18,A19,A16
,Def5;
hence thesis by A9;
end;
end;
then the Arrows of AllIso AllEpi C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
then AllIso AllEpi C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;
theorem
AllIso AllRetr C = AllIso C
proof
A1: AllIso AllRetr C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllRetr C = the carrier of AllRetr C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllRetr C = the carrier of C by Def3;
A5: AllIso C is non empty subcategory of AllRetr C by Th41;
A6: now
let i be object;
assume
A7: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of AllRetr C by A8,Def3;
thus (the Arrows of AllIso AllRetr C).i = (the Arrows of AllIso C).i
proof
thus (the Arrows of AllIso AllRetr C).i c= (the Arrows of AllIso C).i
proof
reconsider r1 = o1, r2 = o2 as Object of C by Def3;
reconsider q1 = o1, q2 = o2 as Object of AllIso AllRetr C by Def5;
A10: <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
let n be object such that
A11: n in (the Arrows of AllIso AllRetr C).i;
n in <^q1,q2^> by A9,A11;
then
A12: <^o2,o1^> <> {} by A10,Th52;
then
A13: <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14: <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15: <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
<^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
then <^q1,q2^> c= <^r1,r2^> by A14;
then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
n in (the Arrows of AllIso AllRetr C).(q1,q2) by A9,A11;
then n2 is iso by Def5;
then n1 is iso by A9,A11,A14,A12,Th40;
then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
hence thesis by A9;
end;
reconsider p1 = o1, p2 = o2 as Object of AllIso C by A4,Def5;
A16: <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
let n be object such that
A17: n in (the Arrows of AllIso C).i;
reconsider n2 = n as Morphism of p1, p2 by A9,A17;
the Arrows of AllIso C cc= the Arrows of AllRetr C by A5,ALTCAT_2:def 11;
then
A18: (the Arrows of AllIso C).i c= (the Arrows of AllRetr C).i by A3,A7;
then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19: n2" in <^p2,p1^> by A9,A17,Th52;
n2 is iso by A9,A17,Th52;
then n1 is iso by A5,A9,A17,A19,Th40;
then
n in (the Arrows of AllIso AllRetr C).(o1,o2) by A9,A17,A18,A19,A16,Def5;
hence thesis by A9;
end;
end;
then the Arrows of AllIso AllRetr C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
then AllIso AllRetr C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;
theorem
AllIso AllCoretr C = AllIso C
proof
A1: AllIso AllCoretr C is transitive non empty SubCatStr of C by ALTCAT_2:21;
A2: the carrier of AllIso AllCoretr C = the carrier of AllCoretr C by Def5;
A3: the carrier of AllIso C = the carrier of C by Def5;
A4: the carrier of AllCoretr C = the carrier of C by Def4;
A5: AllIso C is non empty subcategory of AllCoretr C by Th42;
A6: now
let i be object;
assume
A7: i in [:the carrier of C,the carrier of C:];
then consider o1, o2 being object such that
A8: o1 in the carrier of C & o2 in the carrier of C and
A9: i = [o1,o2] by ZFMISC_1:84;
reconsider o1, o2 as Object of AllCoretr C by A8,Def4;
thus (the Arrows of AllIso AllCoretr C).i = (the Arrows of AllIso C).i
proof
thus (the Arrows of AllIso AllCoretr C).i c= (the Arrows of AllIso C).i
proof
reconsider r1 = o1, r2 = o2 as Object of C by Def4;
reconsider q1 = o1, q2 = o2 as Object of AllIso AllCoretr C by Def5;
A10: <^q2,q1^> c= <^o2,o1^> by ALTCAT_2:31;
let n be object such that
A11: n in (the Arrows of AllIso AllCoretr C).i;
n in <^q1,q2^> by A9,A11;
then
A12: <^o2,o1^> <> {} by A10,Th52;
then
A13: <^r2,r1^> <> {} by ALTCAT_2:31,XBOOLE_1:3;
A14: <^q1,q2^> c= <^o1,o2^> by ALTCAT_2:31;
then reconsider n2 = n as Morphism of o1, o2 by A9,A11;
A15: <^r1,r2^> <> {} by A9,A11,A14,ALTCAT_2:31,XBOOLE_1:3;
<^o1,o2^> c= <^r1,r2^> by ALTCAT_2:31;
then <^q1,q2^> c= <^r1,r2^> by A14;
then reconsider n1 = n as Morphism of r1, r2 by A9,A11;
n in (the Arrows of AllIso AllCoretr C).(q1,q2) by A9,A11;
then n2 is iso by Def5;
then n1 is iso by A9,A11,A14,A12,Th40;
then n in (the Arrows of AllIso C).(r1,r2) by A15,A13,Def5;
hence thesis by A9;
end;
reconsider p1 = o1, p2 = o2 as Object of AllIso C by A4,Def5;
A16: <^p2,p1^> c= <^o2,o1^> by A5,ALTCAT_2:31;
let n be object such that
A17: n in (the Arrows of AllIso C).i;
reconsider n2 = n as Morphism of p1, p2 by A9,A17;
the Arrows of AllIso C cc= the Arrows of AllCoretr C by A5,
ALTCAT_2:def 11;
then
A18: (the Arrows of AllIso C).i c= (the Arrows of AllCoretr C).i by A3,A7;
then reconsider n1 = n as Morphism of o1, o2 by A9,A17;
A19: n2" in <^p2,p1^> by A9,A17,Th52;
n2 is iso by A9,A17,Th52;
then n1 is iso by A5,A9,A17,A19,Th40;
then
n in (the Arrows of AllIso AllCoretr C).(o1,o2) by A9,A17,A18,A19,A16
,Def5;
hence thesis by A9;
end;
end;
then the Arrows of AllIso AllCoretr C = the Arrows of AllIso C by A2,A3,A4,
PBOOLE:3;
then AllIso AllCoretr C is SubCatStr of AllIso C by A2,A3,A4,A1,ALTCAT_2:24;
hence thesis by A2,A3,A4,A6,ALTCAT_2:25,PBOOLE:3;
end;