ValuationTheory.DiscreteValuationField.ValuedExtension.card_inertia_eq_ramificationIndex_of_finite_separable
In a finite separable valued extension, ideal-theoretic inertia has cardinality equal to the canonical ramification index.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w x
namespace ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type w} [Field K] [Field L]
variable [Algebra K L] [FiniteDimensional K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{w, x} L)
variable [base.valuation.HasExtension target.valuation]
variable (G : Type*) [Group G] [Finite G]
variable [MulSemiringAction G target.valuationSubring]
variable [IsGaloisGroup G base.valuationSubring target.valuationSubring]Lean source · statement
theorem card_inertia_eq_ramificationIndex_of_finite_separable
[Algebra.IsSeparable K L]
[IsScalarTower base.valuationSubring target.valuationSubring L]
[Algebra.IsSeparable
(base.valuationSubring ⧸ base.maximalIdeal)
(target.valuationSubring ⧸ target.maximalIdeal)] :
Nat.card (target.maximalIdeal.toAddSubgroup.inertia G) =
ramificationIndex base.toDVF target.toDVF