isoLeftDerivedObj_inv_naturality — Mathlib

English

The inverse part of the isomorphism in LeftDerivedObj is natural with respect to morphisms between objects with resolutions.

Русский

Обратная часть изоморфизма в LeftDerivedObj естественна по отношению к морфизмам между объектами с разрешениями.

LaTeX

$$$\text{inv_nat}: (P.isoLeftDerivedObj F n)^{-1} \circ (F.leftDerived n).map f = \cdots$$$

Lean4

@[reassoc]
theorem isoLeftDerivedObj_inv_naturality {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
    (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f) (F : C ⥤ D) [F.Additive] (n : ℕ) :
    (P.isoLeftDerivedObj F n).inv ≫ (F.leftDerived n).map f =
      (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ ≫ (Q.isoLeftDerivedObj F n).inv :=
  by
  rw [← cancel_mono (Q.isoLeftDerivedObj F n).hom, assoc, assoc,
    ProjectiveResolution.isoLeftDerivedObj_hom_naturality f P Q φ comm F n, Iso.inv_hom_id_assoc, Iso.inv_hom_id,
    comp_id]

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