cochain_ofHom_homOf_eq_coe — Mathlib

English

For a 0-cocycle z, the associated Cochain obtained via homOf then through Cochain.ofHom matches the underlying Cochain component: Cochain.ofHom(homOf z) = (z : Cochain F G 0).

Русский

Для 0-коцикла z соответствующая кокцикл через homOf и затем Cochain.ofHom совпадает с базовым компонентом Cochain: Cochain.ofHom(homOf z) = (z : Cochain F G 0).

LaTeX

$$$\\operatorname{Cochain.ofHom}(\\operatorname{homOf}(z)) = (z : \\operatorname{Cochain} F G 0).$$$

Lean4

@[simp]
theorem cochain_ofHom_homOf_eq_coe (z : Cocycle F G 0) : Cochain.ofHom (homOf z) = (z : Cochain F G 0) := by
  simpa only [Cocycle.ext_iff] using ofHom_homOf_eq_self z

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