Module

InertiaGeneration.lean

Nyll.ClassFieldTheory.RamificationTheory.HilbertRamification.Dedekind.InertiaGeneration

1 declaration indexed from sourceView source ↗

Module documentation

Global cyclotomic inertia argument: completion of the inertia-generation step

The preceding fixed-field lemma shows that a subgroup containing all inertia groups has an everywhere-unramified fixed field. Minkowski's discriminant bound makes that fixed field equal to ℚ, and Galois correspondence then makes the subgroup equal to the full Galois group.

Imports3

Imported by2

theorem

subgroup_eq_top_of_forall_inertiaGroup_le

L38 ↗

HilbertRamification.Dedekind.subgroup_eq_top_of_forall_inertiaGroup_le

Documentation

The global cyclotomic inertia argument, completed global inertia-generation step.

Every subgroup of Gal(M / ℚ) which contains the inertia group at every finite prime of M is the whole Galois group.

Source context 10 commands

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

noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
open AlgebraicNumberTheory.Ramification
variable {G M : Type*}
variable [Group G]
variable [Field M] [NumberField M]
variable [MulSemiringAction G M]
variable [IsGaloisGroup G ℚ M]

Lean source · statement

theorem subgroup_eq_top_of_forall_inertiaGroup_le
    (H : Subgroup G)
    (hI : ∀ (Q : Ideal (𝓞 M)) [Q.IsPrime] [Q.IsMaximal],
      inertiaGroup Q G ≤ H) :
    H = ⊤

Module documentation

Global cyclotomic inertia argument: completion of the inertia-generation step

Declarations

subgroup_eq_top_of_forall_inertiaGroup_le