Module

CharacterMap.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.CharacterMap

60 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: character-map source

This file records the source lemmas for the canonical map I_w -> Hom(Delta / Gamma, lambda*) in prime-decomposition theory. We do not package the final value-group quotient here. Instead, we prove the pieces which make the formula

x ↦ (σ x / x) mod U^1

independent of the unit and base-unit choices used to represent a value class, and we identify the ramification group as the subgroup on which all these classes are trivial.

Imports1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationGroup

Imported by9

theorem

automorphismUnitQuotient_mul_arg

L37 ↗

RamificationTheory.HilbertRamification.ValuationSubring.automorphismUnitQuotient_mul_arg

Documentation

The unit quotient is multiplicative in the unit argument.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem automorphismUnitQuotient_mul_arg
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A)
    (x y : Lˣ) :
    automorphismUnitQuotient K A σ (x * y) =
      automorphismUnitQuotient K A σ x *
        automorphismUnitQuotient K A σ y

theorem

automorphismUnitQuotient_one_arg

L48 ↗

RamificationTheory.HilbertRamification.ValuationSubring.automorphismUnitQuotient_one_arg

Documentation

The unit quotient is trivial on the unit 1.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem automorphismUnitQuotient_one_arg
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) :
    automorphismUnitQuotient K A σ 1 = 1

theorem

automorphismUnitQuotient_algebraMapUnit

L55 ↗

RamificationTheory.HilbertRamification.ValuationSubring.automorphismUnitQuotient_algebraMapUnit

Documentation

A K-unit contributes trivially to the unit quotient.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem automorphismUnitQuotient_algebraMapUnit
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) (a : Kˣ) :
    automorphismUnitQuotient K A σ
        (Units.map (algebraMap K L).toMonoidHom a) = 1

theorem

inertia_automorphismUnitQuotient_mem_principalUnitGroup_of_mem_unitGroup

L65 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertia_automorphismUnitQuotient_mem_principalUnitGroup_of_mem_unitGroup

Documentation

Prime-decomposition statement: an inertia element sends valuation-ring units to the same residue class, hence its unit quotient on such a unit is principal.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertia_automorphismUnitQuotient_mem_principalUnitGroup_of_mem_unitGroup
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    {u : Lˣ} (hu : u ∈ A.unitGroup) :
    automorphismUnitQuotient K A (σ : decompositionGroup K A) u ∈
      A.principalUnitGroup

abbrev

inertiaUnitQuotientClass

L138 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientClass

Documentation

Prime-decomposition statement: for σ ∈ I_w, the class of σ x / x modulo principal units. This is the raw class from which the character χ_σ is assembled after quotienting the value group.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

abbrev inertiaUnitQuotientClass
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) (x : Lˣ) :
    Lˣ ⧸ A.principalUnitGroup

theorem

inertiaUnitQuotientClass_eq_one_iff

L145 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientClass_eq_one_iff

Documentation

States the theorem inertiaUnitQuotientClass_eq_one_iff.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertiaUnitQuotientClass_eq_one_iff
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) (x : Lˣ) :
    inertiaUnitQuotientClass K A σ x = 1 ↔
      automorphismUnitQuotient K A (σ : decompositionGroup K A) x ∈
        A.principalUnitGroup

theorem

inertiaUnitQuotientClass_mul_right_unit

L154 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientClass_mul_right_unit

Documentation

Multiplying the representative by a valuation-ring unit does not change the class of σ x / x modulo principal units.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertiaUnitQuotientClass_mul_right_unit
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    (x u : Lˣ) (hu : u ∈ A.unitGroup) :
    inertiaUnitQuotientClass K A σ (x * u) =
      inertiaUnitQuotientClass K A σ x

theorem

inertiaUnitQuotientClass_eq_one_of_mem_unitGroup

L181 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientClass_eq_one_of_mem_unitGroup

Documentation

Valuation-ring units map to the trivial raw class.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertiaUnitQuotientClass_eq_one_of_mem_unitGroup
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    {u : Lˣ} (hu : u ∈ A.unitGroup) :
    inertiaUnitQuotientClass K A σ u = 1

theorem

inertiaUnitQuotientClass_mul_right_algebraMapUnit

L191 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientClass_mul_right_algebraMapUnit

Documentation

Multiplying the representative by a base-field unit does not change the class of σ x / x.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertiaUnitQuotientClass_mul_right_algebraMapUnit
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    (x : Lˣ) (a : Kˣ) :
    inertiaUnitQuotientClass K A σ
        (x * Units.map (algebraMap K L).toMonoidHom a) =
      inertiaUnitQuotientClass K A σ x

theorem

inertiaUnitQuotientClass_mul_right_algebraMapUnit_mul_unit

L223 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientClass_mul_right_algebraMapUnit_mul_unit

Documentation

Prime-decomposition statement: the residue-unit class is unchanged when a representative is multiplied by a base-field unit and then by a valuation-ring unit.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertiaUnitQuotientClass_mul_right_algebraMapUnit_mul_unit
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    (x : Lˣ) (a : Kˣ) (u : Lˣ) (hu : u ∈ A.unitGroup) :
    inertiaUnitQuotientClass K A σ
        ((x * Units.map (algebraMap K L).toMonoidHom a) * u) =
      inertiaUnitQuotientClass K A σ x

theorem

mem_ramificationGroup_iff_forall_inertiaUnitQuotientClass_eq_one

L237 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroup_iff_forall_inertiaUnitQuotientClass_eq_one

Documentation

Inertia-character exactness: R_w is exactly the subgroup of inertia on which all raw residue-unit classes [σ x / x] are trivial.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem mem_ramificationGroup_iff_forall_inertiaUnitQuotientClass_eq_one
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    σ ∈ ramificationGroup K A ↔
      ∀ x : Lˣ, inertiaUnitQuotientClass K A σ x = 1

def

principalUnitQuotientToValueClass

L250 ↗

RamificationTheory.HilbertRamification.ValuationSubring.principalUnitQuotientToValueClass

Documentation

The quotient map Lˣ/U^1 -> Lˣ/Aˣ. It measures the remaining value class of a raw residue-unit quotient.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

def principalUnitQuotientToValueClass
    (A : _root_.ValuationSubring L) :
    Lˣ ⧸ A.principalUnitGroup →* Lˣ ⧸ A.unitGroup

theorem

principalUnitQuotientToValueClass_mk

L260 ↗

RamificationTheory.HilbertRamification.ValuationSubring.principalUnitQuotientToValueClass_mk

Documentation

States the theorem principalUnitQuotientToValueClass_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem principalUnitQuotientToValueClass_mk
    (A : _root_.ValuationSubring L) (x : Lˣ) :
    principalUnitQuotientToValueClass A
        (QuotientGroup.mk' A.principalUnitGroup x) =
      QuotientGroup.mk' A.unitGroup x

abbrev

valueDisplacementClass

L269 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueDisplacementClass

Documentation

The value displacement of a decomposition-group automorphism at x. It is the class of σ x / x in the value-class quotient Lˣ/Aˣ.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

abbrev valueDisplacementClass
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) (x : Lˣ) :
    Lˣ ⧸ A.unitGroup

theorem

valueDisplacementClass_eq_one_iff

L275 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueDisplacementClass_eq_one_iff

Documentation

States the theorem valueDisplacementClass_eq_one_iff.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueDisplacementClass_eq_one_iff
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) (x : Lˣ) :
    valueDisplacementClass K A σ x = 1 ↔
      automorphismUnitQuotient K A σ x ∈ A.unitGroup

theorem

principalUnitQuotientToValueClass_inertiaUnitQuotientClass

L282 ↗

RamificationTheory.HilbertRamification.ValuationSubring.principalUnitQuotientToValueClass_inertiaUnitQuotientClass

Documentation

States the theorem principalUnitQuotientToValueClass_inertiaUnitQuotientClass.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem principalUnitQuotientToValueClass_inertiaUnitQuotientClass
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) (x : Lˣ) :
    principalUnitQuotientToValueClass A
        (inertiaUnitQuotientClass K A σ x) =
      valueDisplacementClass K A (σ : decompositionGroup K A) x

def

valueDisplacementHom

L290 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueDisplacementHom

Documentation

For fixed σ, value displacement is a group homomorphism on Lˣ.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

