Lean4
/-- “Divide” a functor by a faithful functor. -/
protected def div (F : C ⥤ E) (G : D ⥤ E) [G.Faithful] (obj : C → D) (h_obj : ∀ X, G.obj (obj X) = F.obj X)
(map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y} {f : X ⟶ Y}, G.map (map f) ≍ F.map f) : C ⥤ D :=
{ obj, map := @map,
map_id := by
intro X
apply G.map_injective
apply eq_of_heq
trans F.map (𝟙 X)
· exact h_map
· rw [F.map_id, G.map_id, h_obj X]
map_comp := by
intro X Y Z f g
refine G.map_injective <| eq_of_heq <| h_map.trans ?_
simp only [Functor.map_comp]
grind }
-- This follows immediately from `Functor.hext` (`Functor.hext h_obj @h_map`),
-- but importing `CategoryTheory.EqToHom` causes an import loop:
-- CategoryTheory.EqToHom → CategoryTheory.Opposites →
-- CategoryTheory.Equivalence → CategoryTheory.FullyFaithful
