liftCochain_v_snd_v — Mathlib

English

There is a construction of a homotopy between two lift-morphisms to the mapping cone, given γ1, γ2 and the two base equalities h1, h2.

Русский

Существуют конструктор гомотопии между двумя отображениями подъёма в конус отображения, заданными γ1, γ2 и равенствами h1, h2.

LaTeX

$$$\text{LiftHomotopy}(f_1, f_2, γ_1, γ_2, h_1, h_2) ∈ \mathrm{Homotopy}(f_1, f_2)$$$

Lean4

@[reassoc (attr := simp)]
theorem liftCochain_v_snd_v (p₁ p₂ : ℤ) (h₁₂ : p₁ + n = p₂) :
    (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (snd φ).v p₂ p₂ (add_zero p₂) = β.v p₁ p₂ h₁₂ := by
  simpa only [Cochain.comp_v _ _ (add_zero n) p₁ p₂ p₂ h₁₂ (add_zero p₂)] using
    Cochain.congr_v (liftCochain_snd φ α β h) p₁ p₂ (by cutsat)

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