Finiteness of the ramification locus of an extension of Dedekind domains

Let B be a Dedekind domain, module-finite and torsion-free over a Dedekind domain A, with the extension of fraction fields separable. Mathlib's Algebra.unramifiedLocus A B is the set of primes of B at which B is unramified over A, and Mathlib knows it is open. Here it is shown that its complement — the ramification locus — is finite.

The tool is the different ideal. Mathlib's not_dvd_differentIdeal_iff says a prime is unramified exactly when it does not divide differentIdeal A B, and differentIdeal_ne_bot says that ideal is nonzero; a nonzero ideal of a Dedekind domain has only finitely many divisors.

Main results

• Algebra.finite_compl_unramifiedLocus: the ramification locus is finite.

Stated over Dedekind domains directly rather than in an AKLB tower: no ambient fraction fields K and L and no IsIntegralClosure B A L are needed, since the separability hypothesis can be carried by FractionRing A and FractionRing B themselves, which is the form not_dvd_differentIdeal_iff already takes.

The finiteness is consumed by TauCeti.NumberTheory.Chebotarev.RamifiedPrimes, which contracts the ramification locus of 𝓞 L over 𝓞 K to build the finite set of primes of K ramifying in L.

Provenance

Ported from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, at dev/hasse-weil @ 513e83879e2f), HasseWeil/Curves/RamificationFinite.lean, declarations finite_setOf_dvd_differentIdeal, finite_setOf_ramificationIdx_ne_one and finite_setOf_under_ramified.

Changes from the source. The source works in an AKLB tower and rebuilds the standard instances along the way, including differentIdeal_ne_bot, which Mathlib now proves; those are dropped, and with them the tower. The ramification locus is named by Mathlib's Algebra.unramifiedLocus and the criterion by Mathlib's Algebra.IsUnramifiedAt, in place of the source's hand-rolled ramifiedUnderLocus and its Ideal.ramificationIdx _ _ ≠ 1 spelling. The source's divisor-finiteness step is Mathlib's UniqueFactorizationMonoid.fintypeSubtypeDvd applied to the monoid of ideals, so it is neither rebuilt nor made public API here. Sixteen declarations become one.

theorem Algebra.finite_compl_unramifiedLocus (A : Type u_1) (B : Type u_2) [CommRing A] [IsDedekindDomain A] [CommRing B] [Algebra A B] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] : (unramifiedLocus A B)ᶜ.Finite

A module-finite, torsion-free extension of Dedekind domains whose fraction-field extension is separable ramifies at only finitely many primes: the complement of Algebra.unramifiedLocus is finite. A ramified prime divides the different ideal, which is nonzero and so, being an ideal of a Dedekind domain, has finitely many divisors.