id_comp — Mathlib

English

For any n, and any n-graded cochain z2 from F to G, composing z2 with the image of the identity on F yields z2 itself: (Cochain.ofHom(Id_F)) ∘ z2 = z2.

Русский

Пусть для заданного n‑града коцепи z2: F ⟶ G, тогда композиция с образом Id_F даёт тот же z2: (Cochain.ofHom(Id_F)) ∘ z2 = z2.

LaTeX

$$$\\forall n, \\forall z_2 \\in Cochain F G n, \\ (Cochain.ofHom(\\\\mathrm{id}_F))\\\\circ z_2 \\\\; (zero\_add\; n) = z_2.$$$

Lean4

@[simp]
protected theorem id_comp {n : ℤ} (z₂ : Cochain F G n) : (Cochain.ofHom (𝟙 F)).comp z₂ (zero_add n) = z₂ :=
  by
  ext p q hpq
  simp only [zero_cochain_comp_v, ofHom_v, HomologicalComplex.id_f, id_comp]

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