NYLL
Module

TameNormalizationExponent.lean

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

Module documentation

The actual tame-character normalization exponent

The two inertia-cardinality formulas and the actual tame-degree divisibility show that the ratio of the ramification index to the tame degree divides the wild order. Thus it is a residue-characteristic power, and is prime to the tame degree. No residue-separability assertion is needed for this arithmetic.

Imports2
  • Mathlib.Data.Nat.Prime.Basic
  • Mathlib.Data.Nat.GCD.Basic
Imported by2

Declarations

theorem

divisor_of_normalization_factor

L21 ↗
RamificationTheory.HilbertRamification.divisor_of_normalization_factor
Source context 1 command

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

namespace RamificationTheory.HilbertRamification
Lean source · statement
theorem divisor_of_normalization_factor
    {n e w f : ℕ} (hn : 0 < n) (hne : n ∣ e) (horder : n * w = e * f) :
    e / n ∣ w
theorem

tameNormalizationExponent_eq_prime_pow

L36 ↗
RamificationTheory.HilbertRamification.tameNormalizationExponent_eq_prime_pow
Documentation

The normalization exponent is a characteristic power when the wild order is a characteristic power. The inseparable residue factor can remain arbitrary in the supplied actual cardinality identity.

Source context 1 command

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

namespace RamificationTheory.HilbertRamification
Lean source · statement
theorem tameNormalizationExponent_eq_prime_pow
    {p n e w f a : ℕ} (hp : Nat.Prime p) (hn : 0 < n)
    (hne : n ∣ e) (horder : n * w = e * f) (hw : w = p ^ a) :
    ∃ b : ℕ, e / n = p ^ b
theorem

tameNormalizationExponent_coprime

L46 ↗
RamificationTheory.HilbertRamification.tameNormalizationExponent_coprime
Documentation

The actual normalization power is invertible modulo the tame degree.

Source context 1 command

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

namespace RamificationTheory.HilbertRamification
Lean source · statement
theorem tameNormalizationExponent_coprime
    {p n e w f a : ℕ} (hp : Nat.Prime p) (hn : 0 < n)
    (hne : n ∣ e) (horder : n * w = e * f) (hw : w = p ^ a)
    (hnp : Nat.Coprime n p) : Nat.Coprime n (e / n)
theorem

tameNormalizationExponent_eq_one_of_wild_eq_one

L55 ↗
RamificationTheory.HilbertRamification.tameNormalizationExponent_eq_one_of_wild_eq_one
Documentation

Trivial wild inertia forces the actual normalization exponent to be one.

Source context 1 command

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

namespace RamificationTheory.HilbertRamification
Lean source · statement
theorem tameNormalizationExponent_eq_one_of_wild_eq_one
    {n e w f : ℕ} (hn : 0 < n) (hne : n ∣ e)
    (horder : n * w = e * f) (hw : w = 1) : e / n = 1

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