δ_eq' — Mathlib

English

Given A with arrows x3, x2, x1 satisfying compatibility relations with the δ morphism, the δ equality holds: x3 ≫ hS.δ i j hij = x1 ≫ S.X1.homologyπ j.

Русский

Пусть A имеет стрелы x3, x2, x1, удовлетворяющие совместимости с δ-морфизмом; тогда выполняется равенство δ: x3 ≫ hS.δ i j hij = x1 ≫ S.X1.homologyπ j.

LaTeX

$$$x_3 \\;≫\\; hS.\\delta\\; i\\; j\\; hij = x_1 \\;≫\\; S.X_1.homology\\pi\\ j$$$

Lean4

theorem δ_eq' {A : C} (x₃ : A ⟶ S.X₃.homology i) (x₂ : A ⟶ S.X₂.opcycles i) (x₁ : A ⟶ S.X₁.cycles j)
    (h₂ : x₂ ≫ HomologicalComplex.opcyclesMap S.g i = x₃ ≫ S.X₃.homologyι i)
    (h₁ : x₁ ≫ HomologicalComplex.cyclesMap S.f j = x₂ ≫ S.X₂.opcyclesToCycles i j) :
    x₃ ≫ hS.δ i j hij = x₁ ≫ S.X₁.homologyπ j :=
  (snakeInput hS i j hij).δ_eq x₃ x₂ x₁ h₂ h₁

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