liftToFinset — Mathlib

English

The functor sending a functor Discrete α ⥤ C to a functor Finset (Discrete α) ⥤ C is realized by taking coproducts over finite index sets.

Русский

Функтор, отправляющий функтор Discrete α ⥤ C в функтор Finset(Discrete α) ⥤ C, реализуется взятием копроизведений по конечным индексам.

LaTeX

$$$$ \text{liftToFinset} : (\mathrm{Discrete}\; \alpha \; ⥤ \; C) \; ⥤ \; \mathrm{Finset}(\mathrm{Discrete}\; \alpha) \; ⥤ \; 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 _ => Sigma.map (fun x => β.app x.val) }

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