snake_lemma — Mathlib

English

Let C be an abelian category and S be a SnakeInput in C. Then the six-term diagram consisting of S.L0.X1, S.L0.X2, S.L0.X3, S.L3.X1, S.L3.X2, S.L3.X3 is exact.

Русский

Пусть C — абелианова категория, и S — SnakeInput в C. Тогда диаграмма из шести объектов S.L0.X1, S.L0.X2, S.L0.X3, S.L3.X1, S.L3.X2, S.L3.X3 является точной.

LaTeX

$$$$ \operatorname{Exact}\bigl(S.L_0.X_1 \to S.L_0.X_2 \to S.L_0.X_3 \to S.L_3.X_1 \to S.L_3.X_2 \to S.L_3.X_3\bigr) $$$$

Lean4

/-- The diagram `S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃` is exact
for any `S : SnakeInput C`. -/
theorem snake_lemma : S.composableArrows.Exact :=
  exact_of_δ₀ S.L₀_exact.exact_toComposableArrows
    (exact_of_δ₀ S.L₁'_exact.exact_toComposableArrows
      (exact_of_δ₀ S.L₂'_exact.exact_toComposableArrows S.L₃_exact.exact_toComposableArrows))

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