RamificationTheory.HilbertRamification.CompleteDVF.natCard_decompositionInertiaSubgroup_eq_ramificationIndex
In a finite Galois extension of complete discrete valued fields, the decomposition-side inertia subgroup has cardinality equal to the canonical ramification index.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]Lean source · statement
theorem natCard_decompositionInertiaSubgroup_eq_ramificationIndex
[IsGalois K L]
[Algebra.IsSeparable
(base.valuationSubring ⧸ base.maximalIdeal)
(target.valuationSubring ⧸ target.maximalIdeal)] :
Nat.card (target.valuation.valuationSubring.inertiaSubgroup K) =
ValuedExtension.ramificationIndex base.toDVF target.toDVF