δ — Mathlib · SciLib

English

The map δ_hom is linear over R: δ_hom(z1 + z2) = δ_hom(z1) + δ_hom(z2) and δ_hom(r z) = r δ_hom(z).

Русский

Линейность δ_hom по отношению к R: δ_hom(z1 + z2) = δ_hom(z1) + δ_hom(z2) и δ_hom(r z) = r δ_hom(z).

LaTeX

$$$δ_{hom}: Cochain F G n \\to Cochain F G m \\\\text{ is } R\\-linear, \\\\ δ_{hom}(z_1 + z_2) = δ_{hom}(z_1) + δ_{hom}(z_2), \\\\ δ_{hom}(r z) = r δ_{hom}(z).$$$

Lean4

/-- The differential on the complex of morphisms between cochain complexes. -/
def δ (z : Cochain F G n) : Cochain F G m :=
  Cochain.mk
    (fun p q hpq =>
      z.v p (p + n) rfl ≫ G.d (p + n) q +
        m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q (by rw [hpq, sub_add_cancel]))

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