NYLL
Module

FirstRamificationComparison.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.FirstRamificationComparison
6 declarations indexed from sourceView source ↗

Module documentation

Comparing first principal units in the two ramification conventions

The DVF filtration uses units of the valuation ring, whereas Hilbert's ramification group uses the principal-unit subgroup of the field units. This file identifies their first levels before comparing group actions.

Imports4
Imported by2

Declarations

theorem

mem_dvfHigherPrincipalUnitGroup_one_iff_principalUnitGroup

L32 ↗
RamificationTheory.HilbertRamification.mem_dvfHigherPrincipalUnitGroup_one_iff_principalUnitGroup
Documentation

A valuation-ring unit belongs to the first DVF principal-unit group exactly when its image among field units is principal in Hilbert's sense.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
variable {L : Type u} [Field L]
Lean source · statement
theorem mem_dvfHigherPrincipalUnitGroup_one_iff_principalUnitGroup
    (target : DVF.{u, v} L) (a : target.valuationSubringˣ) :
    a ∈ Higher.dvfHigherPrincipalUnitGroup target 1 ↔
      ((target.valuation.valuationSubring.unitGroupMulEquiv.symm a :
        target.valuation.valuationSubring.unitGroup) : Lˣ) ∈
          target.valuation.valuationSubring.principalUnitGroup
theorem

coe_dvfUniformizerQuotientUnit_eq_automorphismUnitQuotient

L48 ↗
RamificationTheory.HilbertRamification.coe_dvfUniformizerQuotientUnit_eq_automorphismUnitQuotient
Documentation

The DVF unit σ(π)/π and Hilbert's field-unit quotient are the same after the canonical embedding of valuation-ring units into field units.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
variable {L : Type u} [Field L]
Lean source · statement
theorem coe_dvfUniformizerQuotientUnit_eq_automorphismUnitQuotient
    {K : Type w} [Field K] [Algebra K L]
    {base : DVF.{w, x} K} {target : DVF.{u, v} L}
    [base.valuation.HasExtension target.valuation]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{w, x, u, v, v}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (sigma : ValuationSubring.decompositionGroup K
      target.valuation.valuationSubring) :
    ((target.valuation.valuationSubring.unitGroupMulEquiv.symm
        (Higher.dvfUniformizerQuotientUnit
          (base := base) (target := target) huniq pi hpi
          (sigma : Gal(L/K))) :
        target.valuation.valuationSubring.unitGroup) : Lˣ) =
      ValuationSubring.automorphismUnitQuotient K
        target.valuation.valuationSubring sigma
        (Units.mk0 (pi : L) hpi.ne_zero)
theorem

inertia_forall_automorphismUnitQuotient_mem_principal_iff_uniformizer

L86 ↗
RamificationTheory.HilbertRamification.inertia_forall_automorphismUnitQuotient_mem_principal_iff_uniformizer
Documentation

For an inertia element of a discretely valued field, Hilbert's principal-unit condition on every field unit is determined by one uniformizer.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
variable {L : Type u} [Field L]
Lean source · statement
theorem inertia_forall_automorphismUnitQuotient_mem_principal_iff_uniformizer
    {K : Type w} [Field K] [Algebra K L]
    (target : DVF.{u, v} L)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (sigma : ValuationSubring.inertiaGroup K
      target.valuation.valuationSubring) :
    (∀ y : Lˣ,
      ValuationSubring.automorphismUnitQuotient K
        target.valuation.valuationSubring
        (sigma : ValuationSubring.decompositionGroup K
          target.valuation.valuationSubring) y ∈
        target.valuation.valuationSubring.principalUnitGroup) ↔
      ValuationSubring.automorphismUnitQuotient K
        target.valuation.valuationSubring
        (sigma : ValuationSubring.decompositionGroup K
          target.valuation.valuationSubring)
        (Units.mk0 (pi : L) hpi.ne_zero) ∈
          target.valuation.valuationSubring.principalUnitGroup
theorem

mem_lowerRamificationGroup_zero_iff_completeDVF_inertiaGroup

L146 ↗
RamificationTheory.HilbertRamification.mem_lowerRamificationGroup_zero_iff_completeDVF_inertiaGroup
Documentation

The zeroth lower group is the inertia group for a finite separable extension of complete DVFs, under the canonical identification of the Galois and decomposition groups.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
variable {L : Type u} [Field L]
Lean source · statement
theorem mem_lowerRamificationGroup_zero_iff_completeDVF_inertiaGroup
    {K : Type w} [Field K] [Algebra K L]
    (base : CompleteDVF.{w, x} K) (target : CompleteDVF.{u, v} L)
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [base.valuation.HasExtension target.valuation]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{w, x, u, v, v}
        base.toDVF target.toDVF)
    (sigma : Gal(L/K)) :
    sigma ∈ Higher.lowerRamificationGroup
        (base := base.toDVF) (target := target.toDVF) huniq (0 : ℝ) ↔
      sigma ∈ CompleteDVF.inertiaGroup (base := base) (target := target)
theorem

mem_lowerRamificationGroup_one_of_uniformizerQuotient_mem

L184 ↗
RamificationTheory.HilbertRamification.mem_lowerRamificationGroup_one_of_uniformizerQuotient_mem
Documentation

Under separable residue extension, the uniformizer quotient detects the first lower ramification subgroup inside the zeroth one.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
variable {L : Type u} [Field L]
Lean source · statement
theorem mem_lowerRamificationGroup_one_of_uniformizerQuotient_mem
    {K : Type w} [Field K] [Algebra K L]
    {base : DVF.{w, x} K} {target : DVF.{u, v} L}
    [FiniteDimensional K L] [IsGalois K L]
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{w, x, u, v, v}
        base target)
    (pi : target.valuationSubring)
    (hpi : target.valuation.IsUniformizer (pi : L))
    (sigma : Gal(L/K))
    (hzero : sigma ∈ Higher.lowerRamificationGroup
      (base := base) (target := target) huniq (0 : ℝ))
    (hpiUnit : Higher.dvfUniformizerQuotientUnit
        (base := base) (target := target) huniq pi hpi sigma ∈
      Higher.dvfHigherPrincipalUnitGroup target 1) :
    sigma ∈ Higher.lowerRamificationGroup
      (base := base) (target := target) huniq (1 : ℝ)
theorem

lowerRamificationGroup_one_eq_hilbertRamificationGroup

L235 ↗
RamificationTheory.HilbertRamification.lowerRamificationGroup_one_eq_hilbertRamificationGroup
Documentation

For a finite Galois extension of complete DVFs with separable residue extension, the first lower ramification group is Hilbert's ramification group, transported from the decomposition group to the full Galois group.

Source context 5 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
variable {L : Type u} [Field L]
Lean source · statement
theorem lowerRamificationGroup_one_eq_hilbertRamificationGroup
    {K : Type w} [Field K] [Algebra K L]
    (base : CompleteDVF.{w, x} K) (target : CompleteDVF.{u, v} L)
    [FiniteDimensional K L] [IsGalois K L] [Algebra.IsSeparable K L]
    [base.valuation.HasExtension target.valuation]
    [Algebra.IsSeparable base.residueField target.residueField]
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension.{w, x, u, v, v}
        base.toDVF target.toDVF) :
    Higher.lowerRamificationGroup
        (base := base.toDVF) (target := target.toDVF) huniq (1 : ℝ) =
      Subgroup.comap
        (CompleteDVF.galEquivDecompositionGroup
          (base := base) (target := target)).toMonoidHom
        (ValuationSubring.ramificationGroupInDecomposition K
          target.valuation.valuationSubring)

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