leftDerived_id — Mathlib

English

The leftDerived of the identity functor is the identity transformation on the leftDerived functors.

Русский

Левый производный от тождественного функторы равен тождественному отображению на левых производных.

LaTeX

$$$\text{NatTrans.leftDerived}(\mathrm{Id}_F) = \mathrm{Id}_{F.leftDerived}$$$

Lean4

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

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