NYLL
Module

RealLowerGroups.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RealLowerGroups
36 declarations indexed from sourceView source ↗

Module documentation

Real lower ramification groups

This file gives the intrinsic definitions and the elementary structural facts in the real lower-ramification definition and the lower-ramification base-change law. It uses discretely valued fields, not complete discretely valued fields. The unique extension hypothesis is stated for DVF itself and is used to derive (rather than assume) preservation of the chosen valuation ring by the Galois group.

The real index is implemented canonically by the maximal-ideal filtration: the condition at s is membership in m ^ ceil(s + 1). The exponent is truncated at zero, so the definition extends harmlessly to every real number and is the full Galois group for s <= -1.

Imports4
Imported by10

Declarations

def

HasUniqueValuationExtension

L48 ↗
RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension
Documentation

Unique extension of a valuation, at the general DVF level.

This is the direct noncomplete analogue of the existing predicates on HenselianDVF and CompleteDVF: every valuation of L extending the chosen base valuation is equivalent to the chosen target valuation.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
def HasUniqueValuationExtension (base : DVF.{u, v} K)
    (target : DVF.{w, x} L) : Prop
theorem

algEquiv_comap_valuation_hasExtension

L56 ↗
RamificationTheory.DiscreteValuationField.DVF.algEquiv_comap_valuation_hasExtension
Documentation

Pulling the target valuation back along a K-automorphism again gives an extension of the base valuation.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem algEquiv_comap_valuation_hasExtension
    {base : DVF.{u, v} K} {target : DVF.{w, x} L}
    [base.valuation.HasExtension target.valuation]
    (σ : L ≃ₐ[K] L) :
    base.valuation.HasExtension (target.valuation.comap (σ : L →+* L)) where
  val_isEquiv_comap := by
    rw [_root_.Valuation.isEquiv_iff_val_le_one]
    intro a
    simpa [_root_.Valuation.comap, σ.commutes a] using
      (_root_.Valuation.HasExtension.val_map_le_one_iff
        (vR := base.valuation) (vA := target.valuation) a).symm
theorem

mem_valuationSubring_algEquiv_iff_of_hasUniqueValuationExtension

L70 ↗
RamificationTheory.DiscreteValuationField.DVF.mem_valuationSubring_algEquiv_iff_of_hasUniqueValuationExtension
Documentation

Unique extension makes every K-automorphism preserve membership in the chosen target valuation ring.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace DVF
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem mem_valuationSubring_algEquiv_iff_of_hasUniqueValuationExtension
    {base : DVF.{u, v} K} {target : DVF.{w, x} L}
    [base.valuation.HasExtension target.valuation]
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x} base target)
    (σ : L ≃ₐ[K] L) (z : L) :
    z ∈ target.valuation.valuationSubring ↔
      σ z ∈ target.valuation.valuationSubring
def

realRamificationExponent

L108 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationExponent
Documentation

The integral exponent corresponding to a real lower ramification index.

For s >= -1 this is ceil (s + 1). The use of Int.toNat also makes it zero for s <= -1, which gives the expected constant extension below the natural indexing range.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def realRamificationExponent (s : ℝ) : ℕ
theorem

realRamificationExponent_mono

L112 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationExponent_mono
Documentation

States the theorem realRamificationExponent_mono.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationExponent_mono :
    Monotone realRamificationExponent
theorem

realRamificationExponent_neg_one

L120 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationExponent_neg_one
Documentation

States the theorem realRamificationExponent_neg_one.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationExponent_neg_one :
    realRamificationExponent (-1) = 0
theorem

realRamificationExponent_eq_zero_of_le_neg_one

L125 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationExponent_eq_zero_of_le_neg_one
Documentation

States the theorem realRamificationExponent_eq_zero_of_le_neg_one.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationExponent_eq_zero_of_le_neg_one
    {s : ℝ} (hs : s ≤ -1) :
    realRamificationExponent s = 0
theorem

realRamificationExponent_nat

L133 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationExponent_nat
Documentation

States the theorem realRamificationExponent_nat.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationExponent_nat (n : ℕ) :
    realRamificationExponent (n : ℝ) = n + 1
def

realRamificationIdeal

L138 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationIdeal
Documentation

The maximal-ideal power representing the real lower index s.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def realRamificationIdeal (target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L)
    (s : ℝ) : Ideal target.valuationSubring
theorem

realRamificationIdeal_antitone

L143 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationIdeal_antitone
Documentation

States the theorem realRamificationIdeal_antitone.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationIdeal_antitone {s t : ℝ} (hst : s ≤ t) :
    realRamificationIdeal target t ≤ realRamificationIdeal target s
