uliftFunctor — Mathlib

English

There is a canonical functor that lifts truncated simplicial sets along a universe change, mapping each truncated k-simplicial set from universe u to universe max(u,v).

Русский

Существует канонический функтор, поднимающий усечённые симпликсальные множества при смене универсума, переводящий каждое усечённое множество размерности k из множества u в множество max(u,v).

LaTeX

$$$ \mathrm{uliftFunctor}_k: \mathrm{SSet.Truncated}_{u} \, k \longrightarrow \mathrm{SSet.Truncated}_{\max(u,v)} \, k $$$

Lean4

/-- The ulift functor `SSet.Truncated.{u} ⥤ SSet.Truncated.{max u v}` on truncated
simplicial sets. -/
def uliftFunctor (k : ℕ) : SSet.Truncated.{u} k ⥤ SSet.Truncated.{max u v} k :=
  (whiskeringRight _ _ _).obj CategoryTheory.uliftFunctor.{v, u}

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