Module

FiniteIdealCanonicalTameConjugation.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealCanonicalTameConjugation

2 declarations indexed from sourceView source ↗

Module documentation

Conjugation equivariance of finite ideal characters

Proves stabilizer-conjugation equivariance for powers of the finite ideal tame character and for its canonical normalization.

Imports5

Imported by2

theorem

finiteIdealTameCharacterGroupMap_pow_conjugate

L31 ↗

EtaleFundamentalGroups.Inertia.finiteIdealTameCharacterGroupMap_pow_conjugate

Documentation

The same original-prime tame character intertwines literal stabilizer conjugation with the standard local-residue action, including every power.

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 v

Lean source · full declaration

theorem finiteIdealTameCharacterGroupMap_pow_conjugate
    (B G : Type v) [CommRing B] [IsDedekindDomain B]
    [Group G] [Finite G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) (m : ℕ)
    (d : MulAction.stabilizer G Q) (σ : Q.inertia G) :
    letI : IsDiscreteValuationRing (Localization.AtPrime Q) :=
      SchemeTheory.localizationAtPrime_isDiscreteValuationRing B Q hQ
    ((finiteIdealTameCharacterGroupMap B G Q hQ).toFun
        (nativeIdealInertiaConjugate B G Q d σ)) ^ m =
      (RamificationTheory.HilbertRamification.rootsGroupMap
        (MulSemiringAction.toRingHom (MulAction.stabilizer G Q) Q.ResidueField d)
        (finiteIdealTameOrder B G Q hQ)).hom'.toFun
        (((finiteIdealTameCharacterGroupMap B G Q hQ).toFun σ) ^ m) := by
  let : IsDiscreteValuationRing (Localization.AtPrime Q) :=
    SchemeTheory.localizationAtPrime_isDiscreteValuationRing B Q hQ
  have hconj := idealLocalizationInertiaGroupMap_conjugate_value B G Q d σ
  exact Eq.trans
    (congrArg
      (fun τ : (IsLocalRing.maximalIdeal (Localization.AtPrime Q)).inertia
          (MulAction.stabilizer G Q) =>
        ((localTameCharacterGroupMap (Localization.AtPrime Q)
          (MulAction.stabilizer G Q)).toFun τ) ^ m)
      hconj)
    (localTameCharacterGroupMap_pow_conj_value (Localization.AtPrime Q)
      (MulAction.stabilizer G Q)
      m d ((idealLocalizationInertiaGroupMap B G Q).toFun σ))

theorem

finiteIdealCanonicalTameCharacterGroupMap_conjugate

L60 ↗

EtaleFundamentalGroups.Inertia.finiteIdealCanonicalTameCharacterGroupMap_conjugate