isoRightDerivedObj_inv_naturality

English

Naturality of the inverse part of the isomorphism between right-derived objects under morphisms f.

Русский

Естественность обратной части изоморфизма между правыми производными по отображениям f.

LaTeX

$$$ (I.isoRightDerivedObj F n).inv \\; \\cdot \\; F.rightDerived n .map f = \\cdots$$$

Lean4

@[reassoc]
theorem isoRightDerivedObj_inv_naturality {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y)
    (φ : I.cocomplex ⟶ J.cocomplex) (comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0) (F : C ⥤ D) [F.Additive] (n : ℕ) :
    (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f =
      (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ ≫ (J.isoRightDerivedObj F n).inv :=
  by
  rw [← cancel_mono (J.isoRightDerivedObj F n).hom, assoc, assoc,
    InjectiveResolution.isoRightDerivedObj_hom_naturality f I J φ comm F n, Iso.inv_hom_id_assoc, Iso.inv_hom_id,
    comp_id]

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