Module

RingInertiaCharacterFixedElement.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingInertiaCharacterFixedElement

2 declarations indexed from sourceView source ↗

Module documentation

Fixed elements and powers of the inertia character

Proves that fixing a unit times a uniformizer power makes the same power of the inertia character trivial. It deduces the corresponding result using the additive valuation of a nonzero fixed element.

Imports4

Mathlib.Algebra.Ring.Action.Basic
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingInertiaCharacter
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.Tactic.Ring

Imported by2

theorem

inertiaResidueCharacter_pow_eq_one_of_fixed_factor

L33 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaResidueCharacter_pow_eq_one_of_fixed_factor

Documentation

Fixing a unit times a uniformizer power annihilates the same power of the actual residue character. The ratio calculation has no additive valuation in scope.

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_pow_eq_one_of_fixed_factor
    (π : R) (hπ : Irreducible π) (σ : (maximalIdeal R).inertia G)
    (n : ℕ) (u : Rˣ)
    (hfixed : (σ : G) • ((u : R) * π ^ n) = (u : R) * π ^ n) :
    inertiaResidueCharacter R G σ ^ n = 1

theorem

inertiaResidueCharacter_pow_addVal_eq_one_of_fixed

L66 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.inertiaResidueCharacter_pow_addVal_eq_one_of_fixed