Documentation

TauCeti.RingTheory.Unramified.Normal

Unramified algebras over a normal base #

Let R be a Noetherian ring, S a finite type R-algebra and q a prime of S over p, at which S is unramified over R. If R_p is a normal domain and q has height at least that of p, then S is étale over R at q. Compare SGA 1, Exposé I, Théorème 9.5 (ii), on unramified morphisms to a normal scheme; here the hypothesis is a comparison of dimensions. It shows that the unramified points of a dominant morphism of integral schemes, locally of finite type over a locally Noetherian normal scheme, are étale, without purity of the branch locus. Since unramifiedness at q already forces ht q ≤ ht p (Ideal.height_le_height_of_quasiFiniteAt), the height condition says that the two heights agree.

Over a Noetherian integrally closed domain R which is not a field, an integral torsion-free algebra of essentially finite type that is unramified at its primes of height one is also unramified at its primes of height zero. Height-zero primes are the generic points of Spec S; each is a generization of a height-one prime, so the hypothesis of purity of the branch locus (Stacks, Lemma 58.21.4 (0BMB)), which only constrains codimension-one points, extends to them.

Proof #

By the local structure of unramified algebras (Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn), there are f ∉ q and a standard étale R-algebra A with a surjection A → S_f. Let Q be the prime of A under q. The induced map A_Q → S_q is surjective. As A is étale over R and R_p is a normal domain, A_Q is a (normal) domain (Stacks, Lemma 10.163.9 (033C)), and ht Q ≤ ht p ≤ ht q because A is quasi-finite over R. A surjection from a domain of finite dimension onto a ring of at least the same dimension is injective (RingHom.injective_of_surjective_of_ringKrullDim_le), so S_q ≅ A_Q is formally étale over R.

Main results #

References #

Unramified algebras over a normal base of the same dimension are étale (compare SGA 1, Exposé I, Théorème 9.5 (ii)). Let S be a finite type algebra over a Noetherian ring R, unramified at a prime q over p. If R_p is a normal domain and ht p ≤ ht q, then S is étale over R at q.

theorem Algebra.IsUnramifiedAt.of_forall_height_eq_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [IsNoetherianRing R] [Algebra.IsIntegral R S] [Module.IsTorsionFree R S] [EssFiniteType R S] (hR : ¬IsField R) (h : ∀ (Q : Ideal S) [inst : Q.IsPrime], Q.height = 1 → IsUnramifiedAt R Q) (q : Ideal S) [q.IsPrime] (hq : q.height ≤ 1) :

Let S be an integral, torsion-free algebra of essentially finite type over a Noetherian integrally closed domain R which is not a field. If S is unramified over R at every prime of height one, then it is unramified over R at every prime of height at most one.