HilbertRamification.Dedekind.fixedFieldOfSubgroup_forall_isUnramifiedAt_of_inertiaGroup_le
Fixed-field unramifiedness from the global cyclotomic inertia argument.
If H contains every inertia group of M / ℚ, then every finite prime of the fixed field Mᴴ is unramified over ℤ. For a prime P of the fixed field, choose a prime Q of M above it. The inertia group of Q for M / Mᴴ has the same cardinality as the inertia group for M / ℚ, because the latter is contained in H. prime-decomposition theory identifies these cardinalities with the two upper ramification indices. Multiplicativity of ramification indices in the tower then forces the lower ramification index to be one.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace HilbertRamification.Dedekind
open NumberField
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
variable {G M : Type*}
variable [Group G]
variable [Field M] [NumberField M]
variable [MulSemiringAction G M]
variable [IsGaloisGroup G ℚ M]Lean source · statement
theorem fixedFieldOfSubgroup_forall_isUnramifiedAt_of_inertiaGroup_le
(H : Subgroup G)
(hI : ∀ (Q : Ideal (𝓞 M)) [Q.IsPrime] [Q.IsMaximal],
inertiaGroup Q G ≤ H) :
∀ (P : Ideal
(𝓞 (fixedFieldOfSubgroup (K := ℚ) (L := M) G H)))
[P.IsPrime],
Algebra.IsUnramifiedAt ℤ P