w₀₂_τ₁

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁

English

In a snake diagram, the composition along the first column satisfies w0τ1 = 0.

Русский

В змее, композиция по первому столбцу равна нулю.

LaTeX

$$$S.v_{01}.\tau_1 \circ S.v_{12}.\tau_1 = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem w₀₂_τ₁ : S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0 := by rw [← comp_τ₁, S.w₀₂, zero_τ₁]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru