refl

Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.LeftHomotopyRel.refl

English

For any morphism f: X → Y in a model category, f is left-homotopic to itself.

Русский

Для любого морфизма f: X → Y в моделирующей категории существует лево-гомотопия между f и самим собой.

LaTeX

$$$ f \sim_L f$$$

Lean4

theorem refl [ModelCategory C] (f : X ⟶ Y) : LeftHomotopyRel f f :=
  ⟨Classical.arbitrary _, ⟨Cylinder.LeftHomotopy.refl _ _⟩⟩

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

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

Разделы

Аффилиация

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