ofHom_desc — Mathlib

English

The morphism obtained by applying Cochain.ofHom to desc φ α β eq equals the cocycle descCochain φ α (Cochain.ofHom β) (−1 + 1).

Русский

Гомоморфизм Cochain.ofHom(desc φ α β eq) равен кокцикл descCochain φ α (Cochain.ofHom β) (−1 + 1).

LaTeX

$$$\operatorname{Cochain.ofHom}(\desc(\phi, \alpha, \beta, eq)) = \descCochain(\phi, \alpha, \operatorname{Cochain.ofHom}(\beta), -1 + 1)$$$

Lean4

@[simp]
theorem ofHom_desc : Cochain.ofHom (desc φ α β eq) = descCochain φ α (Cochain.ofHom β) (neg_add_cancel 1) := by
  simp [desc]

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