desc

Mathlib.AlgebraicTopology.SimplicialObject.Split

URI: https://scilib.ai/kg/mathlib#SimplicialObject.Splitting.desc

Lean4

/-- The map `X.obj Δ ⟶ Z` obtained by providing a family of morphisms on all the
terms of decomposition given by a splitting `s : Splitting X` -/
def desc {Z : C} (Δ : SimplexCategoryᵒᵖ) (F : ∀ A : IndexSet Δ, s.N A.1.unop.len ⟶ Z) : X.obj Δ ⟶ Z :=
  Cofan.IsColimit.desc (s.isColimit Δ) F

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

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

Разделы

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

Аффилиация

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