shiftFunctorComm_hom_app_f — Mathlib

English

The hom component of the shift-commutation isomorphism equals the XIsoOfEq hom after simplifying the shift data: shift-commutes with addition of indices.

Русский

Гом-компонента изоморфизма коммутации сдвигов совпадает с гомоморфизмом XIsoOfEq после упрощения данных сдвига.

LaTeX

$$$$ ((\mathrm{shiftFunctorComm}(CochainComplex,\mathbb{Z}) a b).hom.app K).f p = (K.XIsoOfEq (show p + b + a = p + a + b by rw[add_assoc])).hom.$$$$

Lean4

theorem shiftFunctorComm_hom_app_f (K : CochainComplex C ℤ) (a b p : ℤ) :
    ((shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p =
      (K.XIsoOfEq (show p + b + a = p + a + b by rw [add_assoc, add_comm b, add_assoc])).hom :=
  by
  rw [shiftFunctorComm_eq _ _ _ _ rfl]
  dsimp
  rw [shiftFunctorAdd'_inv_app_f', shiftFunctorAdd'_hom_app_f']
  simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans]

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