English
For a GlueData D, the forgetful functor toTop preserves the colimit of the multispan diagram associated to D.
Русский
Для данных GlueData D, забывающий функтор к Top сохраняет колимит диаграммы многоспана, связанной с D.
LaTeX
$$$\mathrm{PreservesColimit}(D.\mathrm{diagram.multispan}, \mathrm{forgetToTop})$$$
Lean4
instance : PreservesColimit (𝖣.diagram.multispan) forgetToTop :=
inferInstanceAs
(PreservesColimit (𝖣.diagram).multispan
(forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat))
