NYLL
Module

UniformizerGradedHom.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.UniformizerGradedHom
27 declarations indexed from sourceView source ↗

Module documentation

First ramification-quotient homomorphism over general DVFs

This file constructs the graded uniformizer homomorphism under the standing hypotheses of ramification-number theory. Completeness is not assumed. The injectivity statement includes the necessary separability hypothesis on the residue extension; the unconditional printed assertion is false for fiercely ramified extensions.

Imports1
Imported by4

Declarations

def

dvfHigherPrincipalUnitGroup

L38 ↗
RamificationTheory.HilbertRamification.Higher.dvfHigherPrincipalUnitGroup
Documentation

The principal-unit filtration attached to a general DVF.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · full declaration
def dvfHigherPrincipalUnitGroup
    (target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L) (n : ℕ) :
    Subgroup target.valuationSubringˣ where
  carrier := {a | (a : target.valuationSubring) - 1 ∈ target.maximalIdeal ^ n}
  one_mem' := by simp
  mul_mem' := by
    intro a b ha hb
    have hre :
        ((a * b : target.valuationSubringˣ) : target.valuationSubring) - 1 =
          (a : target.valuationSubring) *
              ((b : target.valuationSubring) - 1) +
            ((a : target.valuationSubring) - 1) := by
      simp
      ring
    change
      ((a * b : target.valuationSubringˣ) : target.valuationSubring) - 1 ∈
        target.maximalIdeal ^ n
    rw [hre]
    exact Ideal.add_mem _
      (Ideal.mul_mem_left _ _ hb) ha
  inv_mem' := by
    intro a ha
    have hre :
        ((a⁻¹ : target.valuationSubringˣ) : target.valuationSubring) - 1 =
          -(((a⁻¹ : target.valuationSubringˣ) : target.valuationSubring) *
            ((a : target.valuationSubring) - 1)) := by
      calc
        ((a⁻¹ : target.valuationSubringˣ) : target.valuationSubring) - 1 =
            ((a⁻¹ : target.valuationSubringˣ) : target.valuationSubring) -
              ((a⁻¹ : target.valuationSubringˣ) : target.valuationSubring) *
                (a : target.valuationSubring) := by simp
        _ = _ := by ring
    change
      ((a⁻¹ : target.valuationSubringˣ) : target.valuationSubring) - 1 ∈
        target.maximalIdeal ^ n
    rw [hre]
    exact (target.maximalIdeal ^ n).neg_mem
      (Ideal.mul_mem_left _ _ ha)
theorem

mem_dvfHigherPrincipalUnitGroup_iff

L78 ↗
RamificationTheory.HilbertRamification.Higher.mem_dvfHigherPrincipalUnitGroup_iff
Documentation

States the theorem mem_dvfHigherPrincipalUnitGroup_iff.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem mem_dvfHigherPrincipalUnitGroup_iff
    (target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L)
    (n : ℕ) (a : target.valuationSubringˣ) :
    a ∈ dvfHigherPrincipalUnitGroup target n ↔
      (a : target.valuationSubring) - 1 ∈ target.maximalIdeal ^ n
theorem

dvfHigherPrincipalUnitGroup_antitone

L86 ↗
RamificationTheory.HilbertRamification.Higher.dvfHigherPrincipalUnitGroup_antitone
Documentation

States the theorem dvfHigherPrincipalUnitGroup_antitone.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem dvfHigherPrincipalUnitGroup_antitone
    (target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L) :
    Antitone (dvfHigherPrincipalUnitGroup target)
abbrev

dvfPrincipalUnitGradedPiece

L93 ↗
RamificationTheory.HilbertRamification.Higher.dvfPrincipalUnitGradedPiece
Documentation

The literal target U_L^n/U_L^(n+1).

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
abbrev dvfPrincipalUnitGradedPiece
    (target : ValuationTheory.DiscreteValuationField.DVF.{w, x} L) (n : ℕ)
abbrev

lowerRamificationGradedPiece

L100 ↗
RamificationTheory.HilbertRamification.Higher.lowerRamificationGradedPiece
Documentation

The literal source G_n/G_(n+1) formed from the real 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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
abbrev lowerRamificationGradedPiece
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (n : ℕ)
abbrev

