hasShift — Mathlib

English

As a companion to comapEq_symm, for h: f = g we have comapEq C h.symm = (comapEq C h).symm; the symmetry relation is preserved under comapEq.

Русский

Как сопутствующее свойство к comapEq_symm, если h: f = g, то comapEq C h.symm = (comapEq C h).symm; симметрия сохраняется под comapEq.

LaTeX

$$$ comapEq\, C\, h^{\\mathrm{symm}} = (comapEq\, C\, h)^{\\mathrm{symm}} $$$

Lean4

instance hasShift {β : Type*} [AddCommGroup β] (s : β) : HasShift (GradedObjectWithShift s C) ℤ :=
  hasShiftMk _ _
    { F := fun n => comap C fun b : β => b + n • s
      zero := comapEq C (by cat_disch) ≪≫ Pi.comapId β fun _ => C
      add := fun m n =>
        comapEq C (by ext; dsimp; rw [add_comm m n, add_zsmul, add_assoc]) ≪≫ (Pi.comapComp _ _ _).symm }

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