liftToFinsetObj — Mathlib

English

Construction of a colimit cocone for a functor on a finite discrete indexing category, using finite coproducts.

Русский

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

LaTeX

$$liftToFinsetColimitCocone(F)$$

Lean4

/-- If `C` has finite coproducts, a functor `Discrete α ⥤ C` lifts to a functor
`Finset (Discrete α) ⥤ C` by taking coproducts. -/
@[simps!]
def liftToFinsetObj (F : Discrete α ⥤ C) : Finset (Discrete α) ⥤ C
    where
  obj s := ∐ fun x : s => F.obj x
  map {_ Y} h := Sigma.desc fun y => Sigma.ι (fun (x : { x // x ∈ Y }) => F.obj x) ⟨y, h.down.down y.2⟩

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