def valueDisplacementHom
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) :
    Lˣ →* Lˣ ⧸ A.unitGroup where
  toFun x := valueDisplacementClass K A σ x
  map_one' := by
    rw [valueDisplacementClass_eq_one_iff,
      automorphismUnitQuotient_one_arg]
    exact A.unitGroup.one_mem
  map_mul' x y := by
    change
      QuotientGroup.mk' A.unitGroup
          (automorphismUnitQuotient K A σ (x * y)) =
        QuotientGroup.mk' A.unitGroup
            (automorphismUnitQuotient K A σ x) *
          QuotientGroup.mk' A.unitGroup
            (automorphismUnitQuotient K A σ y)
    rw [automorphismUnitQuotient_mul_arg]
    exact map_mul (QuotientGroup.mk' A.unitGroup)
      (automorphismUnitQuotient K A σ x)
      (automorphismUnitQuotient K A σ y)

theorem

valueDisplacementHom_apply

L312 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueDisplacementHom_apply

Documentation

States the theorem valueDisplacementHom_apply.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueDisplacementHom_apply
    (A : _root_.ValuationSubring L) (σ : decompositionGroup K A) (x : Lˣ) :
    valueDisplacementHom K A σ x =
      valueDisplacementClass K A σ x

theorem

valueDisplacementClass_eq_one_of_mem_ramificationGroup

L321 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueDisplacementClass_eq_one_of_mem_ramificationGroup

Documentation

Prime-decomposition statement: every element of R_w has trivial value displacement. This is the precise boundary between the raw quotient Lˣ/U^1 and the residue-unit target.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueDisplacementClass_eq_one_of_mem_ramificationGroup
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    (hσ : σ ∈ ramificationGroup K A) (x : Lˣ) :
    valueDisplacementClass K A (σ : decompositionGroup K A) x = 1

def

valueTrivialInertiaGroup

L334 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaGroup

Documentation

In the valuation-subring model, the inertia elements whose value displacement is trivial. For the chosen-valuation decomposition group this condition is automatic; for mathlib's stabilizer of the valuation subring it is the exact source needed to turn the raw Lˣ/U^1 class into a residue field unit.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

def valueTrivialInertiaGroup
    (A : _root_.ValuationSubring L) :
    Subgroup (inertiaGroup K A) where
  carrier :=
    {σ | ∀ x : Lˣ,
      valueDisplacementClass K A (σ : decompositionGroup K A) x = 1}
  one_mem' := by
    intro x
    rw [valueDisplacementClass_eq_one_iff,
      show ((1 : inertiaGroup K A) : decompositionGroup K A) = 1 by rfl,
      automorphismUnitQuotient_one]
    exact A.unitGroup.one_mem
  mul_mem' := by
    intro σ τ hσ hτ x
    rw [valueDisplacementClass_eq_one_iff]
    rw [show
      ((σ * τ : inertiaGroup K A) : decompositionGroup K A) =
        (σ : decompositionGroup K A) * (τ : decompositionGroup K A) by rfl]
    rw [automorphismUnitQuotient_mul]
    exact A.unitGroup.mul_mem
      ((valueDisplacementClass_eq_one_iff (K := K) A
          (σ : decompositionGroup K A)
          (Units.mapEquiv (((τ : decompositionGroup K A) : L ≃ₐ[K] L).toMulEquiv)
            x)).mp
        (hσ _))
      ((valueDisplacementClass_eq_one_iff (K := K) A
          (τ : decompositionGroup K A) x).mp
        (hτ x))
  inv_mem' := by
    intro σ hσ x
    rw [valueDisplacementClass_eq_one_iff]
    let y : Lˣ :=
      (Units.mapEquiv
        ((((σ : inertiaGroup K A)⁻¹ : inertiaGroup K A) :
          decompositionGroup K A) : L ≃ₐ[K] L).toMulEquiv) x
    have hy :
        automorphismUnitQuotient K A (σ : decompositionGroup K A) y ∈
          A.unitGroup :=
      (valueDisplacementClass_eq_one_iff (K := K) A
        (σ : decompositionGroup K A) y).mp (hσ y)
    have hquot :
        automorphismUnitQuotient K A
            ((σ⁻¹ : inertiaGroup K A) : decompositionGroup K A) x =
          (automorphismUnitQuotient K A (σ : decompositionGroup K A) y)⁻¹ := by
      ext
      simp [automorphismUnitQuotient, y, div_eq_mul_inv]
    rw [hquot]
    exact A.unitGroup.inv_mem hy

theorem

ramificationGroup_le_valueTrivialInertiaGroup

L384 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_le_valueTrivialInertiaGroup

Documentation

The ramification group is contained in the value-trivial inertia group.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem ramificationGroup_le_valueTrivialInertiaGroup
    (A : _root_.ValuationSubring L) :
    ramificationGroup K A ≤ valueTrivialInertiaGroup K A

def

valueTrivialAutomorphismUnit

L393 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialAutomorphismUnit

Documentation

For a value-trivial inertia element, the quotient σ x / x is an actual unit of the valuation ring.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

def valueTrivialAutomorphismUnit
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (x : Lˣ) :
    A.unitGroup

theorem

valueTrivialAutomorphismUnit_coe

L404 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialAutomorphismUnit_coe

Documentation

States the theorem valueTrivialAutomorphismUnit_coe.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialAutomorphismUnit_coe
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (x : Lˣ) :
    (valueTrivialAutomorphismUnit K A σ x : Lˣ) =
      automorphismUnitQuotient K A
        ((σ : inertiaGroup K A) : decompositionGroup K A) x

theorem

valueTrivialAutomorphismUnit_one_arg

L413 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialAutomorphismUnit_one_arg

Documentation

States the theorem valueTrivialAutomorphismUnit_one_arg.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialAutomorphismUnit_one_arg
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    valueTrivialAutomorphismUnit K A σ 1 = 1

theorem

valueTrivialAutomorphismUnit_mul_arg

L421 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialAutomorphismUnit_mul_arg

Documentation

States the theorem valueTrivialAutomorphismUnit_mul_arg.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialAutomorphismUnit_mul_arg
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (x y : Lˣ) :
    valueTrivialAutomorphismUnit K A σ (x * y) =
      valueTrivialAutomorphismUnit K A σ x *
        valueTrivialAutomorphismUnit K A σ y

def

valueTrivialInertiaResidueUnitHom

L433 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom

Documentation

The character χ_σ is defined by: for value-trivial inertia, x ↦ σ x / x mod P is a homomorphism Lˣ -> λˣ.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

def valueTrivialInertiaResidueUnitHom
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    Lˣ →* (IsLocalRing.ResidueField A)ˣ where
  toFun x :=
    A.unitGroupToResidueFieldUnits
      (valueTrivialAutomorphismUnit K A σ x)
  map_one' := by
    rw [valueTrivialAutomorphismUnit_one_arg]
    exact map_one A.unitGroupToResidueFieldUnits
  map_mul' x y := by
    rw [valueTrivialAutomorphismUnit_mul_arg]
    exact map_mul A.unitGroupToResidueFieldUnits
      (valueTrivialAutomorphismUnit K A σ x)
      (valueTrivialAutomorphismUnit K A σ y)

theorem

valueTrivialInertiaResidueUnitHom_apply

L450 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_apply

Documentation

States the theorem valueTrivialInertiaResidueUnitHom_apply.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaResidueUnitHom_apply
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (x : Lˣ) :
    valueTrivialInertiaResidueUnitHom K A σ x =
      A.unitGroupToResidueFieldUnits
        (valueTrivialAutomorphismUnit K A σ x)

theorem

unitGroup_le_valueTrivialInertiaResidueUnitHom_ker

L459 ↗

RamificationTheory.HilbertRamification.ValuationSubring.unitGroup_le_valueTrivialInertiaResidueUnitHom_ker

Documentation

Valuation-ring units are killed by the residue-unit character.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem unitGroup_le_valueTrivialInertiaResidueUnitHom_ker
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    A.unitGroup ≤ (valueTrivialInertiaResidueUnitHom K A σ).ker

theorem

valueTrivialInertiaResidueUnitHom_baseUnit

L480 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_baseUnit

Documentation

Base-field units are killed by the residue-unit character.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaResidueUnitHom_baseUnit
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (a : Kˣ) :
    valueTrivialInertiaResidueUnitHom K A σ
        (Units.map (algebraMap K L).toMonoidHom a) = 1

theorem

valueTrivialInertiaResidueUnitHom_mapEquiv_arg

L506 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_mapEquiv_arg

Documentation

A value-trivial inertia element changes a unit representative only by a valuation-ring unit, hence every residue-unit character is unchanged after applying it to the representative.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaResidueUnitHom_mapEquiv_arg
    (A : _root_.ValuationSubring L)
    (σ τ : valueTrivialInertiaGroup K A) (x : Lˣ) :
    valueTrivialInertiaResidueUnitHom K A σ
        (Units.mapEquiv
          ((((τ : inertiaGroup K A) : decompositionGroup K A) :
            L ≃ₐ[K] L).toMulEquiv) x) =
      valueTrivialInertiaResidueUnitHom K A σ x

theorem

valueTrivialInertiaResidueUnitHom_one

L537 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_one

Documentation

The identity inertia element gives the trivial residue-unit character.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaResidueUnitHom_one
    (A : _root_.ValuationSubring L) (x : Lˣ) :
    valueTrivialInertiaResidueUnitHom K A
        (1 : valueTrivialInertiaGroup K A) x = 1

theorem

valueTrivialInertiaResidueUnitHom_mul

L552 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_mul

Documentation

Prime-decomposition statement: the residue-unit characters multiply with the inertia element.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaResidueUnitHom_mul
    (A : _root_.ValuationSubring L)
    (σ τ : valueTrivialInertiaGroup K A) (x : Lˣ) :
    valueTrivialInertiaResidueUnitHom K A (σ * τ) x =
      valueTrivialInertiaResidueUnitHom K A σ x *
        valueTrivialInertiaResidueUnitHom K A τ x

def

valueClassToResidueUnits

L582 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueClassToResidueUnits

Documentation

Prime-decomposition statement: the residue-unit character descends from representatives x : Lˣ to value classes modulo valuation-ring units.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

def valueClassToResidueUnits
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    Lˣ ⧸ A.unitGroup →* (IsLocalRing.ResidueField A)ˣ

theorem

valueClassToResidueUnits_mk

L591 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueClassToResidueUnits_mk

Documentation

States the theorem valueClassToResidueUnits_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueClassToResidueUnits_mk
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (x : Lˣ) :
    valueClassToResidueUnits K A σ
        (QuotientGroup.mk' A.unitGroup x) =
      valueTrivialInertiaResidueUnitHom K A σ x

theorem

valueTrivialInertiaResidueUnitHom_eq_one_of_mem_ramificationGroup

L600 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaResidueUnitHom_eq_one_of_mem_ramificationGroup

Documentation

States the theorem valueTrivialInertiaResidueUnitHom_eq_one_of_mem_ramificationGroup.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaResidueUnitHom_eq_one_of_mem_ramificationGroup
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A)
    (hσ : (σ : inertiaGroup K A) ∈ ramificationGroup K A)
    (x : Lˣ) :
    valueTrivialInertiaResidueUnitHom K A σ x = 1

def

inertiaUnitQuotientHom

L623 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientHom

Documentation

Prime-decomposition statement: for fixed σ ∈ I_w, the raw unit quotient is a group homomorphism Lˣ -> Lˣ / U^1.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

def inertiaUnitQuotientHom
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    Lˣ →* Lˣ ⧸ A.principalUnitGroup where
  toFun x := inertiaUnitQuotientClass K A σ x
  map_one' := by
    rw [inertiaUnitQuotientClass_eq_one_iff,
      automorphismUnitQuotient_one_arg]
    exact A.principalUnitGroup.one_mem
  map_mul' x y := by
    change
      QuotientGroup.mk' A.principalUnitGroup
          (automorphismUnitQuotient K A
            (σ : decompositionGroup K A) (x * y)) =
        QuotientGroup.mk' A.principalUnitGroup
            (automorphismUnitQuotient K A
              (σ : decompositionGroup K A) x) *
          QuotientGroup.mk' A.principalUnitGroup
            (automorphismUnitQuotient K A
              (σ : decompositionGroup K A) y)
    rw [automorphismUnitQuotient_mul_arg]
    exact map_mul (QuotientGroup.mk' A.principalUnitGroup)
      (automorphismUnitQuotient K A (σ : decompositionGroup K A) x)
      (automorphismUnitQuotient K A (σ : decompositionGroup K A) y)

theorem

inertiaUnitQuotientHom_apply

L648 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaUnitQuotientHom_apply

Documentation

States the theorem inertiaUnitQuotientHom_apply.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem inertiaUnitQuotientHom_apply
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) (x : Lˣ) :
    inertiaUnitQuotientHom K A σ x =
      inertiaUnitQuotientClass K A σ x

theorem

principalUnitQuotientToValueClass_comp_inertiaUnitQuotientHom

L656 ↗

RamificationTheory.HilbertRamification.ValuationSubring.principalUnitQuotientToValueClass_comp_inertiaUnitQuotientHom

Documentation

The raw inertia quotient followed by Lˣ/U^1 -> Lˣ/Aˣ is exactly value displacement.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem principalUnitQuotientToValueClass_comp_inertiaUnitQuotientHom
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    (principalUnitQuotientToValueClass A).comp
        (inertiaUnitQuotientHom K A σ) =
      valueDisplacementHom K A (σ : decompositionGroup K A)

theorem

unitGroup_le_inertiaUnitQuotientHom_ker

L665 ↗

RamificationTheory.HilbertRamification.ValuationSubring.unitGroup_le_inertiaUnitQuotientHom_ker

Documentation

The raw quotient homomorphism kills the valuation-ring unit group.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem unitGroup_le_inertiaUnitQuotientHom_ker
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    A.unitGroup ≤ (inertiaUnitQuotientHom K A σ).ker

def

valueClassToPrincipalUnitQuotient

L676 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueClassToPrincipalUnitQuotient

Documentation

Prime-decomposition statement: the raw character descends from representatives x : Lˣ to value classes modulo valuation-ring units. This is the quotient layer corresponding to Delta = w(L*).

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

def valueClassToPrincipalUnitQuotient
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    Lˣ ⧸ A.unitGroup →* Lˣ ⧸ A.principalUnitGroup

theorem

valueClassToPrincipalUnitQuotient_mk

L684 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueClassToPrincipalUnitQuotient_mk

Documentation

States the theorem valueClassToPrincipalUnitQuotient_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueClassToPrincipalUnitQuotient_mk
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) (x : Lˣ) :
    valueClassToPrincipalUnitQuotient K A σ
        (QuotientGroup.mk' A.unitGroup x) =
      inertiaUnitQuotientClass K A σ x

def

baseUnitToValueClass

L693 ↗

RamificationTheory.HilbertRamification.ValuationSubring.baseUnitToValueClass

Documentation

The image of base-field units in Lˣ / A.unitGroup. This is the subgroup that later realizes Gamma inside Delta.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

def baseUnitToValueClass (A : _root_.ValuationSubring L) :
    Kˣ →* Lˣ ⧸ A.unitGroup

theorem

baseUnitToValueClass_apply

L699 ↗

RamificationTheory.HilbertRamification.ValuationSubring.baseUnitToValueClass_apply

Documentation

States the theorem baseUnitToValueClass_apply.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem baseUnitToValueClass_apply
    (A : _root_.ValuationSubring L) (a : Kˣ) :
    baseUnitToValueClass K A a =
      QuotientGroup.mk' A.unitGroup
        (Units.map (algebraMap K L).toMonoidHom a)

abbrev

baseUnitValueClassSubgroup

L707 ↗

RamificationTheory.HilbertRamification.ValuationSubring.baseUnitValueClassSubgroup

Documentation

The subgroup of Lˣ/A.unitGroup generated by base-field value classes.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

abbrev baseUnitValueClassSubgroup (A : _root_.ValuationSubring L) :
    Subgroup (Lˣ ⧸ A.unitGroup)

instance

baseUnitValueClassSubgroup_normal

L712 ↗

RamificationTheory.HilbertRamification.ValuationSubring.baseUnitValueClassSubgroup_normal

Documentation

Provides the instance baseUnitValueClassSubgroup_normal.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

instance baseUnitValueClassSubgroup_normal
    (A : _root_.ValuationSubring L) :
    (baseUnitValueClassSubgroup K A).Normal

theorem

valueClassToPrincipalUnitQuotient_baseUnit

L723 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueClassToPrincipalUnitQuotient_baseUnit

Documentation

Base-field units map trivially under the descended raw character.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueClassToPrincipalUnitQuotient_baseUnit
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) (a : Kˣ) :
    valueClassToPrincipalUnitQuotient K A σ
        (baseUnitToValueClass K A a) = 1

