Purity for finite flat algebras

For a finite free algebra over a Noetherian ring, étaleness is detected on the fibres over primes of height at most one: a nonunit discriminant belongs to such a prime by Krull's principal ideal theorem. Consequently, over a Noetherian local ring of dimension at least two, a finite flat algebra which is unramified away from the closed point is étale everywhere.

The last statement supplies the discriminant step in local purity arguments after flatness has been established. It requires neither regularity nor normality of the base or the algebra. Flatness is essential; this statement does not assert that arbitrary finite covers of a punctured spectrum extend.

Main results

• TauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one: the fibre criterion for a finite free algebra over a Noetherian ring.
• TauCeti.Algebra.etale_of_isUnramifiedAt_of_two_le_ringKrullDim: a finite flat algebra over a Noetherian local ring of dimension at least two is étale if it is unramified at all primes not lying over the closed point.

References

• The Stacks Project, Lemma 58.21.3, the discriminant argument after establishing flatness in dimension two.
• The Stacks Project, Lemma 49.3.1, the discriminant criterion for étaleness.

theorem TauCeti.Algebra.etale_iff_etale_fiber_of_height_le_one {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsNoetherianRing A] [Module.Finite A B] [Module.Free A B] : Algebra.Etale A B ↔ ∀ (p : Ideal A) [inst : p.IsPrime], p.height ≤ 1 → Algebra.Etale p.ResidueField (p.Fiber B)

A finite free algebra over a Noetherian ring is étale if and only if its fibres over all primes of height at most one are étale. Minimal primes must be included; no generic étaleness assumption is imposed.

theorem TauCeti.Algebra.etale_of_isUnramifiedAt_of_two_le_ringKrullDim {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] [IsNoetherianRing A] [IsLocalRing A] [Module.Finite A B] [Module.Flat A B] (hdim : 2 ≤ ringKrullDim A) (h : ∀ (q : Ideal B) [inst : q.IsPrime], Ideal.under A q ≠ IsLocalRing.maximalIdeal A → Algebra.IsUnramifiedAt A q) : Algebra.Etale A B

A finite flat algebra over a Noetherian local ring of dimension at least two is étale everywhere if it is unramified at each prime not lying over the closed point. This is the finite flat case of local purity, with no regularity or normality assumptions.