theorem

realRamificationIdeal_neg_one

L148 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationIdeal_neg_one
Documentation

States the theorem realRamificationIdeal_neg_one.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationIdeal_neg_one :
    realRamificationIdeal target (-1) = ⊤
theorem

realRamificationIdeal_nat

L153 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationIdeal_nat
Documentation

States the theorem realRamificationIdeal_nat.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationIdeal_nat (n : ℕ) :
    realRamificationIdeal target (n : ℝ) = target.maximalIdeal ^ (n + 1)
theorem

realRamificationIdeal_eq_top_of_le_neg_one

L158 ↗
RamificationTheory.HilbertRamification.Higher.realRamificationIdeal_eq_top_of_le_neg_one
Documentation

States the theorem realRamificationIdeal_eq_top_of_le_neg_one.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem realRamificationIdeal_eq_top_of_le_neg_one
    {s : ℝ} (hs : s ≤ -1) :
    realRamificationIdeal target s = ⊤
def

valuationSubringAutOfUniqueExtension

L166 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension
Documentation

The automorphism induced on the target valuation ring by uniqueness of the valuation extension.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · full declaration
def valuationSubringAutOfUniqueExtension
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (σ : Gal(L/K)) :
    target.valuationSubring ≃+* target.valuationSubring where
  toFun a :=
    ⟨σ (a : L),
      (mem_valuationSubring_algEquiv_iff_of_hasUniqueValuationExtension
          (base := base) (target := target) huniq σ (a : L)).1 a.property⟩
  invFun a :=
    ⟨σ⁻¹ (a : L),
      (mem_valuationSubring_algEquiv_iff_of_hasUniqueValuationExtension
          (base := base) (target := target) huniq σ⁻¹ (a : L)).1 a.property⟩
  left_inv a := by
    ext
    simp
  right_inv a := by
    ext
    simp
  map_mul' a b := by
    ext
    simp
  map_add' a b := by
    ext
    simp
theorem

valuationSubringAutOfUniqueExtension_apply_coe

L193 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_apply_coe
Documentation

States the theorem valuationSubringAutOfUniqueExtension_apply_coe.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_apply_coe
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (σ : Gal(L/K)) (a : target.valuationSubring) :
    ((valuationSubringAutOfUniqueExtension
      (base := base) (target := target) huniq σ a :
        target.valuationSubring) : L) = σ (a : L)
theorem

valuationSubringAutOfUniqueExtension_one_apply

L203 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_one_apply
Documentation

States the theorem valuationSubringAutOfUniqueExtension_one_apply.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_one_apply
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (a : target.valuationSubring) :
    valuationSubringAutOfUniqueExtension
      (base := base) (target := target) huniq 1 a = a
theorem

valuationSubringAutOfUniqueExtension_mul_apply

L213 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_mul_apply
Documentation

States the theorem valuationSubringAutOfUniqueExtension_mul_apply.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_mul_apply
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (σ τ : Gal(L/K)) (a : target.valuationSubring) :
    valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq (σ * τ) a =
      valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq σ
        (valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq τ a)
theorem

valuationSubringAutOfUniqueExtension_apply_inv_apply

L227 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_apply_inv_apply
Documentation

States the theorem valuationSubringAutOfUniqueExtension_apply_inv_apply.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_apply_inv_apply
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (σ : Gal(L/K)) (a : target.valuationSubring) :
    valuationSubringAutOfUniqueExtension
      (base := base) (target := target) huniq σ
      (valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq σ⁻¹ a) = a
theorem

valuationSubringAutOfUniqueExtension_mem_maximalIdeal_iff

L240 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_mem_maximalIdeal_iff
Documentation

A uniquely extended valuation-ring automorphism preserves the maximal ideal.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_mem_maximalIdeal_iff
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (σ : Gal(L/K)) (a : target.valuationSubring) :
    valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq σ a ∈ target.maximalIdeal ↔
      a ∈ target.maximalIdeal
theorem

valuationSubringAutOfUniqueExtension_mem_maximalIdeal_pow_iff

L260 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_mem_maximalIdeal_pow_iff
Documentation

A uniquely extended valuation-ring automorphism preserves every power of the maximal ideal.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_mem_maximalIdeal_pow_iff
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (σ : Gal(L/K)) (n : ℕ) (a : target.valuationSubring) :
    valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq σ a ∈ target.maximalIdeal ^ n ↔
      a ∈ target.maximalIdeal ^ n
theorem

valuationSubringAutOfUniqueExtension_mem_realRamificationIdeal_iff

