English
The equivalence between K.sections (sections of a functor K: J ⥤ Type) and (K ⋙ uliftFunctor).sections provides a bridge to carry limits across large index categories via ulift.
Русский
Эквивалентность между K.sections и (K ⋙ uliftFunctor).sections обеспечивает переход лимитов через крупные индексовые категории с помощью ulift.
LaTeX
$$$ \text{sectionsEquiv} {J} [\text{Category } J] (K : J \to \mathbf{Type}) : K.sections \simeq (K \circ \mathrm{uliftFunctor}).sections. $$$
Lean4
/-- The equivalence between `K.sections` and `(K ⋙ uliftFunctor.{v, u}).sections`. This is used to show
that `uliftFunctor` preserves limits that are potentially too large to exist in the source
category.
-/
def sectionsEquiv {J : Type*} [Category J] (K : J ⥤ Type u) : K.sections ≃ (K ⋙ uliftFunctor.{v, u}).sections
where
toFun := fun ⟨u, hu⟩ => ⟨fun j => ⟨u j⟩, fun f => by simp [hu f]⟩
invFun := fun ⟨u, hu⟩ => ⟨fun j => (u j).down, @fun j j' f => by simp [← hu f]⟩
