EtaleFundamentalGroups.Inertia.idealLocalizationInertiaGroupMap_conjugate_value
The actual localization-inertia comparison retains the literal conjugate in the original stabilizer. No conjugation compatibility is assumed.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification.DiscreteValuationRing
open scoped Pointwise
universe u vLean source · statement
theorem idealLocalizationInertiaGroupMap_conjugate_value
(B G : Type v) [CommRing B] [Group G] [MulSemiringAction G B]
(Q : Ideal B) [Q.IsPrime]
(d : MulAction.stabilizer G Q) (σ : Q.inertia G) :
(idealLocalizationInertiaGroupMap B G Q).toFun
(nativeIdealInertiaConjugate B G Q d σ) =
⟨d * ((idealLocalizationInertiaGroupMap B G Q).toFun σ).val * d⁻¹,
(maximalIdeal_inertia_normal (Localization.AtPrime Q)
(MulAction.stabilizer G Q)).conj_mem
((idealLocalizationInertiaGroupMap B G Q).toFun σ).val
((idealLocalizationInertiaGroupMap B G Q).toFun σ).property d⟩