instIsPreimmersionGlueDataObjι — Mathlib

English

For every affine open U, the map glueDataObjι U is a preimmersion, i.e., locally an immersion when restricted appropriately.

Русский

Для каждого афинного открытого набора U отображение glueDataObjι U является предиммерсией, то есть локально — вложением.

LaTeX

$$$ IsPreimmersion (I.glueDataObjι U) $$$

Lean4

instance (U : X.affineOpens) : IsPreimmersion (I.glueDataObjι U) :=
  have : IsPreimmersion (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) :=
    .mk_Spec_map (isClosedEmbedding_comap_of_surjective _ _ Ideal.Quotient.mk_surjective).isEmbedding
      (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
  .comp _ _

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