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 Subcategory of C
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 Subcategory of C
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 Subcategory of C
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 Subcategory of C
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 Subcategory of C
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 Subcategory of C )
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 Subcategory of C
set B = CatStr(# O,M,d,c,p #);
A8:
for a, b being Object of CatStr(# O,M,d,c,p #)
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
proof
let a,
b be
Object of
CatStr(#
O,
M,
d,
c,
p #);
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)let a9,
b9 be
Object of
C;
( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )
assume A9:
(
a = a9 &
b = b9 )
;
Hom (a,b) = Hom (a9,b9)
now for x being object holds
( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )let x be
object ;
( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )thus
(
x in Hom (
a,
b) implies
x in Hom (
a9,
b9) )
( x in Hom (a9,b9) implies x in Hom (a,b) )proof
assume A10:
x in Hom (
a,
b)
;
x in Hom (a9,b9)
then reconsider f =
x as
Morphism of
CatStr(#
O,
M,
d,
c,
p #) ;
reconsider f9 =
f as
Morphism of
C by A5;
cod f = cod f9
by A3, FUNCT_1:49;
then A11:
b = cod f9
by A10, CAT_1:1;
dom f = dom f9
by A2, FUNCT_1:49;
then
a = dom f9
by A10, CAT_1:1;
hence
x in Hom (
a9,
b9)
by A9, A11;
verum
end; assume A12:
x in Hom (
a9,
b9)
;
x in Hom (a,b)then reconsider f9 =
x as
Morphism of
C ;
Hom (
a9,
b9)
in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
by A9;
then reconsider f =
f9 as
Morphism of
CatStr(#
O,
M,
d,
c,
p #)
by A1, A12, TARSKI:def 4;
cod f = cod f9
by A3, FUNCT_1:49;
then A13:
cod f = b9
by A12, CAT_1:1;
dom f = dom f9
by A2, FUNCT_1:49;
then
dom f = a9
by A12, CAT_1:1;
hence
x in Hom (
a,
b)
by A9, A13;
verum end;
hence
Hom (
a,
b)
= Hom (
a9,
b9)
by TARSKI:2;
verum
end;
reconsider B = CatStr(# O,M,d,c,p #) as Category by Lm1, A1, A2, A3, A4;
A14:
for a being Object of B
for a9 being Object of C st a = a9 holds
id a = id a9
proof
let a be
Object of
B;
for a9 being Object of C st a = a9 holds
id a = id a9let a9 be
Object of
C;
( a = a9 implies id a = id a9 )
assume A15:
a = a9
;
id a = id a9
A16:
Hom (
a9,
a9)
in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
by A15;
A17:
id a9 in Hom (
a9,
a9)
by CAT_1:27;
then reconsider ii =
id a9 as
Morphism of
B by A16, A1, TARSKI:def 4;
A18:
dom ii =
dom (id a9)
by A2, FUNCT_1:49
.=
a9
;
A19:
cod ii =
cod (id a9)
by A3, FUNCT_1:49
.=
a9
;
ii in Hom (
a,
a)
by A17, A8, A15;
then reconsider ii =
ii as
Morphism of
a,
a by CAT_1:def 5;
A20:
for
f,
g being
Morphism of
B holds
(
[g,f] in dom p iff
d . g = c . f )
proof
let f,
g be
Morphism of
B;
( [g,f] in dom p iff d . g = c . f )
reconsider gg =
g,
ff =
f as
Morphism of
C by A5;
A21:
(
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 A21, 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;
for
b being
Object of
B holds
( (
Hom (
a,
b)
<> {} implies for
f being
Morphism of
a,
b holds
f (*) ii = f ) & (
Hom (
b,
a)
<> {} implies for
f being
Morphism of
b,
a holds
ii (*) f = f ) )
proof
let b be
Object of
B;
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
b in O
;
then reconsider bb =
b as
Element of
C ;
thus
(
Hom (
a,
b)
<> {} implies for
f being
Morphism of
a,
b holds
f (*) ii = f )
( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )proof
assume A22:
Hom (
a,
b)
<> {}
;
for f being Morphism of a,b holds f (*) ii = f
let g be
Morphism of
a,
b;
g (*) ii = g
reconsider gg =
g as
Morphism of
C by A5;
A23:
dom gg =
dom g
by A2, FUNCT_1:49
.=
a9
by A15, A22, CAT_1:5
;
A24:
cod (id a9) = a9
;
cod gg =
cod g
by A3, FUNCT_1:49
.=
bb
by A22, CAT_1:5
;
then reconsider gg =
gg as
Morphism of
a9,
bb by A23, CAT_1:4;
A25:
dom g = a
by A22, CAT_1:5;
hence g (*) ii =
p . (
g,
ii)
by A19, A20, A15, CAT_1:def 1
.=
the
Comp of
C . (
gg,
(id a9))
by A19, A20, A15, A4, A25, FUNCT_1:47
.=
gg (*) (id a9)
by A23, A24, CAT_1:16
.=
g
by A23, CAT_1:22
;
verum
end;
assume A26:
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;
A27:
cod gg =
cod g
by A3, FUNCT_1:49
.=
a9
by A15, A26, CAT_1:5
;
A28:
dom (id a9) = a9
;
dom gg =
dom g
by A2, FUNCT_1:49
.=
bb
by A26, CAT_1:5
;
then reconsider gg =
gg as
Morphism of
bb,
a9 by A27, CAT_1:4;
A29:
cod g = a
by A26, CAT_1:5;
hence ii (*) g =
p . (
ii,
g)
by A18, A20, A15, CAT_1:def 1
.=
the
Comp of
C . (
(id a9),
gg)
by A18, A20, A15, A4, A29, FUNCT_1:47
.=
(id a9) (*) gg
by A27, A28, CAT_1:16
.=
g
by A27, CAT_1:21
;
verum
end;
hence
id a = id a9
by CAT_1:def 12;
verum
end;
( ( for a, b being Object of B
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of B c= the Comp of C )
by A4, A8, RELAT_1:59;
hence
CatStr(# O,M,d,c,p #) is Subcategory of C
by A14, Def4; verum