English
Given φ: F → G with HasHomotopyCofiber φ, for α: FK(−1) and β: G → K satisfying δ(−1,0) α = Cochain.ofHom(φ ≫ β), there exists a canonical morphism desc φ α β eq: mappingCone φ → K.
Русский
Пусть φ: F → G имеет гомотопическую когерерфактор; для ког-cochain α: F K(−1) и морфизма β: G → K, удовлетворяющих δ(−1,0) α = Cochain.ofHom(φ ≫ β), существует канонический переход desc φ α β eq: mappingCone(φ) → K.
LaTeX
$$$\desc(\phi, \alpha, \beta, \text{eq}) : \mathrm{mappingCone}(\phi) \to K$$$
Lean4
/-- Given `φ : F ⟶ G`, this is the morphism `mappingCone φ ⟶ K` that is constructed
from a cochain `α : Cochain F K (-1)` and a morphism `β : G ⟶ K` such that
`δ (-1) 0 α = Cochain.ofHom (φ ≫ β)`. -/
noncomputable def desc (α : Cochain F K (-1)) (β : G ⟶ K) (eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)) :
mappingCone φ ⟶ K :=
Cocycle.homOf (descCocycle φ α (Cocycle.ofHom β) (neg_add_cancel 1) (by simp [eq]))
