NYLL
Module

DeepPrincipalUnits.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.MixedCharacteristicStructure.DeepPrincipalUnits
17 declarations indexed from sourceView source ↗

Module documentation

Deep principal units in mixed characteristic

This module equips the canonical Z_p lattice with the normalized valuation topology and transports integral-basis coordinates through the deep exponential--logarithm equivalence.

The canonical normalized-valuation model

Continuity for the normalized valuation used by the deep exponential–logarithm

equivalence

the deep exponential–logarithm equivalence connected to the integral basis

Imports1
Imported by2

Declarations

class

MixedWithZeroValuationContext

L37 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.MixedWithZeroValuationContext
Documentation

The canonical mixed-characteristic algebra and topology attached to a normalized ℤᵐ⁰-valued local field. The bundle retains both the integral algebra context and the direct valued-field structure; installing it exposes the coherent Q_p/Z_p scalar towers and valuation topology.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
class MixedWithZeroValuationContext
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] where
  /-- The integral-algebra context for the local-field model obtained by
  restricting the normalized valuation to its nonzero value group. -/
  integralAlgebra :
    MixedIntegralAlgebraContext (ofWithZeroValuation v)
  /-- The valued-field structure on `K` whose valuation is the original
  normalized `WithZero (Multiplicative ℤ)`-valued valuation. -/
  valued : Valued K (WithZero (Multiplicative ℤ))
def

mixedWithZeroValuationContext

L51 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedWithZeroValuationContext
Documentation

The canonical normalized-valuation context.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
def mixedWithZeroValuationContext
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] :
    MixedWithZeroValuationContext v
instance

mixedWithZeroValuationContextIntegralAlgebra

L64 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixedWithZeroValuationContextIntegralAlgebra
Documentation

The valued field carries the integral algebra context MixedIntegralAlgebraContext (ofWithZeroValuation v).

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
instance mixedWithZeroValuationContextIntegralAlgebra
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)]
    [ctx : MixedWithZeroValuationContext v] :
    MixedIntegralAlgebraContext (ofWithZeroValuation v)
theorem

continuous_qpadicNumbersAlgebra_ofWithZeroValuation

L80 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.continuous_qpadicNumbersAlgebra_ofWithZeroValuation
Documentation

For a normalized ℤᵐ⁰-valued local field, the canonical embedding Q_p → K is continuous for the direct topology induced by v.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  mrangeRestrict_nontriviallyNormedField
) in
Lean source · full declaration
theorem continuous_qpadicNumbersAlgebra_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Continuous (algebraMap ℚ_[F.residueCharacteristic] K) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let p : ℕ := F.residueCharacteristic
  let direct : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let restricted : Valued K F.mrangeValueGroup :=
    _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F.toCompleteDVF
  have hrestricted :
      @Continuous ℚ_[p] K inferInstance restricted.toTopologicalSpace
        (algebraMap ℚ_[p] K) := by
    let : Valued K F.mrangeValueGroup := restricted
    let : NontriviallyNormedField K :=
      mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    change Continuous
      (fun x : ℚ_[p] =>
        ((F.qpadicNumbersEquivQpadicClosureSubfield x :
          F.qpadicClosureSubfield) : K))
    exact continuous_subtype_val.comp
      F.qpadicNumbersToQpadicClosureSubfield_isUniformInducing.uniformContinuous.continuous
  have huniform :
      (Valued.mk' v).toUniformSpace =
        (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued
          F.toCompleteDVF).toUniformSpace := by
    change (Valued.mk' v).toUniformSpace =
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued
        (WithZeroValuationTopology.completeDVF v)).toUniformSpace
    exact WithZeroValuationTopology.valuedMk_uniformSpace_eq_mrangeRestrict v
  let : Valued K (WithZero (Multiplicative ℤ)) := direct
  rw [show direct.toTopologicalSpace = restricted.toTopologicalSpace by
    exact congrArg (fun U : UniformSpace K => U.toTopologicalSpace) huniform]
  exact hrestricted
theorem

continuous_padicIntToValuationSubring_ofWithZeroValuation

L124 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.continuous_padicIntToValuationSubring_ofWithZeroValuation
Documentation

The restricted map Z_p → O_K is continuous in the direct valuation topology.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem continuous_padicIntToValuationSubring_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Continuous F.padicIntToValuationSubring := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  apply Continuous.subtype_mk
  exact (continuous_qpadicNumbersAlgebra_ofWithZeroValuation v).comp
    continuous_subtype_val
theorem

continuousSMul_padicInt_valuationSubring_ofWithZeroValuation

L142 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.continuousSMul_padicInt_valuationSubring_ofWithZeroValuation
Documentation

The natural scalar multiplication of Z_p on O_K is continuous.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem continuousSMul_padicInt_valuationSubring_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    ContinuousSMul ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  refine ⟨?_⟩
  apply Continuous.subtype_mk
  change Continuous
    (fun z : ℤ_[F.residueCharacteristic] ×
        F.toCompleteDVF.valuationSubring =>
      ((F.padicIntToValuationSubring z.1 :
        F.toCompleteDVF.valuationSubring) : K) * (z.2 : K))
  exact
    (continuous_subtype_val.comp
      ((continuous_padicIntToValuationSubring_ofWithZeroValuation v).comp
        continuous_fst)).mul
      (continuous_subtype_val.comp continuous_snd)
theorem

continuousSMul_padicInt_maximalIdealPow_ofWithZeroValuation

L170 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.continuousSMul_padicInt_maximalIdealPow_ofWithZeroValuation
Documentation

The induced action on every maximal-ideal power is continuous.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
theorem continuousSMul_padicInt_maximalIdealPow_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (n : ℕ) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    ContinuousSMul ℤ_[F.residueCharacteristic]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : ContinuousSMul ℤ_[F.residueCharacteristic]
      F.toCompleteDVF.valuationSubring :=
    continuousSMul_padicInt_valuationSubring_ofWithZeroValuation v
  refine ⟨?_⟩
  apply Continuous.subtype_mk
  change Continuous
    (fun z : ℤ_[F.residueCharacteristic] ×
        ((F.toCompleteDVF.maximalIdeal ^ n :
          Ideal F.toCompleteDVF.valuationSubring)) =>
      z.1 • (z.2 : F.toCompleteDVF.valuationSubring))
  exact continuous_fst.smul (continuous_subtype_val.comp continuous_snd)
theorem

continuousSMul_padicInt_firstPrincipalUnit_ofWithZeroValuation

L203 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.continuousSMul_padicInt_firstPrincipalUnit_ofWithZeroValuation
Documentation

The canonical p-adic action on U^1 is jointly continuous for the direct normalized valuation topology.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
theorem continuousSMul_padicInt_firstPrincipalUnit_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    ContinuousSMul ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) 1)) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact
    CompleteDVF.higherPrincipalUnitGroup.principalUnitPadicContinuousSMulOfWithZeroValuation
      v
