ofFaithful — Mathlib

Lean4
/-- If G : C → D is a faithful functor which sends t to a colimit cocone,
  then it suffices to check that the induced maps for the image of t
  can be lifted to maps of C. -/
def ofFaithful {t : Cocone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [G.Faithful] (ht : IsColimit (mapCocone G t))
    (desc : ∀ s : Cocone F, t.pt ⟶ s.pt) (h : ∀ s, G.map (desc s) = ht.desc (mapCocone G s)) : IsColimit t :=
  { desc
    fac := fun s j => by apply G.map_injective; rw [G.map_comp, h]; apply ht.fac
    uniq := fun s m w => by
      apply G.map_injective; rw [h]
      refine ht.uniq (mapCocone G s) _ fun j => ?_
      convert ← congrArg (fun f => G.map f) (w j)
      apply G.map_comp }
Похожие утверждения