RamificationTheory.HilbertRamification.DiscreteValuationRing.localTameCharacterGroupMap_pow_conj_value
The proved same-character equation on the literal conjugate, using the existing native map of roots induced by the standard residue coefficient map.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u
attribute [local instance] maximalIdeal_inertia_normalLean source · statement
theorem localTameCharacterGroupMap_pow_conj_value
(R G : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
[Group G] [Finite G] [MulSemiringAction G R]
(m : ℕ) (g : G) (σ : (maximalIdeal R).inertia G) :
((localTameCharacterGroupMap R G).toFun
⟨g * σ.val * g⁻¹, (maximalIdeal_inertia_normal R G).conj_mem σ.val σ.property g⟩) ^ m =
(rootsGroupMap (MulSemiringAction.toRingHom G (ResidueField R) g)
(tameOrder R G)).hom'.toFun (((localTameCharacterGroupMap R G).toFun σ) ^ m)