let C be Category; for E being Subcategory of C holds
( incl E is full iff for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) )
let E be Subcategory of C; ( incl E is full iff for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) )
set T = incl E;
thus
( incl E is full implies for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) )
( ( for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9) ) 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 )
;
CAT_1:def 26 for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
let a,
b be
Object of
E;
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 A2:
(
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) ) )
Hom (
a,
b)
c= Hom (
a9,
b9)
by A2, Def4;
hence
(
x in Hom (
a,
b) implies
x in Hom (
a9,
b9) )
;
( x in Hom (a9,b9) implies x in Hom (a,b) )assume A3:
x in Hom (
a9,
b9)
;
x in Hom (a,b)A4:
(
(incl E) . a = a9 &
(incl E) . b = b9 )
by A2, Th10;
then reconsider g =
x as
Morphism of
(incl E) . a,
(incl E) . b by A3, CAT_1:def 5;
consider f being
Morphism of
a,
b such that A5:
g = (incl E) . f
by A1, A4, A3;
A6:
g = f
by A5, FUNCT_1:18;
Hom (
a,
b)
<> {}
by A1, A4, A3;
hence
x in Hom (
a,
b)
by A6, CAT_1:def 5;
verum end;
hence
Hom (
a,
b)
= Hom (
a9,
b9)
by TARSKI:2;
verum
end;
assume A7:
for a, b being Object of E
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) = Hom (a9,b9)
; incl E is full
let a, b be Object of E; CAT_1:def 26 ( 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 A8:
Hom (((incl E) . a),((incl E) . b)) <> {}
; 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; ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st g = (incl E) . b1 )
A9:
g in Hom (((incl E) . a),((incl E) . b))
by A8, CAT_1:def 5;
A10:
( a = (incl E) . a & b = (incl E) . b )
by Th10;
hence
Hom (a,b) <> {}
by A7, A8; ex b1 being Morphism of a,b st g = (incl E) . b1
Hom (a,b) = Hom (((incl E) . a),((incl E) . b))
by A7, A10;
then reconsider f = g as Morphism of a,b by A9, CAT_1:def 5;
take
f
; g = (incl E) . f
thus
g = (incl E) . f
by FUNCT_1:18; verum