liftFunctorCompIso — Mathlib

Lean4

/-- A functor `G : J ⥤ D` to the essential image of a fully functor `F : C ⥤ D` does factor through
`essImage.liftFunctor G F hG`. -/
@[simps!]
def liftFunctorCompIso : essImage.liftFunctor G F hG ⋙ F ≅ G :=
  NatIso.ofComponents (fun i ↦ F.essImage.ι.mapIso (F.toEssImage.objObjPreimageIso ⟨G.obj i, hG _⟩)) fun {i j} f ↦
    by
    simp only [Functor.comp_obj, liftFunctor_obj, Functor.comp_map, liftFunctor_map, Functor.map_preimage,
      Functor.mapIso_hom, ObjectProperty.ι_map, Category.assoc]
    congr 1
    convert Category.comp_id _
    exact (F.toEssImage.objObjPreimageIso ⟨G.obj j, hG j⟩).inv_hom_id

Похожие утверждения