English
There is a canonical isomorphism between liftToFinset precomposed with evaluation on a finite subset I and the whiskering-left diagram precomposed with colim; this aligns the two ways of evaluating the finite-subset construction.
Русский
Существует каноническое изоморфизм между liftToFinset после применения evaluation на I и whiskering-left диаграммой, согласующий способы вычисления конструкций по конечному подмножеству.
LaTeX
$$$$ \mathrm{liftToFinsetEvaluationIso}(I):\; \mathrm{liftToFinset} \circ \mathrm{evaluation} \;=\; (\mathrm{Functor.whiskeringLeft} \circ \mathrm{Discrete.functor}) \circ \mathrm{colim}. $$$$
Lean4
/-- `liftToFinset`, when composed with the evaluation functor, results in the whiskering composed
with `colim`. -/
def liftToFinsetEvaluationIso (I : Finset (Discrete α)) :
liftToFinset C α ⋙ (evaluation _ _).obj ⟨I⟩ ≅
(Functor.whiskeringLeft _ _ _).obj (Discrete.functor (·.val)) ⋙ lim (J := Discrete I) :=
NatIso.ofComponents (fun _ => HasLimit.isoOfNatIso (Discrete.natIso fun _ => Iso.refl _)) fun _ => by dsimp; ext; simp
