ofFactorizationData

Mathlib.AlgebraicTopology.ModelCategory.PathObject

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.PathObject.ofFactorizationData

Lean4

/-- A path object for `A` can be obtained from a factorization of the obvious
map `A ⟶ A ⨯ A` as a trivial cofibration followed by a fibration. -/
@[simps]
noncomputable def ofFactorizationData : PathObject A
    where
  P := h.Z
  p₀ := h.p ≫ prod.fst
  p₁ := h.p ≫ prod.snd
  ι := h.i

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

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

Разделы

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

Аффилиация

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