RamificationTheory.HilbertRamification.DiscreteValuationRing.tameCharacter_pow_eq_uniformizer
Every power of the actual tame character is computed using any uniformizer. In particular this applies to the original e/n exponent.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
attribute [local instance] maximalIdeal_inertia_normal
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
(G : Type v) [Group G] [Finite G] [MulSemiringAction G R]Lean source · statement
theorem tameCharacter_pow_eq_uniformizer
(m : ℕ) (π : R) (hπ : Irreducible π)
(σ : (maximalIdeal R).inertia G) :
(((tameCharacter R G).toFun σ) ^ m).val.val =
(residue R (uniformizerRatioUnit R G π hπ σ.val).val) ^ m