mapHomologicalComplex_commShiftIso_eq

English

The hom component of the commShiftIso for a functor F equals the identity map when specialized to the level of Hom objects, reflecting naturality.

Русский

Гом-компонента commShiftIso для функторa F равна тождественному отображению на уровне Hom-объектов, отражая естественность.

LaTeX

$$$$ \forall F, K, n \ :\ (((F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n).hom.app K).f i = \mathbb{1}.$$$$

Lean4

theorem mapHomologicalComplex_commShiftIso_eq (n : ℤ) :
    (F.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso n = F.mapCochainComplexShiftIso n :=
  rfl

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