Module

NormValue.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.NormValue

3 declarations indexed from sourceView source ↗

Module documentation

Norm control of value cosets

For a finite extension of a Henselian valued field, the norm formula says that the extension degree times the value of an element is the value of its norm. Thus the order of every value-group coset divides the field degree, as required by the tame radical-generation argument.

Imports2

Imported by2

instance

exponentialValueGroupQuotientAddCommGroupNorm

L29 ↗

AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotientAddCommGroupNorm

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section NormValue
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]

Lean source · statement

instance exponentialValueGroupQuotientAddCommGroupNorm
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w)

theorem

exponentialValuation_norm_eq_finrank_nsmul

L37 ↗

AlgebraicNumberTheory.Valuations.exponentialValuation_norm_eq_finrank_nsmul

Documentation

Additive exponential form of the finite Henselian norm formula.

Source context 7 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section NormValue
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
local instance exponentialValueGroupQuotientAddCommGroupNorm
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem exponentialValuation_norm_eq_finrank_nsmul
    (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)
    (x : L) (hx : x ≠ 0) :
    v (Algebra.norm K x) = Module.finrank K L • w x

theorem

exponentialValueGroupQuotient_addOrderOf_dvd_finrank

L114 ↗

AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotient_addOrderOf_dvd_finrank

Documentation

The order of every actual value-group coset divides the field degree.

Source context 7 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section NormValue
variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
local instance exponentialValueGroupQuotientAddCommGroupNorm
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance

Lean source · statement

theorem exponentialValueGroupQuotient_addOrderOf_dvd_finrank
    (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)
    (q : ExponentialValueGroupQuotient v w) :
    addOrderOf q ∣ Module.finrank K L

Module documentation

Norm control of value cosets

Declarations

exponentialValueGroupQuotientAddCommGroupNorm

exponentialValuation_norm_eq_finrank_nsmul

exponentialValueGroupQuotient_addOrderOf_dvd_finrank