liftCochain — Mathlib

English

Given φ, α, β and a HasHomotopyCofiber φ, the liftCochain φ α β h is a cochain K F m ⟶ mappingCone φ of degree n, assembled from α, β and the morphism φ.

Русский

Пусть φ, α, β и имеет место HasHomotopyCofiber φ; liftCochain φ α β h есть ког-cochain K F m → mappingCone φ степени n, сконструированный из α, β и φ.

LaTeX

$$$\text{liftCochain}(\phi, \alpha, \beta, h) ∈ \mathrm{Cochain}(K, \mathrm{mappingCone}(\phi))_{n}$$$

Lean4

/-- Given `φ : F ⟶ G`, this is the cochain in `Cochain (mappingCone φ) K n` that is
constructed from two cochains `α : Cochain F K m` (with `m + 1 = n`) and `β : Cochain F K n`. -/
noncomputable def liftCochain (α : Cochain K F m) (β : Cochain K G n) (h : n + 1 = m) : Cochain K (mappingCone φ) n :=
  α.comp (inl φ) (by cutsat) + β.comp (Cochain.ofHom (inr φ)) (add_zero n)

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