Module

RingInertiaCharacter.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingInertiaCharacter

11 declarations indexed from sourceView source ↗

Module documentation

The inertia character directly on a DVR

This owner starts from the actual ideal inertia of a group acting on a DVR. It constructs the uniformizer-ratio unit inside the ring and then reduces it. No ambient fraction field, scalar tower, chosen value group, or supplied character is used.

Imports6

Mathlib.Algebra.Group.Action.End
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.Ideal.Defs
Mathlib.Algebra.Ring.Action.Basic
Mathlib.Algebra.Group.Units.Hom

Imported by9

def

uniformizerRatioUnit

L35 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioUnit

Documentation

The actual quotient unit g(π)/π, constructed using associated uniformizers.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

def uniformizerRatioUnit (π : R) (hπ : Irreducible π) (g : G) : Rˣ

theorem

uniformizerRatioUnit_spec

L39 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioUnit_spec

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem uniformizerRatioUnit_spec (π : R) (hπ : Irreducible π) (g : G) :
    π * (uniformizerRatioUnit R G π hπ g : R) = g • π

theorem

uniformizerRatioUnit_one

L44 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioUnit_one

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem uniformizerRatioUnit_one (π : R) (hπ : Irreducible π) :
    uniformizerRatioUnit R G π hπ (1 : G) = 1

theorem

uniformizerRatioUnit_mul

L52 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioUnit_mul

Documentation

The ratio is a cocycle before restriction to inertia.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem uniformizerRatioUnit_mul (π : R) (hπ : Irreducible π) (g h : G) :
    uniformizerRatioUnit R G π hπ (g * h) =
      uniformizerRatioUnit R G π hπ g *
        Units.map (MulSemiringAction.toRingHom G R g).toMonoidHom
          (uniformizerRatioUnit R G π hπ h)

theorem

uniformizerRatioUnit_change

L67 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioUnit_change

Documentation

A change of uniformizer changes the unit cocycle by the unit coboundary.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem uniformizerRatioUnit_change (π π' : R)
    (hπ : Irreducible π) (hπ' : Irreducible π')
    (a : Rˣ) (ha : π' = π * (a : R)) (g : G) :
    uniformizerRatioUnit R G π' hπ' g * a =
      uniformizerRatioUnit R G π hπ g *
        Units.map (MulSemiringAction.toRingHom G R g).toMonoidHom a

theorem

inertia_residue_fixed

L85 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertia_residue_fixed

Documentation

Actual ideal inertia fixes every residue class.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem inertia_residue_fixed
    (σ : (maximalIdeal R).inertia G) (x : R) :
    residue R ((σ : G) • x) = residue R x

theorem

inertia_residueUnits_fixed

L93 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertia_residueUnits_fixed

Documentation

The same fixedness on the units of the residue field.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem inertia_residueUnits_fixed
    (σ : (maximalIdeal R).inertia G) (a : Rˣ) :
    Units.map (residue R).toMonoidHom
        (Units.map (MulSemiringAction.toRingHom G R (σ : G)).toMonoidHom a) =
      Units.map (residue R).toMonoidHom a

def

inertiaUniformizerCharacter

L102 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaUniformizerCharacter

Documentation

The actual uniformizer character on ideal inertia.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · full declaration

def inertiaUniformizerCharacter (π : R) (hπ : Irreducible π) :
    (maximalIdeal R).inertia G →* (ResidueField R)ˣ where
  toFun σ := Units.map (residue R).toMonoidHom
    (uniformizerRatioUnit R G π hπ (σ : G))
  map_one' := by
    rw [Subgroup.coe_one, uniformizerRatioUnit_one, map_one]
  map_mul' σ τ := by
    rw [Subgroup.coe_mul, uniformizerRatioUnit_mul, map_mul,
      inertia_residueUnits_fixed]

theorem

inertiaUniformizerCharacter_eq

L113 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaUniformizerCharacter_eq

Documentation

The ideal-inertia character is independent of the uniformizer.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem inertiaUniformizerCharacter_eq
    (π π' : R) (hπ : Irreducible π) (hπ' : Irreducible π') :
    inertiaUniformizerCharacter R G π hπ = inertiaUniformizerCharacter R G π' hπ'

def

inertiaResidueCharacter

L125 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaResidueCharacter

Documentation

The actual uniformizer-independent inertia character of a DVR action.

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

def inertiaResidueCharacter :
    (maximalIdeal R).inertia G →* (ResidueField R)ˣ

theorem

inertiaResidueCharacter_eq_uniformizer

L131 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaResidueCharacter_eq_uniformizer

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
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]

Lean source · statement

theorem inertiaResidueCharacter_eq_uniformizer (π : R) (hπ : Irreducible π) :
    inertiaResidueCharacter R G = inertiaUniformizerCharacter R G π hπ

Module documentation

The inertia character directly on a DVR

Declarations