Going down for torsion-free integral algebras

Mathlib proves going down for an integral extension R ⊆ S of an integrally closed domain R when S is a domain (Stacks, Proposition 10.38.7 (00H8)). This file removes the requirement that S be a domain, replacing injectivity of R → S by torsion-freeness of S as an R-module.

A prime Q of S contains a minimal prime 𝔭 of S. Elements of a minimal prime are zero divisors, while torsion-freeness makes the image of every nonzero element of R a non-zero-divisor, so 𝔭 lies over the zero ideal of R. Thus S ⧸ 𝔭 is an integral extension domain of R, Mathlib's theorem applies to it, and primes of S ⧸ 𝔭 pull back to primes of S below Q.

Torsion-freeness cannot be dropped. Over an integrally closed local domain (R, 𝔪) of positive dimension, the finite algebra R × R ⧸ 𝔪 has the prime R × 0 lying over 𝔪, and no smaller prime of R × R ⧸ 𝔪 lies over 0. This is the closed-point factor that finite normal algebras over a local ring must exclude when studying finite étale covers of punctured spectra.

Main results

• Algebra.HasGoingDown.of_isIntegral_of_isTorsionFree: an integral, torsion-free algebra over an integrally closed domain satisfies going down.

References

• Stacks Project, Proposition 10.38.7, going down for integral extensions of a normal domain.

instance Algebra.HasGoingDown.of_isIntegral_of_isTorsionFree {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [IsIntegrallyClosed R] [Algebra.IsIntegral R S] [Module.IsTorsionFree R S] : HasGoingDown R S

An integral algebra S over an integrally closed domain R satisfies going down as soon as S is torsion free as an R-module. This generalizes Stacks, Proposition 10.38.7 (00H8), where S is a domain containing R.