rightShift_rightUnshift — Mathlib

English

Similarly, leftUnshift and leftShift are inverse to each other on the appropriate Hom-complexes: applying leftShift then leftUnshift yields the original cochain.

Русский

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

LaTeX

$$$\\big(\\gamma.leftShift a n' hn').leftUnshift n hn' = \\gamma$$$

Lean4

@[simp]
theorem rightShift_rightUnshift {a n' : ℤ} (γ : Cochain K (L⟦a⟧) n') (n : ℤ) (hn' : n' + a = n) :
    (γ.rightUnshift n hn').rightShift a n' hn' = γ := by
  ext p q hpq
  simp only [(γ.rightUnshift n hn').rightShift_v a n' hn' p q hpq (p + n) rfl,
    γ.rightUnshift_v n hn' p (p + n) rfl q hpq, shiftFunctorObjXIso, assoc, Iso.hom_inv_id, comp_id]

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