shiftFunctor₁₂CommIso — Mathlib

English

The two shift functors on a bicomplex, shifting in the first and second indices, commute strictly. There is a canonical isomorphism between their successive compositions, and it is the identity in this setting.

Русский

Два сдвига по двум индексам на би-комплексах коммутируют строго: существует каноническое изоморождение между их последовательными композициями, равное тождественному отображению.

LaTeX

$$$\text{shift}_2\,C\ y \;\circ\; \text{shift}_1\,C\ x \;\cong\; \text{shift}_1\,C\ x \;\circ\; \text{shift}_2\,C\ y$$$

Lean4

/-- The shift functors `shiftFunctor₁ C x` and `shiftFunctor₂ C y` on bicomplexes
with respect to both variables commute. -/
def shiftFunctor₁₂CommIso (x y : ℤ) : shiftFunctor₂ C y ⋙ shiftFunctor₁ C x ≅ shiftFunctor₁ C x ⋙ shiftFunctor₂ C y :=
  Iso.refl _

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