theorem

continuousSMul_padicInt_higherPrincipalUnit_ofWithZeroValuation

L226 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.continuousSMul_padicInt_higherPrincipalUnit_ofWithZeroValuation
Documentation

Every stable higher principal-unit subgroup inherits the joint continuous p-adic action from U^1.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
theorem continuousSMul_padicInt_higherPrincipalUnit_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    {r : ℕ} (hr : 1 ≤ r) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
      F.higherPrincipalUnitPadicModule hr
    ContinuousSMul ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) r)) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : Module ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) r)) :=
    F.higherPrincipalUnitPadicModule hr
  let : ContinuousSMul ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) 1)) :=
    continuousSMul_padicInt_firstPrincipalUnit_ofWithZeroValuation v
  have hinc : Continuous (F.higherPrincipalUnitAddToFirst hr) := by
    apply Continuous.subtype_mk
    exact continuous_subtype_val
  have hsmulFirst : Continuous
      (fun z : ℤ_[F.residueCharacteristic] ×
          Additive (higherPrincipalUnitGroup
            F.toCompleteDVF r) =>
        z.1 • F.higherPrincipalUnitAddToFirst hr z.2) :=
    continuous_fst.smul (hinc.comp continuous_snd)
  refine ⟨?_⟩
  apply Continuous.subtype_mk
  apply (continuous_subtype_val.comp hsmulFirst).congr
  intro z
  exact congrArg
    (fun y :
        Additive (higherPrincipalUnitGroup
          F.toCompleteDVF 1) =>
      ((Additive.toMul y :
        higherPrincipalUnitGroup
          F.toCompleteDVF 1) : F.toCompleteDVF.valuationSubringˣ))
    (F.higherPrincipalUnitAddToFirst_smul hr z.1 z.2).symm
def

mixed_maximalIdealPowHomeomorphPi_ofWithZeroValuation

L274 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_maximalIdealPowHomeomorphPi_ofWithZeroValuation
Documentation

