English
There is a compatibility between liftCochain φ α β h and the cocycle lifting described by liftCocycle, i.e., the following equation holds: liftCochain φ α β h composed with the cofibre projection equals liftCochain φ α β h.
Русский
Существует совместимость liftCochain φ α β h с сопряжённым подъемом, описанным liftCocycle: выполняется соответствующее равенство композиции.
LaTeX
$$$\text{liftCochain}(φ, α, β, h) \text{ and } \text{liftCocycle}(φ, α, β, h) \text{ agree under projection}$$$
Lean4
/-- Given `φ : F ⟶ G`, this is the cocycle in `Cocycle K (mappingCone φ) n` that is
constructed from `α : Cochain K F m` (with `n + 1 = m`) and `β : Cocycle K G n`,
when a suitable cocycle relation is satisfied. -/
@[simps!]
noncomputable def liftCocycle {K : CochainComplex C ℤ} {n m : ℤ} (α : Cocycle K F m) (β : Cochain K G n) (h : n + 1 = m)
(eq : δ n m β + α.1.comp (Cochain.ofHom φ) (add_zero m) = 0) : Cocycle K (mappingCone φ) n :=
Cocycle.mk (liftCochain φ α β h) m h
(by simp only [δ_liftCochain φ α β h (m + 1) rfl, eq, Cocycle.δ_eq_zero, Cochain.zero_comp, neg_zero, add_zero])
