lift_f_fst_v — Mathlib

English

There exists a canonical lift of a pair of cochains to the mapping cone giving a morphism to the cone respecting the inl and inr projections.

Русский

Существует канонический подъём пары когочейн в отображение к конусу так, чтобы он уважал проекции inl и inr.

LaTeX

$$$\text{liftCochain}(φ, α, β, h) : K \to \mathrm{mappingCone}(φ)$ with respecting inl and inr$$

Lean4

@[reassoc (attr := simp)]
theorem lift_f_fst_v (p q : ℤ) (hpq : p + 1 = q) : (lift φ α β eq).f p ≫ (fst φ).1.v p q hpq = α.1.v p q hpq := by
  simp [lift]

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