NYLL
Module

FiniteInertiaCentrality.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FiniteInertiaCentrality
4 declarations indexed from sourceView source ↗

Module documentation

Finite inertia and roots of unity

Roots of unity in the base force trivial residue action on those roots. For a finite extension with Henselian valuation ring and residue characteristic zero, the corresponding finite-order inertia elements commute with decomposition.

Imports7
Imported by2

Declarations

theorem

residueAction_fixes_pow_eq_one_of_primitiveRoot_of_henselianRing

L33 ↗
RamificationTheory.HilbertRamification.ValuationSubring.residueAction_fixes_pow_eq_one_of_primitiveRoot_of_henselianRing
Documentation

If all roots of a fixed order split over the base, decomposition acts trivially on the roots of that order in the Henselian residue field.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open ValuationTheory.DiscreteValuationField
universe u v w
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem residueAction_fixes_pow_eq_one_of_primitiveRoot_of_henselianRing
    (A : _root_.ValuationSubring L)
    [HenselianRing A (IsLocalRing.maximalIdeal A)] (n : ℕ)
    [NeZero (n : (IsLocalRing.ResidueField A))]
    (ζ : K) (hζ : IsPrimitiveRoot ζ n)
    (σ : decompositionGroup K A)
    (ξ : (IsLocalRing.ResidueField A)) (hξ : ξ ^ n = 1) :
    residueAction K A σ ξ = ξ
theorem

inertia_commutes_of_primitiveRoot_of_henselianRing

L65 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertia_commutes_of_primitiveRoot_of_henselianRing
Documentation

In a finite valued extension, an inertia element of order dividing n commutes with the entire decomposition group if a primitive n-th root belongs to the base.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open ValuationTheory.DiscreteValuationField
universe u v w
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem inertia_commutes_of_primitiveRoot_of_henselianRing [FiniteDimensional K L]
    (A : _root_.ValuationSubring L)
    [HenselianRing A (IsLocalRing.maximalIdeal A)] [CharZero (IsLocalRing.ResidueField A)]
    (n : ℕ) (hn : 0 < n) (ζ : K) (hζ : IsPrimitiveRoot ζ n)
    (τ : inertiaGroup K A) (hτ : τ ^ n = 1)
    (g : decompositionGroup K A) :
    Commute g (τ : decompositionGroup K A)
theorem

residueAction_fixes_pow_eq_one_of_primitiveRoot

L113 ↗
RamificationTheory.HilbertRamification.ValuationSubring.residueAction_fixes_pow_eq_one_of_primitiveRoot
Documentation

The Henselian DVF form of rootwise residue-action triviality.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open ValuationTheory.DiscreteValuationField
universe u v w
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem residueAction_fixes_pow_eq_one_of_primitiveRoot
    (F : HenselianDVF.{v, w} L) (n : ℕ) [NeZero (n : F.residueField)]
    (ζ : K) (hζ : IsPrimitiveRoot ζ n)
    (σ : decompositionGroup K F.valuation.valuationSubring)
    (ξ : F.residueField) (hξ : ξ ^ n = 1) :
    residueAction K F.valuation.valuationSubring σ ξ = ξ
theorem

inertia_commutes_of_primitiveRoot

L123 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertia_commutes_of_primitiveRoot
Documentation

The Henselian DVF form of finite inertia centrality.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open ValuationTheory.DiscreteValuationField
universe u v w
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem inertia_commutes_of_primitiveRoot [FiniteDimensional K L]
    (F : HenselianDVF.{v, w} L) [CharZero F.residueField]
    (n : ℕ) (hn : 0 < n) (ζ : K) (hζ : IsPrimitiveRoot ζ n)
    (τ : inertiaGroup K F.valuation.valuationSubring) (hτ : τ ^ n = 1)
    (g : decompositionGroup K F.valuation.valuationSubring) :
    Commute g (τ : decompositionGroup K F.valuation.valuationSubring)

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