ι₀_π

Mathlib.Algebra.Homology.HomotopyCofiber

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.cylinder.ι₀_π

English

For every cylinder K, the composition of the left inclusion ι0 with the projection π is the identity on K: ι0(K) ≫ π(K) = id_K.

Русский

Для цилиндра K композиция левого включения ι0 с проекцией π даёт тождество на K: ι0(K) ≫ π(K) = id_K.

LaTeX

$$$ι_0 K \circ \pi K = \mathrm{Id}_K$$$

Lean4

@[reassoc (attr := simp)]
theorem ι₀_π : ι₀ K ≫ π K = 𝟙 K := by simp [π]

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

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

Разделы

Аффилиация

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