shiftZero' — Mathlib

English

The zero-shift functor behaves as the identity up to the standard isomorphisms: shifting by 0 is naturally isomorphic to the identity functor.

Русский

Сдвиг нулём ведёт себя как тождественный переход, то есть сдвиг на 0 естественным образом изоморфен тождественному функтору.

LaTeX

$$$ (\\mathrm{shiftZero} \\, A \\, X).hom = \\mathrm{identity\_up\_to\_isomorphism} $$$

Lean4

theorem shiftZero' : f⟦(0 : A)⟧' = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv :=
  by
  symm
  rw [Iso.app_inv, Iso.app_hom]
  apply NatIso.naturality_2

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