δ_hom — Mathlib

English

δ(n,m)(0) = 0.

Русский

δ(n,m)(0) = 0.

LaTeX

$$$δ(n,m)(0) = 0$$$

Lean4

/-- The differential on the complex of morphisms between cochain complexes, as a linear map. -/
@[simps!]
def δ_hom : Cochain F G n →ₗ[R] Cochain F G m where
  toFun := δ n m
  map_add' α
    β := by
    by_cases h : n + 1 = m
    · ext p q hpq
      dsimp
      simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.add_v, add_comp, comp_add, smul_add]
      abel
    · simp only [δ_shape _ _ h, add_zero]
  map_smul' r
    a := by
    by_cases h : n + 1 = m
    · ext p q hpq
      dsimp
      simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.smul_v, Linear.comp_smul, Linear.smul_comp, smul_add,
        smul_comm m.negOnePow r]
    · simp only [δ_shape _ _ h, smul_zero]

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