NYLL
Module

FieldUnitStructure.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FieldUnitStructure
3 declarations indexed from sourceView source ↗

Module documentation

Topological structure of local-field units

This file assembles the valuation, Teichmuller, and principal-unit factors in the canonical factor order. All topologies are the ones carried directly by the given WithZero (Multiplicative ℤ)-valued valuation.

Imports3
Imported by4

Declarations

def

chosenFieldUnitsStructure_mixedCharacteristic

L40 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.chosenFieldUnitsStructure_mixedCharacteristic
Documentation

The local-field structure theory, the mixed-characteristic field-unit structure theorem. In mixed characteristic the first principal units are a finite cyclic p-group times [K : ℚ_p] copies of ℤ_p; adjoining the valuation and Teichmuller factors gives the displayed topological decomposition of Kˣ in the canonical factor order.

Source context 8 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsContinuousMulEquivUniformizerRootsPrincipalUnitsOfWithZeroValuation) in
Lean source · full declaration
def chosenFieldUnitsStructure_mixedCharacteristic
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    let d := Module.finrank ℚ_[F.residueCharacteristic] K
    Σ a : ℕ,
      Multiplicative ℤ ×
          (Multiplicative (ZMod (Nat.card F.residueField - 1)) ×
            Multiplicative
      (ZMod (F.residueCharacteristic ^ a) ×
                (Fin d → ℤ_[F.residueCharacteristic]))) ≃ₜ* Kˣ := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  letI : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let d := Module.finrank ℚ_[F.residueCharacteristic] K
  let hex :=
    WithZeroValuation.exists_valuationSubring_valuation_eq_exp_neg_one_of_surjective
      v hv
  let π := Classical.choose hex
  have hπval : v (π : K) = WithZero.exp (-1 : ℤ) :=
    Classical.choose_spec hex
  have hπ : v.IsUniformizer (π : K) :=
    WithZeroValuation.isUniformizer_of_valuation_eq_exp_neg_one
      v (π : K) hπval
  obtain ⟨a, e⟩ :=
    chosenMixed_firstPrincipalUnitStructure_ofWithZeroValuation
      v hv
  exact ⟨a,
    fieldUnitsContinuousMulEquivUniformizerRootsPrincipalUnitsOfWithZeroValuation
      v hπ
      (Multiplicative
        (ZMod (F.residueCharacteristic ^ a) ×
          (Fin d → ℤ_[F.residueCharacteristic]))) e⟩
def

chosenFirstPrincipalUnitStructure_equalCharacteristic

L85 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.chosenFirstPrincipalUnitStructure_equalCharacteristic
Documentation

The exact principal-unit factor in the equal-characteristic field-unit structure theorem, reindexed from the prime-to-p degrees and residue-basis coordinates by ℕ.

Source context 8 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (adicPrincipalUnitsContinuousAddEquivUnderlyingOfWithZeroValuation) in
Lean source · full declaration
def chosenFirstPrincipalUnitStructure_equalCharacteristic
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)]
    [CharP K (ofWithZeroValuation v).residueCharacteristic] :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Multiplicative (ℕ → ℤ_[F.residueCharacteristic]) ≃ₜ*
      LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
        F.toCompleteDVF 1 := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let hex := F.toCompleteDVF.exists_uniformizer
  let π := Classical.choose hex
  have hπ : v.IsUniformizer (π : K) := Classical.choose_spec hex
  let : ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete
      (Valued.v : _root_.Valuation K
        (WithZero (Multiplicative ℤ))) := by
    change ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v
    infer_instance
  let E :=
    (CompleteDVF.higherPrincipalUnitGroup.iwasawaGlobalAdicPrincipalUnitsContinuousAddEquiv
      F hπ).trans
      (adicPrincipalUnitsContinuousAddEquivUnderlyingOfWithZeroValuation
        v)
  let I := iwasawaPadicIntProductContinuousAddEquivNat
    F.residueCharacteristic
    (CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F)
    F.residueCharacteristic_prime.pos
    Module.finrank_pos
  let eAdd : (ℕ → ℤ_[F.residueCharacteristic]) ≃ₜ+
      Additive
        (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
          F.toCompleteDVF 1) :=
    I.symm.trans E
  exact LocalFieldTheory.DiscreteValuationField.continuousMulEquivOfAdditiveTarget eAdd
def

chosenFieldUnitsStructure_equalCharacteristic

L129 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.chosenFieldUnitsStructure_equalCharacteristic
Documentation

The local-field structure theory, the equal-characteristic field-unit structure theorem. In equal characteristic the Iwasawa generators identify the first principal units with a countable product of ℤ_p; adjoining the valuation and Teichmuller factors gives the canonical topological decomposition of Kˣ.

Source context 8 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsContinuousMulEquivUniformizerRootsPrincipalUnitsOfWithZeroValuation) in
Lean source · full declaration
def chosenFieldUnitsStructure_equalCharacteristic
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)]
    [CharP K (ofWithZeroValuation v).residueCharacteristic] :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Multiplicative ℤ ×
        (Multiplicative (ZMod (Nat.card F.residueField - 1)) ×
          Multiplicative (ℕ → ℤ_[F.residueCharacteristic])) ≃ₜ* Kˣ := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let hex := F.toCompleteDVF.exists_uniformizer
  let π := Classical.choose hex
  have hπ : v.IsUniformizer (π : K) := Classical.choose_spec hex
  let ePrincipal :=
    chosenFirstPrincipalUnitStructure_equalCharacteristic v
  exact
    fieldUnitsContinuousMulEquivUniformizerRootsPrincipalUnitsOfWithZeroValuation
      v hπ (Multiplicative (ℕ → ℤ_[F.residueCharacteristic])) ePrincipal

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