hasCoproducts_of_finite_and_filtered

English

A compatibility identity holds between the canonical injections and the colimit maps for the lifted finite-subset diagram; this is a technical auxiliary equality used to build a natural isomorphism with colimits.

Русский

Справедлива совместимая тождественность между каноническими включениями и колимитными отображениями для диаграммы, поднятой до конечного подмножества; служит вспомогательным равенством для построения натуральной изоморфности с колимитом.

LaTeX

$$$$ \Sigma.ι(F)j \;;\; \mathrm{colimit.ι}(\mathrm{liftToFinsetObj}F) \;;\; (\mathrm{colimit.isoColimitCocone}(\mathrm{liftToFinsetColimitCocone}F))^{-1} \;=\; \mathrm{colimit.ι}Fj. $$$$

Lean4

theorem hasCoproducts_of_finite_and_filtered [HasFiniteCoproducts C] [HasFilteredColimitsOfSize.{w, w} C] :
    HasCoproducts.{w} C := fun α => by classical exact ⟨fun F => HasColimit.mk (liftToFinsetColimitCocone F)⟩

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