Module

RealLowerRamificationGroup.lean

Nyll.ClassFieldTheory.Definitions.HasseArf.RealLowerRamificationGroup

3 declarations indexed from sourceView source ↗

Module documentation

Real-index lower ramification groups

The ideal exponent at a real index s is max(0, ceil(s + 1)). Consequently, indices at or below -1 give the whole decomposition group, and natural indices recover the usual m^(n+1) displacement condition.

Imports4

Nyll.ClassFieldTheory.Definitions.HasseArf.LowerRamificationGroup
Mathlib.Algebra.Order.Archimedean.Real.Basic
Mathlib.Algebra.Order.Floor.Ring
Mathlib.Basic.Real.Basic

Imported by6

lemma

smul_mem_maximalIdeal_pow_real

L28 ↗

ClassFieldTheory.smul_mem_maximalIdeal_pow_real

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

lemma smul_mem_maximalIdeal_pow_real
    (A : ValuationSubring L) (k : ℕ)
    (σ : A.decompositionSubgroup K) {x : A}
    (hx : x ∈ (IsLocalRing.maximalIdeal A) ^ k) :
    σ • x ∈ (IsLocalRing.maximalIdeal A) ^ k

def

realLowerRamificationGroup

L41 ↗

ClassFieldTheory.realLowerRamificationGroup

Documentation

The real-index lower ramification group of a valuation subring. Its elements act trivially modulo m ^ max(0, ceil(s + 1)).

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · full declaration

def realLowerRamificationGroup (A : ValuationSubring L) (s : ℝ) :
    Subgroup (A.decompositionSubgroup K) where
  carrier := {σ | ∀ x : A,
    σ • x - x ∈
      (IsLocalRing.maximalIdeal A) ^ (Int.ceil (s + 1)).toNat}
  one_mem' := by simp
  mul_mem' := by
    intro σ τ hσ hτ x
    have hτ' := smul_mem_maximalIdeal_pow_real K A
      (Int.ceil (s + 1)).toNat σ (hτ x)
    have hsum :=
      (IsLocalRing.maximalIdeal A ^ (Int.ceil (s + 1)).toNat).add_mem
        hτ' (hσ x)
    simpa [mul_smul, smul_sub, sub_eq_add_neg, add_assoc] using hsum
  inv_mem' := by
    intro σ hσ x
    simpa [smul_smul] using
      (IsLocalRing.maximalIdeal A ^ (Int.ceil (s + 1)).toNat).neg_mem
        (hσ (σ⁻¹ • x))

theorem

realLowerRamificationGroup_eq_top_of_le_neg_one

L63 ↗

ClassFieldTheory.realLowerRamificationGroup_eq_top_of_le_neg_one

Documentation

At or below index -1, the real lower ramification group is the full decomposition group.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem realLowerRamificationGroup_eq_top_of_le_neg_one
    (A : ValuationSubring L) {s : ℝ} (hs : s ≤ -1) :
    realLowerRamificationGroup K A s = ⊤

Module documentation

Real-index lower ramification groups

Declarations

smul_mem_maximalIdeal_pow_real

realLowerRamificationGroup

realLowerRamificationGroup_eq_top_of_le_neg_one