altcat_4.miz
begin
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 ::
ALTCAT_4:1
Th1: for v be
Morphism of o1, o2, u be
Morphism of o1, o3 holds for f be
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 ::
ALTCAT_4:2
Th2: for v be
Morphism of o2, o3, u be
Morphism of o1, o3 holds for f be
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 ::
ALTCAT_4:3
Th3: for m be
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 ::
ALTCAT_4:4
Th4: for C be
with_units non
empty
AltCatStr, o be
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 ::
ALTCAT_4:5
for f be
Morphism of o1, o2, g,h be
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 ::
ALTCAT_4:6
(for o1,o2 be
Object of C, f be
Morphism of o1, o2 holds f is
coretraction) implies for a,b be
Object of C, g be
Morphism of a, b st
<^a, b^>
<>
{} &
<^b, a^>
<>
{} holds g is
iso
proof
assume
A1: for o1,o2 be
Object of C, f be
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
theorem ::
ALTCAT_4:7
for m,m9 be
Morphism of o1, o2 st m is
_zero & m9 is
_zero & ex O be
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 be
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 ::
ALTCAT_4:8
for C be non
empty
AltCatStr, O,A be
Object of C holds for M be
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 be
Morphism of o, O such that N
in
<^o, O^> and
A3: for M1 be
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 ::
ALTCAT_4:9
for C be non
empty
AltCatStr, O,A be
Object of C holds for M be
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 be
Morphism of O, o such that N
in
<^O, o^> and
A3: for M1 be
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 ::
ALTCAT_4:10
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 be
Object of C holds ex M be
Morphism of o3, o1 st M
in
<^o3, o1^> & for v be
Morphism of o3, o1 st v
in
<^o3, o1^> holds M
= v
proof
consider f be
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 be
Morphism of o3, o2 such that
A5: u
in
<^o3, o2^> and
A6: for M1 be
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 ::
ALTCAT_4:11
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 be
Object of C holds ex M be
Morphism of o2, o3 st M
in
<^o2, o3^> & for v be
Morphism of o2, o3 st v
in
<^o2, o3^> holds M
= v
proof
consider f be
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 be
Morphism of o1, o3 such that
A5: u
in
<^o1, o3^> and
A6: for M1 be
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 ::
ALTCAT_4:12
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 be
Morphism of o1, o2 such that
A3: l
in
<^o1, o2^> and for M1 be
Morphism of o1, o2 st M1
in
<^o1, o2^> holds l
= M1 by
A1,
ALTCAT_3: 25;
assume
<^o2, o1^>
<>
{} ;
then
consider m be
object such that
A4: m
in
<^o2, o1^> by
XBOOLE_0:def 1;
reconsider m as
Morphism of o2, o1 by
A4;
for o3 be
Object of C holds ex M be
Morphism of o2, o3 st M
in
<^o2, o3^> & for M1 be
Morphism of o2, o3 st M1
in
<^o2, o3^> holds M
= M1
proof
let o3 be
Object of C;
consider M be
Morphism of o1, o3 such that
A5: M
in
<^o1, o3^> and
A6: for M1 be
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 be
Morphism of o2, o2 such that i2
in
<^o2, o2^> and
A8: for M1 be
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 be
Object of C holds ex M be
Morphism of o3, o1 st M
in
<^o3, o1^> & for M1 be
Morphism of o3, o1 st M1
in
<^o3, o1^> holds M
= M1
proof
let o3 be
Object of C;
consider M be
Morphism of o3, o2 such that
A9: M
in
<^o3, o2^> and
A10: for M1 be
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 be
Morphism of o1, o1 such that i1
in
<^o1, o1^> and
A12: for M1 be
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
theorem ::
ALTCAT_4:13
Th13: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
contravariant
Functor of A, B holds for a be
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 ::
ALTCAT_4:14
Th14: for C1,C2 be non
empty
AltCatStr holds for F be
Contravariant
FunctorStr over C1, C2 holds F is
full iff for o1,o2 be
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 be
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 be
Object of C1 holds (
Morph-Map (F,o2,o1)) is
onto;
ex I29 be non
empty
set, B9 be
ManySortedSet of I29, f9 be
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 be
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 ::
ALTCAT_4:15
Th15: for C1,C2 be non
empty
AltCatStr holds for F be
Contravariant
FunctorStr over C1, C2 holds F is
faithful iff for o1,o2 be
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 be
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 be
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 ::
ALTCAT_4:16
Th16: for C1,C2 be non
empty
AltCatStr holds for F be
Covariant
FunctorStr over C1, C2 holds for o1,o2 be
Object of C1, Fm be
Morphism of (F
. o1), (F
. o2) st
<^o1, o2^>
<>
{} & F is
full
feasible holds ex m be
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 be
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 ::
ALTCAT_4:17
Th17: for C1,C2 be non
empty
AltCatStr holds for F be
Contravariant
FunctorStr over C1, C2 holds for o1,o2 be
Object of C1, Fm be
Morphism of (F
. o2), (F
. o1) st
<^o1, o2^>
<>
{} & F is
full
feasible holds ex m be
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 be
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 ::
ALTCAT_4:18
Th18: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
covariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 ::
ALTCAT_4:19
Th19: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
covariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 ::
ALTCAT_4:20
Th20: for A,B be
category, F be
covariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 ::
ALTCAT_4:21
for A,B be
category, F be
covariant
Functor of A, B holds for o1,o2 be
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 be
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 ::
ALTCAT_4:22
Th22: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
contravariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 ::
ALTCAT_4:23
Th23: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
contravariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 ::
ALTCAT_4:24
Th24: for A,B be
category, F be
contravariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 ::
ALTCAT_4:25
for A,B be
category, F be
contravariant
Functor of A, B holds for o1,o2 be
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 be
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 ::
ALTCAT_4:26
Th26: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
covariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 be
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 ::
ALTCAT_4:27
Th27: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
covariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 be
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 ::
ALTCAT_4:28
Th28: for A,B be
category, F be
covariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 ::
ALTCAT_4:29
for A,B be
category, F be
covariant
Functor of A, B holds for o1,o2 be
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 be
Morphism of (F
. o1), (F
. o2) such that
A5: Fa is
iso by
A4;
consider a be
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 ::
ALTCAT_4:30
Th30: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
contravariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 be
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 ::
ALTCAT_4:31
Th31: for A,B be
transitive
with_units non
empty
AltCatStr holds for F be
contravariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 be
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 be
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 ::
ALTCAT_4:32
Th32: for A,B be
category, F be
contravariant
Functor of A, B holds for o1,o2 be
Object of A, a be
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 ::
ALTCAT_4:33
for A,B be
category, F be
contravariant
Functor of A, B holds for o1,o2 be
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 be
Morphism of (F
. o2), (F
. o1) such that
A5: Fa is
iso by
A4;
consider a be
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 be
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 be
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
theorem ::
ALTCAT_4:34
Th34: for C be
AltCatStr, D be
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 ::
ALTCAT_4:35
Th35: for C be
with_units non
empty
AltCatStr, D be
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 ::
ALTCAT_4:36
Th36: for B be non
empty
subcategory of C holds for A be 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 ::
ALTCAT_4:37
Th37: for C be non
empty
transitive
AltCatStr holds for D be non
empty
transitive
SubCatStr of C holds for o1,o2 be
Object of C, p1,p2 be
Object of D holds for m be
Morphism of o1, o2, n be
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 ::
ALTCAT_4:38
Th38: for D be non
empty
subcategory of C holds for o1,o2 be
Object of C, p1,p2 be
Object of D holds for m be
Morphism of o1, o2, m1 be
Morphism of o2, o1 holds for n be
Morphism of p1, p2, n1 be
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 ::
ALTCAT_4:39
for D be
full non
empty
subcategory of C holds for o1,o2 be
Object of C, p1,p2 be
Object of D holds for m be
Morphism of o1, o2, n be
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 be
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 be
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,
ALTCAT_3: 6;
end;
theorem ::
ALTCAT_4:40
Th40: for D be non
empty
subcategory of C holds for o1,o2 be
Object of C, p1,p2 be
Object of D holds for m be
Morphism of o1, o2, n be
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 be
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 be
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,
ALTCAT_3: 6;
end;
definition
let C be
category;
::
ALTCAT_4:def1
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 be
Object of C, m be
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 be
set st D2
= $2 & for x be
set holds x
in D2 iff ex o1,o2 be
Object of C, m be
Morphism of o1, o2 st $1
=
[o1, o2] &
<^o1, o2^>
<>
{} & x
= m & m is
mono;
set I = the
carrier of C;
A1: for i be
object st i
in
[:I, I:] holds ex X be
object st
P[i, X]
proof
let i be
object;
assume i
in
[:I, I:];
then
consider o1,o2 be
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 be
Morphism of o1, o2 st
<^o1, o2^>
<>
{} & m
= $1 & m is
mono;
consider X be
set such that
A4: for x be
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 be
Object of C, m be
Morphism of o1, o2 st i
=
[o1, o2] &
<^o1, o2^>
<>
{} & x
= m & m is
mono
proof
assume x
in X;
then
consider m be
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 be
Object of C, m be
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 be
ManySortedSet of
[:I, I:] such that
A8: for i be
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 be
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 be
object st i
in
[:I, I, I:] holds ex j be
object st
R[i, j]
proof
let i be
object;
assume i
in
[:I, I, I:];
then
consider p1,p2,p3 be
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 be
ManySortedSet of
[:I, I, I:] such that
A12: for i be
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 be
Object of C, m be
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 be
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 be
object such that
A26: k
in
[:(Ar
. (p2,p3)), (Ar
. (p1,p2)):] by
XBOOLE_0:def 1;
consider u1,u2 be
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 be
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 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
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 be
object such that
A54: m2
in
<^p1, p2^> by
A52,
XBOOLE_0:def 1;
consider m1 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
Object of C, n be
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 be
Object of C, m be
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 be
Object of C, m be
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 be
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;
::
ALTCAT_4:def2
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 be
Object of C, m be
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 be
set st D2
= $2 & for x be
set holds x
in D2 iff ex o1,o2 be
Object of C, m be
Morphism of o1, o2 st $1
=
[o1, o2] &
<^o1, o2^>
<>
{} & x
= m & m is
epi;
set I = the
carrier of C;
A1: for i be
object st i
in
[:I, I:] holds ex X be
object st
P[i, X]
proof
let i be
object;
assume i
in
[:I, I:];
then
consider o1,o2 be
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 be
Morphism of o1, o2 st
<^o1, o2^>
<>
{} & m
= $1 & m is
epi;
consider X be
set such that
A4: for x be
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 be
Object of C, m be
Morphism of o1, o2 st i
=
[o1, o2] &
<^o1, o2^>
<>
{} & x
= m & m is
epi
proof
assume x
in X;
then
consider m be
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 be
Object of C, m be
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 be
ManySortedSet of
[:I, I:] such that
A8: for i be
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 be
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 be
object st i
in
[:I, I, I:] holds ex j be
object st
R[i, j]
proof
let i be
object;
assume i
in
[:I, I, I:];
then
consider p1,p2,p3 be
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 be
ManySortedSet of
[:I, I, I:] such that
A12: for i be
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 be
Object of C, m be
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 be
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 be
object such that
A26: k
in
[:(Ar
. (p2,p3)), (Ar
. (p1,p2)):] by
XBOOLE_0:def 1;
consider u1,u2 be
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 be
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 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
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 be
object such that
A54: m2
in
<^p1, p2^> by
A52,
XBOOLE_0:def 1;
consider m1 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
Object of C, n be
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 be
Object of C, m be
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 be
Object of C, m be
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 be
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;
::
ALTCAT_4:def3
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 be
Object of C, m be
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 be
set st D2
= $2 & for x be
set holds x
in D2 iff ex o1,o2 be
Object of C, m be
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 be
object st i
in
[:I, I:] holds ex X be
object st
P[i, X]
proof
let i be
object;
assume i
in
[:I, I:];
then
consider o1,o2 be
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 be
Morphism of o1, o2 st
<^o1, o2^>
<>
{} &
<^o2, o1^>
<>
{} & m
= $1 & m is
retraction;
consider X be
set such that
A4: for x be
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 be
Object of C, m be
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 be
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 be
Object of C, m be
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 be
ManySortedSet of
[:I, I:] such that
A8: for i be
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 be
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 be
object st i
in
[:I, I, I:] holds ex j be
object st
R[i, j]
proof
let i be
object;
assume i
in
[:I, I, I:];
then
consider p1,p2,p3 be
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 be
ManySortedSet of
[:I, I, I:] such that
A12: for i be
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 be
Object of C, m be
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 be
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 be
object such that
A26: k
in
[:(Ar
. (p2,p3)), (Ar
. (p1,p2)):] by
XBOOLE_0:def 1;
consider u1,u2 be
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 be
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 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
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 be
object such that
A57: m2
in
<^p1, p2^> by
A55,
XBOOLE_0:def 1;
consider m1 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
Object of C, n be
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 be
Object of C, m be
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 be
Object of C, m be
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 be
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;
::
ALTCAT_4:def4
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 be
Object of C, m be
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 be
set st D2
= $2 & for x be
set holds x
in D2 iff ex o1,o2 be
Object of C, m be
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 be
object st i
in
[:I, I:] holds ex X be
object st
P[i, X]
proof
let i be
object;
assume i
in
[:I, I:];
then
consider o1,o2 be
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 be
Morphism of o1, o2 st
<^o1, o2^>
<>
{} &
<^o2, o1^>
<>
{} & m
= $1 & m is
coretraction;
consider X be
set such that
A4: for x be
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 be
Object of C, m be
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 be
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 be
Object of C, m be
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 be
ManySortedSet of
[:I, I:] such that
A8: for i be
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 be
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 be
object st i
in
[:I, I, I:] holds ex j be
object st
R[i, j]
proof
let i be
object;
assume i
in
[:I, I, I:];
then
consider p1,p2,p3 be
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 be
ManySortedSet of
[:I, I, I:] such that
A12: for i be
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 be
Object of C, m be
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 be
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 be
object such that
A26: k
in
[:(Ar
. (p2,p3)), (Ar
. (p1,p2)):] by
XBOOLE_0:def 1;
consider u1,u2 be
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 be
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 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
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 be
object such that
A57: m2
in
<^p1, p2^> by
A55,
XBOOLE_0:def 1;
consider m1 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
Object of C, n be
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 be
Object of C, m be
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 be
Object of C, m be
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 be
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;
::
ALTCAT_4:def5
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 be
Object of C, m be
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 be
set st D2
= $2 & for x be
set holds x
in D2 iff ex o1,o2 be
Object of C, m be
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 be
object st i
in
[:I, I:] holds ex X be
object st
P[i, X]
proof
let i be
object;
assume i
in
[:I, I:];
then
consider o1,o2 be
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 be
Morphism of o1, o2 st
<^o1, o2^>
<>
{} &
<^o2, o1^>
<>
{} & m
= $1 & m is
iso;
consider X be
set such that
A4: for x be
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 be
Object of C, m be
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 be
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 be
Object of C, m be
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 be
ManySortedSet of
[:I, I:] such that
A8: for i be
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 be
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 be
object st i
in
[:I, I, I:] holds ex j be
object st
R[i, j]
proof
let i be
object;
assume i
in
[:I, I, I:];
then
consider p1,p2,p3 be
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 be
ManySortedSet of
[:I, I, I:] such that
A12: for i be
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 be
Object of C, m be
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 be
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 be
object such that
A26: k
in
[:(Ar
. (p2,p3)), (Ar
. (p1,p2)):] by
XBOOLE_0:def 1;
consider u1,u2 be
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 be
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 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
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 be
object such that
A57: m2
in
<^p1, p2^> by
A55,
XBOOLE_0:def 1;
consider m1 be
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 be
Object of C, qq be
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 be
Object of C, rr be
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 be
Object of C, m be
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 be
Object of C, n be
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 be
Object of C, m be
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 be
Object of C, m be
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 be
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 ::
ALTCAT_4:41
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 be
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 ::
ALTCAT_4:42
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 be
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 ::
ALTCAT_4:43
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 be
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 ::
ALTCAT_4:44
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 be
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 ::
ALTCAT_4:45
(for o1,o2 be
Object of C, m be
Morphism of o1, o2 holds m is
mono) implies the AltCatStr of C
= (
AllMono C)
proof
assume
A1: for o1,o2 be
Object of C, m be
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 be
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 ::
ALTCAT_4:46
(for o1,o2 be
Object of C, m be
Morphism of o1, o2 holds m is
epi) implies the AltCatStr of C
= (
AllEpi C)
proof
assume
A1: for o1,o2 be
Object of C, m be
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 be
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 ::
ALTCAT_4:47
(for o1,o2 be
Object of C, m be
Morphism of o1, o2 holds m is
retraction &
<^o2, o1^>
<>
{} ) implies the AltCatStr of C
= (
AllRetr C)
proof
assume
A1: for o1,o2 be
Object of C, m be
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 be
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 ::
ALTCAT_4:48
(for o1,o2 be
Object of C, m be
Morphism of o1, o2 holds m is
coretraction &
<^o2, o1^>
<>
{} ) implies the AltCatStr of C
= (
AllCoretr C)
proof
assume
A1: for o1,o2 be
Object of C, m be
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 be
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 ::
ALTCAT_4:49
(for o1,o2 be
Object of C, m be
Morphism of o1, o2 holds m is
iso &
<^o2, o1^>
<>
{} ) implies the AltCatStr of C
= (
AllIso C)
proof
assume
A1: for o1,o2 be
Object of C, m be
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 be
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 ::
ALTCAT_4:50
Th50: for o1,o2 be
Object of (
AllMono C) holds for m be
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 ::
ALTCAT_4:51
Th51: for o1,o2 be
Object of (
AllEpi C) holds for m be
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 ::
ALTCAT_4:52
Th52: for o1,o2 be
Object of (
AllIso C) holds for m be
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 ::
ALTCAT_4:53
(
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 be
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 ::
ALTCAT_4:54
(
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 be
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 ::
ALTCAT_4:55
(
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 be
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 ::
ALTCAT_4:56
(
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 be
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 ::
ALTCAT_4:57
(
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 be
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 ::
ALTCAT_4:58
(
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 be
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 ::
ALTCAT_4:59
(
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 be
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;