NYLL
Module

FixedFieldRamification.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FixedFieldRamification
7 declarations indexed from sourceView source ↗

Module documentation

Canonical ramification numbers on an actual fixed field

For M = L ^ H, this file works with the literal restricted valuation ring O_M = O_L ∩ M. The ramification number of an actual element of Gal(M/K) is the value of the principal ideal generated by all of its integral displacements. Thus the public definition is independent of a monogenic generator.

Imports4
Imported by3

Declarations

def

fixedFieldDisplacementIdealDVF

L40 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldDisplacementIdealDVF
Documentation

The displacement ideal in the literal restricted valuation ring of the actual fixed field.

Source context 9 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]
Lean source · statement
def fixedFieldDisplacementIdealDVF
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (q : Gal((fixedFieldDVF (K := K) H)/K)) :
    Ideal (fixedFieldValuationSubringDVF (K := K) (target := target) H)
def

fixedFieldRamificationNumber

L56 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldRamificationNumber
Documentation

The canonical fixed-field ramification number. Since the restricted valuation ring is a DVR, its displacement ideal is principal; the additive value of an ideal generator is independent of the chosen generator.

Source context 9 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]
Lean source · statement
def fixedFieldRamificationNumber
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (q : Gal((fixedFieldDVF (K := K) H)/K)) : ℕ∞
def

fixedFieldRamificationIdealDVF

L72 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldRamificationIdealDVF
Documentation

The real-index ideal on the actual restricted valuation ring.

Source context 9 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]
Lean source · statement
def fixedFieldRamificationIdealDVF
    (H : Subgroup Gal(L/K)) (s : ℝ) :
    Ideal (fixedFieldValuationSubringDVF (K := K) (target := target) H)
def

fixedFieldLowerRamificationGroup

L81 ↗
RamificationTheory.HilbertRamification.Higher.fixedFieldLowerRamificationGroup
Documentation

The real lower ramification group of the actual Galois extension (L ^ H)/K, formed using the literal restricted valuation ring.

Source context 9 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]
Lean source · full declaration
def fixedFieldLowerRamificationGroup
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (s : ℝ) : Subgroup Gal((fixedFieldDVF (K := K) H)/K) where
  carrier :=
    {q | ∀ a : fixedFieldValuationSubringDVF
        (K := K) (target := target) H,
      fixedFieldValuationSubringAutDVF
          (base := base) (target := target) huniq H q a - a ∈
        fixedFieldRamificationIdealDVF
          (K := K) (target := target) H s}
  one_mem' := by
    intro a
    simp [fixedFieldValuationSubringAutDVF]
  mul_mem' := by
    intro q r hq hr a
    let eqv := fixedFieldValuationSubringAutDVF
      (base := base) (target := target) huniq H q
    have hra := hr a
    have hmap : eqv
        (fixedFieldValuationSubringAutDVF
            (base := base) (target := target) huniq H r a - a) ∈
        fixedFieldRamificationIdealDVF
          (K := K) (target := target) H s :=
      (ValuationTheory.ringEquiv_mem_maximalIdeal_pow_iff eqv
        (realRamificationExponent s) _).2 hra
    have hqa := hq a
    have hdecomp :
        fixedFieldValuationSubringAutDVF
              (base := base) (target := target) huniq H (q * r) a - a =
          eqv
              (fixedFieldValuationSubringAutDVF
                (base := base) (target := target) huniq H r a - a) +
            (eqv a - a) := by
      rw [fixedFieldValuationSubringAutDVF_mul_apply, map_sub]
      ring
    rw [hdecomp]
    exact Ideal.add_mem _ hmap hqa
  inv_mem' := by
    intro q hq a
    let b := fixedFieldValuationSubringAutDVF
      (base := base) (target := target) huniq H q⁻¹ a
    have hb := hq b
    have hqb :
        fixedFieldValuationSubringAutDVF
          (base := base) (target := target) huniq H q b = a := by
      rw [show b = fixedFieldValuationSubringAutDVF
        (base := base) (target := target) huniq H q⁻¹ a by rfl]
      rw [← fixedFieldValuationSubringAutDVF_mul_apply]
      simp [fixedFieldValuationSubringAutDVF]
    have hab : a - b ∈ fixedFieldRamificationIdealDVF
        (K := K) (target := target) H s := by
      simpa [hqb] using hb
    have hba : b - a ∈ fixedFieldRamificationIdealDVF
        (K := K) (target := target) H s := by
      simpa [sub_eq_add_neg, add_comm] using
        (fixedFieldRamificationIdealDVF
          (K := K) (target := target) H s).neg_mem hab
    simpa [b] using hba
theorem

mem_fixedFieldLowerRamificationGroup_iff

L144 ↗
RamificationTheory.HilbertRamification.Higher.mem_fixedFieldLowerRamificationGroup_iff
Documentation

States the theorem mem_fixedFieldLowerRamificationGroup_iff.

Source context 9 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]
Lean source · statement
theorem mem_fixedFieldLowerRamificationGroup_iff
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (s : ℝ) (q : Gal((fixedFieldDVF (K := K) H)/K)) :
    q ∈ fixedFieldLowerRamificationGroup
        (base := base) (target := target) huniq H s ↔
      ∀ a : fixedFieldValuationSubringDVF
          (K := K) (target := target) H,
        fixedFieldValuationSubringAutDVF
            (base := base) (target := target) huniq H q a - a ∈
          fixedFieldRamificationIdealDVF
            (K := K) (target := target) H s
theorem

mem_fixedFieldLowerRamificationGroup_iff_ramificationNumber

L162 ↗
RamificationTheory.HilbertRamification.Higher.mem_fixedFieldLowerRamificationGroup_iff_ramificationNumber
Documentation

Real lower-group membership is exactly the threshold imposed by the canonical fixed-field ramification number.

Source context 9 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]
Lean source · statement
theorem mem_fixedFieldLowerRamificationGroup_iff_ramificationNumber
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (s : ℝ) (q : Gal((fixedFieldDVF (K := K) H)/K)) :
    q ∈ fixedFieldLowerRamificationGroup
        (base := base) (target := target) huniq H s ↔
      (realRamificationExponent s : ℕ∞) ≤
        fixedFieldRamificationNumber
          (base := base) (target := target) huniq H q
theorem

mem_fixedFieldLowerRamificationGroup_nat_iff

L217 ↗
RamificationTheory.HilbertRamification.Higher.mem_fixedFieldLowerRamificationGroup_nat_iff
Documentation

At integral lower indices, actual fixed-field group membership is equivalent to the canonical ramification-number inequality.

Source context 9 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]
Lean source · statement
theorem mem_fixedFieldLowerRamificationGroup_nat_iff
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (H : Subgroup Gal(L/K)) [H.Normal]
    (n : ℕ) (q : Gal((fixedFieldDVF (K := K) H)/K)) :
    q ∈ fixedFieldLowerRamificationGroup
        (base := base) (target := target) huniq H (n : ℝ) ↔
      ((n + 1 : ℕ) : ℕ∞) ≤
        fixedFieldRamificationNumber
          (base := base) (target := target) huniq H q

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