forgetMapIsOpenImmersion — Mathlib

English

If f is an open immersion between sheafed spaces, then the induced map on presheafed spaces obtained by forgetting the extra structure is also an open immersion.

Русский

Если f — открытое вложение между пространства сохраняющих слои, то порождаемое отображение на пространстве без учёта дополнительной структуры также является открытым вложением.

LaTeX

$$$\\operatorname{IsOpenImmersion}(((\\mathrm{forget}).map\\ f))$$$

Lean4

instance forgetMapIsOpenImmersion : PresheafedSpace.IsOpenImmersion ((forget).map f) :=
  ⟨H.base_open, H.c_iso⟩

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