liftToFinset — Mathlib

English

As a consequence of the finite-coproducts and filtered-colimits framework, the global HasColimitsOfSize follows, enabling colimits of small diagrams to exist.

Русский

Следствием ограничений на конечные копроизводы и фильтрованные пределы становится существование колимитов для всех малых диаграмм.

LaTeX

$$$$ \mathrm{has\_colimits\_of\_finite\_and\_filtered} \;:\; [HasFiniteColimits\, C] \to [HasFilteredColimitsOfSize\, {w,w}\, C] \to [HasColimitsOfSize\, {w,w}\, C]. $$$$

Lean4

/-- The functor taking a functor `Discrete α ⥤ C` to a functor `Finset (Discrete α) ⥤ C` by taking
coproducts. -/
@[simps!]
def liftToFinset : (Discrete α ⥤ C) ⥤ ((Finset (Discrete α))ᵒᵖ ⥤ C)
    where
  obj := liftToFinsetObj
  map := fun β => { app := fun _ => Pi.map (fun x => β.app x.val) }

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