Module

CanonicalCharacterTower.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.CanonicalCharacterTower

3 declarations indexed from sourceView source ↗

Module documentation

Normalization of a raw character transition

The canonical finite tame character is the raw uniformizer character raised to e / n. The raw tower exponent is the relative ramification index. The following arithmetic converts that exponent into the ratio of the actual finite tame orders. Coprimality with the upper normalization factor also supplies divisibility of the tame orders without inertia surjectivity.

Imports3

Mathlib.Data.Nat.GCD.Basic
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Tactic.Ring

Imported by3

theorem

tameOrder_dvd_of_ramificationIdx_dvd

L26 ↗

RamificationTheory.HilbertRamification.tameOrder_dvd_of_ramificationIdx_dvd

Documentation

A prime-to-wild divisor of a lower ramification index divides the upper tame order. In the actual tower the coprimality comes from residue invertibility and the upper normalization factor being a characteristic power.

Source context 1 command

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

namespace RamificationTheory.HilbertRamification

Lean source · statement

theorem tameOrder_dvd_of_ramificationIdx_dvd
    {nE nF eE eF : ℕ} (hnE : nE ∣ eE) (hnF : nF ∣ eF)
    (he : eE ∣ eF) (hcoprime : Nat.Coprime nE (eF / nF)) : nE ∣ nF

theorem

normalizationExponents_tower

L33 ↗

RamificationTheory.HilbertRamification.normalizationExponents_tower

Source context 1 command

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

namespace RamificationTheory.HilbertRamification

Lean source · statement

theorem normalizationExponents_tower
    {nE nF eE eF r : ℕ} (hnEpos : 0 < nE)
    (hnE : nE ∣ eE) (hnF : nF ∣ eF) (hn : nE ∣ nF)
    (he : eF = r * eE) :
    r * (eE / nE) = (eF / nF) * (nF / nE)

theorem

normalizedCharacter_tower

L54 ↗

RamificationTheory.HilbertRamification.normalizedCharacter_tower

Documentation

A raw character relation at the relative ramification index becomes the canonical relation at the ratio of the actual tame orders after normalizing both characters by their own e / n. The coefficient map is retained literally; no new carrier or comparison map is introduced.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification
universe u v

Lean source · statement

theorem normalizedCharacter_tower
    {M : Type u} {N : Type v} [Monoid M] [Monoid N]
    (i : M →* N) (x : M) (y : N)
    {nE nF eE eF r : ℕ} (hnEpos : 0 < nE)
    (hnE : nE ∣ eE) (hnF : nF ∣ eF) (hn : nE ∣ nF)
    (he : eF = r * eE) (hraw : i.toFun x = y ^ r) :
    i.toFun (x ^ (eE / nE)) = (y ^ (eF / nF)) ^ (nF / nE)

Module documentation

Normalization of a raw character transition

Declarations

tameOrder_dvd_of_ramificationIdx_dvd

normalizationExponents_tower

normalizedCharacter_tower