The integral-basis coordinates on a maximal-ideal power are a homeomorphism for the direct normalized valuation topology.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · full declaration
def mixed_maximalIdealPowHomeomorphPi_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (n : ℕ) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) ≃ₜ
      (Fin (Module.finrank ℚ_[F.residueCharacteristic] K) →
        ℤ_[F.residueCharacteristic]) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  letI : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let p : ℕ := F.residueCharacteristic
  let d : ℕ := Module.finrank ℚ_[p] K
  letI : Module.Finite ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) :=
    F.mixed_maximalIdealPow_moduleFinite n
  letI : Module.Free ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) :=
    F.mixed_maximalIdealPow_moduleFree n
  letI : ContinuousSMul ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) :=
    continuousSMul_padicInt_maximalIdealPow_ofWithZeroValuation v n
  letI : ContinuousAdd
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) := by
    refine ⟨?_⟩
    apply Continuous.subtype_mk
    apply Continuous.subtype_mk
    exact
      (continuous_subtype_val.comp
        (continuous_subtype_val.comp continuous_fst)).add
      (continuous_subtype_val.comp
        (continuous_subtype_val.comp continuous_snd))
  let b : Basis (Fin d) ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) :=
    Module.finBasisOfFinrankEq ℤ_[p]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring))
      (by simpa [d] using
        F.mixed_maximalIdealPow_finrank n)
  let e := b.equivFun
  have heinv : Continuous e.symm := by
    have hsum : Continuous (fun x : Fin d → ℤ_[p] => ∑ i, x i • b i) := by
      fun_prop
    convert hsum using 1
    funext x
    exact b.equivFun_symm_apply x
  exact
    (e.symm.toEquiv.toHomeomorphOfContinuousClosed
      heinv heinv.isClosedMap).symm
theorem

mixed_one_le_of_log_level

L338 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_one_le_of_log_level
Documentation

The logarithmic depth inequality forces a positive filtration level.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
Lean source · statement
theorem mixed_one_le_of_log_level
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (n : ℕ)
    (hlevel :
      (ramificationIndexOfWithZeroValuation v : ℚ) /
          (((ofWithZeroValuation v).residueCharacteristic : ℚ) - 1) <
        (n : ℚ)) :
    1 ≤ n
def

mixed_deepLogContinuousAddEquiv

L365 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_deepLogContinuousAddEquiv
Documentation

The logarithm direction of the deep exponential–logarithm equivalence, written as a topological additive equivalence U^n ≃ₜ+ m^n.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
def mixed_deepLogContinuousAddEquiv
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v)
    (n : ℕ)
    (hlevel :
      (ramificationIndexOfWithZeroValuation v : ℚ) /
          (((ofWithZeroValuation v).residueCharacteristic : ℚ) - 1) <
        (n : ℚ)) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n) ≃ₜ+
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  letI : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact continuousAddEquivOfMultiplicativeSource
    (MultiplicativeIntegerValuation.chosenExpLogContinuousMulEquiv
      v hv n hlevel)
theorem

mixed_deepLog_map_natCast_smul

L395 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_deepLog_map_natCast_smul
Documentation

The deep logarithm is compatible with natural scalars (ordinary powers) before the density argument upgrades it to all of Z_p.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
theorem mixed_deepLog_map_natCast_smul
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v)
    (n : ℕ)
    (hlevel :
      (ramificationIndexOfWithZeroValuation v : ℚ) /
          (((ofWithZeroValuation v).residueCharacteristic : ℚ) - 1) <
        (n : ℚ))
    (m : ℕ)
    (x : Additive
      (higherPrincipalUnitGroup ((ofWithZeroValuation v).toCompleteDVF) n)) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
      F.higherPrincipalUnitPadicModule hn
    mixed_deepLogContinuousAddEquiv
        v hv n hlevel
        ((m : ℤ_[F.residueCharacteristic]) • x) =
      (m : ℤ_[F.residueCharacteristic]) •
        mixed_deepLogContinuousAddEquiv
          v hv n hlevel x := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : Module ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
    F.higherPrincipalUnitPadicModule hn
  dsimp only
  rw [Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul]
  change
    (mixed_deepLogContinuousAddEquiv v hv n hlevel).toAddEquiv.toAddMonoidHom
        (m • x) =
      m •
        (mixed_deepLogContinuousAddEquiv v hv n hlevel).toAddEquiv.toAddMonoidHom x
  exact
    (mixed_deepLogContinuousAddEquiv v hv n hlevel).toAddEquiv.toAddMonoidHom.map_nsmul
      m x
def

mixed_deepLogLinearEquiv

L446 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_deepLogLinearEquiv
Documentation

