forgetToTop_preserves_of_left — Mathlib

English

If f: X → Z is open immersion and g: Y → Z is open immersion, then the base change of f along g is an open immersion; equivalently, the projection from the pullback is open immersion.

Русский

Если f: X → Z и g: Y → Z — открытые вложения, то базисное изменение вдоль g сохраняет открытое вложение, то есть проекция из петли открыта.

LaTeX

$$$IsOpenImmersion( pullback.fst\, g\, f )$$$

Lean4

instance forgetToTop_preserves_of_left : PreservesLimit (cospan f g) Scheme.forgetToTop :=
  by
  delta Scheme.forgetToTop
  refine
    @Limits.comp_preservesLimit _ _ _ _ _ _ (K := cospan f g) _ _ (F := forget) (G := LocallyRingedSpace.forgetToTop) ?_
      ?_
  · infer_instance
  refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_
  dsimp [LocallyRingedSpace.forgetToTop]
  infer_instance

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