postcomp

Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.LeftHomotopyClass.postcomp

Lean4

/-- The postcomposition map `LeftHomotopyClass X Y → (Y ⟶ Z) → LeftHomotopyClass X Z`. -/
def postcomp [CategoryWithWeakEquivalences C] : LeftHomotopyClass X Y → (Y ⟶ Z) → LeftHomotopyClass X Z := fun f g ↦
  Quot.lift (fun f ↦ mk (f ≫ g)) (fun _ _ h ↦ sound (h.postcomp g)) f

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

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

Разделы

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

Аффилиация

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