trans

Mathlib.AlgebraicTopology.ModelCategory.PathObject

URI: https://scilib.ai/kg/mathlib#HomotopicalAlgebra.PrepathObject.trans

Lean4

/-- The gluing of two pre-path objects. -/
@[simps]
noncomputable def trans (P' : PrepathObject A) [HasPullback P.p₁ P'.p₀] : PrepathObject A
    where
  P := pullback P.p₁ P'.p₀
  p₀ := pullback.fst _ _ ≫ P.p₀
  p₁ := pullback.snd _ _ ≫ P'.p₁
  ι := pullback.lift P.ι P'.ι (by simp)

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

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

Разделы

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

Аффилиация

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