liftCochain_v_fst_v — Mathlib

English

The lift φ α β eq defines a morphism K ⟶ mappingCone φ when δ 0 1 β + α.1 ∘ φ = 0; this is the standard lifting construction in mapping cones.

Русский

Пусть δ 0 1 β + α.1 ∘ φ = 0; тогда lift φ α β eq задаёт отображение K ⟶ mappingCone φ — стандартная конструкция подъёма в конусе отображения.

LaTeX

$$$\text{lift}(\phi, \alpha, \beta, eq) : K \to \mathrm{mappingCone}(\phi)$$$

Lean4

@[reassoc (attr := simp)]
theorem liftCochain_v_fst_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + 1 = p₃) :
    (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (fst φ).1.v p₂ p₃ h₂₃ = α.v p₁ p₃ (by cutsat) := by
  simpa only [Cochain.comp_v _ _ h p₁ p₂ p₃ h₁₂ h₂₃] using Cochain.congr_v (liftCochain_fst φ α β h) p₁ p₃ (by cutsat)

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