At a depth allowed by the deep exponential–logarithm equivalence, logarithm is a Z_p-linear equivalence from U^n to the additive ideal m^n.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
def mixed_deepLogLinearEquiv
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v)
    (n : ℕ)
    (hlevel :
      (ramificationIndexOfWithZeroValuation v : ℚ) /
          (((ofWithZeroValuation v).residueCharacteristic : ℚ) - 1) <
        (n : ℚ)) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
      F.higherPrincipalUnitPadicModule hn
    Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n) ≃ₗ[
        ℤ_[F.residueCharacteristic]]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
  letI : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  letI : Module ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
    F.higherPrincipalUnitPadicModule hn
  letI : ContinuousSMul ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
    continuousSMul_padicInt_higherPrincipalUnit_ofWithZeroValuation v hn
  letI : ContinuousSMul ℤ_[F.residueCharacteristic]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) :=
    continuousSMul_padicInt_maximalIdealPow_ofWithZeroValuation v n
  let e := mixed_deepLogContinuousAddEquiv
    v hv n hlevel
  exact padicLinearEquivOfContinuousAddEquiv e.toAddEquiv e.continuous
theorem

mixed_deepPrincipalUnit_moduleFinite

L492 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_deepPrincipalUnit_moduleFinite
Documentation

The deep principal-unit group is finite over Z_p; via logarithm it is finite free of the same rank as O_K.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
theorem mixed_deepPrincipalUnit_moduleFinite
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v)
    (n : ℕ)
    (hlevel :
      (ramificationIndexOfWithZeroValuation v : ℚ) /
          (((ofWithZeroValuation v).residueCharacteristic : ℚ) - 1) <
        (n : ℚ)) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
      F.higherPrincipalUnitPadicModule hn
    Module.Finite ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
  let : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : Module ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
    F.higherPrincipalUnitPadicModule hn
  let : Module.Finite ℤ_[F.residueCharacteristic]
      ((F.toCompleteDVF.maximalIdeal ^ n :
        Ideal F.toCompleteDVF.valuationSubring)) :=
    F.mixed_maximalIdealPow_moduleFinite n
  exact Module.Finite.equiv
    (mixed_deepLogLinearEquiv
      v hv n hlevel).symm
def

mixed_deepPrincipalUnitLinearEquivPi

L533 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_deepPrincipalUnitLinearEquivPi
Documentation

Integral-basis coordinates after logarithm give the algebraic coordinate isomorphism U^n ≃ Z_p^d.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
def mixed_deepPrincipalUnitLinearEquivPi
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v)
    (n : ℕ)
    (hlevel :
      (ramificationIndexOfWithZeroValuation v : ℚ) /
          (((ofWithZeroValuation v).residueCharacteristic : ℚ) - 1) <
        (n : ℚ)) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    letI : Module ℤ_[F.residueCharacteristic]
        (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
      F.higherPrincipalUnitPadicModule hn
    Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n) ≃ₗ[
        ℤ_[F.residueCharacteristic]]
      (Fin (Module.finrank ℚ_[F.residueCharacteristic] K) →
        ℤ_[F.residueCharacteristic]) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  let hn : 1 ≤ n := mixed_one_le_of_log_level v n hlevel
  letI : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  letI : Module ℤ_[F.residueCharacteristic]
      (Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n)) :=
    F.higherPrincipalUnitPadicModule hn
  exact
    (mixed_deepLogLinearEquiv
      v hv n hlevel).trans
        (F.mixed_maximalIdealPowLinearEquivPi n)
def

mixed_deepPrincipalUnitHomeomorphPi

L573 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.mixed_deepPrincipalUnitHomeomorphPi
Documentation

The same coordinate identification is a homeomorphism, as asserted explicitly in the mixed-characteristic field-unit structure theorem.

Source context 8 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped WithZero nonZeroDivisors
open Module
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
def mixed_deepPrincipalUnitHomeomorphPi
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (hv : Function.Surjective v)
    (n : ℕ)
    (hlevel :
      (ramificationIndexOfWithZeroValuation v : ℚ) /
          (((ofWithZeroValuation v).residueCharacteristic : ℚ) - 1) <
        (n : ℚ)) :
    let F : LocalField.{u, 0} K := ofWithZeroValuation v
    letI : MixedWithZeroValuationContext v :=
      mixedWithZeroValuationContext v
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Additive (higherPrincipalUnitGroup (F.toCompleteDVF) n) ≃ₜ
      (Fin (Module.finrank ℚ_[F.residueCharacteristic] K) →
        ℤ_[F.residueCharacteristic]) := by
  let F : LocalField.{u, 0} K := ofWithZeroValuation v
  letI : MixedWithZeroValuationContext v :=
    mixedWithZeroValuationContext v
  letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact
    (mixed_deepLogContinuousAddEquiv
      v hv n hlevel).toHomeomorph.trans
        (mixed_maximalIdealPowHomeomorphPi_ofWithZeroValuation
          v n)

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