theorem

baseUnitValueClassSubgroup_le_valueClassToPrincipalUnitQuotient_ker

L735 ↗

RamificationTheory.HilbertRamification.ValuationSubring.baseUnitValueClassSubgroup_le_valueClassToPrincipalUnitQuotient_ker

Documentation

The base-field value classes lie in the kernel of the descended raw character.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem baseUnitValueClassSubgroup_le_valueClassToPrincipalUnitQuotient_ker
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    baseUnitValueClassSubgroup K A ≤
      (valueClassToPrincipalUnitQuotient K A σ).ker

def

valueModuloBaseToPrincipalUnitQuotient

L747 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueModuloBaseToPrincipalUnitQuotient

Documentation

Prime-decomposition statement: the raw character descends further modulo the base value group. This quotient is the group-theoretic model of Delta/Gamma before identifying it with a concrete value-group quotient.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

def valueModuloBaseToPrincipalUnitQuotient
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    (Lˣ ⧸ A.unitGroup) ⧸ baseUnitValueClassSubgroup K A →*
      Lˣ ⧸ A.principalUnitGroup

theorem

valueModuloBaseToPrincipalUnitQuotient_mk

L757 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueModuloBaseToPrincipalUnitQuotient_mk

Documentation

States the theorem valueModuloBaseToPrincipalUnitQuotient_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueModuloBaseToPrincipalUnitQuotient_mk
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A)
    (x : Lˣ ⧸ A.unitGroup) :
    valueModuloBaseToPrincipalUnitQuotient K A σ
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K A) x) =
      valueClassToPrincipalUnitQuotient K A σ x

