natTransPInfty_f — Mathlib

English

In degree n, the n-th component of the PInfty natural transformation agrees with PInfty.f n after evaluating at degree n.

Русский

В степени n компонент natTransPInfty_f согласуется с PInfty.f n при вычислении на степени n.

LaTeX

$$$ (\text{natTransPInfty})_n = PInfty.f n $$$

Lean4

/-- The natural transformation in each degree that is induced by `natTransPInfty`. -/
@[simps!]
noncomputable def natTransPInfty_f (n : ℕ) :=
  natTransPInfty C ◫ 𝟙 (HomologicalComplex.eval _ _ n)

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