liftToFinsetLimIso — Mathlib

English

Given a diagram F: Discrete α ⥤ C, the functor liftToFinsetObj F assigns to each finite subset S the product over S of the objects F(x).

Русский

Для диаграммы F: Discrete α ⥤ C функтор liftToFinsetObj F назначает каждому конечному подмножеству S произведение объектов F(x) по x в S.

LaTeX

$$$$ (\mathrm{liftToFinsetObj}F)(S) = \prod^{\wedge}_{x \in S} F(x). $$$$

Lean4

/-- The `liftToFinset` functor, precomposed with forming a colimit, is a coproduct on the original
functor. -/
def liftToFinsetLimIso [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C] [HasLimitsOfShape (Discrete α) C] :
    liftToFinset C α ⋙ lim ≅ lim :=
  NatIso.ofComponents (fun F => Iso.symm <| limit.isoLimitCone (liftToFinsetLimitCone F))
    (fun β => by
      simp only [Functor.comp_obj, lim_obj, Functor.comp_map, lim_map, Iso.symm_hom]
      ext J
      simp [liftToFinset])

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