shiftFunctorCompIsoId_zero_zero_hom_app

English

Special case of the shiftFunctorCompIsoId with zero shifts: the hom component equals the composition of the shiftFunctorZero at X and X with the identity.

Русский

Особый случай сдвигов нулевых: гом-компонента равна композиции shiftFunctorZero на X и X с тождеством.

LaTeX

$$$ (\\mathrm{shiftFunctorCompIsoId} \\ C 0 0 (\\mathrm{add_zero} 0)).hom.app X = ((\\mathrm{shiftFunctorZero} \\ C A).hom.app X) \\langle 0 \\rangle' \\gg (\\mathrm{shiftFunctorZero} \\ C A).hom.app X $$$

Lean4

theorem shiftFunctorCompIsoId_zero_zero_hom_app (X : C) :
    (shiftFunctorCompIsoId C 0 0 (add_zero 0)).hom.app X =
      ((shiftFunctorZero C A).hom.app X)⟦0⟧' ≫ (shiftFunctorZero C A).hom.app X :=
  by simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_inv_app]

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