begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem
Lm1:
now
let C be non
empty transitive AltCatStr ;
for p1, p2, p3 being object of st the Arrows of C . p1,p3 = {} holds
[:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] = {} let p1,
p2,
p3 be
object of ;
( the Arrows of C . p1,p3 = {} implies [:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] = {} )assume A1:
the
Arrows of
C . p1,
p3 = {}
;
[:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] = {} thus
[:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] = {}
verum
proof
assume
[:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] <> {}
;
contradiction
then consider k being
set such that A2:
k in [:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):]
by XBOOLE_0:def 1;
consider u1,
u2 being
set 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 4;
hence
contradiction
by A1;
verum
end;
end;
begin
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
definition
let C be
category;
func AllMono C -> non
empty transitive strict SubCatStr of
C means :
Def1:
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
for
m being
Morphism of , holds
(
m in the
Arrows of
it . o1,
o2 iff (
<^o1,o2^> <> {} &
m is
mono ) ) ) );
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & m is mono ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & m is mono ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b2 . o1,o2 iff ( <^o1,o2^> <> {} & m is mono ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines AllMono ALTCAT_4:def 1 :
definition
let C be
category;
func AllEpi C -> non
empty transitive strict SubCatStr of
C means :
Def2:
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
for
m being
Morphism of , holds
(
m in the
Arrows of
it . o1,
o2 iff (
<^o1,o2^> <> {} &
m is
epi ) ) ) );
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & m is epi ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & m is epi ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b2 . o1,o2 iff ( <^o1,o2^> <> {} & m is epi ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines AllEpi ALTCAT_4:def 2 :
definition
let C be
category;
func AllRetr C -> non
empty transitive strict SubCatStr of
C means :
Def3:
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
for
m being
Morphism of , holds
(
m in the
Arrows of
it . o1,
o2 iff (
<^o1,o2^> <> {} &
<^o2,o1^> <> {} &
m is
retraction ) ) ) );
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b2 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) holds
b1 = b2
end;
:: deftheorem Def3 defines AllRetr ALTCAT_4:def 3 :
definition
let C be
category;
func AllCoretr C -> non
empty transitive strict SubCatStr of
C means :
Def4:
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
for
m being
Morphism of , holds
(
m in the
Arrows of
it . o1,
o2 iff (
<^o1,o2^> <> {} &
<^o2,o1^> <> {} &
m is
coretraction ) ) ) );
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b2 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is coretraction ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines AllCoretr ALTCAT_4:def 4 :
definition
let C be
category;
func AllIso C -> non
empty transitive strict SubCatStr of
C means :
Def5:
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
for
m being
Morphism of , holds
(
m in the
Arrows of
it . o1,
o2 iff (
<^o1,o2^> <> {} &
<^o2,o1^> <> {} &
m is
iso ) ) ) );
existence
ex b1 being non empty transitive strict SubCatStr of C st
( the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) )
uniqueness
for b1, b2 being non empty transitive strict SubCatStr of C st the carrier of b1 = the carrier of C & the Arrows of b1 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b1 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) & the carrier of b2 = the carrier of C & the Arrows of b2 cc= the Arrows of C & ( for o1, o2 being object of
for m being Morphism of , holds
( m in the Arrows of b2 . o1,o2 iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines AllIso ALTCAT_4:def 5 :
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem
theorem
theorem
theorem
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
theorem
theorem
theorem
theorem