let C be Category; for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let O be non empty Subset of the carrier of C; for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let M be non empty set ; for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let d, c be Function of M,O; for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let p be PartFunc of [:M,M:],M; for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category
let i be Function of O,M; ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Category )
set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
assume that
A1:
M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
and
A2:
d = the Source of C | M
and
A3:
c = the Target of C | M
and
A4:
p = the Comp of C || M
; CatStr(# O,M,d,c,p #) is Category
set B = CatStr(# O,M,d,c,p #);
A8:
for f, g being Morphism of CatStr(# O,M,d,c,p #) holds
( [g,f] in dom p iff d . g = c . f )
proof
let f,
g be
Morphism of
CatStr(#
O,
M,
d,
c,
p #);
( [g,f] in dom p iff d . g = c . f )
reconsider gg =
g,
ff =
f as
Morphism of
C by A5;
A9:
(
d . g = dom gg &
c . f = cod ff )
by A2, A3, FUNCT_1:49;
thus
(
[g,f] in dom p implies
d . g = c . f )
( d . g = c . f implies [g,f] in dom p )
assume
d . g = c . f
;
[g,f] in dom p
then
[g,f] in dom the
Comp of
C
by A9, CAT_1:def 6;
then
[g,f] in (dom the Comp of C) /\ [:M,M:]
by XBOOLE_0:def 4;
hence
[g,f] in dom p
by A4, RELAT_1:61;
verum
end;
A10:
CatStr(# O,M,d,c,p #) is Category-like
by A8;
A11:
CatStr(# O,M,d,c,p #) is transitive
proof
thus
for
f,
g being
Morphism of
CatStr(#
O,
M,
d,
c,
p #) st
dom g = cod f holds
(
dom (g (*) f) = dom f &
cod (g (*) f) = cod g )
CAT_1:def 7 verumproof
let f,
g be
Morphism of
CatStr(#
O,
M,
d,
c,
p #);
( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
reconsider ff =
f,
gg =
g as
Morphism of
C by A5;
A12:
(
d . g = dom gg &
c . f = cod ff )
by A2, A3, FUNCT_1:49;
assume A13:
dom g = cod f
;
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
A14:
[g,f] in dom the
Comp of
CatStr(#
O,
M,
d,
c,
p #)
by A13, A8;
A15:
p . (
g,
f)
= g (*) f
by A13, A8, CAT_1:def 1;
A16:
dom p c= dom the
Comp of
C
by A4, RELAT_1:60;
A17:
p . [g,f] =
the
Comp of
C . (
g,
f)
by A4, A8, A13, FUNCT_1:47
.=
gg (*) ff
by A16, A14, CAT_1:def 1
;
thus dom (g (*) f) =
dom (gg (*) ff)
by A17, A2, A15, FUNCT_1:49
.=
dom ff
by A13, A12, CAT_1:def 7
.=
dom f
by A2, FUNCT_1:49
;
cod (g (*) f) = cod g
thus cod (g (*) f) =
cod (gg (*) ff)
by A17, A3, A15, FUNCT_1:49
.=
cod gg
by A13, A12, CAT_1:def 7
.=
cod g
by A3, FUNCT_1:49
;
verum
end;
end;
A18:
CatStr(# O,M,d,c,p #) is associative
proof
thus
for
f,
g,
h being
Morphism of
CatStr(#
O,
M,
d,
c,
p #) st
dom h = cod g &
dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f
CAT_1:def 8 verumproof
let f,
g,
h be
Morphism of
CatStr(#
O,
M,
d,
c,
p #);
( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider ff =
f,
gg =
g,
hh =
h as
Morphism of
C by A5;
assume that A19:
dom h = cod g
and A20:
dom g = cod f
;
h (*) (g (*) f) = (h (*) g) (*) f
A21:
h (*) g = the
Comp of
CatStr(#
O,
M,
d,
c,
p #)
. (
h,
g)
by A19, A8, CAT_1:def 1;
A22:
g (*) f = the
Comp of
CatStr(#
O,
M,
d,
c,
p #)
. (
g,
f)
by A20, A8, CAT_1:def 1;
A23:
dom (h (*) g) = dom g
by A11, A19;
A24:
(
c . g = cod gg &
d . g = dom gg )
by A2, A3, FUNCT_1:49;
A25:
c . f = cod ff
by A3, FUNCT_1:49;
A26:
(
f is
Morphism of
C &
d . h = dom hh )
by A2, A5, FUNCT_1:49;
A27:
dom gg =
d . g
by A2, FUNCT_1:49
.=
cod ff
by A3, A20, FUNCT_1:49
;
then A28:
gg (*) ff = the
Comp of
C . (
gg,
ff)
by CAT_1:16;
A29:
dom hh =
d . h
by A2, FUNCT_1:49
.=
cod gg
by A3, A19, FUNCT_1:49
;
then A30:
cod (gg (*) ff) = dom hh
by A27, CAT_1:def 7;
A31:
hh (*) gg = the
Comp of
C . (
hh,
gg)
by A29, CAT_1:16;
A32:
cod ff = dom (hh (*) gg)
by A27, A29, CAT_1:def 7;
A33:
cod (g (*) f) = cod g
by A11, A20;
hence h (*) (g (*) f) =
the
Comp of
CatStr(#
O,
M,
d,
c,
p #)
. (
h,
( the Comp of CatStr(# O,M,d,c,p #) . (g,f)))
by A22, A19, A8, CAT_1:def 1
.=
the
Comp of
C . [h,(p . [g,f])]
by A4, A8, A19, A33, A22, FUNCT_1:47
.=
the
Comp of
C . (
hh,
(gg (*) ff))
by A4, A8, A20, A28, FUNCT_1:47
.=
hh (*) (gg (*) ff)
by A30, CAT_1:16
.=
(hh (*) gg) (*) ff
by A19, A20, A26, A24, A25, CAT_1:def 8
.=
the
Comp of
C . (
( the Comp of C . (hh,gg)),
ff)
by A31, A32, CAT_1:16
.=
the
Comp of
C . [(p . [h,g]),f]
by A4, A8, A19, FUNCT_1:47
.=
the
Comp of
CatStr(#
O,
M,
d,
c,
p #)
. (
( the Comp of CatStr(# O,M,d,c,p #) . (h,g)),
f)
by A4, A8, A20, A23, A21, FUNCT_1:47
.=
(h (*) g) (*) f
by A21, A20, A8, A23, CAT_1:def 1
;
verum
end;
end;
A34:
CatStr(# O,M,d,c,p #) is reflexive
proof
let b be
Object of
CatStr(#
O,
M,
d,
c,
p #);
CAT_1:def 9 not Hom (b,b) = {}
b in O
;
then reconsider bb =
b as
Object of
C ;
A35:
Hom (
bb,
bb)
in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
;
id bb in Hom (
bb,
bb)
by CAT_1:27;
then reconsider ii =
id bb as
Morphism of
CatStr(#
O,
M,
d,
c,
p #)
by A35, A1, TARSKI:def 4;
A36:
dom ii =
dom (id bb)
by A2, FUNCT_1:49
.=
bb
;
cod ii =
cod (id bb)
by A3, FUNCT_1:49
.=
bb
;
then
ii in Hom (
b,
b)
by A36;
hence
Hom (
b,
b)
<> {}
;
verum
end;
CatStr(# O,M,d,c,p #) is with_identities
proof
let a be
Element of
CatStr(#
O,
M,
d,
c,
p #);
CAT_1:def 10 ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
a in O
;
then reconsider aa =
a as
Object of
C ;
A37:
Hom (
aa,
aa)
in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
;
id aa in Hom (
aa,
aa)
by CAT_1:27;
then reconsider ii =
id aa as
Morphism of
CatStr(#
O,
M,
d,
c,
p #)
by A37, A1, TARSKI:def 4;
A38:
dom ii =
dom (id aa)
by A2, FUNCT_1:49
.=
aa
;
A39:
cod ii =
cod (id aa)
by A3, FUNCT_1:49
.=
aa
;
then reconsider ii =
ii as
Morphism of
a,
a by A38, CAT_1:4;
take
ii
;
for b1 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
let b be
Element of
CatStr(#
O,
M,
d,
c,
p #);
( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
b in O
;
then reconsider bb =
b as
Object of
C ;
thus
(
Hom (
a,
b)
<> {} implies for
g being
Morphism of
a,
b holds
g (*) ii = g )
( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )proof
assume A40:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) ii = g
let g be
Morphism of
a,
b;
g (*) ii = g
reconsider gg =
g as
Morphism of
C by A5;
A41:
dom gg =
dom g
by A2, FUNCT_1:49
.=
aa
by A40, CAT_1:5
;
A42:
cod (id aa) = aa
;
cod gg =
cod g
by A3, FUNCT_1:49
.=
bb
by A40, CAT_1:5
;
then reconsider gg =
gg as
Morphism of
aa,
bb by A41, CAT_1:4;
A43:
dom g = a
by A40, CAT_1:5;
hence g (*) ii =
p . (
g,
ii)
by A39, A8, CAT_1:def 1
.=
the
Comp of
C . (
gg,
(id aa))
by A43, A4, A39, A8, FUNCT_1:47
.=
gg (*) (id aa)
by A41, A42, CAT_1:16
.=
g
by A41, CAT_1:22
;
verum
end;
thus
(
Hom (
b,
a)
<> {} implies for
f being
Morphism of
b,
a holds
ii (*) f = f )
verumproof
assume A44:
Hom (
b,
a)
<> {}
;
for f being Morphism of b,a holds ii (*) f = f
let g be
Morphism of
b,
a;
ii (*) g = g
reconsider gg =
g as
Morphism of
C by A5;
A45:
cod gg =
cod g
by A3, FUNCT_1:49
.=
aa
by A44, CAT_1:5
;
A46:
dom (id aa) = aa
;
dom gg =
dom g
by A2, FUNCT_1:49
.=
bb
by A44, CAT_1:5
;
then reconsider gg =
gg as
Morphism of
bb,
aa by A45, CAT_1:4;
A47:
cod g = a
by A44, CAT_1:5;
hence ii (*) g =
p . (
ii,
g)
by A38, A8, CAT_1:def 1
.=
the
Comp of
C . (
(id aa),
gg)
by A4, A47, A38, A8, FUNCT_1:47
.=
(id aa) (*) gg
by A45, A46, CAT_1:16
.=
g
by A45, CAT_1:21
;
verum
end;
end;
hence
CatStr(# O,M,d,c,p #) is Category
by A10, A11, A18, A34; verum