φ₁_L₂_f

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f

English

The relation φ₁, L₂.f, and φ₂ satisfy φ₁_L₂_f, i.e., φ₁ ≫ L₂.f = φ₂.

Русский

Соотношение φ₁, L₂.f и φ₂ удовлетворяет φ₁_L₂_f: φ₁ ≫ L₂.f = φ₂.

LaTeX

$$$S.\\phi_1 \\circ S.L_2.f = S.\\phi_2$$$

Lean4

@[reassoc (attr := simp)]
theorem φ₁_L₂_f : S.φ₁ ≫ S.L₂.f = S.φ₂ :=
  S.L₂_exact.lift_f _ _

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

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

Разделы

Аффилиация

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