Lean4
/-- Lift a functor `G : J ⥤ D` to the essential image of a fully functor `F : C ⥤ D` to a functor
`G' : J ⥤ C` such that `G' ⋙ F ≅ G`. See `essImage.liftFunctorCompIso`. -/
@[simps]
def liftFunctor : J ⥤ C
where
obj
j :=
F.toEssImage.objPreimage
⟨G.obj j, hG j⟩
-- TODO: `map` isn't type-correct:
-- It conflates `⟨G.obj i, hG i⟩ ⟶ ⟨G.obj j, hG j⟩` and `G.obj i ⟶ G.obj j`.
map {i j}
f :=
F.preimage <|
(F.toEssImage.objObjPreimageIso ⟨G.obj i, hG i⟩).hom ≫
G.map f ≫ (F.toEssImage.objObjPreimageIso ⟨G.obj j, hG j⟩).inv
map_id
i := F.map_injective <| by simpa [-Iso.hom_inv_id] using (F.toEssImage.objObjPreimageIso ⟨G.obj i, hG i⟩).hom_inv_id
map_comp {i j k} f
g :=
F.map_injective <| by
simp only [Functor.map_comp, Category.assoc, Functor.map_preimage]
congr 2
symm
convert
(F.toEssImage.objObjPreimageIso ⟨G.obj j, hG j⟩).inv_hom_id_assoc
(G.map g ≫ (F.toEssImage.objObjPreimageIso ⟨G.obj k, hG k⟩).inv)
