functorality and postcomposition with a faithful functor

1. Proposition

Let 20240104-functorality_and_postcomposition_with_a_faithful_functor_46fb4247bc4923debeebbd99308829d5bbbf0ec7.svg be categories, a functor-candidate and a faithful functor.

TFAE:

is a functor
is a functor

2. Proof

2.1. 1) 2)

follows from composition of functors as functor

2.2. 2) 1)

2.2.1. identity

by assumption, 20240104-functorality_and_postcomposition_with_a_faithful_functor_e349db71bd9830868d480037d6d3d7f63b6b964d.svg . Here since is faithful, there exists a unique morphism such that . Since is a functor, it follows, that and hence it follows, that

2.2.2. composition

faithful functor and preimage as diagram Note that composition is precisely states, that

20240104-functorality_and_postcomposition_with_a_faithful_functor_876ee691e400db6dc0002674d72111ea6d998e13.svg

commutes By assumption

20240104-functorality_and_postcomposition_with_a_faithful_functor_484236801ad5452b800d054faa30c937ab7113cf.svg

commutes, since 20240104-functorality_and_postcomposition_with_a_faithful_functor_fe734f7f8429ef51b71aaef9e4268fc741b1221b.svg is a functor. Furthermore