let C be Category; :: thesis: for E being Subcategory of C holds
( incl E is full iff for a, b being Object of E
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b' )
let E be Subcategory of C; :: thesis: ( incl E is full iff for a, b being Object of E
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b' )
set T = incl E;
thus
( incl E is full implies for a, b being Object of E
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b' )
:: thesis: ( ( for a, b being Object of E
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b' ) implies incl E is full )proof
assume A1:
for
a,
b being
Object of
E st
Hom ((incl E) . a),
((incl E) . b) <> {} holds
for
g being
Morphism of
(incl E) . a,
(incl E) . b holds
(
Hom a,
b <> {} & ex
f being
Morphism of
a,
b st
g = (incl E) . f )
;
:: according to CAT_1:def 23 :: thesis: for a, b being Object of E
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b'
let a,
b be
Object of
E;
:: thesis: for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b'let a',
b' be
Object of
C;
:: thesis: ( a = a' & b = b' implies Hom a,b = Hom a',b' )
assume A2:
(
a = a' &
b = b' )
;
:: thesis: Hom a,b = Hom a',b'
now let x be
set ;
:: thesis: ( ( x in Hom a,b implies x in Hom a',b' ) & ( x in Hom a',b' implies x in Hom a,b ) )
Hom a,
b c= Hom a',
b'
by A2, Def4;
hence
(
x in Hom a,
b implies
x in Hom a',
b' )
;
:: thesis: ( x in Hom a',b' implies x in Hom a,b )A3:
(
(incl E) . a = a' &
(incl E) . b = b' )
by A2, Th22;
assume A4:
x in Hom a',
b'
;
:: thesis: x in Hom a,bthen reconsider g =
x as
Morphism of
(incl E) . a,
(incl E) . b by A3, CAT_1:def 7;
consider f being
Morphism of
a,
b such that A5:
g = (incl E) . f
by A1, A3, A4;
(
g = f &
Hom a,
b <> {} )
by A1, A3, A4, A5, FUNCT_1:35;
hence
x in Hom a,
b
by CAT_1:def 7;
:: thesis: verum end;
hence
Hom a,
b = Hom a',
b'
by TARSKI:2;
:: thesis: verum
end;
assume A6:
for a, b being Object of E
for a', b' being Object of C st a = a' & b = b' holds
Hom a,b = Hom a',b'
; :: thesis: incl E is full
let a, b be Object of E; :: according to CAT_1:def 23 :: thesis: ( Hom ((incl E) . a),((incl E) . b) = {} or for b1 being Morphism of (incl E) . a,(incl E) . b holds
( not Hom a,b = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 ) )
assume A7:
Hom ((incl E) . a),((incl E) . b) <> {}
; :: thesis: for b1 being Morphism of (incl E) . a,(incl E) . b holds
( not Hom a,b = {} & ex b2 being Morphism of a,b st b1 = (incl E) . b2 )
let g be Morphism of (incl E) . a,(incl E) . b; :: thesis: ( not Hom a,b = {} & ex b1 being Morphism of a,b st g = (incl E) . b1 )
A8:
( a = (incl E) . a & b = (incl E) . b )
by Th22;
then A9:
Hom a,b = Hom ((incl E) . a),((incl E) . b)
by A6;
thus
Hom a,b <> {}
by A6, A7, A8; :: thesis: ex b1 being Morphism of a,b st g = (incl E) . b1
g in Hom ((incl E) . a),((incl E) . b)
by A7, CAT_1:def 7;
then reconsider f = g as Morphism of a,b by A9, CAT_1:def 7;
take
f
; :: thesis: g = (incl E) . f
thus
g = (incl E) . f
by FUNCT_1:35; :: thesis: verum