NYLL
Module

RamificationNumber.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationNumber
12 declarations indexed from sourceView source ↗

Module documentation

Ramification numbers for a general discretely valued field

This file gives the noncomplete version of the ramification number used in ramification-number theory. Under the stated unique-extension and separable-residue hypotheses, the monogenic integral-generator theorem supplies an integral generator. We choose that generator internally, so downstream statements do not carry a generator hypothesis.

Imports3
Imported by6

Declarations

def

valuationSubringDisplacementSubalgebraOfUniqueExtension

L38 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringDisplacementSubalgebraOfUniqueExtension
Documentation

Elements whose displacement has a fixed maximal-ideal lower bound form a base valuation-ring subalgebra.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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 valuationSubringDisplacementSubalgebraOfUniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (n : ℕ) (sigma : Gal(L/K)) :
    Subalgebra base.valuationSubring target.valuationSubring where
  carrier :=
    {a | valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a - a ∈
        target.maximalIdeal ^ n}
  zero_mem' := by simp
  one_mem' := by simp
  add_mem' := by
    intro a b ha hb
    change
      valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq sigma (a + b) - (a + b) ∈
        target.maximalIdeal ^ n
    change valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a - a ∈
        target.maximalIdeal ^ n at ha
    change valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma b - b ∈
        target.maximalIdeal ^ n at hb
    have hrewrite :
        valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq sigma (a + b) - (a + b) =
          (valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq sigma a - a) +
            (valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq sigma b - b) := by
      simp
      ring
    rw [hrewrite]
    exact Ideal.add_mem _ ha hb
  mul_mem' := by
    intro a b ha hb
    change
      valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq sigma (a * b) - a * b ∈
        target.maximalIdeal ^ n
    change valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a - a ∈
        target.maximalIdeal ^ n at ha
    change valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma b - b ∈
        target.maximalIdeal ^ n at hb
    have hrewrite :
        valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq sigma (a * b) - a * b =
          valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq sigma a *
              (valuationSubringAutOfUniqueExtension
                (base := base) (target := target) huniq sigma b - b) +
            (valuationSubringAutOfUniqueExtension
                (base := base) (target := target) huniq sigma a - a) * b := by
      simp
      ring
    rw [hrewrite]
    exact Ideal.add_mem _
      (Ideal.mul_mem_left _ _ hb)
      (Ideal.mul_mem_right _ _ ha)
  algebraMap_mem' := by
    intro r
    change
      valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq sigma
            (algebraMap base.valuationSubring target.valuationSubring r) -
          algebraMap base.valuationSubring target.valuationSubring r ∈
        target.maximalIdeal ^ n
    have hcomm :
        valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq sigma
            (algebraMap base.valuationSubring target.valuationSubring r) =
          algebraMap base.valuationSubring target.valuationSubring r := by
      apply Subtype.ext
      exact sigma.commutes (r : K)
    rw [hcomm, sub_self]
    exact Ideal.zero_mem _
theorem

mem_valuationSubringDisplacementSubalgebraOfUniqueExtension_iff

L119 ↗
RamificationTheory.HilbertRamification.Higher.mem_valuationSubringDisplacementSubalgebraOfUniqueExtension_iff
Documentation

States the theorem mem_valuationSubringDisplacementSubalgebraOfUniqueExtension_iff.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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_valuationSubringDisplacementSubalgebraOfUniqueExtension_iff
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (n : ℕ) (sigma : Gal(L/K)) (a : target.valuationSubring) :
    a ∈ valuationSubringDisplacementSubalgebraOfUniqueExtension
        (base := base) (target := target) huniq n sigma ↔
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a - a ∈
        target.maximalIdeal ^ n
theorem

valuationSubringAutOfUniqueExtension_sub_mem_of_mem_adjoin

L133 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_sub_mem_of_mem_adjoin
Documentation

A displacement bound on a generator extends to every integral polynomial expression in that generator.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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_sub_mem_of_mem_adjoin
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {a z : target.valuationSubring} {n : ℕ} {sigma : Gal(L/K)}
    (ha : valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a - a ∈
        target.maximalIdeal ^ n)
    (hz : z ∈ Algebra.adjoin base.valuationSubring
      ({a} : Set target.valuationSubring)) :
    valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma z - z ∈
      target.maximalIdeal ^ n
def

ramificationNumberOfUniqueExtension

L159 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberOfUniqueExtension
Documentation

