shift_shift_neg' — Mathlib

English

Shifting by i and then by -i is naturally isomorphic to the identity; the natural isomorphism is given by the shiftFunctorCompIsoId between the composed shifts.

Русский

Сдвиг на i затем на -i естественным образом изоморфен тождению; естественное изоморование задаётся через shiftFunctorCompIsoId.

LaTeX

$$$ f \\mapsto (\\mathrm{shiftFunctorCompIsoId} \\ C \\ i \\ (-i) \\ (\\mathrm{add\\_cancel}\\ i)).hom.app X \\;\\; : \\; X \\to X $$$

Lean4

theorem shift_shift_neg' (i : A) :
    f⟦i⟧'⟦-i⟧' =
      (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)).hom.app X ≫
        f ≫ (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)).inv.app Y :=
  (NatIso.naturality_2 (shiftFunctorCompIsoId C i (-i) (add_neg_cancel i)) f).symm

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