mapHomologicalComplex_commShiftIso_inv_app_f

English

The inverse of the commShiftIso when applied to K has its f-coordinate equal to the identity map as well, reflecting the inverse nature.

Русский

Обратный компонент commShiftIso при применении к K имеет f-координату, равную единице.

LaTeX

$$$$ ((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).inv.app K).f i = \mathbb{1}_{K(i+n)}. $$$$

Lean4

@[simp]
theorem mapHomologicalComplex_commShiftIso_inv_app_f (K : CochainComplex C ℤ) (n i : ℤ) :
    (((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).inv.app K).f i = 𝟙 _ :=
  rfl

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