Ramification number attached to an integral element, before choosing the integral generator.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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 ramificationNumberOfUniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (a : target.valuationSubring) (sigma : Gal(L/K)) : ℕ∞
theorem

ramificationNumberOfUniqueExtension_one

L169 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberOfUniqueExtension_one
Documentation

States the theorem ramificationNumberOfUniqueExtension_one.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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 ramificationNumberOfUniqueExtension_one
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (a : target.valuationSubring) :
    ramificationNumberOfUniqueExtension
      (base := base) (target := target) huniq a 1 = ⊤
theorem

natCast_le_ramificationNumberOfUniqueExtension_iff

L179 ↗
RamificationTheory.HilbertRamification.Higher.natCast_le_ramificationNumberOfUniqueExtension_iff
Documentation

States the theorem natCast_le_ramificationNumberOfUniqueExtension_iff.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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 natCast_le_ramificationNumberOfUniqueExtension_iff
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (a : target.valuationSubring) (sigma : Gal(L/K)) (n : ℕ) :
    (n : ℕ∞) ≤ ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq a sigma ↔
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a - a ∈
        target.maximalIdeal ^ n
theorem

ramificationNumberOfUniqueExtension_eq_of_adjoin_eq_top

L194 ↗
RamificationTheory.HilbertRamification.Higher.ramificationNumberOfUniqueExtension_eq_of_adjoin_eq_top
Documentation

The ramification number is independent of the monogenic generator.

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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 ramificationNumberOfUniqueExtension_eq_of_adjoin_eq_top
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {a b : target.valuationSubring}
    (ha : Algebra.adjoin base.valuationSubring
      ({a} : Set target.valuationSubring) = ⊤)
    (hb : Algebra.adjoin base.valuationSubring
      ({b} : Set target.valuationSubring) = ⊤)
    (sigma : Gal(L/K)) :
    ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq a sigma =
      ramificationNumberOfUniqueExtension
        (base := base) (target := target) huniq b sigma
def

chosenRamificationGeneratorOfUniqueExtension

L225 ↗
RamificationTheory.HilbertRamification.Higher.chosenRamificationGeneratorOfUniqueExtension
Documentation

The integral generator supplied internally by the monogeneity theorem under the standing hypotheses.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
def chosenRamificationGeneratorOfUniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target) : target.valuationSubring
theorem

chosenRamificationGeneratorOfUniqueExtension_adjoin_eq_top

L234 ↗
RamificationTheory.HilbertRamification.Higher.chosenRamificationGeneratorOfUniqueExtension_adjoin_eq_top
Documentation

States the theorem chosenRamificationGeneratorOfUniqueExtension_adjoin_eq_top.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
theorem chosenRamificationGeneratorOfUniqueExtension_adjoin_eq_top
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target) :
    Algebra.adjoin base.valuationSubring
        ({chosenRamificationGeneratorOfUniqueExtension
            (base := base) (target := target) huniq} :
          Set target.valuationSubring) = ⊤
def

intrinsicRamificationNumberOfUniqueExtension

L248 ↗
RamificationTheory.HilbertRamification.Higher.intrinsicRamificationNumberOfUniqueExtension
Documentation

The canonical ramification number. Its generator is supplied internally by the monogenic integral-generator theorem.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
def intrinsicRamificationNumberOfUniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (sigma : Gal(L/K)) : ℕ∞
theorem

intrinsicRamificationNumberOfUniqueExtension_one

L259 ↗
RamificationTheory.HilbertRamification.Higher.intrinsicRamificationNumberOfUniqueExtension_one
Documentation

States the theorem intrinsicRamificationNumberOfUniqueExtension_one.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
theorem intrinsicRamificationNumberOfUniqueExtension_one
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target) :
    intrinsicRamificationNumberOfUniqueExtension
      (base := base) (target := target) huniq 1 = ⊤
theorem

mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge

L268 ↗
RamificationTheory.HilbertRamification.Higher.mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge
Documentation

The canonical ramification number recovers the integral lower groups.

Source context 10 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
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]
variable [FiniteDimensional K L] [IsGalois K L]
variable [Algebra.IsSeparable base.residueField target.residueField]
Lean source · statement
theorem mem_lowerRamificationGroup_nat_iff_intrinsicRamificationNumberOfUniqueExtension_ge
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (n : ℕ) (sigma : Gal(L/K)) :
    sigma ∈ lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ) ↔
      ((n + 1 : ℕ) : ℕ∞) ≤
        intrinsicRamificationNumberOfUniqueExtension
          (base := base) (target := target) huniq sigma

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