comp_cokerπ

Mathlib.Algebra.Category.ModuleCat.Topology.Homology

URI: https://scilib.ai/kg/mathlib#TopModuleCat.comp_cokerπ

English

The composition φ ≫ cokerπ φ equals zero morphism.

Русский

Составление φ ⋙ cokerπ φ равно нулю.

LaTeX

$$$φ \;\circ\; \mathrm{cokerπ}(φ) = 0$$$

Lean4

@[simp]
theorem comp_cokerπ : φ ≫ cokerπ φ = 0 := by
  ext m
  change Submodule.mkQ _ (φ m) = 0
  simp

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

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

Разделы

Аффилиация

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