L304 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_mem_realRamificationIdeal_iff
Documentation

States the theorem valuationSubringAutOfUniqueExtension_mem_realRamificationIdeal_iff.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_mem_realRamificationIdeal_iff
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (σ : Gal(L/K)) (s : ℝ) (a : target.valuationSubring) :
    valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq σ a ∈
          realRamificationIdeal target s ↔
      a ∈ realRamificationIdeal target s
def

lowerRamificationGroup

L320 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup
Documentation

The real lower-ramification definition: the real-index lower ramification group. On the natural range s >= -1, membership is exactly the condition that all integral displacements have normalized additive value at least s + 1, expressed intrinsically as membership in m ^ ceil(s + 1).

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · full declaration
def lowerRamificationGroup
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (s : ℝ) : Subgroup Gal(L/K) where
  carrier :=
    {σ | ∀ a : target.valuationSubring,
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq σ a - a ∈
        realRamificationIdeal target s}
  one_mem' := by
    intro a
    simp
  mul_mem' := by
    intro σ τ hσ hτ a
    have hτa :
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq τ a - a ∈
          realRamificationIdeal target s :=
      hτ a
    have hmapτa :
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq σ
            (valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq τ a - a) ∈
          realRamificationIdeal target s :=
      (valuationSubringAutOfUniqueExtension_mem_realRamificationIdeal_iff
        (base := base) (target := target) huniq σ s _).2 hτa
    have hσa :
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq σ a - a ∈
          realRamificationIdeal target s :=
      hσ a
    have hdecomp :
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq (σ * τ) a - a =
          valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq σ
              (valuationSubringAutOfUniqueExtension
                (base := base) (target := target) huniq τ a - a) +
            (valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq σ a - a) := by
      rw [valuationSubringAutOfUniqueExtension_mul_apply, map_sub]
      ring
    rw [hdecomp]
    exact Ideal.add_mem _ hmapτa hσa
  inv_mem' := by
    intro σ hσ a
    let b := valuationSubringAutOfUniqueExtension
      (base := base) (target := target) huniq σ⁻¹ a
    have hb :
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq σ b - b ∈
          realRamificationIdeal target s :=
      hσ b
    have hab : a - b ∈ realRamificationIdeal target s := by
      simpa [b] using hb
    have hba : b - a ∈ realRamificationIdeal target s := by
      simpa [sub_eq_add_neg, add_comm] using
        (realRamificationIdeal target s).neg_mem hab
    simpa [b] using hba
theorem

mem_lowerRamificationGroup_iff

L382 ↗
RamificationTheory.HilbertRamification.Higher.mem_lowerRamificationGroup_iff
Documentation

States the theorem mem_lowerRamificationGroup_iff.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem mem_lowerRamificationGroup_iff
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (s : ℝ) (σ : Gal(L/K)) :
    σ ∈ lowerRamificationGroup
        (base := base) (target := target) huniq s ↔
      ∀ a : target.valuationSubring,
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq σ a - a ∈
          realRamificationIdeal target s
theorem

mem_lowerRamificationGroup_nat_iff

L396 ↗
RamificationTheory.HilbertRamification.Higher.mem_lowerRamificationGroup_nat_iff
Documentation

At an integral index, the real definition is exactly the usual m^(n+1) displacement condition.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem mem_lowerRamificationGroup_nat_iff
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (n : ℕ) (σ : Gal(L/K)) :
    σ ∈ lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ) ↔
      ∀ a : target.valuationSubring,
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq σ a - a ∈
          target.maximalIdeal ^ (n + 1)
theorem

lowerRamificationGroup_antitone

L409 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup_antitone
Documentation

The real lower-ramification definition: the lower groups are decreasing in their real index.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem lowerRamificationGroup_antitone
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    Antitone (lowerRamificationGroup
      (base := base) (target := target) huniq)
theorem

lowerRamificationGroup_normal

L418 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup_normal
Documentation

The real lower-ramification definition: every real lower ramification group is normal.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem lowerRamificationGroup_normal
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (s : ℝ) :
    (lowerRamificationGroup
      (base := base) (target := target) huniq s).Normal
instance

instNormal

L452 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup.instNormal
Documentation

Provides the instance instNormal.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
instance lowerRamificationGroup.instNormal
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (s : ℝ) :
    (lowerRamificationGroup
      (base := base) (target := target) huniq s).Normal
theorem

lowerRamificationGroup_neg_one

L462 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup_neg_one
Documentation

