φ_π

Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.kernelCokernelCompSequence.φ_π

← MathLib Explorer

English

The boundary map is killed by π.

Русский

Граница отображения уничтожается π.

LaTeX

$$φ f g \circ π f g = 0$$

Lean4

@[reassoc (attr := simp)]
theorem φ_π : φ f g ≫ π f g = 0 := by
  dsimp [φ, π]
  ext
  · rw [biprod.inl_desc_assoc, assoc, biprod.inl_desc, comp_zero, ← assoc, cokernel.condition]
  · simp

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

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

Разделы

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

Аффилиация

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