NYLL
Module

RingInertiaCharacterConjugation.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingInertiaCharacterConjugation
3 declarations indexed from sourceView source ↗

Module documentation

Conjugation of the DVR inertia character

Proves normality of maximal-ideal inertia and computes the conjugation of uniformizer-ratio units. The residue character intertwines group conjugation with the induced residue-field action.

Imports5
Imported by3

Declarations

theorem

maximalIdeal_inertia_normal

L32 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.maximalIdeal_inertia_normal
Documentation

Ring automorphisms preserve the unique maximal ideal, so its actual inertia subgroup is normal in the full acting group.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
open scoped Pointwise
universe u v
Lean source · statement
theorem maximalIdeal_inertia_normal
    (R : Type u) [CommRing R] [IsLocalRing R]
    (G : Type v) [Group G] [MulSemiringAction G R] :
    ((maximalIdeal R).inertia G).Normal
theorem

uniformizerRatioUnit_conj

L55 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioUnit_conj
Documentation

Conjugation carries the actual ratio unit at a uniformizer to the ratio unit at its image. This is an identity in the original DVR.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
open scoped Pointwise
universe u v
attribute [local instance] maximalIdeal_inertia_normal
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  (G : Type v) [Group G] [MulSemiringAction G R]
Lean source · statement
theorem uniformizerRatioUnit_conj
    (π : R) (hπ : Irreducible π) (g s : G) :
    uniformizerRatioUnit R G (g • π)
        (hπ.map (MulDistribMulAction.toMulEquiv R g)) (g * s * g⁻¹) =
      (Units.map (MulSemiringAction.toRingHom G R g).toMonoidHom).toFun
        (uniformizerRatioUnit R G π hπ s)
theorem

inertiaResidueCharacter_conj

L81 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaResidueCharacter_conj
Documentation

The same uniformizer-independent inertia character intertwines actual group conjugation with the standard action on residue-field units.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
open scoped Pointwise
universe u v
attribute [local instance] maximalIdeal_inertia_normal
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  (G : Type v) [Group G] [MulSemiringAction G R]
Lean source · statement
theorem inertiaResidueCharacter_conj
    (g : G) (σ : (maximalIdeal R).inertia G) :
    (inertiaResidueCharacter R G).toFun
        (((MulAut.conjNormal (H := (maximalIdeal R).inertia G)).toFun g).toFun σ) =
      (Units.map
        (MulSemiringAction.toRingHom G (ResidueField R) g).toMonoidHom).toFun
        ((inertiaResidueCharacter R G).toFun σ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.