ι₁_π

Mathlib.Algebra.Homology.HomotopyCofiber

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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