Finiteness of the normalization of a polynomial ring over a field

Let k be a field, P = k[X_1, …, X_r] a polynomial ring in finitely many variables, K its fraction field and L / K a finite field extension. This file proves that the integral closure of P in L is a finite P-module, with no separability hypothesis on L / K. For one variable this is the finiteness of the normalization of k[x] in an algebraic function field: the integral closure of k[x] in a finite extension of k(x) is a finitely generated k[x]-module, including when k is imperfect and the extension is inseparable.

Mathlib's IsIntegralClosure.finite needs L / K separable, since it works through the trace form. The inseparable case is supplied by TauCeti.IsIntegralClosure.finite_mvPolynomial_of_isPurelyInseparable. The two combine through the splitting of a normal extension E / K at the fixed field M = E ^ Aut(E/K): M / K is purely inseparable (TauCeti.IntermediateField.isPurelyInseparable_fixedField_top) and E / M is Galois. The integral closure B of P in M is therefore a finite P-module; it is a Noetherian integrally closed domain with fraction field M, so its integral closure in the separable extension E / M is a finite B-module, and that ring is also the integral closure of P in E. A general L embeds into a normal closure E, and finiteness descends along the embedding because P is Noetherian.

Main results

• TauCeti.IsIntegralClosure.finite_mvPolynomial: the integral closure of a polynomial ring in finitely many variables over a field, in a finite extension of its fraction field, is a finite module.
• TauCeti.IsIntegralClosure.finite_polynomial: the one-variable form over k[X].
• TauCeti.IsIntegralClosure.finite_adjoin_of_transcendental: the same form over the subring k[x] generated by a transcendental element x of a field, with k(x) as fraction field.

References

• Stacks Project, Lemma 10.161.12 (tag 032N) and Lemma 10.161.13 (tag 032O), whose argument (reduce to a normal extension, split it into a purely inseparable and a separable step) is the one followed here for a polynomial ring over a field.

theorem TauCeti.IsIntegralClosure.finite_mvPolynomial (k : Type u_1) [Field k] {σ : Type u_2} [Finite σ] (K : Type u_3) [Field K] [Algebra (MvPolynomial σ k) K] [IsFractionRing (MvPolynomial σ k) K] (L : Type u_4) [Field L] [Algebra K L] [Algebra (MvPolynomial σ k) L] [IsScalarTower (MvPolynomial σ k) K L] [FiniteDimensional K L] (C : Type u_5) [CommRing C] [Algebra (MvPolynomial σ k) C] [Algebra C L] [IsScalarTower (MvPolynomial σ k) C L] [IsIntegralClosure C (MvPolynomial σ k) L] : Module.Finite (MvPolynomial σ k) C

Finiteness of normalization for a polynomial ring over a field. Let P = k[X_1, …, X_r] be a polynomial ring in finitely many variables over a field k, with fraction field K, and let L / K be a finite extension. Then any integral closure C of P in L is a finite P-module. No separability of L / K is assumed.

theorem TauCeti.IsIntegralClosure.finite_polynomial (k : Type u_1) [Field k] (K : Type u_4) [Field K] [Algebra (Polynomial k) K] [IsFractionRing (Polynomial k) K] (L : Type u_5) [Field L] [Algebra K L] [Algebra (Polynomial k) L] [IsScalarTower (Polynomial k) K L] [FiniteDimensional K L] (C : Type u_6) [CommRing C] [Algebra (Polynomial k) C] [Algebra C L] [IsScalarTower (Polynomial k) C L] [IsIntegralClosure C (Polynomial k) L] : Module.Finite (Polynomial k) C

Finiteness of normalization for k[X]: the integral closure of the polynomial ring k[X] over a field k in a finite extension L of its fraction field K is a finite k[X]-module. No separability of L / K is assumed. For K = k(X) and L an algebraic function field this is the finiteness of the normalization of k[x] in L.

theorem TauCeti.IsIntegralClosure.finite_adjoin_of_transcendental (k : Type u_1) [Field k] {E : Type u_4} [Field E] [Algebra k E] {x : E} (hx : Transcendental k x) (L : Type u_5) [Field L] [Algebra (↥k⟮x⟯) L] [Algebra (↥k[x]) L] [IsScalarTower (↥k[x]) (↥k⟮x⟯) L] [FiniteDimensional (↥k⟮x⟯) L] (C : Type u_6) [CommRing C] [Algebra (↥k[x]) C] [Algebra C L] [IsScalarTower (↥k[x]) C L] [IsIntegralClosure C (↥k[x]) L] : Module.Finite (↥k[x]) C

Finiteness of normalization for the subring k[x] generated by an element x of a field E transcendental over k: the integral closure of k[x] in a finite extension L of k(x) = k⟮x⟯ is a finite k[x]-module. No separability of L / k(x) is assumed. When E is an algebraic function field over k, this is the finiteness of the normalization of k[x] in any finite extension of E, with x taken inside E rather than as an abstract variable.