The real lower-ramification definition: G_{-1} is the full Galois group.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem lowerRamificationGroup_neg_one
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target) :
    lowerRamificationGroup
      (base := base) (target := target) huniq (-1) = ⊤
theorem

lowerRamificationGroup_eq_top_of_le_neg_one

L472 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroup_eq_top_of_le_neg_one
Documentation

The all-real extension is constant at the full Galois group below the distinguished endpoint -1.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem lowerRamificationGroup_eq_top_of_le_neg_one
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    {s : ℝ} (hs : s ≤ -1) :
    lowerRamificationGroup
      (base := base) (target := target) huniq s = ⊤
def

galRestrictScalarsToIntermediate

L483 ↗
RamificationTheory.HilbertRamification.Higher.galRestrictScalarsToIntermediate
Documentation

Restriction of scalars from Gal(L/M) to Gal(L/K).

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · full declaration
def galRestrictScalarsToIntermediate (M : IntermediateField K L) :
    Gal(L/M) →* Gal(L/K) where
  toFun σ := AlgEquiv.restrictScalars K σ
  map_one' := rfl
  map_mul' _ _ := rfl
theorem

galRestrictScalarsToIntermediate_apply

L490 ↗
RamificationTheory.HilbertRamification.Higher.galRestrictScalarsToIntermediate_apply
Documentation

States the theorem galRestrictScalarsToIntermediate_apply.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem galRestrictScalarsToIntermediate_apply
    (M : IntermediateField K L) (σ : Gal(L/M)) :
    galRestrictScalarsToIntermediate M σ = AlgEquiv.restrictScalars K σ
theorem

galRestrictScalarsToIntermediate_injective

L496 ↗
RamificationTheory.HilbertRamification.Higher.galRestrictScalarsToIntermediate_injective
Documentation

States the theorem galRestrictScalarsToIntermediate_injective.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem galRestrictScalarsToIntermediate_injective
    (M : IntermediateField K L) :
    Function.Injective (galRestrictScalarsToIntermediate M)
theorem

galRestrictScalarsToIntermediate_range

L503 ↗
RamificationTheory.HilbertRamification.Higher.galRestrictScalarsToIntermediate_range
Documentation

The range of restriction of scalars is precisely the subgroup fixing the intermediate field.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem galRestrictScalarsToIntermediate_range
    (M : IntermediateField K L) :
    (galRestrictScalarsToIntermediate M).range = M.fixingSubgroup
def

lowerRamificationGroupOverIntermediate

L521 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroupOverIntermediate
Documentation

The lower ramification group for L/M, using the same normalized top valuation as for L/K. This is the real lower-ramification definition with only the automorphism group changed.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
def lowerRamificationGroupOverIntermediate
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (M : IntermediateField K L) (s : ℝ) : Subgroup Gal(L/M)
theorem

mem_lowerRamificationGroupOverIntermediate_iff

L530 ↗
RamificationTheory.HilbertRamification.Higher.mem_lowerRamificationGroupOverIntermediate_iff
Documentation

States the theorem mem_lowerRamificationGroupOverIntermediate_iff.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem mem_lowerRamificationGroupOverIntermediate_iff
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (M : IntermediateField K L) (s : ℝ) (σ : Gal(L/M)) :
    σ ∈ lowerRamificationGroupOverIntermediate
        (base := base) (target := target) huniq M s ↔
      ∀ a : target.valuationSubring,
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq
            (galRestrictScalarsToIntermediate M σ) a - a ∈
          realRamificationIdeal target s
theorem

lowerRamificationGroupOverIntermediate_map_eq_inf

L547 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGroupOverIntermediate_map_eq_inf
Documentation

The lower-ramification base-change law: changing only the base field intersects the lower ramification group with Gal(L/M). The left side is transported into Gal(L/K) by restriction of scalars, so the statement is a literal subgroup equality.

Source context 11 commands

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

noncomputable section
open scoped Pointwise
universe u v w x y
namespace RamificationTheory.HilbertRamification
namespace Higher
open RamificationTheory.DiscreteValuationField.DVF
open RamificationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : ValuationTheory.DiscreteValuationField.DVF.{u, v} K}
variable {target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]
Lean source · statement
theorem lowerRamificationGroupOverIntermediate_map_eq_inf
    (huniq : HasUniqueValuationExtension.{u, v, w, x, x}
      base target)
    (M : IntermediateField K L) (s : ℝ) :
    Subgroup.map (galRestrictScalarsToIntermediate M)
        (lowerRamificationGroupOverIntermediate
          (base := base) (target := target) huniq M s) =
      lowerRamificationGroup
          (base := base) (target := target) huniq s ⊓ M.fixingSubgroup

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