English
There is a natural isomorphism between liftToFinset composed with colim and colim itself, exhibiting that forming a colimit commutes with lifting to finite subsets.
Русский
Существует естественное изоморфизм между liftToFinset ∘ colim и colim, что показывает совместимость образования колимита с подъёмом к конечным подмножествам.
LaTeX
$$$$ \mathrm{liftToFinsetColimIso}: \mathrm{liftToFinset} \circ \mathrm{colim} \;\cong\; \mathrm{colim}. $$$$
Lean4
/-- The `liftToFinset` functor, precomposed with forming a colimit, is a coproduct on the original
functor. -/
def liftToFinsetColimIso : liftToFinset C α ⋙ colim ≅ colim :=
NatIso.ofComponents (fun F => Iso.symm <| colimit.isoColimitCocone (liftToFinsetColimitCocone F))
(fun β => by
simp only [Functor.comp_obj, colim_obj, Functor.comp_map, colim_map, Iso.symm_hom]
ext J
simp only [liftToFinset_obj_obj]
ext j
simp only [liftToFinset, ι_colimMap_assoc, liftToFinsetObj_obj, Discrete.functor_obj_eq_as, Discrete.natTrans_app,
liftToFinsetColimIso_aux, liftToFinsetColimIso_aux_assoc, ι_colimMap])