theorem

valueModuloBaseToPrincipalUnitQuotient_mk_mk

L766 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueModuloBaseToPrincipalUnitQuotient_mk_mk

Documentation

States the theorem valueModuloBaseToPrincipalUnitQuotient_mk_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueModuloBaseToPrincipalUnitQuotient_mk_mk
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) (x : Lˣ) :
    valueModuloBaseToPrincipalUnitQuotient K A σ
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K A)
          (QuotientGroup.mk' A.unitGroup x)) =
      inertiaUnitQuotientClass K A σ x

theorem

baseUnitValueClassSubgroup_le_valueClassToResidueUnits_ker

L775 ↗

RamificationTheory.HilbertRamification.ValuationSubring.baseUnitValueClassSubgroup_le_valueClassToResidueUnits_ker

Documentation

The base value classes are killed by the residue-unit character.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem baseUnitValueClassSubgroup_le_valueClassToResidueUnits_ker
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    baseUnitValueClassSubgroup K A ≤
      (valueClassToResidueUnits K A σ).ker

def

valueModuloBaseToResidueUnits

L788 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueModuloBaseToResidueUnits

Documentation

Prime-decomposition statement: the residue-unit character on Delta/Gamma, modeled as (Lˣ/Aˣ)/(Kˣ), for value-trivial inertia.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

def valueModuloBaseToResidueUnits
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    (Lˣ ⧸ A.unitGroup) ⧸ baseUnitValueClassSubgroup K A →*
      (IsLocalRing.ResidueField A)ˣ

theorem

valueModuloBaseToResidueUnits_mk

L799 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueModuloBaseToResidueUnits_mk

Documentation

States the theorem valueModuloBaseToResidueUnits_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueModuloBaseToResidueUnits_mk
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (x : Lˣ ⧸ A.unitGroup) :
    valueModuloBaseToResidueUnits K A σ
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K A) x) =
      valueClassToResidueUnits K A σ x

