rightDerived_id — Mathlib

English

A second formulation of the app-component equality for right-derived natural transformations, via an injective resolution.

Русский

Вторая формулировка равенства компоненты app для правой производной натурального преобразования через инъективное разрешение.

LaTeX

$$$(\\mathrm{rightDerived} \\alpha n).\\mathrm{app}X = (P.isoRightDerivedObj F n).hom \\circ (\\mathrm{mapHomologicalComplex} \\alpha) \\circ (P.isoRightDerivedObj G n)^{-1}$$$

Lean4

@[simp]
theorem rightDerived_id (F : C ⥤ D) [F.Additive] (n : ℕ) : NatTrans.rightDerived (𝟙 F) n = 𝟙 (F.rightDerived n) :=
  by
  dsimp only [rightDerived]
  simp only [rightDerivedToHomotopyCategory_id, Functor.whiskerRight_id']
  rfl

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