NYLL
Module

LowerRamificationGroupEventuallyBot.lean

Nyll.ClassFieldTheory.Theorems.HasseArf.LowerRamificationGroupEventuallyBot
1 declaration indexed from sourceView source ↗

Module documentation

Eventual triviality of lower ramification groups

For a finite field extension and a Noetherian valuation subring, each nonidentity automorphism moves an element of the valuation ring by a nonzero amount. Krull's intersection theorem then excludes that automorphism from some lower group. Finiteness gives a common bound for all automorphisms.

Imports5
Imported by2

Declarations

theorem

lowerRamificationGroup_eventually_bot

L29 ↗
ClassFieldTheory.lowerRamificationGroup_eventually_bot
Documentation

All sufficiently high lower ramification groups are trivial.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v
Lean source · statement
theorem lowerRamificationGroup_eventually_bot
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (A : ValuationSubring L) [IsNoetherianRing A] :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → lowerRamificationGroup K A n = ⊥

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