:: On the Categories Without Uniqueness of { \bf cod } and { \bfdom } . Some Properties of the Morphisms and the Functors
:: by Artur Korni{\l}owicz
::
:: Received October 3, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: ALTCAT_4:1
theorem Th2: :: ALTCAT_4:2
theorem Th3: :: ALTCAT_4:3
theorem Th4: :: ALTCAT_4:4
theorem :: ALTCAT_4:5
theorem :: ALTCAT_4:6
theorem :: ALTCAT_4:7
theorem :: ALTCAT_4:8
theorem :: ALTCAT_4:9
theorem :: ALTCAT_4:10
theorem :: ALTCAT_4:11
theorem :: ALTCAT_4:12
theorem Th13: :: ALTCAT_4:13
theorem Th14: :: ALTCAT_4:14
theorem Th15: :: ALTCAT_4:15
theorem Th16: :: ALTCAT_4:16
theorem Th17: :: ALTCAT_4:17
theorem Th18: :: ALTCAT_4:18
theorem Th19: :: ALTCAT_4:19
theorem Th20: :: ALTCAT_4:20
theorem :: ALTCAT_4:21
theorem Th22: :: ALTCAT_4:22
theorem Th23: :: ALTCAT_4:23
theorem Th24: :: ALTCAT_4:24
theorem :: ALTCAT_4:25
theorem Th26: :: ALTCAT_4:26
theorem Th27: :: ALTCAT_4:27
theorem Th28: :: ALTCAT_4:28
theorem :: ALTCAT_4:29
theorem Th30: :: ALTCAT_4:30
theorem Th31: :: ALTCAT_4:31
theorem Th32: :: ALTCAT_4:32
theorem :: ALTCAT_4:33
Lm1:
now
let C be non
empty transitive AltCatStr ;
:: thesis: for p1, p2, p3 being object of C 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
C;
:: thesis: ( 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 = {}
;
:: thesis: [:(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):] = {}
:: thesis: verum
proof
assume
[:(the Arrows of C . p2,p3),(the Arrows of C . p1,p2):] <> {}
;
:: thesis: 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 &
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;
:: thesis: verum
end;
end;
theorem Th34: :: ALTCAT_4:34
theorem Th35: :: ALTCAT_4:35
theorem Th36: :: ALTCAT_4:36
theorem Th37: :: ALTCAT_4:37
theorem Th38: :: ALTCAT_4:38
theorem :: ALTCAT_4:39
theorem Th40: :: ALTCAT_4:40
definition
let C be
category;
func AllMono C -> non
empty transitive strict SubCatStr of
C means :
Def1:
:: ALTCAT_4:def 1
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
C for
m being
Morphism of
o1,
o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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:
:: ALTCAT_4:def 2
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
C for
m being
Morphism of
o1,
o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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:
:: ALTCAT_4:def 3
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
C for
m being
Morphism of
o1,
o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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:
:: ALTCAT_4:def 4
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
C for
m being
Morphism of
o1,
o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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:
:: ALTCAT_4:def 5
( the
carrier of
it = the
carrier of
C & the
Arrows of
it cc= the
Arrows of
C & ( for
o1,
o2 being
object of
C for
m being
Morphism of
o1,
o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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 C
for m being Morphism of o1,o2 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: :: ALTCAT_4:41
theorem Th42: :: ALTCAT_4:42
theorem Th43: :: ALTCAT_4:43
theorem Th44: :: ALTCAT_4:44
theorem :: ALTCAT_4:45
theorem :: ALTCAT_4:46
theorem :: ALTCAT_4:47
theorem :: ALTCAT_4:48
theorem :: ALTCAT_4:49
theorem Th50: :: ALTCAT_4:50
theorem Th51: :: ALTCAT_4:51
theorem Th52: :: ALTCAT_4:52
theorem :: ALTCAT_4:53
theorem :: ALTCAT_4:54
theorem :: ALTCAT_4:55
theorem :: ALTCAT_4:56
theorem :: ALTCAT_4:57
theorem :: ALTCAT_4:58
theorem :: ALTCAT_4:59