Detecting formal unramifiedness on field-valued fibres

A finite-type algebra is formally unramified if all its base changes to fields are formally unramified. This criterion passes from fibre computations to relative unramifiedness without requiring flatness or finite presentation.

The proof uses finite generation of Kähler differentials, their base-change equivalence KaehlerDifferential.tensorKaehlerEquivBase, and the residue-field description of module support Module.mem_support_iff_nontrivial_residueField_tensorProduct.

Algebra.IsUnramifiedIn.formallyUnramified_fiber gives the converse comparison at one prime: unramifiedness at every prime over p implies formal unramifiedness of the fibre over p, without a finiteness assumption.

References

• The Stacks Project, Tag 02G8 (the fibre criterion for unramified morphisms).

theorem Algebra.IsUnramifiedIn.formallyUnramified_fiber {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {p : Ideal R} [p.IsPrime] (h : IsUnramifiedIn S p) : FormallyUnramified p.ResidueField (p.Fiber S)

If an algebra is unramified at every prime over p, its fibre over p is formally unramified. No finiteness hypothesis is needed.

theorem Algebra.FormallyUnramified.of_formallyUnramified_baseChange_field {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] [FiniteType R S] (h : ∀ (K : Type v) [inst : Field K] [inst_1 : Algebra R K], FormallyUnramified K (TensorProduct R K S)) : FormallyUnramified R S

A finite-type algebra is formally unramified if every base change to a field is formally unramified. No flatness assumption is required.