LeftHomotopy

Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.Cylinder.LeftHomotopy

Lean4

/-- Given a cylinder `P` for `X`, two maps `f` and `g` in `X ⟶ Y`
are homotopic relative to `P` when there is a morphism `h : P.I ⟶ Y`
such that `P.i₀ ≫ h = f` and `P.i₁ ≫ h = g`. -/
abbrev LeftHomotopy [CategoryWithWeakEquivalences C] (P : Cylinder X) (f g : X ⟶ Y) : Type v :=
  P.toPrecylinder.LeftHomotopy f g

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

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

Разделы

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

Аффилиация

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