The maximal tamely ramified subextension

For a finite Galois subextension L/K of the algebraic closure of a nonarchimedean local field, its maximal tamely ramified subextension is Kᵗ ⊓ L, where Kᵗ is the canonical maximal tamely ramified extension. This field is the fixed field of the first lower ramification group G₁(L/K). Its degree over K is [L : K] / p ^ (v_p e(L/K)), where p is the residue characteristic. These statements accept any compatible local-field structures on L.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §2.
• J. Neukirch, Algebraic Number Theory, Chapter II, §7.

theorem TauCeti.LocalFieldsRamification.finrank_fixedField_lowerRamificationGroup_one (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] : Module.finrank K ↥(IntermediateField.fixedField (lowerRamificationGroup K L 1)) = Module.finrank K L / ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ (ramificationIndex K L).factorization (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))

The degree over the base of the field fixed by wild inertia is [L : K] / p ^ (v_p e(L/K)).

@[simp]

theorem IntermediateField.lift_fixedField_lowerRamificationGroup_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] : lift (fixedField (TauCeti.LocalFieldsRamification.lowerRamificationGroup K (↥L) 1)) = TauCeti.maximalTameExtension K (AlgebraicClosure K) ⊓ L

The fixed field of finite wild inertia, lifted to the algebraic closure, is the intersection of L with the maximal tamely ramified extension.

theorem IntermediateField.finrank_maximalTameExtension_inf {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] : Module.finrank K ↥(TauCeti.maximalTameExtension K (AlgebraicClosure K) ⊓ L) = Module.finrank K ↥L / ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ (TauCeti.ramificationIndex K ↥L).factorization (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))

The degree of the maximal tamely ramified subextension of a finite Galois extension is [L : K] / p ^ (v_p e(L/K)).