liftToFinsetEvaluationIso — Mathlib

English

The liftToFinset functor, after evaluation on a finite subset I, is naturally isomorphic to whiskeringLeft with a discrete functor, followed by a colimit.

Русский

Функтор liftToFinset после применения Evaluation на фиксированном подмножестве I естественным образом изоморфен к whiskeringLeft на дискретном функторе и затем к колимиту.

LaTeX

$$$$ \mathrm{liftToFinsetEvaluationIso}(I): \mathrm{liftToFinset}\,C\,\alpha \;;\; \mathrm{evaluation}_{\_} \; \Rightarrow \; (\mathrm{Functor.whiskeringLeft}\,\_\,\_.\_)\; \circ \mathrm{lim}. $$$$

Lean4

/-- `liftToFinset`, when composed with the evaluation functor, results in the whiskering composed
with `colim`. -/
def liftToFinsetEvaluationIso [HasFiniteCoproducts C] (I : Finset (Discrete α)) :
    liftToFinset C α ⋙ (evaluation _ _).obj I ≅
      (Functor.whiskeringLeft _ _ _).obj (Discrete.functor (·.val)) ⋙ colim (J := Discrete I) :=
  NatIso.ofComponents (fun _ => HasColimit.isoOfNatIso (Discrete.natIso fun _ => Iso.refl _)) fun _ => by dsimp; ext;
    simp

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