fromLeftDerivedZero' — Mathlib

English

IsIso((ProjectiveResolution.self X).fromLeftDerivedZero' F) for any F; the map is an isomorphism.

Русский

Изоморфизм (ProjectiveResolution.self X).fromLeftDerivedZero' F существует для любого F; отображение изоморфно.

LaTeX

$$$ \text{IsIso}((\text{ProjectiveResolution.self } X).fromLeftDerivedZero' F)$$$

Lean4

/-- If `P : ProjectiveResolution X` and `F` is an additive functor, this is
the canonical morphism from the opcycles in degree `0` of
`(F.mapHomologicalComplex _).obj P.complex` to `F.obj X`. -/
noncomputable def fromLeftDerivedZero' {X : C} (P : ProjectiveResolution X) (F : C ⥤ D) [F.Additive] :
    ((F.mapHomologicalComplex _).obj P.complex).opcycles 0 ⟶ F.obj X :=
  HomologicalComplex.descOpcycles _ (F.map (P.π.f 0)) 1 (by simp)
    (by
      dsimp
      rw [← F.map_comp, complex_d_comp_π_f_zero, F.map_zero])

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