ValuationTheory.DiscreteValuationField.exists_finite_inertia_pGroup_of_prime_residue_trivial_extension
A prime-degree extension with unchanged residue field gives a nontrivial p-group inertia layer inside every selected overfield valuation.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.ValuationSubring
universe u v w tLean source · statement
theorem exists_finite_inertia_pGroup_of_prime_residue_trivial_extension
{K L Ω : Type u} [Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω] [IsScalarTower K L Ω]
[FiniteDimensional K L] [IsGalois K L]
(D : HenselianDVF.{u, v} K) (T : HenselianDVF.{u, w} L)
[D.valuation.HasExtension T.valuation]
{Γ : Type t} [LinearOrderedCommGroupWithZero Γ]
(z : Valuation Ω Γ) [T.valuation.HasExtension z]
(p : ℕ) [Fact p.Prime] (hdegree : Module.finrank K L = p)
(hres : Function.Surjective (algebraMap D.residueField T.residueField)) :
∃ E : FiniteGaloisIntermediateField K Ω,
IsPGroup p (inertiaGroup K (z.valuationSubring.comap E.toIntermediateField.val.toRingHom)) ∧
∃ τ : inertiaGroup K (z.valuationSubring.comap E.toIntermediateField.val.toRingHom),
τ ≠ 1