Formally unramified morphisms

A morphism of schemes f : X ⟶ Y is formally unramified if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is formally unramified.

We show that these properties are local, and are stable under compositions and base change.

instance Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [FormallyUnramified R S] [EssFiniteType R S] : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (TensorProduct.lmul' R).toRingHom))

If S is a formally unramified R-algebra, essentially of finite type, the diagonal is an open immersion.

class AlgebraicGeometry.FormallyUnramified {X Y : Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes f : X ⟶ Y is formally unramified if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is formally unramified.

• formallyUnramified_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified

theorem AlgebraicGeometry.formallyUnramified_iff {X Y : Scheme} (f : X ⟶ Y) : FormallyUnramified f ↔ ∀ {U : Y.Opens}, IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified

theorem AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE {X Y : Scheme} (f : X ⟶ Y) [self : FormallyUnramified f] {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (appLE f U V e)).FormallyUnramified

Alias of AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE.

@[deprecated AlgebraicGeometry.Scheme.Hom.formallyUnramified_appLE (since := "2026-01-20")]

theorem AlgebraicGeometry.FormallyUnramified.formallyUnramified_of_affine_subset {X Y : Scheme} (f : X ⟶ Y) [self : FormallyUnramified f] {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified

Alias of AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE.

---

Alias of AlgebraicGeometry.FormallyUnramified.formallyUnramified_appLE.

instance AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified : HasRingHomProperty @FormallyUnramified fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FormallyUnramified

instance AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @FormallyUnramified

@[instance 900]

instance AlgebraicGeometry.FormallyUnramified.instOfIsOpenImmersionDiagonalScheme {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)] : FormallyUnramified f

f : X ⟶ S is formally unramified if X ⟶ X ×ₛ X is an open immersion. In particular, monomorphisms (e.g. immersions) are formally unramified. The converse is true if f is locally of finite type.

theorem AlgebraicGeometry.FormallyUnramified.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [FormallyUnramified (CategoryTheory.CategoryStruct.comp f g)] : FormallyUnramified f

instance AlgebraicGeometry.FormallyUnramified.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @FormallyUnramified

instance AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @FormallyUnramified

instance AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f] : IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)

The diagonal of a formally unramified morphism of finite type is an open immersion.