begin
:: deftheorem Def1 defines is_left_inverse_of ALTCAT_3:def 1 :
:: deftheorem Def2 defines retraction ALTCAT_3:def 2 :
:: deftheorem Def3 defines coretraction ALTCAT_3:def 3 :
theorem Th1:
:: deftheorem Def4 defines " ALTCAT_3:def 4 :
theorem Th2:
theorem Th3:
theorem Th4:
:: deftheorem Def5 defines iso ALTCAT_3:def 5 :
theorem Th5:
theorem Th6:
theorem Th7:
definition
let C be
category;
let o1,
o2 be
object of
C;
pred o1,
o2 are_iso means :
Def6:
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} & ex
A being
Morphism of
o1,
o2 st
A is
iso );
reflexivity
for o1 being object of C holds
( <^o1,o1^> <> {} & <^o1,o1^> <> {} & ex A being Morphism of o1,o1 st A is iso )
symmetry
for o1, o2 being object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso holds
( <^o2,o1^> <> {} & <^o1,o2^> <> {} & ex A being Morphism of o2,o1 st A is iso )
end;
:: deftheorem Def6 defines are_iso ALTCAT_3:def 6 :
theorem
:: deftheorem Def7 defines mono ALTCAT_3:def 7 :
:: deftheorem Def8 defines epi ALTCAT_3:def 8 :
theorem Th9:
theorem Th10:
theorem
theorem
Lm1:
now
let C be non
empty with_units AltCatStr ;
for a being object of C holds
( idm a is epi & idm a is mono )let a be
object of
C;
( idm a is epi & idm a is mono )thus
idm a is
epi
idm a is mono
proof
let o be
object of
C;
ALTCAT_3:def 8 ( <^a,o^> <> {} implies for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds
B = C )
assume A1:
<^a,o^> <> {}
;
for B, C being Morphism of a,o st B * (idm a) = C * (idm a) holds
B = C
let B,
C be
Morphism of
a,
o;
( B * (idm a) = C * (idm a) implies B = C )
assume A2:
B * (idm a) = C * (idm a)
;
B = C
thus B =
B * (idm a)
by A1, ALTCAT_1:def 19
.=
C
by A1, A2, ALTCAT_1:def 19
;
verum
end;
thus
idm a is
mono
verum
proof
let o be
object of
C;
ALTCAT_3:def 7 ( <^o,a^> <> {} implies for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds
B = C )
assume A3:
<^o,a^> <> {}
;
for B, C being Morphism of o,a st (idm a) * B = (idm a) * C holds
B = C
let B,
C be
Morphism of
o,
a;
( (idm a) * B = (idm a) * C implies B = C )
assume A4:
(idm a) * B = (idm a) * C
;
B = C
thus B =
(idm a) * B
by A3, ALTCAT_1:24
.=
C
by A3, A4, ALTCAT_1:24
;
verum
end;
end;
theorem
theorem
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines initial ALTCAT_3:def 9 :
theorem
theorem Th26:
:: deftheorem Def10 defines terminal ALTCAT_3:def 10 :
theorem
theorem
:: deftheorem Def11 defines _zero ALTCAT_3:def 11 :
theorem
:: deftheorem Def12 defines _zero ALTCAT_3:def 12 :
theorem