shiftIso_zero — Mathlib

English

When a = 0, the hom component of shiftIso is the shift by zero transported via shiftFunctor.

Русский

При a = 0 гом-компонента shiftIso совпадает с переносом нулевого сдвига через shiftFunctor.

LaTeX

$$$ (F.shiftIso 0 a a (zero_add a)).hom.app X = (shift F a).map ((shiftFunctorZero C M).hom.app X) $$$

Lean4

theorem shiftIso_zero (a : M) :
    F.shiftIso 0 a a (zero_add a) = isoWhiskerRight (shiftFunctorZero C M) _ ≪≫ leftUnitor _ :=
  ShiftSequence.shiftIso_zero a

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