dvfValuationSubringUnitAut

L113 ↗
RamificationTheory.HilbertRamification.Higher.dvfValuationSubringUnitAut
Documentation

The unique-extension action on target valuation-ring units.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
abbrev dvfValuationSubringUnitAut
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (sigma : Gal(L/K)) :
    target.valuationSubringˣ →* target.valuationSubringˣ
theorem

dvfValuationSubringUnitAut_apply

L125 ↗
RamificationTheory.HilbertRamification.Higher.dvfValuationSubringUnitAut_apply
Documentation

States the theorem dvfValuationSubringUnitAut_apply.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfValuationSubringUnitAut_apply
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (sigma : Gal(L/K)) (a : target.valuationSubringˣ) :
    ((dvfValuationSubringUnitAut
      (base := base) (target := target) huniq sigma a :
        target.valuationSubringˣ) : target.valuationSubring) =
      valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq sigma
        (a : target.valuationSubring)
theorem

exists_dvfUniformizerQuotientUnit

L141 ↗
RamificationTheory.HilbertRamification.Higher.exists_dvfUniformizerQuotientUnit
Documentation

Every Galois conjugate of a target uniformizer differs from it by a valuation-ring unit.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem exists_dvfUniformizerQuotientUnit
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {pi : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (sigma : Gal(L/K)) :
    ∃ a : target.valuationSubringˣ,
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma pi =
        (a : target.valuationSubring) * pi
def

dvfUniformizerQuotientUnit

L225 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerQuotientUnit
Documentation

The chosen unit sigma(pi)/pi.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
def dvfUniformizerQuotientUnit
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (sigma : Gal(L/K)) : target.valuationSubringˣ
theorem

dvfUniformizerQuotientUnit_mul_uniformizer

L238 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerQuotientUnit_mul_uniformizer
Documentation

States the theorem dvfUniformizerQuotientUnit_mul_uniformizer.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfUniformizerQuotientUnit_mul_uniformizer
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (sigma : Gal(L/K)) :
    valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq sigma pi =
      (dvfUniformizerQuotientUnit
        (base := base) (target := target) huniq pi hpi sigma :
          target.valuationSubring) * pi
theorem

dvfUniformizerQuotientUnit_mul_eq

L256 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerQuotientUnit_mul_eq
Documentation

Exact cocycle identity for the chosen quotient units.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfUniformizerQuotientUnit_mul_eq
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (sigma tau : Gal(L/K)) :
    dvfUniformizerQuotientUnit
        (base := base) (target := target) huniq pi hpi (sigma * tau) =
      dvfValuationSubringUnitAut
          (base := base) (target := target) huniq sigma
          (dvfUniformizerQuotientUnit
            (base := base) (target := target) huniq pi hpi tau) *
        dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi sigma
theorem

dvfUniformizerQuotientUnit_mem_iff_uniformizer_sub_mem

L316 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerQuotientUnit_mem_iff_uniformizer_sub_mem
Documentation

Quotient-unit membership is equivalent to one-deeper displacement of the uniformizer.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfUniformizerQuotientUnit_mem_iff_uniformizer_sub_mem
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {pi : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (n : ℕ) (sigma : Gal(L/K)) :
    dvfUniformizerQuotientUnit
        (base := base) (target := target) huniq pi hpi sigma ∈
      dvfHigherPrincipalUnitGroup target n ↔
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma pi - pi ∈
        target.maximalIdeal ^ (n + 1)
theorem

dvfUniformizerQuotientUnit_mem_of_mem_lowerRamificationGroup

L374 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerQuotientUnit_mem_of_mem_lowerRamificationGroup
Documentation

If sigma lies in G_n, then sigma(pi)/pi lies in U_L^n.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfUniformizerQuotientUnit_mem_of_mem_lowerRamificationGroup
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {pi : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    {n : ℕ} {sigma : Gal(L/K)}
    (hsigma :
      sigma ∈ lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ)) :
    dvfUniformizerQuotientUnit
        (base := base) (target := target) huniq pi hpi sigma ∈
      dvfHigherPrincipalUnitGroup target n
theorem

dvfValuationSubringUnitAut_div_mem_succ

L395 ↗
RamificationTheory.HilbertRamification.Higher.dvfValuationSubringUnitAut_div_mem_succ
Documentation

A G_n automorphism acts trivially on every unit modulo U_L^(n+1).

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfValuationSubringUnitAut_div_mem_succ
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {n : ℕ} {sigma : Gal(L/K)}
    (hsigma :
      sigma ∈ lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ))
    (a : target.valuationSubringˣ) :
    dvfValuationSubringUnitAut
        (base := base) (target := target) huniq sigma a / a ∈
      dvfHigherPrincipalUnitGroup target (n + 1)
theorem

exists_dvf_unit_mul_uniformizer_eq_uniformizer

L436 ↗
RamificationTheory.HilbertRamification.Higher.exists_dvf_unit_mul_uniformizer_eq_uniformizer
Documentation

Any two target uniformizers differ by a valuation-ring unit.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem exists_dvf_unit_mul_uniformizer_eq_uniformizer
    {pi pi' : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hpi' : target.valuation.IsUniformizer (pi' : L)) :
    ∃ a : target.valuationSubringˣ,
      pi' = (a : target.valuationSubring) * pi
theorem

dvfUniformizerQuotientUnit_eq_of_uniformizer_eq_unit_mul

L449 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerQuotientUnit_eq_of_uniformizer_eq_unit_mul
Documentation

Exact change-of-uniformizer formula.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfUniformizerQuotientUnit_eq_of_uniformizer_eq_unit_mul
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {pi pi' : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hpi' : target.valuation.IsUniformizer (pi' : L))
    (a : target.valuationSubringˣ)
    (hpiA : pi' = (a : target.valuationSubring) * pi)
    (sigma : Gal(L/K)) :
    dvfUniformizerQuotientUnit
        (base := base) (target := target) huniq pi' hpi' sigma =
      dvfValuationSubringUnitAut
          (base := base) (target := target) huniq sigma a *
        dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi sigma * a⁻¹
def

dvfUniformizerRepresentativeHom

L512 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerRepresentativeHom
Documentation

Representative homomorphism from G_n to the literal principal-unit graded quotient.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · full declaration
def dvfUniformizerRepresentativeHom
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (n : ℕ) :
    lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ) →*
      dvfPrincipalUnitGradedPiece target n where
  toFun sigma :=
    QuotientGroup.mk'
      ((dvfHigherPrincipalUnitGroup target (n + 1)).subgroupOf
        (dvfHigherPrincipalUnitGroup target n))
      ⟨dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi
          (sigma : Gal(L/K)),
        dvfUniformizerQuotientUnit_mem_of_mem_lowerRamificationGroup
          (base := base) (target := target) huniq hpi sigma.property⟩
  map_one' := by
    let oneN :
        lowerRamificationGroup
          (base := base) (target := target) huniq (n : ℝ) := 1
    let u1 : dvfHigherPrincipalUnitGroup target n :=
      ⟨dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi 1,
        dvfUniformizerQuotientUnit_mem_of_mem_lowerRamificationGroup
          (base := base) (target := target) huniq hpi oneN.property⟩
    change
      QuotientGroup.mk'
          ((dvfHigherPrincipalUnitGroup target (n + 1)).subgroupOf
            (dvfHigherPrincipalUnitGroup target n)) u1 = 1
    apply
      (QuotientGroup.eq_one_iff
        (N := (dvfHigherPrincipalUnitGroup target (n + 1)).subgroupOf
          (dvfHigherPrincipalUnitGroup target n)) u1).2
    change
      dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi 1 ∈
        dvfHigherPrincipalUnitGroup target (n + 1)
    exact
      dvfUniformizerQuotientUnit_mem_of_mem_lowerRamificationGroup
        (base := base) (target := target) huniq hpi
        (lowerRamificationGroup
          (base := base) (target := target) huniq
          ((n + 1 : ℕ) : ℝ)).one_mem
  map_mul' := by
    intro sigma tau
    apply
      (QuotientGroup.eq_iff_div_mem
        (N := (dvfHigherPrincipalUnitGroup target (n + 1)).subgroupOf
          (dvfHigherPrincipalUnitGroup target n))).2
    change
      dvfUniformizerQuotientUnit
            (base := base) (target := target) huniq pi hpi
            ((sigma : Gal(L/K)) * (tau : Gal(L/K))) /
          (dvfUniformizerQuotientUnit
              (base := base) (target := target) huniq pi hpi
              (sigma : Gal(L/K)) *
            dvfUniformizerQuotientUnit
              (base := base) (target := target) huniq pi hpi
              (tau : Gal(L/K))) ∈
        dvfHigherPrincipalUnitGroup target (n + 1)
    have hact :=
      dvfValuationSubringUnitAut_div_mem_succ
        (base := base) (target := target) huniq sigma.property
        (dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi
          (tau : Gal(L/K)))
    rw [dvfUniformizerQuotientUnit_mul_eq
      (base := base) (target := target) huniq pi hpi
      (sigma : Gal(L/K)) (tau : Gal(L/K))]
    simpa [div_eq_mul_inv, mul_assoc, mul_comm, mul_left_comm] using hact
theorem

dvfUniformizerRepresentativeHom_apply

L588 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerRepresentativeHom_apply
Documentation

States the theorem dvfUniformizerRepresentativeHom_apply.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfUniformizerRepresentativeHom_apply
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (n : ℕ)
    (sigma :
      lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ)) :
    dvfUniformizerRepresentativeHom
        (base := base) (target := target) huniq pi hpi n sigma =
      QuotientGroup.mk'
        ((dvfHigherPrincipalUnitGroup target (n + 1)).subgroupOf
          (dvfHigherPrincipalUnitGroup target n))
        ⟨dvfUniformizerQuotientUnit
            (base := base) (target := target) huniq pi hpi
            (sigma : Gal(L/K)),
          dvfUniformizerQuotientUnit_mem_of_mem_lowerRamificationGroup
            (base := base) (target := target) huniq hpi sigma.property⟩
theorem

dvfUniformizerRepresentativeHom_apply_eq_of_uniformizers

L612 ↗
RamificationTheory.HilbertRamification.Higher.dvfUniformizerRepresentativeHom_apply_eq_of_uniformizers
Documentation

Representative-level independence of the chosen uniformizer.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem dvfUniformizerRepresentativeHom_apply_eq_of_uniformizers
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {pi pi' : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hpi' : target.valuation.IsUniformizer (pi' : L))
    (n : ℕ)
    (sigma :
      lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ)) :
    dvfUniformizerRepresentativeHom
        (base := base) (target := target) huniq pi' hpi' n sigma =
      dvfUniformizerRepresentativeHom
        (base := base) (target := target) huniq pi hpi n sigma
def

uniformizerGradedHom

L652 ↗
RamificationTheory.HilbertRamification.Higher.uniformizerGradedHom
Documentation

The first ramification-quotient homomorphism: the uniformizer quotient descends to G_n/G_(n+1) with values in U_L^n/U_L^(n+1).

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
def uniformizerGradedHom
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (n : ℕ) :
    lowerRamificationGradedPiece (base := base) (target := target) huniq n →*
      dvfPrincipalUnitGradedPiece target n
theorem

uniformizerGradedHom_mk

L703 ↗
RamificationTheory.HilbertRamification.Higher.uniformizerGradedHom_mk
Documentation

States the theorem uniformizerGradedHom_mk.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem uniformizerGradedHom_mk
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (n : ℕ)
    (sigma :
      lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ)) :
    uniformizerGradedHom
        (base := base) (target := target) huniq pi hpi n
        (QuotientGroup.mk'
          ((lowerRamificationGroup
            (base := base) (target := target) huniq
            ((n + 1 : ℕ) : ℝ)).subgroupOf
            (lowerRamificationGroup
              (base := base) (target := target) huniq (n : ℝ))) sigma) =
      dvfUniformizerRepresentativeHom
        (base := base) (target := target) huniq pi hpi n sigma
theorem

uniformizerGradedHom_eq_of_uniformizers

L727 ↗
RamificationTheory.HilbertRamification.Higher.uniformizerGradedHom_eq_of_uniformizers
Documentation

The graded homomorphism is independent of the chosen uniformizer.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem uniformizerGradedHom_eq_of_uniformizers
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {pi pi' : target.valuationSubring}
    (hpi : target.valuation.IsUniformizer (pi : L))
    (hpi' : target.valuation.IsUniformizer (pi' : L))
    (n : ℕ) :
    uniformizerGradedHom
        (base := base) (target := target) huniq pi' hpi' n =
      uniformizerGradedHom
        (base := base) (target := target) huniq pi hpi n
theorem

uniformizerGradedHom_mk_eq_one_iff

L754 ↗
RamificationTheory.HilbertRamification.Higher.uniformizerGradedHom_mk_eq_one_iff
Documentation

Kernel criterion at a representative.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem uniformizerGradedHom_mk_eq_one_iff
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (n : ℕ)
    (sigma :
      lowerRamificationGroup
        (base := base) (target := target) huniq (n : ℝ)) :
    uniformizerGradedHom
        (base := base) (target := target) huniq pi hpi n
        (QuotientGroup.mk'
          ((lowerRamificationGroup
            (base := base) (target := target) huniq
            ((n + 1 : ℕ) : ℝ)).subgroupOf
            (lowerRamificationGroup
              (base := base) (target := target) huniq (n : ℝ))) sigma) = 1 ↔
      dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi
          (sigma : Gal(L/K)) ∈
        dvfHigherPrincipalUnitGroup target (n + 1)
def

valuationSubringAlgEquivOfUniqueExtension

L789 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAlgEquivOfUniqueExtension
Documentation

The unique-extension ring automorphism as an algebra automorphism over the base valuation ring.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
def valuationSubringAlgEquivOfUniqueExtension
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    (sigma : Gal(L/K)) :
    target.valuationSubring ≃ₐ[base.valuationSubring]
      target.valuationSubring
theorem

polynomial_argument_sub_mem_succ_dvf

L804 ↗
RamificationTheory.HilbertRamification.Higher.polynomial_argument_sub_mem_succ_dvf
Documentation

Taylor's one-step argument over a general DVF.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem polynomial_argument_sub_mem_succ_dvf
    {P : Polynomial target.valuationSubring}
    {a b : target.valuationSubring} {n : ℕ}
    (hderiv : IsUnit (P.derivative.eval a))
    (hab : b - a ∈ target.maximalIdeal ^ (n + 1))
    (hP : P.eval b - P.eval a ∈ target.maximalIdeal ^ (n + 2)) :
    b - a ∈ target.maximalIdeal ^ (n + 2)
theorem

valuationSubringAutOfUniqueExtension_sub_mem_of_mem_adjoin_graded

L870 ↗
RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_sub_mem_of_mem_adjoin_graded
Documentation

A displacement bound on an algebra generator propagates to the algebra it generates.

Source context 11 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem valuationSubringAutOfUniqueExtension_sub_mem_of_mem_adjoin_graded
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    {generator : target.valuationSubring} {r : ℕ} {sigma : Gal(L/K)}
    (hgenerator :
      valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma generator -
        generator ∈ target.maximalIdeal ^ r)
    {a : target.valuationSubring}
    (ha :
      a ∈ Algebra.adjoin base.valuationSubring
        ({generator} : Set target.valuationSubring)) :
    valuationSubringAutOfUniqueExtension
          (base := base) (target := target) huniq sigma a -
        a ∈ target.maximalIdeal ^ r
theorem

uniformizerGradedHom_injective_of_residue_isSeparable

L936 ↗
RamificationTheory.HilbertRamification.Higher.uniformizerGradedHom_injective_of_residue_isSeparable
Documentation

Corrected maximal form of the first ramification-quotient homomorphism over general DVFs. Residue separability is essential: the unconditional injectivity without additional hypotheses fails for fiercely ramified extensions.

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
open ValuationTheory.DiscreteValuationField.ResidueField
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 [FiniteDimensional K L] [base.valuation.HasExtension target.valuation]
variable [IsGalois K L]
Lean source · statement
theorem uniformizerGradedHom_injective_of_residue_isSeparable
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{u, v, w, x, x}
        base target)
    [Algebra.IsSeparable base.residueField target.residueField]
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (n : ℕ) :
    Function.Injective
      (uniformizerGradedHom
        (base := base) (target := target) huniq pi hpi n)

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