pOpcycles_comp_fromLeftDerivedZero'

English

The app component of leftDerived for a morphism f is computed via descent through the projective resolutions.

Русский

Компонента app у leftDerived для морфизма f вычисляется через спад через проективные разрешения.

LaTeX

$$$ (\text{NatTrans.leftDerived } \alpha n).app X = \cdots$$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_comp_fromLeftDerivedZero' {C} [Category C] [Abelian C] {X : C} (P : ProjectiveResolution X)
    (F : C ⥤ D) [F.Additive] : HomologicalComplex.pOpcycles _ _ ≫ P.fromLeftDerivedZero' F = F.map (P.π.f 0) := by
  simp [fromLeftDerivedZero']

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