let C, D be Category; :: thesis: for E being Subcategory of D
for F being Functor of C,D st rng F c= the carrier' of E holds
F is Functor of C,E
let E be Subcategory of D; :: thesis: for F being Functor of C,D st rng F c= the carrier' of E holds
F is Functor of C,E
let F be Functor of C,D; :: thesis: ( rng F c= the carrier' of E implies F is Functor of C,E )
assume A1: rng F c= the carrier' of E ; :: thesis: F is Functor of C,E
A2: dom F = the carrier' of C by FUNCT_2:def 1;
A3: dom (Obj F) = the carrier of C by FUNCT_2:def 1;
reconsider G = F as Function of the carrier' of C, the carrier' of E by A1, A2, FUNCT_2:def 1, RELSET_1:4;
A4: rng (Obj F) c= the carrier of E
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Obj F) or y in the carrier of E )
assume y in rng (Obj F) ; :: thesis: y in the carrier of E
then consider x being object such that
A5: x in dom (Obj F) and
A6: y = (Obj F) . x by FUNCT_1:def 3;
reconsider x = x as Object of C by A5;
F . (id x) = id ((Obj F) . x) by CAT_1:68;
then id ((Obj F) . x) in rng F by A2, FUNCT_1:def 3;
then reconsider f = id ((Obj F) . x) as Morphism of E by A1;
A7: dom (id ((Obj F) . x)) = y by A6;
dom (id ((Obj F) . x)) = dom f by CAT_2:9;
hence y in the carrier of E by A7; :: thesis: verum
end;
A8: now :: thesis: for c being Object of C ex d being Object of E st G . (id c) = id d
let c be Object of C; :: thesis: ex d being Object of E st G . (id c) = id d
(Obj F) . c in rng (Obj F) by A3, FUNCT_1:def 3;
then reconsider d = (Obj F) . c as Object of E by A4;
take d = d; :: thesis: G . (id c) = id d
thus G . (id c) = id ((Obj F) . c) by CAT_1:68
.= id d by CAT_2:def 4 ; :: thesis: verum
end;
A9: now :: thesis: for f being Morphism of C holds
( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) )
let f be Morphism of C; :: thesis: ( G . (id (dom f)) = id (dom (G . f)) & G . (id (cod f)) = id (cod (G . f)) )
A10: dom (F . f) = dom (G . f) by CAT_2:9;
A11: cod (F . f) = cod (G . f) by CAT_2:9;
thus G . (id (dom f)) = id (F . (dom f)) by CAT_1:71
.= id (dom (F . f)) by CAT_1:72
.= id (dom (G . f)) by A10, CAT_2:def 4 ; :: thesis: G . (id (cod f)) = id (cod (G . f))
thus G . (id (cod f)) = id (F . (cod f)) by CAT_1:71
.= id (cod (F . f)) by CAT_1:72
.= id (cod (G . f)) by A11, CAT_2:def 4 ; :: thesis: verum
end;
now :: thesis: for f, g being Morphism of C st dom g = cod f holds
G . (g (*) f) = (G . g) (*) (G . f)
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies G . (g (*) f) = (G . g) (*) (G . f) )
assume A12: dom g = cod f ; :: thesis: G . (g (*) f) = (G . g) (*) (G . f)
then A13: F . (g (*) f) = (F . g) (*) (F . f) by CAT_1:64;
A14: dom (F . g) = cod (F . f) by A12, CAT_1:64;
A15: dom (F . g) = dom (G . g) by CAT_2:9;
cod (F . f) = cod (G . f) by CAT_2:9;
hence G . (g (*) f) = (G . g) (*) (G . f) by A13, A14, A15, CAT_2:11; :: thesis: verum
end;
hence F is Functor of C,E by A8, A9, CAT_1:61; :: thesis: verum