Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.UnramifiedRationals

Module documentation

No nontrivial everywhere-unramified extension of ℚ

The global Kronecker--Weber argument forms a fixed field which is unramified at every finite prime. Minkowski's discriminant bound to show that this field is ℚ. This file records that source theorem directly in terms of the local unramified predicates on the prime ideals of the ring of integers.

theorem

numberField_finrank_eq_one_of_forall_isUnramifiedAt

L31 ↗

AlgebraicNumberTheory.Ramification.numberField_finrank_eq_one_of_forall_isUnramifiedAt

Documentation

A number field unramified at every prime over ℤ has degree one over ℚ.

The proof first shows that its different ideal is the unit ideal. Its absolute discriminant therefore has absolute value one, while the Hermite--Minkowski bound says that every number field of degree greater than one has absolute discriminant greater than two.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory.Ramification
open NumberField

Lean source · statement

theorem numberField_finrank_eq_one_of_forall_isUnramifiedAt
    (K : Type*) [Field K] [NumberField K]
    (hunramified : ∀ (P : Ideal (𝓞 K)) [P.IsPrime],
      Algebra.IsUnramifiedAt ℤ P) :
    Module.finrank ℚ K = 1

Module documentation

No nontrivial everywhere-unramified extension of ℚ

Declarations

numberField_finrank_eq_one_of_forall_isUnramifiedAt