NYLL
Module

LowerRamificationGroup.lean

Nyll.ClassFieldTheory.Definitions.HasseArf.LowerRamificationGroup
2 declarations indexed from sourceView source ↗

Module documentation

Lower ramification groups

Imports1
  • Mathlib.RingTheory.Valuation.RamificationGroup
Imported by8

Declarations

lemma

smul_mem_maximalIdeal_pow

L19 ↗
ClassFieldTheory.smul_mem_maximalIdeal_pow
Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
lemma smul_mem_maximalIdeal_pow
    (A : ValuationSubring L) (n : ℕ)
    (σ : A.decompositionSubgroup K) {x : A}
    (hx : x ∈ (IsLocalRing.maximalIdeal A) ^ n) :
    σ • x ∈ (IsLocalRing.maximalIdeal A) ^ n
def

lowerRamificationGroup

L32 ↗
ClassFieldTheory.lowerRamificationGroup
Documentation

The n-th ramification group in lower numbering for the valuation subring A. Its elements act trivially on A / m^(n + 1).

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
def lowerRamificationGroup (A : ValuationSubring L) (n : ℕ) :
    Subgroup (A.decompositionSubgroup K) where
  carrier := {σ | ∀ x : A,
    σ • x - x ∈ (IsLocalRing.maximalIdeal A) ^ (n + 1)}
  one_mem' := by simp
  mul_mem' := by
    intro σ τ hσ hτ x
    have hτ' := smul_mem_maximalIdeal_pow K A (n + 1) σ (hτ x)
    have hsum :=
      (IsLocalRing.maximalIdeal A ^ (n + 1)).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 ^ (n + 1)).neg_mem (hσ (σ⁻¹ • x))

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