instHasRingHomPropertyFormallyUnramified

English

If R → S is formally unramified and essentially of finite type, then a canonical Spec-map is an open immersion.

Русский

Если R → S формально неразрушаемо и существенно конечного типа, то соответствующее отображение Spec является открытым вложением.

LaTeX

$$$\\text{IsOpenImmersion}(\\Spec.map(\\dots))$ for formally unramified and ess finite type$$

Lean4

instance : HasRingHomProperty (@FormallyUnramified) RingHom.FormallyUnramified
    where
  isLocal_ringHomProperty := RingHom.FormallyUnramified.propertyIsLocal
  eq_affineLocally' := by
    ext X Y f
    rw [formallyUnramified_iff, affineLocally_iff_affineOpens_le]

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