Module

ValueGroup.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Book.ValueGroup

7 declarations indexed from sourceView source ↗

Module documentation

Book value groups of tame radical extensions

This file supplies the value-group generation source needed for the classical ramification-index form of Abhyankar's lemma. It starts with the group-theory comparison between the order of one value coset and the relative index of the subgroup generated by that value.

Imports28

Imported by3

instance

bookValueGroupQuotientAddCommGroup

L53 ↗

TameAbhyankar.bookValueGroupQuotientAddCommGroup

Source context 4 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations

Lean source · statement

instance bookValueGroupQuotientAddCommGroup
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w)

theorem

bookRamificationIndex_eq_valueSubgroup_relIndex

L63 ↗

TameAbhyankar.bookRamificationIndex_eq_valueSubgroup_relIndex

Documentation

The book ramification index is the relative index of the source value subgroup in the target value subgroup, both viewed inside ℝ.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
local instance bookValueGroupQuotientAddCommGroup
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem bookRamificationIndex_eq_valueSubgroup_relIndex
    {K L : Type u} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    exponentialRamificationIndex v w =
      (exponentialValueSubgroup v).relIndex
        (exponentialValueSubgroup w)

theorem

bookRamificationIndex_pos

L74 ↗

TameAbhyankar.bookRamificationIndex_pos

Documentation

The actual value-group ramification index of a finite extension is positive.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
local instance bookValueGroupQuotientAddCommGroup
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem bookRamificationIndex_pos
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    0 < exponentialRamificationIndex v w

theorem

bookExponentialValueSubgroup_eq_of_ramificationIndex_eq_one

L87 ↗

TameAbhyankar.bookExponentialValueSubgroup_eq_of_ramificationIndex_eq_one

Documentation

Ramification index one means equality of the actual value subgroups.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
local instance bookValueGroupQuotientAddCommGroup
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem bookExponentialValueSubgroup_eq_of_ramificationIndex_eq_one
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (he : exponentialRamificationIndex v w = 1) :
    exponentialValueSubgroup w = exponentialValueSubgroup v

theorem

relIndex_sup_zmultiples_eq_addOrderOf

L102 ↗

TameAbhyankar.relIndex_sup_zmultiples_eq_addOrderOf

Documentation

Adjoining one additive generator to a subgroup has relative index equal to the additive order of that generator modulo the original subgroup.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
local instance bookValueGroupQuotientAddCommGroup
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem relIndex_sup_zmultiples_eq_addOrderOf
    {G : Type u} [AddCommGroup G] (H : AddSubgroup G) (x : G) :
    H.relIndex (H ⊔ AddSubgroup.zmultiples x) =
      addOrderOf (QuotientAddGroup.mk x : G ⧸ H)

theorem

bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical_of_separableResidue

L140 ↗

TameAbhyankar.bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical_of_separableResidue

Documentation

A single prime-to-the-residue-characteristic radical generates the whole target value group over the base value group. This is the subgroup form of the degree computation in Proposition 7.7.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
local instance bookValueGroupQuotientAddCommGroup
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical_of_separableResidue
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (hresidue : SeparableResidueRootLifts v w hExt)
    (alpha : L) (halpha0 : alpha ≠ 0)
    (hgen : IntermediateField.adjoin K ({alpha} : Set L) = ⊤)
    (m : ℕ) (hmpos : 0 < m)
    (hmcop : Nat.Coprime m (residueCharacteristic v))
    (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    exponentialValueSubgroup w =
      exponentialValueSubgroup v ⊔
        AddSubgroup.zmultiples (w alpha).untop₀

theorem

bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical

L216 ↗

TameAbhyankar.bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical

Documentation

Surjective-residue-field specialization of the single-radical value group generation theorem.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
local instance bookValueGroupQuotientAddCommGroup
    {K L : Type*} [Field K] [Field L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (hresidue : Function.Surjective (tameResidueFieldMap v w hExt))
    (alpha : L) (halpha0 : alpha ≠ 0)
    (hgen : IntermediateField.adjoin K ({alpha} : Set L) = ⊤)
    (m : ℕ) (hmpos : 0 < m)
    (hmcop : Nat.Coprime m (residueCharacteristic v))
    (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    exponentialValueSubgroup w =
      exponentialValueSubgroup v ⊔
        AddSubgroup.zmultiples (w alpha).untop₀

Module documentation

Book value groups of tame radical extensions

Declarations

bookValueGroupQuotientAddCommGroup

bookRamificationIndex_eq_valueSubgroup_relIndex

bookRamificationIndex_pos

bookExponentialValueSubgroup_eq_of_ramificationIndex_eq_one

relIndex_sup_zmultiples_eq_addOrderOf

bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical_of_separableResidue

bookExponentialValueSubgroup_eq_sup_zmultiples_of_single_radical