isOpenImmersion_glueDataObjMap — Mathlib

English

As above, the glueDataObjMap arising from an affine cover is an open immersion.

Русский

Как выше, отображение glueDataObjMap, возникающее из афинного покрытия, является открытым вложением.

LaTeX

$$$ IsOpenImmersion (I.glueDataObjMap \\cdot \\cdots) $$$

Lean4

instance isOpenImmersion_glueDataObjMap {V : X.affineOpens} (f : Γ(X, V.1)) :
    IsOpenImmersion (I.glueDataObjMap (X.affineBasicOpen_le f)) :=
  by
  letI := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra
  have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
  exact IsOpenImmersion.of_isLocalization (Ideal.Quotient.mk _ f)

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