mapProjectiveResolution — Mathlib

Lean4

/-- An additive functor `F` which preserves homology and sends projective objects to projective
objects sends a projective resolution of `Z` to a projective resolution of `F.obj Z`. -/
@[simps complex π]
noncomputable def mapProjectiveResolution (F : C ⥤ D) [F.Additive] [F.PreservesProjectiveObjects] [F.PreservesHomology]
    {Z : C} (P : ProjectiveResolution Z) : ProjectiveResolution (F.obj Z)
    where
  complex := (F.mapHomologicalComplex _).obj P.complex
  projective n := PreservesProjectiveObjects.projective_obj (P.projective n)
  π := (F.mapHomologicalComplex _).map P.π ≫ (HomologicalComplex.singleMapHomologicalComplex _ _ _).hom.app _
  quasiIso := inferInstance

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