The fibre criterion for formal unramifiedness, and equalizers

A morphism locally of finite type is formally unramified exactly when its residue-field fibres are formally unramified. Thus relative unramifiedness can be established by calculations over fields, even over a nonreduced or nonnoetherian base and without flatness.

The affine case uses Algebra.FormallyUnramified.of_formallyUnramified_baseChange_field. The passage between arbitrary field-valued points and residue-field fibres uses Mathlib's factorization of a field-valued point through the residue field of its image.

Dually to Mathlib's isClosedImmersion_equalizer_ι_left for separated targets, the equalizer of two morphisms over S into a scheme formally unramified and locally of finite type over S is an open subscheme of their source (isOpenImmersion_equalizer_ι_left): it is a base change of the diagonal, which is an open immersion by Mathlib's FormallyUnramified.isOpenImmersion_diagonal. In particular two sections of an unramified morphism agree on an open subscheme, and two morphisms into an unramified scheme that agree after a surjective morphism are equal (ext_of_surjective_of_formallyUnramified).

If the target is also separated, two morphisms that agree after a dominant morphism are equal (ext_of_isDominant_of_isSeparated_of_formallyUnramified). Unlike Mathlib's ext_of_isDominant_of_isSeparated, whose equalizer argument this follows, this does not require a reduced source: the equalizer is open as well as closed.

For the same reason, a morphism formally unramified and locally of finite type is a monomorphism exactly when it is universally injective (AlgebraicGeometry.FormallyUnramified.mono_iff_universallyInjective): its diagonal is an open immersion, which is an isomorphism exactly when it is surjective.

References

• The Stacks Project, Tag 02G8 (the fibre criterion for unramified morphisms).
• The Stacks Project, Tag 05VH (an unramified universally injective morphism is a monomorphism).

theorem AlgebraicGeometry.Scheme.Hom.formallyUnramified_of_formallyUnramified_baseChange_field {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] (h : ∀ (K : Type u) [inst : Field K] (s : Spec ↧K ⟶ Y), FormallyUnramified (CategoryTheory.Limits.pullback.snd f s)) : FormallyUnramified f

A morphism locally of finite type is formally unramified if its base change along every field-valued point of the target is formally unramified.

theorem AlgebraicGeometry.FormallyUnramified.of_formallyUnramified_fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] (h : ∀ (y : ↥Y), FormallyUnramified (Scheme.Hom.fiberToSpecResidueField f y)) : FormallyUnramified f

A morphism locally of finite type is formally unramified if all its residue-field fibres are formally unramified.

theorem AlgebraicGeometry.FormallyUnramified.iff_formallyUnramified_fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] : FormallyUnramified f ↔ ∀ (y : ↥Y), FormallyUnramified (Scheme.Hom.fiberToSpecResidueField f y)

A morphism locally of finite type is formally unramified exactly when all its residue-field fibres are formally unramified.

instance AlgebraicGeometry.isOpenImmersion_equalizer_ι_left {S : Scheme} {X Y : CategoryTheory.Over S} [FormallyUnramified Y.hom] [LocallyOfFiniteType Y.hom] (f g : X ⟶ Y) : IsOpenImmersion (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.equalizer.ι f g))

Equalizers into an unramified scheme are open. If Y is formally unramified and locally of finite type over S, the equalizer of two morphisms X ⟶ Y over S is an open subscheme of X: it is the base change of the diagonal of Y ⟶ S, which is an open immersion.

theorem AlgebraicGeometry.ext_of_isDominant_of_isSeparated_of_formallyUnramified {X Y W Z : Scheme} {f g : X ⟶ Y} (s : Y ⟶ Z) [IsSeparated s] [FormallyUnramified s] [LocallyOfFiniteType s] (h : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.comp g s) (ι : W ⟶ X) [IsDominant ι] (hU : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) : f = g

Morphisms into a separated unramified scheme agree if they agree after precomposition with a dominant morphism. The source may be nonreduced.

theorem AlgebraicGeometry.ext_of_surjective_of_formallyUnramified {X Y W Z : Scheme} {f g : X ⟶ Y} (s : Y ⟶ Z) [FormallyUnramified s] [LocallyOfFiniteType s] (h : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.comp g s) (ι : W ⟶ X) [Surjective ι] (hU : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) : f = g

Morphisms into an unramified scheme agree if they agree after precomposition with a surjective morphism. Neither a reduced source nor a separated target is needed.

theorem AlgebraicGeometry.FormallyUnramified.mono_iff_universallyInjective {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f] : CategoryTheory.Mono f ↔ UniversallyInjective f

An unramified morphism is a monomorphism exactly when it is universally injective. Stacks, Tag 05VH.