ofHom_homOf_eq_self — Mathlib

English

For any 0-cocycle z in Cocycle F G 0, applying the forward map homOf to z and then back via ofHom recovers z: ofHom(homOf z) = z.

Русский

Для любого нулевого кокцикла z из Cocycle F G 0 применение отображения гомологизма к z (homOf z) и обратное отображение via ofHom восстанавливают z: ofHom(homOf z) = z.

LaTeX

$$$\\forall z \\in \\mathrm{Cocycle}(F,G,0),\\ \\mathrm{ofHom}(\\mathrm{homOf}(z)) = z.$$$

Lean4

@[simp]
theorem ofHom_homOf_eq_self (z : Cocycle F G 0) : ofHom (homOf z) = z := by cat_disch

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