theorem

valueModuloBaseToResidueUnits_mk_mk

L808 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueModuloBaseToResidueUnits_mk_mk

Documentation

States the theorem valueModuloBaseToResidueUnits_mk_mk.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueModuloBaseToResidueUnits_mk_mk
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) (x : Lˣ) :
    valueModuloBaseToResidueUnits K A σ
        (QuotientGroup.mk' (baseUnitValueClassSubgroup K A)
          (QuotientGroup.mk' A.unitGroup x)) =
      valueTrivialInertiaResidueUnitHom K A σ x

theorem

valueModuloBaseToResidueUnits_eq_one_of_mem_ramificationGroup

L821 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueModuloBaseToResidueUnits_eq_one_of_mem_ramificationGroup

Documentation

The inertia-character construction satisfies: an element of R_w gives the trivial residue-unit character on Delta/Gamma. This is the kernel direction for the canonical map from inertia to Hom(Delta/Gamma, lambda*).

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueModuloBaseToResidueUnits_eq_one_of_mem_ramificationGroup
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A)
    (hσ : (σ : inertiaGroup K A) ∈ ramificationGroup K A) :
    valueModuloBaseToResidueUnits K A σ = 1

def

valueTrivialInertiaCharacterHom

L842 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaCharacterHom

Documentation

prime-decomposition theory: σ ↦ χ_σ, realized on the group-theoretic model of Delta/Gamma.

For mathlib's valuation-subring stabilizer this is stated on the value-trivial inertia subgroup; for a chosen valuation in the exact-extension sense this is the ordinary inertia group.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

def valueTrivialInertiaCharacterHom
    (A : _root_.ValuationSubring L) :
    valueTrivialInertiaGroup K A →*
      ((Lˣ ⧸ A.unitGroup) ⧸ baseUnitValueClassSubgroup K A →*
        (IsLocalRing.ResidueField A)ˣ) where
  toFun σ := valueModuloBaseToResidueUnits K A σ
  map_one' := by
    apply QuotientGroup.monoidHom_ext
    apply QuotientGroup.monoidHom_ext
    apply MonoidHom.ext
    intro x
    simp only [MonoidHom.comp_apply,
      valueModuloBaseToResidueUnits_mk_mk,
      MonoidHom.one_apply]
    exact valueTrivialInertiaResidueUnitHom_one (K := K) A x
  map_mul' σ τ := by
    apply QuotientGroup.monoidHom_ext
    apply QuotientGroup.monoidHom_ext
    apply MonoidHom.ext
    intro x
    change
      valueModuloBaseToResidueUnits K A (σ * τ)
          (QuotientGroup.mk' (baseUnitValueClassSubgroup K A)
            (QuotientGroup.mk' A.unitGroup x)) =
        valueModuloBaseToResidueUnits K A σ
            (QuotientGroup.mk' (baseUnitValueClassSubgroup K A)
              (QuotientGroup.mk' A.unitGroup x)) *
          valueModuloBaseToResidueUnits K A τ
            (QuotientGroup.mk' (baseUnitValueClassSubgroup K A)
              (QuotientGroup.mk' A.unitGroup x))
    rw [valueModuloBaseToResidueUnits_mk_mk,
      valueModuloBaseToResidueUnits_mk_mk,
      valueModuloBaseToResidueUnits_mk_mk]
    exact valueTrivialInertiaResidueUnitHom_mul (K := K) A σ τ x

theorem

valueTrivialInertiaCharacterHom_apply

L878 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaCharacterHom_apply

Documentation

States the theorem valueTrivialInertiaCharacterHom_apply.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaCharacterHom_apply
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    valueTrivialInertiaCharacterHom K A σ =
      valueModuloBaseToResidueUnits K A σ

theorem

valueTrivialInertiaCharacterHom_mem_ker_of_mem_ramificationGroup

L886 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaCharacterHom_mem_ker_of_mem_ramificationGroup

Documentation

The ramification group is contained in the kernel of the character map.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaCharacterHom_mem_ker_of_mem_ramificationGroup
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A)
    (hσ : (σ : inertiaGroup K A) ∈ ramificationGroup K A) :
    σ ∈ (valueTrivialInertiaCharacterHom K A).ker

theorem

mem_ramificationGroup_of_valueTrivialInertiaCharacterHom_mem_ker

L897 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroup_of_valueTrivialInertiaCharacterHom_mem_ker

Documentation

Conversely, a value-trivial inertia element with trivial character lies in the ramification group.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem mem_ramificationGroup_of_valueTrivialInertiaCharacterHom_mem_ker
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A)
    (hσ : σ ∈ (valueTrivialInertiaCharacterHom K A).ker) :
    (σ : inertiaGroup K A) ∈ ramificationGroup K A

theorem

valueTrivialInertiaCharacterHom_mem_ker_iff

L936 ↗

RamificationTheory.HilbertRamification.ValuationSubring.valueTrivialInertiaCharacterHom_mem_ker_iff

Documentation

Prime-decomposition statement: on value-trivial inertia, the kernel of σ ↦ χ_σ is exactly R_w.

Source context 6 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valueTrivialInertiaCharacterHom_mem_ker_iff
    (A : _root_.ValuationSubring L)
    (σ : valueTrivialInertiaGroup K A) :
    σ ∈ (valueTrivialInertiaCharacterHom K A).ker ↔
      (σ : inertiaGroup K A) ∈ ramificationGroup K A

Module documentation

Hilbert ramification theory: character-map source

Declarations