forgetToPresheafedSpacePreservesOpenImmersion

English

Forgetful functor to Top preserves pullbacks on the left when comparing to open immersions.

Русский

Забывающий функтор к Top сохраняет pullback слева при сравнении с открытыми погружениями.

LaTeX

$$$ \mathrm{forgetToTop_preservesPullback_of_left} \; : \; \mathrm{PreservesLimit}(cospan f g,\; \mathrm{forgetToSheafedSpace}\,\circ\, \mathrm{SheafedSpace.forgetToPresheafedSpace})$$$

Lean4

instance forgetToPresheafedSpacePreservesOpenImmersion :
    PresheafedSpace.IsOpenImmersion
      ((LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f) :=
  H

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