ofHom_lift — Mathlib

English

There is a compatibility between liftCochain φ α β h and descCochain φ α β' h' under suitable h and h'.

Русский

Существует совместимость liftCochain φ α β h с descCochain φ α β' h' при надлежащих h и h'.

LaTeX

$$$\text{liftCochain}(φ, α, β, h) \circ \text{descCochain}(φ, α', β', h') = \text{descCochain}(φ, α, β', h')$$$

Lean4

@[simp]
theorem ofHom_lift : Cochain.ofHom (lift φ α β eq) = liftCochain φ α β (zero_add 1) := by
  simp only [lift, Cocycle.cochain_ofHom_homOf_eq_coe, liftCocycle_coe]

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