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.

source

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.

source

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.

See FormallyUnramified.hom_ext and FormallyUnramified.of_hom_ext for the infinitesimal lifting criterion.

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

Instances

source

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

source

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.

source

@[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.

source

instance AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified :

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

source

instance AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme :

CategoryTheory.MorphismProperty.IsStableUnderComposition @FormallyUnramified

source

@[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.

source

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

FormallyUnramified f

source

instance AlgebraicGeometry.FormallyUnramified.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @FormallyUnramified

source

instance AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @FormallyUnramified

source

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.

source

theorem AlgebraicGeometry.FormallyUnramified.stalkMap {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] (x : ↥X) :

(CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallyUnramified

source

instance AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f] (x : ↥X) :

Algebra.IsSeparable ↑(Y.residueField (f x)) ↑(X.residueField x)

source

theorem AlgebraicGeometry.FormallyUnramified.hom_ext {X Y Z' Z : Scheme} (i : Z' ⟶ Z) (hi : IsNilpotent (Scheme.Hom.ker i)) [IsClosedImmersion i] (f : X ⟶ Y) [FormallyUnramified f] {g₁ g₂ : Z ⟶ X} (hig : CategoryTheory.CategoryStruct.comp i g₁ = CategoryTheory.CategoryStruct.comp i g₂) (hgf : CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f) :

g₁ = g₂

Given any commuting diagram

Z' --→ X
|      |
↓      ↓
Z  --→ Y

With X ⟶ Y formally unramified and Z' ⟶ Z an infinitesimal thickening, there exists at most one arrow Z ⟶ X making the diagram commute.

source

theorem AlgebraicGeometry.FormallyUnramified.of_hom_ext {X Y : Scheme} (f : X ⟶ Y) (H : ∀ (R S : CommRingCat) (φ : R ⟶ S), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ) → RingHom.ker (CommRingCat.Hom.hom φ) ^ 2 = ⊥ → ∀ (g₁ g₂ : Spec R ⟶ X), CategoryTheory.CategoryStruct.comp (Spec.map φ) g₁ = CategoryTheory.CategoryStruct.comp (Spec.map φ) g₂ → CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f → g₁ = g₂) :

FormallyUnramified f

To show that f : X ⟶ Y is formally unramified, it suffices to check for that every following commuting diagram

Spec R --→ X
  |        |
  ↓        ↓
Spec S --→ Y

with S = R/I for some I² = 0, there exists at most one arrow Spec S ⟶ X making the diagram commute.

Documentation

Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Formally unramified morphisms #