Documentation

TauCeti.RingTheory.IntegralClosure.NormalizationFinite

Krull–Akizuki: an integral closure that is Noetherian without separability #

Let A be a Noetherian domain of Krull dimension at most one, let K be its fraction field and let L be a domain containing A that is a finite-dimensional K-vector space, compatibly with the action of A — for example a finite extension of K. This file proves that any integral closure of A in L is a Noetherian ring. No separability over K is assumed, and the integral closure is not claimed to be a finite A-module — it need not be.

The engine is a length bound. Write aM for the image of multiplication by a on a module M, which is LinearMap.range (LinearMap.lsmul A M a). For a finite-dimensional K-vector space V, an arbitrary A-submodule M ≤ V and a nonzero a : A,

length_A (M ⧸ aM) ≤ dim_K V * ord_A a,

where ord_A a = length_A (A ⧸ aA) is Mathlib's Ring.ord. The right-hand side is finite because the quotient by a nonzero principal ideal of a one-dimensional Noetherian domain has finite length. Applied to M the integral closure sitting inside V = L, this makes C ⧸ aC a Noetherian A-module, which is enough to finitely generate every ideal of C.

Main results #

The general facts about Module.length that the bound rests on — additivity along a filtration, the reduction of a length bound to finitely generated submodules, and the rank-one computation length (I ⧸ aI) = ord_A a for an ideal I — are in TauCeti/RingTheory/Length.lean.

Proof outline #

The bound is proved by induction on n ≥ dim_K U for a K-subspace U containing M, with M finitely generated (length_quotient_lsmul_le_mul_ord_of_finrank_le); TauCeti.length_quotient_lsmul_le_of_forall_fg then removes the finite generation. The inductive step runs on the projection e = id - φ(·) • x for a functional φ with φ x = 1, supplied by Mathlib's Module.Projective.exists_dual_eq_one; Module.Dual.ker_id_sub_smulRight and Module.Dual.finrank_ker_inf_add_one compute its kernel and the dimension it removes. Filtration additivity splits length (M ⧸ aM) into the part supported on N = M ⊓ K ∙ x and the part seen by the projection e. The first is bounded by length_quotient_lsmul_le_ord_of_le_span_singleton, which clears denominators to reach the rank-one case in Length.lean; the second is length (e M ⧸ a e M), and e M lies one dimension lower.

Design #

Ring.KrullDimLE 1 is used rather than Ring.DimensionLEOne. Over a domain Ring.krullDimLE_one_iff_of_noZeroDivisors converts one into the other, so a caller holding either can supply the hypothesis.

Multiplication by a is written as LinearMap.range (LinearMap.lsmul A M a) throughout rather than as a pointwise scalar action on submodules. That keeps every statement inside the plain Submodule API, and the compatibility of the two readings is confined to Length.lean, where TauCeti.map_lsmul_eq_smul is the single bridge.

Krull–Akizuki is stated for an abstract C with [IsIntegralClosure C A L], following Mathlib's convention for IsIntegralClosure.isNoetherianRing, with the integralClosure A L form derived from it. The abstract form applies to rings known only to be an integral closure, such as a Subring of a function field, which are not literally Mathlib's integralClosure subalgebra. The ambient L is only asked to be a domain with a K-module structure compatible with A, rather than a field with [Algebra K L], since the length bound sees L only as a K-vector space.

References #

The argument is the classical one: H. Matsumura, Commutative Ring Theory, Theorem 11.7.

The induced map on a linear image #

The rank-one case over the fraction field #

The rank induction #

source
theorem TauCeti.length_quotient_lsmul_le_finrank_mul_ord {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [IsNoetherianRing A] [Ring.KrullDimLE 1 A] [Module.Finite K V] (M : Submodule A V) (a : A) (ha : a ≠ 0) :
Module.length A (↥M ⧸ ((LinearMap.lsmul A ↥M) a).range) ≤ ↑(Module.finrank K V) * Ring.ord A a

Krull–Akizuki's length bound. For any A-submodule M of a finite-dimensional K-vector space V — finitely generated or not — and any nonzero a : A, length (M ⧸ aM) ≤ dim_K V * ord_A a.

source
theorem TauCeti.isFiniteLength_quotient_lsmul {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module A V] [IsScalarTower A K V] [IsNoetherianRing A] [Ring.KrullDimLE 1 A] [Module.Finite K V] (M : Submodule A V) (a : A) (ha : a ≠ 0) :
IsFiniteLength A (↥M ⧸ ((LinearMap.lsmul A ↥M) a).range)

Krull–Akizuki's finiteness. Under the hypotheses of the length bound, M ⧸ aM has finite length; equivalently it is both Noetherian and Artinian over A.

Krull–Akizuki #

source
theorem TauCeti.IsIntegralClosure.isNoetherianRing {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.KrullDimLE 1 A] {L : Type u_2} [CommRing L] [IsDomain L] [Algebra A L] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [Module K L] [IsScalarTower A K L] [Module.Finite K L] (C : Type u_4) [CommRing C] [Algebra A C] [Algebra C L] [IsScalarTower A C L] [IsIntegralClosure C A L] :
IsNoetherianRing C

Krull–Akizuki. Let A be a Noetherian domain of Krull dimension at most one with fraction field K, and let L be a domain containing A that is a finite-dimensional K-vector space compatibly with A, such as a finite extension of K. Then an integral closure C of A in L is a Noetherian ring. No separability over K is assumed, and C need not be a finite A-module.

source
theorem TauCeti.integralClosure.isNoetherianRing {A : Type u_1} [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.KrullDimLE 1 A] {L : Type u_2} [CommRing L] [IsDomain L] [Algebra A L] (K : Type u_3) [Field K] [Algebra A K] [IsFractionRing A K] [Module K L] [IsScalarTower A K L] [Module.Finite K L] :
IsNoetherianRing ↥(integralClosure A L)

Krull–Akizuki for Mathlib's integralClosure. The specialisation of TauCeti.IsIntegralClosure.isNoetherianRing to the integral closure of A in L as a subalgebra.