opEquiv'_symm_add — Mathlib

English

More detailed additivity interaction of opEquiv' on pairs of shifted morphisms; expresses the compatibility with addition.

Русский

Дополнительное свойство совместимости opEquiv' с операцией сложения на парах сдвинутых морфизмов.

LaTeX

$$$$ opEquiv' (n+m) a a'' ⋯ = (opEquiv' m a' a'') ⋯ \\circ (opEquiv' n a a' h) $$$$

Lean4

@[simp]
theorem opEquiv'_symm_add {n a : ℤ} (x y : (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧)) (a' : ℤ) (h : n + a = a') :
    (opEquiv' n a a' h).symm (x + y) = (opEquiv' n a a' h).symm x + (opEquiv' n a a' h).symm y :=
  by
  dsimp [opEquiv']
  erw [opEquiv_symm_add, Iso.homToEquiv_apply, Iso.homToEquiv_apply, Iso.homToEquiv_apply]
  rw [Preadditive.add_comp]
  rfl

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