sheafedSpace_pullback_to_base_isOpenImmersion

English

If f: X → Z and g: Y → Z are open immersions, then the canonical projection limit.π (cospan f g) 1: pullback f g → Z is an open immersion.

Русский

Если f: X → Z и g: Y → Z — открытые вложения, то каноническая проекция limit.π (cospan f g) 1: pullback f g → Z является открытым вложением.

LaTeX

$$$\text{IsOpenImmersion}\left(\lim\limits_{\longleftarrow}(\mathrm{cospan}\, f\, g)\, \mathrm{one}\right).$$$

Lean4

instance sheafedSpace_pullback_to_base_isOpenImmersion [SheafedSpace.IsOpenImmersion g] :
    SheafedSpace.IsOpenImmersion (limit.π (cospan f g) one : pullback f g ⟶ Z) :=
  by
  rw [← limit.w (cospan f g) Hom.inl, cospan_map_inl]
  infer_instance

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