rightUnshift_rightShift — Mathlib

English

The two operations rightShift and rightUnshift are inverse to each other on the appropriate Hom-complex: applying rightShift to γ and then rightUnshift returns γ.

Русский

Операции rightShift и rightUnshift образуют взаимно обратные отображения на соответствующем Hom-комплексe: применение rightShift к γ, затем rightUnshift возвращает γ.

LaTeX

$$$\\big(\\gamma.rightShift a n' hn'\\big).rightUnshift n hn' = \\gamma$$$

Lean4

@[simp]
theorem rightUnshift_rightShift (a n' : ℤ) (hn' : n' + a = n) : (γ.rightShift a n' hn').rightUnshift n hn' = γ :=
  by
  ext p q hpq
  simp only [rightUnshift_v _ n hn' p q hpq (p + n') rfl, γ.rightShift_v _ _ hn' p (p + n') rfl q hpq,
    shiftFunctorObjXIso, assoc, Iso.inv_hom_id, comp_id]

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