The integral closure of 𝓞 K in a finite extension of number fields

For a finite extension L of a number field K, the integral closure of 𝓞 K in L is the integral closure of ℤ in L — that is TauCeti.IsIntegralClosure.tower_bot applied along ℤ → 𝓞 K → L — hence isomorphic to 𝓞 L. Two consequences transfer along that identification and are the finiteness inputs of the Mordell–Weil descent: the class group of the integral closure is finite, and its unit group is finitely generated.

Both are stated for integralClosure (𝓞 K) L rather than for 𝓞 L, because that is the ring the descent actually produces — WeierstrassCurve.Affine.ringOfIntegersFactor is an integral closure in a quotient K[X] ⧸ (p), not a ring of integers presented as such.

Main results

• NumberField.finite_classGroup_integralClosure : the class number theorem for it.
• NumberField.fg_units_integralClosure : the finite-generation half of Dirichlet's unit theorem for it.

References

• M. Stoll, EllipticCurves, commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, EllipticCurves/Mathlib/Basic.lean, Apache-2.0. That file collects general-purpose results its author flags as Mathlib candidates; NumberField.finite_classGroup_integralClosure and NumberField.fg_units_integralClosure are adapted from it essentially verbatim. The ℤ → 𝓞 K → L identification they rest on is TauCeti.IsIntegralClosure.tower_bot, credited to Stacks in its own module.

theorem NumberField.finite_classGroup_integralClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] : Finite (ClassGroup ↥(integralClosure (RingOfIntegers K) L))

The class number theorem for the integral closure of 𝓞 K in a finite extension L of the number field K: its class group is finite.

theorem NumberField.fg_units_integralClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [FiniteDimensional K L] : Group.FG (↥(integralClosure (RingOfIntegers K) L))ˣ

Dirichlet's unit theorem (finite generation) for the integral closure of 𝓞 K in a finite extension L of the number field K: its unit group is finitely generated.