Discriminants, ramification and ideals

Discriminants and their bounds, ramification and inertia, orders, units, ideal counting, local degrees under completion, field enumeration and towers.

• Class field towers
• Completions of number fields at finite places
• Counting ideals of bounded norm
• Discriminants of number fields
• Discriminants of truncated logarithmic polynomials
• Enumerating number fields
• Maximal unramified subextension
• Orders in number fields
• Ramification in extensions of number fields
• Residue maps of singly generated algebras
• Van der Waerden's conjecture on Galois groups

TheoremMartinet's totally real towers#●ready to prove

There is a real constant \(C > 0\) such that for every \(N \in \mathbb{N}\) there exist a natural number \(d \ge N\) and a totally real number field \(K\) of degree \([K : \mathbb{Q}] = d\) whose discriminant \(\Delta_K\) satisfies \(|\Delta_K| \le C^d\).

public theorem_wanted exists_totallyReal_discr_le :
    ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, ∃ d : ℕ, N ≤ d ∧
      ∃ (K : Type) (_ : Field K) (_ : NumberField K) (_ : NumberField.IsTotallyReal K),
        Module.finrank ℚ K = d ∧ |(NumberField.discr K : ℝ)| ≤ C ^ d

Sources

• Theorem 3.2 of T. F. Bloom, W. Sawin, C. Schildkraut, D. Zhelezov, The sum-product conjecture is false for real numbers, arXiv:2605.28781. Lean axiom: https://github.com/mathlib-initiative/sum_product (SumProduct.exists_totallyReal_discr_le). Underlying result: J. Martinet, Tours de corps de classes et estimations de discriminants, Invent. Math. 44 (1978), 65–73. Problem martinet_totally_real_towers of the lean-eval benchmark.

TheoremOdlyzko's root discriminant bound in degree at least 18#●ready to prove

Let \(K\) be a totally complex number field of degree \(n = [K : \mathbb{Q}] \ge 18\) and discriminant \(d_K\). Then \(|d_K| \ge 8.25^n\); equivalently, the root discriminant \(|d_K|^{1/n}\) of \(K\) is at least \(8.25\).

Minkowski's elementary argument is not strong enough; the bound comes from analysing the zeros of the Dedekind zeta function of \(K\).

theorem_wanted odlyzko_root_discr_ge (K : Type*) [Field K] [NumberField K]
    [IsTotallyComplex K] (hdim : finrank ℚ K ≥ 18) :
    |(discr K : ℝ)| ≥ 8.25 ^ finrank ℚ K

Sources

• A. M. Odlyzko, Bounds for discriminants and related estimates for class numbers, regulators and zeros of zeta functions: a survey of recent results, Sém. Delange-Pisot-Poitou 18(1) (1976–1977), exp. 6, https://www.numdam.org/item/SDPP_1976-1977__18_1_A6_0/.

TheoremOrder of the inertia group#✓fully proved

Let \(A\) and \(B\) be integral domains, with \(B\) an \(A\)-algebra that is finite and flat as an \(A\)-module, and let \(G\) be a finite group acting faithfully on \(B\) by \(A\)-algebra automorphisms such that every \(G\)-invariant element of \(B\) comes from \(A\). Let \(\mathfrak p\) be a maximal ideal of \(A\) and \(\mathfrak P\) a maximal ideal of \(B\) lying over \(\mathfrak p\). Then the inertia group of \(\mathfrak P\), consisting of the \(\sigma \in G\) with \(\sigma(b) - b \in \mathfrak P\) for all \(b \in B\), has order \(e \cdot i\), where \(e\) is the ramification index of \(\mathfrak p\) in \(B\) (the common ramification index of the primes of \(B\) over \(\mathfrak p\)) and \(i\) is the inseparable degree of the residue field extension \((B/\mathfrak P)/(A/\mathfrak p)\), that is, the degree of \(B/\mathfrak P\) over the separable closure of \(A/\mathfrak p\) in it.

theorem card_inertia_eq_ramificationIdxIn_mul_finInsepDegree
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B] [IsGaloisGroup G A B]
    [IsDomain A] [IsDomain B] [Module.Finite A B] [Module.Flat A B] {p : Ideal A} [p.IsMaximal]
    (P : Ideal B) [P.LiesOver p] [P.IsMaximal] :
    Nat.card (P.inertia G) =
      ramificationIdxIn p B * Field.finInsepDegree (A ⧸ p) (B ⧸ P)

TheoremUnits small away from the diagonal generate a subgroup of finite index#✓fully proved

Let \(F\) be a number field and let \((u_v)\) be a family of units of the ring of integers of \(F\), indexed by the infinite places \(v\) of \(F\). Write \(w(x)\) for the absolute value of \(x\) at an infinite place \(w\). If \(w(u_v) < 1\) for all infinite places \(v\) and \(w\) with \(w \ne v\), then the subgroup of the unit group of the ring of integers generated by the \(u_v\) has finite index.

After dropping the coordinate of one infinite place, the logarithmic embeddings of the remaining \(u_v\) form a square matrix with negative off-diagonal entries and positive column sums. It is therefore strictly diagonally dominant by columns, hence invertible, so these units generate a subgroup of maximal rank.

theorem finiteIndex_closure_range_of_lt_one_off_diagonal
    (u : NumberField.InfinitePlace F → (𝓞 F)ˣ)
    (hu : ∀ v w : NumberField.InfinitePlace F, w ≠ v → w (u v) < 1) :
    (Subgroup.closure (Set.range u)).FiniteIndex

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.