L₁_f_φ₁

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁

← MathLib Explorer

English

The sequence L₀.X₂ → L₀.X₃ → L₃.X₁ is exact.

Русский

Последовательность L₀.X₂ → L₀.X₃ → L₃.X₁ точна.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem L₁_f_φ₁ : S.L₀'.f ≫ S.φ₁ = S.v₁₂.τ₁ := by
  dsimp only [L₀']
  simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, φ₂, pullback.lift_fst_assoc, S.v₁₂.comm₁₂]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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