instIsEquivalenceShiftFunctor — Mathlib

English

For any i ∈ A, the shift by i is an equivalence of categories, i.e., has a quasi-inverse given by shift by -i.

Русский

Для любого i ∈ A сдвиг на i является эквивалентностью категорий, то есть имеет квазиобратную по отношению к сдвигу на -i.

LaTeX

$$$ (\\mathrm{shiftFunctor} \\ C \\ i).IsEquivalence $$$

Lean4

/-- Shifting by `i` is an equivalence. -/
instance (i : A) : (shiftFunctor C i).IsEquivalence :=
  by
  change (shiftEquiv C i).functor.IsEquivalence
  infer_instance

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