Module

IwasawaPrincipalUnits.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.IwasawaPrincipalUnits

104 declarations indexed from sourceView source ↗

Module documentation

The convergent Iwasawa product for principal units

This module assembles the finite-level Iwasawa factors into a compatible family in the principal-unit inverse limit, proves continuity and bijectivity, and packages the resulting topological additive equivalence.

Finite-level Iwasawa generators for principal units

This file develops an explicit topological product decomposition of principal units. In equal characteristic, choose a residue-field basis omega_i over F_p. For a positive degree n, the prime-to-p Iwasawa map is

g_n(a_i) = product_i (1 + [omega_i] pi^n) ^ a_i.

The powers by p-adic integers are the canonical powers constructed from the finite principal-unit quotients in PrincipalUnitPadicAction. This module constructs each finite-level factor g_n, proves its filtration properties, and establishes its algebraic injectivity. The convergent global product is assembled in IwasawaPrincipalUnits.

Reduction of p-adic exponents on one graded layer

Algebraic injectivity of each Iwasawa factor

The convergent product, constructed through finite quotients

Imports8

Mathlib.Algebra.Algebra.ZMod
Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.IwasawaIndexing
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitInverseLimitSurjectivity
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.EqualCharacteristicLaurent
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.LinearAlgebra.Finsupp.VectorSpace
Mathlib.NumberTheory.Padics.ProperSpace

Imported by3

instance

residueFieldZModAlgebra

L61 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueFieldZModAlgebra

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

instance residueFieldZModAlgebra
    (F : LocalField.{u, v} K) :
    Algebra (ZMod F.residueCharacteristic) F.residueField

abbrev

iwasawaResidueRank

L68 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank

Documentation

The number of vectors in a basis of the residue field over its prime field. This is the f in q = p^f in the field-unit structure theorem.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

abbrev iwasawaResidueRank (F : LocalField.{u, v} K) : ℕ

def

iwasawaResidueBasis

L73 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueBasis

Documentation

A fixed F_p-basis of the residue field, denoted omega_1,...,omega_f in this construction.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaResidueBasis (F : LocalField.{u, v} K) :
    Module.Basis (Fin (iwasawaResidueRank F))
      (ZMod F.residueCharacteristic) F.residueField

theorem

residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank

L80 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank

Documentation

The rank chosen above is the exponent in the finite-field cardinality identity q = p^f.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank
    (F : LocalField.{u, v} K) :
    Nat.card F.residueField =
      F.residueCharacteristic ^ iwasawaResidueRank F

def

iwasawaSeedIdeal

L89 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSeedIdeal

Documentation

The element [omega_i] pi^n of the n-th maximal-ideal power.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaSeedIdeal
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (i : Fin (iwasawaResidueRank F)) :
    ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)

theorem

iwasawaSeedIdeal_val

L104 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSeedIdeal_val

Documentation

Establishes the identity (iwasawaSeedIdeal F hpi n i : F.valuationSubring) = CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift F.toCompleteDVF (iwasawaResidueBasis F i) * pi ^ n.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaSeedIdeal_val
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (i : Fin (iwasawaResidueRank F)) :
    (iwasawaSeedIdeal F hpi n i : F.valuationSubring) =
      residueTeichmullerLift F.toCompleteDVF
          (iwasawaResidueBasis F i) * pi ^ n

def

iwasawaSeedAtLevel

L115 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSeedAtLevel

Documentation

The generator 1 + [omega_i] pi^n, first as an element of U^n.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaSeedAtLevel
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (i : Fin (iwasawaResidueRank F)) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) n

theorem

iwasawaSeedAtLevel_val

L131 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSeedAtLevel_val

Documentation

Establishes the identity (((iwasawaSeedAtLevel F hpi n hn i : ((CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF)) n) : F.valuationSubringˣ) : F.valuationSubring) = 1 + CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift F.toCompleteDVF (iwasawaResidueBasis F i) * pi ^ n.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaSeedAtLevel_val
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (i : Fin (iwasawaResidueRank F)) :
    (((iwasawaSeedAtLevel F hpi n hn i :
        ((higherPrincipalUnitGroup F.toCompleteDVF)) n) : F.valuationSubringˣ) :
      F.valuationSubring) =
      1 + residueTeichmullerLift F.toCompleteDVF
          (iwasawaResidueBasis F i) * pi ^ n

def

iwasawaSeed

L148 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSeed

Documentation

The same generator regarded as a first principal unit, so that the canonical p-adic scalar action is available.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaSeed
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (i : Fin (iwasawaResidueRank F)) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) 1

theorem

iwasawaSeed_val

L164 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSeed_val

Documentation

Establishes the identity (((iwasawaSeed F hpi n hn i : ((CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) : F.valuationSubring) = 1 + CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift F.toCompleteDVF (iwasawaResidueBasis F i) * pi ^ n.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaSeed_val
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (i : Fin (iwasawaResidueRank F)) :
    (((iwasawaSeed F hpi n hn i : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) :
        F.valuationSubringˣ) : F.valuationSubring) =
      1 + residueTeichmullerLift F.toCompleteDVF
          (iwasawaResidueBasis F i) * pi ^ n

theorem

principalUnitSuccQuotAddEquivResidue_iwasawaSeed

L177 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotAddEquivResidue_iwasawaSeed

Documentation

The leading coefficient of 1 + [omega_i] pi^n in U^n/U^(n+1) is exactly the basis vector omega_i.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitSuccQuotAddEquivResidue_iwasawaSeed
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (i : Fin (iwasawaResidueRank F)) :
    principalUnitSuccQuotAddEquivResidueOfUniformizer
        F.toCompleteDVF hpi n hn
      (Additive.ofMul
        (principalUnitSuccQuotMk F.toCompleteDVF n
          (iwasawaSeedAtLevel F hpi n hn i))) =
      iwasawaResidueBasis F i

def

iwasawaLeadingLayerAddEquiv

L205 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaLeadingLayerAddEquiv

Documentation

The basis-coordinate form of the leading-layer calculation. This is the linear algebra behind formula (1) at s = 0: the chosen f seed units give every class in U^n/U^(n+1), uniquely modulo p.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaLeadingLayerAddEquiv
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) :
    (Fin (iwasawaResidueRank F) → ZMod F.residueCharacteristic) ≃+
      Additive (principalUnitSuccQuot
        F.toCompleteDVF n)

theorem

iwasawaLeadingLayerAddEquiv_single

L222 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaLeadingLayerAddEquiv_single

Documentation

Establishes the identity iwasawaLeadingLayerAddEquiv F hpi n hn (Pi.single i 1) = Additive.ofMul (CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotMk F.toCompleteDVF n (iwasawaSeedAtLevel F hpi n hn i)).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaLeadingLayerAddEquiv_single
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (i : Fin (iwasawaResidueRank F)) :
    iwasawaLeadingLayerAddEquiv F hpi n hn (Pi.single i 1) =
      Additive.ofMul
        (principalUnitSuccQuotMk F.toCompleteDVF n
          (iwasawaSeedAtLevel F hpi n hn i))

theorem

iwasawaLeadingLayerAddEquiv_eq_zero_iff

L251 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaLeadingLayerAddEquiv_eq_zero_iff

Documentation

Characterizes iwasawaLeadingLayerAddEquiv F hpi n hn a = 0 by the equivalent condition a = 0.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaLeadingLayerAddEquiv_eq_zero_iff
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ZMod F.residueCharacteristic) :
    iwasawaLeadingLayerAddEquiv F hpi n hn a = 0 ↔ a = 0

theorem

exists_padicInt_sub_toZMod_val_eq_residueCharacteristic_mul

L269 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_padicInt_sub_toZMod_val_eq_residueCharacteristic_mul

Documentation

A p-adic integer differs from the ordinary representative of its reduction modulo p by a multiple of p.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_padicInt_sub_toZMod_val_eq_residueCharacteristic_mul
    (F : LocalField.{u, v} K)
    (a : ℤ_[F.residueCharacteristic]) :
    ∃ b : ℤ_[F.residueCharacteristic],
      a - ((PadicInt.toZMod a).val : ℤ_[F.residueCharacteristic]) =
        (F.residueCharacteristic : ℤ_[F.residueCharacteristic]) * b

def

principalUnitPadicSmulAtLevel

L285 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadicSmulAtLevel

Documentation

A p-adic power of a first principal unit, remembered at a specified higher-unit level.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def principalUnitPadicSmulAtLevel
    (F : LocalField.{u, v} K) (r : ℕ) (hr : 1 ≤ r)
    (a : ℤ_[F.residueCharacteristic])
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1)
    (hx : (x : F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) r) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) r

theorem

principalUnitSuccQuotMk_padicSmulAtLevel_eq_toZMod_val

L298 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotMk_padicSmulAtLevel_eq_toZMod_val

Documentation

On U^r/U^(r+1), a p-adic exponent may be replaced by its first ordinary approximation. This is the precise version of choosing the integers b_i ≡ a_i (mod p) in the coefficient calculation.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitSuccQuotMk_padicSmulAtLevel_eq_toZMod_val
    (F : LocalField.{u, v} K) (r : ℕ) (hr : 1 ≤ r)
    (a : ℤ_[F.residueCharacteristic])
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1)
    (hx : (x : F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) r) :
    principalUnitSuccQuotMk F.toCompleteDVF r
        (principalUnitPadicSmulAtLevel F r hr a x hx) =
      principalUnitSuccQuotMk F.toCompleteDVF r
        (principalUnitPadicSmulAtLevel F r hr
          ((PadicInt.toZMod a).val : ℤ_[F.residueCharacteristic]) x hx)

def

principalUnitLeadingCoefficientAddHom

L336 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom

Documentation

The leading coefficient map U^r -> k, written additively.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def principalUnitLeadingCoefficientAddHom
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (r : ℕ) (hr : 1 ≤ r) :
    Additive (((higherPrincipalUnitGroup F.toCompleteDVF)) r) →+ F.residueField

theorem

principalUnitLeadingCoefficientAddHom_eq_zero_iff_mem_succ

L367 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom_eq_zero_iff_mem_succ

Documentation

Characterizes principalUnitLeadingCoefficientAddHom F hpi n hn (Additive.ofMul x) = 0 by the equivalent condition ((x : F.valuationSubringˣ) : F.valuationSubringˣ) ∈ ((CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF)) (n + 1).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitLeadingCoefficientAddHom_eq_zero_iff_mem_succ
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) n) :
    principalUnitLeadingCoefficientAddHom F hpi n hn (Additive.ofMul x) = 0 ↔
      ((x : F.valuationSubringˣ) : F.valuationSubringˣ) ∈
        ((higherPrincipalUnitGroup F.toCompleteDVF)) (n + 1)

theorem

padicInt_toZMod_eq_zero_iff_exists_residueCharacteristic_mul

L392 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.padicInt_toZMod_eq_zero_iff_exists_residueCharacteristic_mul

Documentation

Reduction modulo p detects divisibility by p in Z_p.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem padicInt_toZMod_eq_zero_iff_exists_residueCharacteristic_mul
    (F : LocalField.{u, v} K) (a : ℤ_[F.residueCharacteristic]) :
    PadicInt.toZMod a = 0 ↔
      ∃ b : ℤ_[F.residueCharacteristic],
        a = (F.residueCharacteristic : ℤ_[F.residueCharacteristic]) * b

theorem

exists_residueCharacteristic_smul_eq_iff_toZMod_eq_zero

L411 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_residueCharacteristic_smul_eq_iff_toZMod_eq_zero

Documentation

A vector lies in p Z_p^f exactly when all of its residue coordinates vanish.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_residueCharacteristic_smul_eq_iff_toZMod_eq_zero
    (F : LocalField.{u, v} K)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    (∃ b : Fin (iwasawaResidueRank F) →
        ℤ_[F.residueCharacteristic],
      a = (F.residueCharacteristic : ℤ_[F.residueCharacteristic]) • b) ↔
      ∀ i, PadicInt.toZMod (a i) = 0

theorem

iwasawa_residue_combination_eq_zero_iff

L432 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawa_residue_combination_eq_zero_iff

Documentation

The residue-basis combination is zero exactly when all reduced coordinates are zero.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawa_residue_combination_eq_zero_iff
    (F : LocalField.{u, v} K)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    (∑ i, PadicInt.toZMod (a i) • iwasawaResidueBasis F i) = 0 ↔
      ∀ i, PadicInt.toZMod (a i) = 0

def

principalUnitOneAddUniformizerPowAtLevel

L451 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddUniformizerPowAtLevel

Documentation

The principal unit 1 + r*pi^n, used as a canonical representative of a prescribed leading residue coefficient.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def principalUnitOneAddUniformizerPowAtLevel
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (r : F.valuationSubring) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) n

theorem

principalUnitOneAddUniformizerPowAtLevel_val

L466 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddUniformizerPowAtLevel_val

Documentation

Establishes the identity (((principalUnitOneAddUniformizerPowAtLevel F hpi n hn r : ((CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF)) n) : F.valuationSubringˣ) : F.valuationSubring) = 1 + r * pi ^ n.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitOneAddUniformizerPowAtLevel_val
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (r : F.valuationSubring) :
    (((principalUnitOneAddUniformizerPowAtLevel F hpi n hn r :
        ((higherPrincipalUnitGroup F.toCompleteDVF)) n) : F.valuationSubringˣ) :
      F.valuationSubring) = 1 + r * pi ^ n

theorem

principalUnitLeadingCoefficientAddHom_oneAddUniformizerPow

L480 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom_oneAddUniformizerPow

Documentation

The leading coefficient of 1 + r*pi^n is the residue of r.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitLeadingCoefficientAddHom_oneAddUniformizerPow
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (r : F.valuationSubring) :
    principalUnitLeadingCoefficientAddHom F hpi n hn
        (Additive.ofMul
          (principalUnitOneAddUniformizerPowAtLevel F hpi n hn r)) =
      F.residueMap r

theorem

pow_residueCharacteristic_pow_mem_higher_mul

L503 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.pow_residueCharacteristic_pow_mem_higher_mul

Documentation

In equal characteristic, a p^s-th power sends U^n into U^(n*p^s). This is the depth multiplication used in both (1) and (2).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem pow_residueCharacteristic_pow_mem_higher_mul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {n : ℕ} (s : ℕ)
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1)
    (hx : (x : F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) n) :
    (((x ^ (F.residueCharacteristic ^ s) :
        ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) :
      F.valuationSubringˣ) ∈
        ((higherPrincipalUnitGroup F.toCompleteDVF))
          (n * F.residueCharacteristic ^ s)

def

higherUnitToFirst

L547 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.higherUnitToFirst

Documentation

Inclusion U^n -> U^1.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def higherUnitToFirst
    (F : LocalField.{u, v} K) (n : ℕ) (hn : 1 ≤ n)
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) n) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) 1

theorem

one_le_mul_residueCharacteristic_pow

L555 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.one_le_mul_residueCharacteristic_pow

Documentation

Proves the bound 1 ≤ n * F.residueCharacteristic ^ s.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem one_le_mul_residueCharacteristic_pow
    (F : LocalField.{u, v} K) {n : ℕ} (hn : 1 ≤ n) (s : ℕ) :
    1 ≤ n * F.residueCharacteristic ^ s

def

principalUnitFrobeniusAtLevel

L564 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitFrobeniusAtLevel

Documentation

A p^s-th power from U^n, with its exact equal-characteristic depth n*p^s built into the codomain.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def principalUnitFrobeniusAtLevel
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) n) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) (n * F.residueCharacteristic ^ s)

theorem

principalUnitFrobeniusAtLevel_oneAddUniformizerPow

L577 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitFrobeniusAtLevel_oneAddUniformizerPow

Documentation

Frobenius on a canonical representative: (1+r*pi^n)^(p^s) = 1+r^(p^s) pi^(n*p^s).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem principalUnitFrobeniusAtLevel_oneAddUniformizerPow
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ) (r : F.valuationSubring) :
    let m := n * F.residueCharacteristic ^ s
    let hm : 1 ≤ m := one_le_mul_residueCharacteristic_pow F hn s
    principalUnitFrobeniusAtLevel F n hn s
        (principalUnitOneAddUniformizerPowAtLevel F hpi n hn r) =
      principalUnitOneAddUniformizerPowAtLevel F hpi m hm
        (r ^ (F.residueCharacteristic ^ s)) := by
  dsimp only
  apply Subtype.ext
  apply Units.ext
  change
    (1 + r * pi ^ n) ^ (F.residueCharacteristic ^ s) =
      1 + r ^ (F.residueCharacteristic ^ s) *
        pi ^ (n * F.residueCharacteristic ^ s)
  rw [add_pow_char_pow, mul_pow, pow_mul]
  simp

theorem

principalUnitLeadingCoefficientAddHom_frobenius

L601 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom_frobenius

Documentation

Frobenius raises the leading residue coefficient to its p^s-th power.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem principalUnitLeadingCoefficientAddHom_frobenius
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) n) :
    let m := n * F.residueCharacteristic ^ s
    let hm : 1 ≤ m := one_le_mul_residueCharacteristic_pow F hn s
    principalUnitLeadingCoefficientAddHom F hpi m hm
        (Additive.ofMul (principalUnitFrobeniusAtLevel F n hn s x)) =
      (principalUnitLeadingCoefficientAddHom F hpi n hn
        (Additive.ofMul x)) ^ (F.residueCharacteristic ^ s) := by
  dsimp only
  let q : ℕ := F.residueCharacteristic ^ s
  let m : ℕ := n * q
  have hq : 1 ≤ q := by
    exact pow_pos F.residueCharacteristic_prime.pos s
  have hm : 1 ≤ m := by
    exact one_le_mul_residueCharacteristic_pow F hn s
  let lead : F.residueField :=
    principalUnitLeadingCoefficientAddHom F hpi n hn (Additive.ofMul x)
  let r : F.valuationSubring :=
    residueTeichmullerLift F.toCompleteDVF lead
  let y : ((higherPrincipalUnitGroup F.toCompleteDVF)) n :=
    principalUnitOneAddUniformizerPowAtLevel F hpi n hn r
  have hyLead :
      principalUnitLeadingCoefficientAddHom F hpi n hn
          (Additive.ofMul y) = lead := by
    rw [principalUnitLeadingCoefficientAddHom_oneAddUniformizerPow]
    exact residueMap_residueTeichmullerLift F.toCompleteDVF lead
  have hxyQuot :
      principalUnitSuccQuotMk F.toCompleteDVF n x =
        principalUnitSuccQuotMk F.toCompleteDVF n y := by
    apply (principalUnitSuccQuotAddEquivResidueOfUniformizer
      F.toCompleteDVF hpi n hn).injective
    change
      principalUnitLeadingCoefficientAddHom F hpi n hn (Additive.ofMul x) =
        principalUnitLeadingCoefficientAddHom F hpi n hn (Additive.ofMul y)
    exact hyLead.symm
  have hxyDeep :
      (((x / y : ((higherPrincipalUnitGroup F.toCompleteDVF)) n) : F.valuationSubringˣ) :
        F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) (n + 1) :=
    (principalUnitSuccQuotMk_eq_iff_div_mem F.toCompleteDVF n x y).1 hxyQuot
  let d : ((higherPrincipalUnitGroup F.toCompleteDVF)) (n + 1) :=
    ⟨((x / y : ((higherPrincipalUnitGroup F.toCompleteDVF)) n) : F.valuationSubringˣ), hxyDeep⟩
  have hdPow := pow_residueCharacteristic_pow_mem_higher_mul F s
    (higherUnitToFirst F (n + 1) (Nat.succ_le_succ (Nat.zero_le n)) d)
    d.property
  have hlevel : m + 1 ≤ (n + 1) * q := by
    calc
      m + 1 ≤ m + q := Nat.add_le_add_left hq m
      _ = (n + 1) * q := by simp [m, Nat.add_mul]
  have hdPow' :
      ((((higherUnitToFirst F (n + 1)
          (Nat.succ_le_succ (Nat.zero_le n)) d) ^ q :
          ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) :
        F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) (m + 1) :=
    antitone F.toCompleteDVF hlevel (by
      simpa [q] using hdPow)
  have hpowQuot :
      principalUnitSuccQuotMk F.toCompleteDVF m
          (principalUnitFrobeniusAtLevel F n hn s x) =
        principalUnitSuccQuotMk F.toCompleteDVF m
          (principalUnitFrobeniusAtLevel F n hn s y) := by
    apply (principalUnitSuccQuotMk_eq_iff_div_mem F.toCompleteDVF m _ _).2
    change
      (((principalUnitFrobeniusAtLevel F n hn s x /
          principalUnitFrobeniusAtLevel F n hn s y :
        ((higherPrincipalUnitGroup F.toCompleteDVF)) m) : F.valuationSubringˣ) :
        F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) (m + 1)
    simpa [principalUnitFrobeniusAtLevel, higherUnitToFirst, d, q, m,
      div_pow] using hdPow'
  have hleadEq :
      principalUnitLeadingCoefficientAddHom F hpi m hm
          (Additive.ofMul (principalUnitFrobeniusAtLevel F n hn s x)) =
        principalUnitLeadingCoefficientAddHom F hpi m hm
          (Additive.ofMul (principalUnitFrobeniusAtLevel F n hn s y)) := by
    exact congrArg
      (fun z : principalUnitSuccQuot F.toCompleteDVF m =>
        (principalUnitSuccQuotAddEquivResidueOfUniformizer
          F.toCompleteDVF hpi m hm) (Additive.ofMul z)) hpowQuot
  rw [hleadEq, principalUnitFrobeniusAtLevel_oneAddUniformizerPow,
    principalUnitLeadingCoefficientAddHom_oneAddUniformizerPow, map_pow]
  change F.residueMap r ^ q = lead ^ q
  rw [show F.residueMap r = lead from
    residueMap_residueTeichmullerLift F.toCompleteDVF lead]

theorem

principalUnitLeadingCoefficientAddHom_iwasawaSeed

L693 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom_iwasawaSeed

Documentation

Establishes the identity principalUnitLeadingCoefficientAddHom F hpi r hr (Additive.ofMul (iwasawaSeedAtLevel F hpi r hr i)) = iwasawaResidueBasis F i.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitLeadingCoefficientAddHom_iwasawaSeed
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (r : ℕ) (hr : 1 ≤ r) (i : Fin (iwasawaResidueRank F)) :
    principalUnitLeadingCoefficientAddHom F hpi r hr
        (Additive.ofMul (iwasawaSeedAtLevel F hpi r hr i)) =
      iwasawaResidueBasis F i

theorem

principalUnitLeadingCoefficientAddHom_padicSmul_iwasawaSeed

L705 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom_padicSmul_iwasawaSeed

Documentation

The leading coefficient of one p-adically powered seed only depends on the exponent modulo p.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitLeadingCoefficientAddHom_padicSmul_iwasawaSeed
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (r : ℕ) (hr : 1 ≤ r)
    (a : ℤ_[F.residueCharacteristic])
    (i : Fin (iwasawaResidueRank F)) :
    principalUnitLeadingCoefficientAddHom F hpi r hr
        (Additive.ofMul
          (principalUnitPadicSmulAtLevel F r hr a
            (iwasawaSeed F hpi r hr i)
            (iwasawaSeedAtLevel F hpi r hr i).property)) =
      PadicInt.toZMod a •
        iwasawaResidueBasis F i

def

iwasawaGn

L766 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGn

Documentation

The Iwasawa homomorphism g_n : Z_p^f -> U^1. Its range is shown below to lie in U^n. In additive notation the Iwasawa product is a finite sum of p-adic scalar multiples of the seed units.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaGn
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) :
    (Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) →ₗ[ℤ_[F.residueCharacteristic]]
      Additive (((higherPrincipalUnitGroup F.toCompleteDVF)) 1)

theorem

iwasawaGn_apply

L780 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGn_apply

Documentation

The defining evaluation formula for iwasawaGn is iwasawaGn F hpi n hn a = ∑ i, a i • Additive.ofMul (iwasawaSeed F hpi n hn i).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaGn_apply
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    iwasawaGn F hpi n hn a =
      ∑ i, a i • Additive.ofMul (iwasawaSeed F hpi n hn i)

theorem

iwasawaGn_mem_higher

L794 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGn_mem_higher

Documentation

Every value of g_n belongs to U^n, as asserted by its codomain in the canonical construction.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaGn_mem_higher
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    ((Additive.toMul (iwasawaGn F hpi n hn a) :
        ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) ∈
      ((higherPrincipalUnitGroup F.toCompleteDVF)) n

def

iwasawaGnAtLevel

L825 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGnAtLevel

Documentation

g_n(a), now with its proved membership in U^n built into the type.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaGnAtLevel
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) n

theorem

additive_iwasawaGnAtLevel_eq_sum

L841 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.additive_iwasawaGnAtLevel_eq_sum

Documentation

Establishes the identity Additive.ofMul (iwasawaGnAtLevel F hpi n hn a) = ∑ i, Additive.ofMul (principalUnitPadicSmulAtLevel F n hn (a i) (iwasawaSeed F hpi n hn i) (iwasawaSeedAtLevel F hpi n hn i).property).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem additive_iwasawaGnAtLevel_eq_sum
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    Additive.ofMul (iwasawaGnAtLevel F hpi n hn a) =
      ∑ i, Additive.ofMul
        (principalUnitPadicSmulAtLevel F n hn (a i)
          (iwasawaSeed F hpi n hn i)
          (iwasawaSeedAtLevel F hpi n hn i).property)

theorem

principalUnitLeadingCoefficientAddHom_iwasawaGnAtLevel

L901 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom_iwasawaGnAtLevel

Documentation

The exact leading coefficient of g_n(a): it is the residue-basis linear combination of the reductions of the p-adic coordinates.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnitLeadingCoefficientAddHom_iwasawaGnAtLevel
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    principalUnitLeadingCoefficientAddHom F hpi n hn
        (Additive.ofMul (iwasawaGnAtLevel F hpi n hn a)) =
      ∑ i,
        PadicInt.toZMod (a i) •
          iwasawaResidueBasis F i

theorem

iwasawaGn_residueCharacteristic_pow_smul_eq_pow

L920 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGn_residueCharacteristic_pow_smul_eq_pow

Documentation

Multiplying every coordinate by the ordinary scalar p^s turns g_n into the ordinary p^s-th power of g_n(a).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaGn_residueCharacteristic_pow_smul_eq_pow
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    Additive.toMul
        (iwasawaGn F hpi n hn
          ((F.residueCharacteristic ^ s :
              ℤ_[F.residueCharacteristic]) • a)) =
      (Additive.toMul (iwasawaGn F hpi n hn a)) ^
        (F.residueCharacteristic ^ s)

def

iwasawaGnScaledAtLevel

L948 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGnScaledAtLevel

Documentation

The canonical g_n(p^s a), with the exact depth m = n*p^s built into its type.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaGnScaledAtLevel
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF))
      (n * F.residueCharacteristic ^ s)

theorem

iwasawaGnScaledAtLevel_eq_frobenius

L971 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGnScaledAtLevel_eq_frobenius

Documentation

Establishes the identity iwasawaGnScaledAtLevel F hpi n hn s a = principalUnitFrobeniusAtLevel F n hn s (iwasawaGnAtLevel F hpi n hn a).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaGnScaledAtLevel_eq_frobenius
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    iwasawaGnScaledAtLevel F hpi n hn s a =
      principalUnitFrobeniusAtLevel F n hn s
        (iwasawaGnAtLevel F hpi n hn a)

theorem

principalUnitLeadingCoefficientAddHom_iwasawaGnScaledAtLevel

L989 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitLeadingCoefficientAddHom_iwasawaGnScaledAtLevel

Documentation

The coefficient congruence: the leading coefficient of g_n(p^s a) is the p^s-th power of the residue-basis combination represented by a.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem principalUnitLeadingCoefficientAddHom_iwasawaGnScaledAtLevel
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    let m := n * F.residueCharacteristic ^ s
    let hm : 1 ≤ m := one_le_mul_residueCharacteristic_pow F hn s
    principalUnitLeadingCoefficientAddHom F hpi m hm
        (Additive.ofMul (iwasawaGnScaledAtLevel F hpi n hn s a)) =
      (∑ i, PadicInt.toZMod (a i) • iwasawaResidueBasis F i) ^
        (F.residueCharacteristic ^ s) := by
  dsimp only
  rw [iwasawaGnScaledAtLevel_eq_frobenius,
    principalUnitLeadingCoefficientAddHom_frobenius,
    principalUnitLeadingCoefficientAddHom_iwasawaGnAtLevel]

theorem

exists_iwasawaGnScaled_mul_mem_succ

L1009 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_iwasawaGnScaled_mul_mem_succ

Documentation

The first coefficient congruence, for m = n*p^s: U^m = g_n(p^s Z_p^f) U^(m+1).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_iwasawaGnScaled_mul_mem_succ
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF))
      (n * F.residueCharacteristic ^ s)) :
    ∃ a : Fin (iwasawaResidueRank F) →
        ℤ_[F.residueCharacteristic],
      (((x / iwasawaGnScaledAtLevel F hpi n hn s a :
          ((higherPrincipalUnitGroup F.toCompleteDVF))
            (n * F.residueCharacteristic ^ s)) : F.valuationSubringˣ) :
        F.valuationSubringˣ) ∈
          ((higherPrincipalUnitGroup F.toCompleteDVF))
            (n * F.residueCharacteristic ^ s + 1)

theorem

iwasawaGnScaled_mem_succ_iff_exists_residueCharacteristic_smul

L1079 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGnScaled_mem_succ_iff_exists_residueCharacteristic_smul

Documentation

Positive form of formula (2): g_n(p^s a) drops into U^(m+1) exactly when every coordinate of a is divisible by p.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaGnScaled_mem_succ_iff_exists_residueCharacteristic_smul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    (((iwasawaGnScaledAtLevel F hpi n hn s a :
        ((higherPrincipalUnitGroup F.toCompleteDVF))
          (n * F.residueCharacteristic ^ s)) : F.valuationSubringˣ) :
      F.valuationSubringˣ) ∈
        ((higherPrincipalUnitGroup F.toCompleteDVF))
          (n * F.residueCharacteristic ^ s + 1) ↔
      ∃ b : Fin (iwasawaResidueRank F) →
          ℤ_[F.residueCharacteristic],
        a = (F.residueCharacteristic : ℤ_[F.residueCharacteristic]) • b

theorem

iwasawa_formula_two

L1136 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawa_formula_two

Documentation

The second coefficient congruence.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawa_formula_two
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (s : ℕ)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    (¬ ∃ b : Fin (iwasawaResidueRank F) →
          ℤ_[F.residueCharacteristic],
        a = (F.residueCharacteristic : ℤ_[F.residueCharacteristic]) • b) ↔
      ¬ (((iwasawaGnScaledAtLevel F hpi n hn s a :
          ((higherPrincipalUnitGroup F.toCompleteDVF))
            (n * F.residueCharacteristic ^ s)) : F.valuationSubringˣ) :
        F.valuationSubringˣ) ∈
          ((higherPrincipalUnitGroup F.toCompleteDVF))
            (n * F.residueCharacteristic ^ s + 1)

theorem

padicInt_eq_zero_of_forall_exists_eq_pow_mul

L1159 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.padicInt_eq_zero_of_forall_exists_eq_pow_mul

Documentation

A p-adic integer divisible by every power of p is zero.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem padicInt_eq_zero_of_forall_exists_eq_pow_mul
    (F : LocalField.{u, v} K) (a : ℤ_[F.residueCharacteristic])
    (h : ∀ r : ℕ, ∃ b : ℤ_[F.residueCharacteristic],
      a = (F.residueCharacteristic : ℤ_[F.residueCharacteristic]) ^ r * b) :
    a = 0

theorem

principalUnit_residueCharacteristic_smul_eq_zero

L1184 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnit_residueCharacteristic_smul_eq_zero

Documentation

Equal-characteristic first principal units have no p-torsion.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem principalUnit_residueCharacteristic_smul_eq_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (x : Additive (((higherPrincipalUnitGroup F.toCompleteDVF)) 1))
    (hx : (F.residueCharacteristic :
        ℤ_[F.residueCharacteristic]) • x = 0) :
    x = 0

theorem

forall_exists_iwasawaGn_eq_pow_smul_of_eq_zero

L1218 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.forall_exists_iwasawaGn_eq_pow_smul_of_eq_zero

Documentation

If g_n(a)=1, then all coordinates of a are divisible by every power of p.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem forall_exists_iwasawaGn_eq_pow_smul_of_eq_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic])
    (ha : iwasawaGn F hpi n hn a = 0) :
    ∀ r : ℕ, ∃ b : Fin (iwasawaResidueRank F) →
        ℤ_[F.residueCharacteristic],
      a = (F.residueCharacteristic ^ r :
        ℤ_[F.residueCharacteristic]) • b

theorem

iwasawaGn_injective

L1276 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGn_injective

Documentation

Every individual Iwasawa map g_n is injective in equal characteristic.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaGn_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) :
    Function.Injective (iwasawaGn F hpi n hn)

def

IwasawaPrimitive

L1302 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.IwasawaPrimitive

Documentation

A vector of p-adic coefficients is primitive when it is not divisible coordinatewise by the residue characteristic.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def IwasawaPrimitive
    (F : LocalField.{u, v} K)
    (a : Fin (iwasawaResidueRank F) →
      ℤ_[F.residueCharacteristic]) : Prop

theorem

exists_pow_smul_iwasawaPrimitive_of_ne_zero

L1314 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_pow_smul_iwasawaPrimitive_of_ne_zero

Documentation

Every nonzero p-adic coefficient block has a unique-depth form p^s b with b primitive. This is the coefficient valuation used in Iwasawa's minimal-depth argument.

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_pow_smul_iwasawaPrimitive_of_ne_zero
    (F : LocalField.{u, v} K)
    (a : Fin (iwasawaResidueRank F) →
      ℤ_[F.residueCharacteristic]) (ha : a ≠ 0) :
    ∃ s : ℕ, ∃ b : Fin (iwasawaResidueRank F) →
        ℤ_[F.residueCharacteristic],
      a = (F.residueCharacteristic ^ s :
          ℤ_[F.residueCharacteristic]) • b ∧
        IwasawaPrimitive F b

theorem

exists_iwasawaGn_mul_mem_succ

L1378 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_iwasawaGn_mul_mem_succ

Documentation

The first coefficient congruence in the base case s = 0: U^n = g_n(Z_p^f) U^(n+1).

Source context 11 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_iwasawaGn_mul_mem_succ
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) n) :
    ∃ a : Fin (iwasawaResidueRank F) →
        ℤ_[F.residueCharacteristic],
      (((x / iwasawaGnAtLevel F hpi n hn a :
          ((higherPrincipalUnitGroup F.toCompleteDVF)) n) : F.valuationSubringˣ) :
        F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) (n + 1)

abbrev

iwasawaDomain

L1458 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDomain

Documentation

The product of one copy of Z_p^f for every positive prime-to-p degree.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

abbrev iwasawaDomain (F : LocalField.{u, v} K)

def

iwasawaBlock

L1463 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaBlock

Documentation

The p-adic coefficient vector belonging to one prime-to-p degree.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaBlock
    (F : LocalField.{u, v} K) (a : iwasawaDomain F)
    (d : IwasawaDegree F.residueCharacteristic) :
    Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]

def

IwasawaDepthWitness

L1470 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.IwasawaDepthWitness

Documentation

A depth occurring in a nonzero Iwasawa coefficient family.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def IwasawaDepthWitness
    (F : LocalField.{u, v} K) (a : iwasawaDomain F) (m : ℕ) : Prop

theorem

exists_minimal_iwasawaDepthWitness_of_ne_zero

L1482 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_minimal_iwasawaDepthWitness_of_ne_zero

Documentation

A nonzero coefficient family has a least depth n*p^s.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_minimal_iwasawaDepthWitness_of_ne_zero
    (F : LocalField.{u, v} K) (a : iwasawaDomain F) (ha : a ≠ 0) :
    ∃ m : ℕ, ∃ d : IwasawaDegree F.residueCharacteristic,
      ∃ s : ℕ, ∃ b : Fin (iwasawaResidueRank F) →
          ℤ_[F.residueCharacteristic],
        iwasawaBlock F a d =
            (F.residueCharacteristic ^ s :
              ℤ_[F.residueCharacteristic]) • b ∧
          IwasawaPrimitive F b ∧
          m = d.1 * F.residueCharacteristic ^ s ∧
          ∀ e : IwasawaDegree F.residueCharacteristic,
            ∀ t : ℕ, ∀ c : Fin (iwasawaResidueRank F) →
                ℤ_[F.residueCharacteristic],
              iwasawaBlock F a e =
                  (F.residueCharacteristic ^ t :
                    ℤ_[F.residueCharacteristic]) • c →
                IwasawaPrimitive F c →
                m ≤ e.1 * F.residueCharacteristic ^ t

def

iwasawaSingleBlock

L1523 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSingleBlock

Documentation

A vector supported in one prime-to-p degree.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaSingleBlock
    (F : LocalField.{u, v} K)
    (d : IwasawaDegree F.residueCharacteristic)
    (b : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    iwasawaDomain F

theorem

iwasawaSingleBlock_apply_same

L1532 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSingleBlock_apply_same

Documentation

Establishes the identity iwasawaSingleBlock F d b (d, i) = b i.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaSingleBlock_apply_same
    (F : LocalField.{u, v} K)
    (d : IwasawaDegree F.residueCharacteristic)
    (b : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic])
    (i : Fin (iwasawaResidueRank F)) :
    iwasawaSingleBlock F d b (d, i) = b i

theorem

iwasawaSingleBlock_apply_ne

L1542 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaSingleBlock_apply_ne

Documentation

Establishes the identity iwasawaSingleBlock F d b (e, i) = 0.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaSingleBlock_apply_ne
    (F : LocalField.{u, v} K)
    {d e : IwasawaDegree F.residueCharacteristic} (hde : e ≠ d)
    (b : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic])
    (i : Fin (iwasawaResidueRank F)) :
    iwasawaSingleBlock F d b (e, i) = 0

def

iwasawaPrimeToPPart

L1552 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaPrimeToPPart

Documentation

Remove the largest residue-characteristic power from a positive depth.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaPrimeToPPart (F : LocalField.{u, v} K) (m : ℕ) : ℕ

theorem

iwasawaPrimeToPPart_spec

L1557 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaPrimeToPPart_spec

Documentation

Every positive depth has the canonical form m = n*p^s, with n positive and prime to p.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaPrimeToPPart_spec
    (F : LocalField.{u, v} K) {m : ℕ} (hm : 1 ≤ m) :
    1 ≤ iwasawaPrimeToPPart F m ∧
      Nat.Coprime (iwasawaPrimeToPPart F m) F.residueCharacteristic ∧
      iwasawaPrimeToPPart F m *
          F.residueCharacteristic ^ padicValNat F.residueCharacteristic m = m

theorem

iwasawaDepth_eq_iff

L1590 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDepth_eq_iff

Documentation

The depths n*p^s attached to distinct prime-to-p factors are distinct. This is the uniqueness assertion used in Iwasawa's injectivity coefficient-lifting argument.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDepth_eq_iff
    (F : LocalField.{u, v} K)
    (d e : IwasawaDegree F.residueCharacteristic) (s t : ℕ) :
    d.1 * F.residueCharacteristic ^ s =
        e.1 * F.residueCharacteristic ^ t ↔
      d = e ∧ s = t

def

iwasawaDegreeTerm

L1628 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm

Documentation

The n-th factor in Iwasawa's infinite product. It is 1 when n is zero or is divisible by p; this lets finite partial products be indexed by ordinary ranges without making any choice of an enumeration.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaDegreeTerm
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (n : ℕ) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) 1

theorem

iwasawaDegreeTerm_eq_iwasawaGnScaled

L1642 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm_eq_iwasawaGnScaled

Documentation

A coefficient block p^s b gives exactly the scaled factor occurring at depth n*p^s.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDegreeTerm_eq_iwasawaGnScaled
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F)
    (d : IwasawaDegree F.residueCharacteristic) (s : ℕ)
    (b : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic])
    (hab : iwasawaBlock F a d =
      (F.residueCharacteristic ^ s :
        ℤ_[F.residueCharacteristic]) • b) :
    ((iwasawaDegreeTerm F hpi a d.1 :
        ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) =
      ((iwasawaGnScaledAtLevel F hpi d.1 d.property.1 s b :
        ((higherPrincipalUnitGroup F.toCompleteDVF))
          (d.1 * F.residueCharacteristic ^ s)) : F.valuationSubringˣ)

theorem

iwasawaDegreeTerm_mem_higher

L1679 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm_mem_higher

Documentation

Establishes the membership statement ((iwasawaDegreeTerm F hpi a n : ((CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) ∈ ((CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF)) n.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDegreeTerm_mem_higher
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (n : ℕ) :
    ((iwasawaDegreeTerm F hpi a n : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) :
      F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) n

theorem

iwasawaDegreeTerm_zero

L1694 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm_zero

Documentation

Establishes the identity iwasawaDegreeTerm F hpi (0 : iwasawaDomain F) n = 1.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDegreeTerm_zero
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    iwasawaDegreeTerm F hpi (0 : iwasawaDomain F) n = 1

theorem

iwasawaDegreeTerm_add

L1713 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm_add

Documentation

iwasawaDegreeTerm satisfies the addition formula iwasawaDegreeTerm F hpi (a + b) n = iwasawaDegreeTerm F hpi a n * iwasawaDegreeTerm F hpi b n.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDegreeTerm_add
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a b : iwasawaDomain F) (n : ℕ) :
    iwasawaDegreeTerm F hpi (a + b) n =
      iwasawaDegreeTerm F hpi a n * iwasawaDegreeTerm F hpi b n

def

iwasawaPartialProduct

L1734 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaPartialProduct

Documentation

The product of the Iwasawa factors of degree at most r.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaPartialProduct
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (r : ℕ) :
    ((higherPrincipalUnitGroup F.toCompleteDVF)) 1

theorem

iwasawaPartialProduct_singleBlock

L1744 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaPartialProduct_singleBlock

Documentation

A single-block domain element contributes precisely its one g_n factor to every sufficiently deep partial product.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaPartialProduct_singleBlock
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (d : IwasawaDegree F.residueCharacteristic)
    (b : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic])
    {r : ℕ} (hdr : d.1 ≤ r) :
    iwasawaPartialProduct F hpi (iwasawaSingleBlock F d b) r =
      Additive.toMul (iwasawaGn F hpi d.1 d.property.1 b)

theorem

iwasawaPartialProduct_zero_input

L1793 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaPartialProduct_zero_input

Documentation

Establishes the identity iwasawaPartialProduct F hpi (0 : iwasawaDomain F) r = 1.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaPartialProduct_zero_input
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (r : ℕ) :
    iwasawaPartialProduct F hpi (0 : iwasawaDomain F) r = 1

theorem

iwasawaPartialProduct_add

L1805 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaPartialProduct_add

Documentation

iwasawaPartialProduct satisfies the addition formula iwasawaPartialProduct F hpi (a + b) r = iwasawaPartialProduct F hpi a r * iwasawaPartialProduct F hpi b r.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaPartialProduct_add
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a b : iwasawaDomain F) (r : ℕ) :
    iwasawaPartialProduct F hpi (a + b) r =
      iwasawaPartialProduct F hpi a r *
        iwasawaPartialProduct F hpi b r

theorem

iwasawaDegreeTerm_eq_one_of_block_eq_zero

L1818 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm_eq_one_of_block_eq_zero

Documentation

Establishes the identity iwasawaDegreeTerm F hpi a n = 1.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDegreeTerm_eq_one_of_block_eq_zero
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (n : ℕ)
    (ha : ∀ hn : 1 ≤ n ∧ Nat.Coprime n F.residueCharacteristic,
      ∀ i : Fin (iwasawaResidueRank F), a (⟨n, hn⟩, i) = 0) :
    iwasawaDegreeTerm F hpi a n = 1

theorem

iwasawaPartialProduct_succ

L1841 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaPartialProduct_succ

Documentation

Expanding the cutoff by one only adds the factor whose degree is the new cutoff.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaPartialProduct_succ
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (r : ℕ) :
    iwasawaPartialProduct F hpi a (r + 1) =
      iwasawaPartialProduct F hpi a r *
        iwasawaDegreeTerm F hpi a (r + 1)

theorem

exists_iwasawaPartialProduct_div_mem_higher

L1860 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_iwasawaPartialProduct_div_mem_higher

Documentation

The finite approximation implicit in formula (1): every first principal unit is represented modulo U^(r+1) by the product of the Iwasawa factors of degree at most r. The support condition records the inductive coefficient construction.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_iwasawaPartialProduct_div_mem_higher
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (x : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) (r : ℕ) :
    ∃ a : iwasawaDomain F,
      (∀ j, r < j.1.1 → a j = 0) ∧
      (((x / iwasawaPartialProduct F hpi a r :
          ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) :
        F.valuationSubringˣ) ∈ ((higherPrincipalUnitGroup F.toCompleteDVF)) (r + 1)

theorem

principalUnitQuotientCarrier_mk_iwasawaPartialProduct_eq_of_le

L1969 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrier_mk_iwasawaPartialProduct_eq_of_le

Documentation

Higher-degree factors disappear in every fixed finite quotient. Thus the partial products define a compatible family; this is the formal convergence argument for the infinite product.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.principalUnitQuotientCarrier_mk_iwasawaPartialProduct_eq_of_le
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) {m r : ℕ} (hmr : m ≤ r) :
    (higherPrincipalUnitGroup.toPrincipalUnitFiltration
        F.toCompleteDVF).principalUnitSubquotientMk
          1 (m + 1) (iwasawaPartialProduct F hpi a r) =
      (higherPrincipalUnitGroup.toPrincipalUnitFiltration
        F.toCompleteDVF).principalUnitSubquotientMk
          1 (m + 1) (iwasawaPartialProduct F hpi a m)

def

iwasawaGlobalInverseLimitCarrier

L2015 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.iwasawaGlobalInverseLimitCarrier

Documentation

The compatible family of all finite Iwasawa partial products.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def Internal.iwasawaGlobalInverseLimitCarrier
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) :
    Internal.principalUnitInverseLimitCarrier F.toCompleteDVF

theorem

iwasawaGlobalInverseLimitCarrier_apply

L2037 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.iwasawaGlobalInverseLimitCarrier_apply

Documentation

The defining evaluation formula for Internal.iwasawaGlobalInverseLimitCarrier is (iwasawaGlobalInverseLimitCarrier F hpi a).1 r = (higherPrincipalUnitGroup.toPrincipalUnitFiltration F.toCompleteDVF).principalUnitSubquotientMk 1 (r + 1) (iwasawaPartialProduct F hpi a r).

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.iwasawaGlobalInverseLimitCarrier_apply
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (r : ℕ) :
    (iwasawaGlobalInverseLimitCarrier F hpi a).1 r =
      (higherPrincipalUnitGroup.toPrincipalUnitFiltration
        F.toCompleteDVF).principalUnitSubquotientMk
          1 (r + 1) (iwasawaPartialProduct F hpi a r)

theorem

surjective_iwasawaGlobalInverseLimitCarrier_coordinate

L2051 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.surjective_iwasawaGlobalInverseLimitCarrier_coordinate

Documentation

Every finite coordinate of the Iwasawa product is onto. This is the finite-quotient consequence of formula (1) used in the compactness argument in the coefficient calculation.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem Internal.surjective_iwasawaGlobalInverseLimitCarrier_coordinate
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (r : ℕ) :
    Function.Surjective (fun a : iwasawaDomain F =>
      (iwasawaGlobalInverseLimitCarrier F hpi a).1 r) := by
  intro q
  obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective
    ((((higherPrincipalUnitGroup F.toCompleteDVF)) (r + 1)).subgroupOf
      (((higherPrincipalUnitGroup F.toCompleteDVF)) 1)) q
  obtain ⟨a, _haSupport, ha⟩ :=
    exists_iwasawaPartialProduct_div_mem_higher F hpi x r
  refine ⟨a, ?_⟩
  change
    (QuotientGroup.mk (iwasawaPartialProduct F hpi a r) :
        Internal.principalUnitQuotientCarrier F.toCompleteDVF r) =
      QuotientGroup.mk x
  symm
  let U := toPrincipalUnitFiltration F.toCompleteDVF
  exact (U.principalUnitSubquotient_mk_eq_iff_div_mem x
    (iwasawaPartialProduct F hpi a r)).2 ha

def

adicIwasawaGn

L2075 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicIwasawaGn

Documentation

One Iwasawa factor valued in the type-level adic principal-unit model.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def adicIwasawaGn
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n)
    (a : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic]) :
    AdicPrincipalUnits F.toCompleteDVF

def

adicIwasawaDegreeTerm

L2085 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicIwasawaDegreeTerm

Documentation

One degree term valued in the type-level adic principal-unit model.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def adicIwasawaDegreeTerm
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (n : ℕ) :
    AdicPrincipalUnits F.toCompleteDVF

def

adicIwasawaPartialProduct

L2096 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicIwasawaPartialProduct

Documentation

A finite Iwasawa partial product valued in the type-level adic principal-unit model.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def adicIwasawaPartialProduct
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (r : ℕ) :
    AdicPrincipalUnits F.toCompleteDVF

theorem

continuous_adicIwasawaGn

L2107 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuous_adicIwasawaGn

Documentation

Continuity of one Iwasawa factor; the adic topology is carried by the codomain type.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem continuous_adicIwasawaGn
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) :
    Continuous (adicIwasawaGn F hpi n hn)

theorem

continuous_adicIwasawaDegreeTerm

L2139 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuous_adicIwasawaDegreeTerm

Documentation

The specified map is continuous: Continuous fun a : iwasawaDomain F => adicIwasawaDegreeTerm F hpi a n.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem continuous_adicIwasawaDegreeTerm
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (n : ℕ) :
    Continuous fun a : iwasawaDomain F =>
      adicIwasawaDegreeTerm F hpi a n := by
  classical
  by_cases hn : 1 ≤ n ∧ Nat.Coprime n F.residueCharacteristic
  · have hcoordinates : Continuous fun a : iwasawaDomain F =>
        (fun i => a (⟨n, hn⟩, i)) := by
      exact continuous_pi fun i => continuous_apply
        ((⟨n, hn⟩ : IwasawaDegree F.residueCharacteristic), i)
    have hcont :=
      (continuous_adicIwasawaGn F hpi n hn.1).comp hcoordinates
    apply hcont.congr
    intro a
    simp only [Function.comp_apply, adicIwasawaDegreeTerm,
      iwasawaDegreeTerm, dite_eq_left hn, adicIwasawaGn, ofMul_toMul]
  · simpa only [adicIwasawaDegreeTerm, iwasawaDegreeTerm, dite_eq_right hn,
      ofMul_one] using
      (continuous_const : Continuous fun _ : iwasawaDomain F =>
        AdicPrincipalUnits.of F.toCompleteDVF 0)

theorem

continuous_adicIwasawaPartialProduct

L2166 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuous_adicIwasawaPartialProduct

Documentation

The specified map is continuous: Continuous fun a : iwasawaDomain F => adicIwasawaPartialProduct F hpi a r.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem continuous_adicIwasawaPartialProduct
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (r : ℕ) :
    Continuous fun a : iwasawaDomain F =>
      adicIwasawaPartialProduct F hpi a r := by
  unfold adicIwasawaPartialProduct iwasawaPartialProduct
  classical
  induction Finset.range (r + 1) using Finset.induction_on with
  | empty =>
      simpa only [Finset.prod_empty, ofMul_one] using
        (continuous_const : Continuous fun _ : iwasawaDomain F =>
          AdicPrincipalUnits.of F.toCompleteDVF 0)
  | @insert n s hns ih =>
      simp only [Finset.prod_insert hns]
      have hcont := (continuous_adicIwasawaDegreeTerm F hpi n).add ih
      apply hcont.congr
      intro a
      apply (AdicPrincipalUnits.addEquiv F.toCompleteDVF).injective
      change
        Additive.ofMul (iwasawaDegreeTerm F hpi a n) +
            Additive.ofMul
              (∏ k ∈ s, iwasawaDegreeTerm F hpi a k) =
          Additive.ofMul
            (iwasawaDegreeTerm F hpi a n *
              ∏ k ∈ s, iwasawaDegreeTerm F hpi a k)
      rw [ofMul_mul]

theorem

continuous_iwasawaPartialProduct

L2196 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.continuous_iwasawaPartialProduct

Documentation

Internal bridge from the type-level adic partial product to the raw carrier used by the algebraic inverse-limit construction.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem Internal.continuous_iwasawaPartialProduct
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) (r : ℕ) :
    letI : TopologicalSpace F.valuationSubring :=
      (LubinTate.Valuations.uniformizerPowerIdeal
        (chosenPrincipalUnitPadicUniformizer F.toCompleteDVF) 1).adicTopology
    Continuous fun a : iwasawaDomain F =>
      iwasawaPartialProduct F hpi a r := by
  let : TopologicalSpace F.valuationSubring :=
    (LubinTate.Valuations.uniformizerPowerIdeal
      (chosenPrincipalUnitPadicUniformizer F.toCompleteDVF) 1).adicTopology
  let e := Internal.adicPrincipalUnitsHomeomorphUnderlying F.toCompleteDVF
  have h := e.continuous.comp
    (continuous_adicIwasawaPartialProduct F hpi r)
  exact h

theorem

continuous_iwasawaGlobalInverseLimitCarrier

L2215 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.continuous_iwasawaGlobalInverseLimitCarrier

Documentation

Continuity of the compatible finite products. The target has the product topology of the discrete finite principal-unit quotients.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

theorem Internal.continuous_iwasawaGlobalInverseLimitCarrier
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    letI : (n : ℕ) → TopologicalSpace
        (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := fun _ => ⊥
    Continuous (iwasawaGlobalInverseLimitCarrier F hpi) := by
  let : TopologicalSpace F.valuationSubring :=
    (LubinTate.Valuations.uniformizerPowerIdeal
      (chosenPrincipalUnitPadicUniformizer F.toCompleteDVF) 1).adicTopology
  let : (n : ℕ) → TopologicalSpace
      (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := fun _ => ⊥
  let E := Internal.principalUnitHomeomorphInverseLimitCarrier F.toCompleteDVF
  exact Continuous.subtype_mk
    (continuous_pi fun r => by
      have hcoord : Continuous fun x : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1 =>
          (E x).1 r :=
        ((continuous_apply r).comp continuous_subtype_val).comp E.continuous
      change Continuous fun x : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1 =>
        Internal.principalUnitInverseLimitCarrierEval F.toCompleteDVF r
          (Internal.principalUnitMulEquivInverseLimitCarrier
            F.toCompleteDVF x) at hcoord
      have hquot : Continuous fun x : ((higherPrincipalUnitGroup F.toCompleteDVF)) 1 =>
          (higherPrincipalUnitGroup.toPrincipalUnitFiltration
            F.toCompleteDVF).principalUnitSubquotientMk 1 (r + 1) x := by
        simpa only [principalUnitMulEquivInverseLimitCarrier_apply] using hcoord
      exact hquot.comp (Internal.continuous_iwasawaPartialProduct F hpi r))
    (fun a => by
      intro m r hmr
      exact (iwasawaGlobalInverseLimitCarrier F hpi a).property hmr)

def

iwasawaGlobalInverseLimitCarrierAddHom

L2248 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.iwasawaGlobalInverseLimitCarrierAddHom

Documentation

Additive-homomorphism form of the infinite product in the inverse limit.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · full declaration

def Internal.iwasawaGlobalInverseLimitCarrierAddHom
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    iwasawaDomain F →+
      Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF) where
  toFun a := Additive.ofMul (iwasawaGlobalInverseLimitCarrier F hpi a)
  map_zero' := by
    apply Additive.toMul.injective
    apply Subtype.ext
    funext r
    change
      (higherPrincipalUnitGroup.toPrincipalUnitFiltration
        F.toCompleteDVF).principalUnitSubquotientMk 1 (r + 1)
          (iwasawaPartialProduct F hpi (0 : iwasawaDomain F) r) =
        (1 : Internal.principalUnitQuotientCarrier F.toCompleteDVF r)
    rw [iwasawaPartialProduct_zero_input]
    exact map_one _
  map_add' a b := by
    apply Additive.toMul.injective
    apply Subtype.ext
    funext r
    change
      (QuotientGroup.mk (iwasawaPartialProduct F hpi (a + b) r) :
        Internal.principalUnitQuotientCarrier F.toCompleteDVF r) =
      (QuotientGroup.mk (iwasawaPartialProduct F hpi a r) :
          Internal.principalUnitQuotientCarrier F.toCompleteDVF r) *
        (QuotientGroup.mk (iwasawaPartialProduct F hpi b r) :
          Internal.principalUnitQuotientCarrier F.toCompleteDVF r)
    rw [iwasawaPartialProduct_add]
    exact map_mul
      (QuotientGroup.mk'
        ((((higherPrincipalUnitGroup F.toCompleteDVF)) (r + 1)).subgroupOf
          (((higherPrincipalUnitGroup F.toCompleteDVF)) 1))) _ _

def

iwasawaGlobalProdiscreteLimitAddHom

L2285 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGlobalProdiscreteLimitAddHom

Documentation

The Iwasawa compatible family valued in its type-level prodiscrete model. For a local field all coordinate quotients are finite.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaGlobalProdiscreteLimitAddHom
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    iwasawaDomain F →+
      PrincipalUnitProdiscreteLimit F.toCompleteDVF

theorem

continuous_iwasawaGlobalProdiscreteLimitAddHom

L2295 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.continuous_iwasawaGlobalProdiscreteLimitAddHom

Documentation

The specified map is continuous: Continuous (iwasawaGlobalProdiscreteLimitAddHom F hpi).

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.continuous_iwasawaGlobalProdiscreteLimitAddHom
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    Continuous (iwasawaGlobalProdiscreteLimitAddHom F hpi)

theorem

continuous_iwasawaGlobalProdiscreteLimitAddHom

L2310 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuous_iwasawaGlobalProdiscreteLimitAddHom

Documentation

Continuity of the Iwasawa compatible family; discreteness of every finite coordinate is encoded by the codomain type.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem continuous_iwasawaGlobalProdiscreteLimitAddHom
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    Continuous (iwasawaGlobalProdiscreteLimitAddHom F hpi)

theorem

surjective_iwasawaGlobalProdiscreteLimitAddHom

L2319 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.surjective_iwasawaGlobalProdiscreteLimitAddHom

Documentation

Compactness upgrades formula (1), already proved on every finite coordinate, to surjectivity of the complete Iwasawa product.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem surjective_iwasawaGlobalProdiscreteLimitAddHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    Function.Surjective (iwasawaGlobalProdiscreteLimitAddHom F hpi)

theorem

surjective_iwasawaGlobalInverseLimitCarrierAddHom

L2341 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.surjective_iwasawaGlobalInverseLimitCarrierAddHom

Documentation

The specified map is surjective: Function.Surjective (iwasawaGlobalInverseLimitCarrierAddHom F hpi).

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.surjective_iwasawaGlobalInverseLimitCarrierAddHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    Function.Surjective (iwasawaGlobalInverseLimitCarrierAddHom F hpi)

def

iwasawaGlobalAddHom

L2352 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.iwasawaGlobalAddHom

Documentation

Iwasawa's product homomorphism g : A -> U^1, obtained from its compatible finite quotients via the adic inverse-limit isomorphism.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def Internal.iwasawaGlobalAddHom
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    iwasawaDomain F →+
      Additive (((higherPrincipalUnitGroup F.toCompleteDVF)) 1)

theorem

surjective_iwasawaGlobalAddHom

L2362 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.surjective_iwasawaGlobalAddHom

Documentation

The specified map is surjective: Function.Surjective (iwasawaGlobalAddHom F hpi).

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.surjective_iwasawaGlobalAddHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    Function.Surjective (iwasawaGlobalAddHom F hpi)

theorem

principalUnitAddEquivInverseLimitCarrier_iwasawaGlobalAddHom

L2377 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitAddEquivInverseLimitCarrier_iwasawaGlobalAddHom

Documentation

Establishes the identity principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF (iwasawaGlobalAddHom F hpi a) = Additive.ofMul (iwasawaGlobalInverseLimitCarrier F hpi a).

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.principalUnitAddEquivInverseLimitCarrier_iwasawaGlobalAddHom
    (F : LocalField.{u, v} K)
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) :
    principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF
        (iwasawaGlobalAddHom F hpi a) =
      Additive.ofMul (iwasawaGlobalInverseLimitCarrier F hpi a)

theorem

iwasawaDegreeTerm_mem_succ_of_ne_minimal

L2390 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm_mem_succ_of_ne_minimal

Documentation

Every factor distinct from a chosen least-depth factor vanishes in the next finite quotient.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDegreeTerm_mem_succ_of_ne_minimal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (m : ℕ)
    (d : IwasawaDegree F.residueCharacteristic) (s : ℕ)
    (hm : m = d.1 * F.residueCharacteristic ^ s)
    (hmin : ∀ e : IwasawaDegree F.residueCharacteristic,
      ∀ t : ℕ, ∀ c : Fin (iwasawaResidueRank F) →
          ℤ_[F.residueCharacteristic],
        iwasawaBlock F a e =
            (F.residueCharacteristic ^ t :
              ℤ_[F.residueCharacteristic]) • c →
          IwasawaPrimitive F c →
          m ≤ e.1 * F.residueCharacteristic ^ t)
    (k : ℕ)
    (hk : 1 ≤ k ∧ Nat.Coprime k F.residueCharacteristic)
    (hkd : k ≠ d.1) :
    ((iwasawaDegreeTerm F hpi a k :
        ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) ∈
      ((higherPrincipalUnitGroup F.toCompleteDVF)) (m + 1)

theorem

iwasawaDegreeTerm_not_mem_succ_of_primitive

L2462 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaDegreeTerm_not_mem_succ_of_primitive

Documentation

The chosen primitive least-depth factor survives in the next quotient; this is the second coefficient congruence.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem iwasawaDegreeTerm_not_mem_succ_of_primitive
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (m : ℕ)
    (d : IwasawaDegree F.residueCharacteristic) (s : ℕ)
    (b : Fin (iwasawaResidueRank F) → ℤ_[F.residueCharacteristic])
    (hab : iwasawaBlock F a d =
      (F.residueCharacteristic ^ s :
        ℤ_[F.residueCharacteristic]) • b)
    (hb : IwasawaPrimitive F b)
    (hm : m = d.1 * F.residueCharacteristic ^ s) :
    ¬ (((iwasawaDegreeTerm F hpi a d.1 :
          ((higherPrincipalUnitGroup F.toCompleteDVF)) 1) : F.valuationSubringˣ) ∈
        ((higherPrincipalUnitGroup F.toCompleteDVF)) (m + 1))

theorem

iwasawaGlobalInverseLimitCarrierAddHom_ne_zero_of_ne_zero

L2489 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.iwasawaGlobalInverseLimitCarrierAddHom_ne_zero_of_ne_zero

Documentation

A nonzero coefficient family has nonzero image in the inverse limit. The least depth supplied above is detected in its m-th coordinate.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.iwasawaGlobalInverseLimitCarrierAddHom_ne_zero_of_ne_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : iwasawaDomain F) (ha : a ≠ 0) :
    iwasawaGlobalInverseLimitCarrierAddHom F hpi a ≠ 0

theorem

injective_iwasawaGlobalInverseLimitCarrierAddHom

L2563 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.injective_iwasawaGlobalInverseLimitCarrierAddHom

Documentation

The specified map is injective: Function.Injective (iwasawaGlobalInverseLimitCarrierAddHom F hpi).

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem Internal.injective_iwasawaGlobalInverseLimitCarrierAddHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    Function.Injective (iwasawaGlobalInverseLimitCarrierAddHom F hpi)

theorem

injective_iwasawaGlobalProdiscreteLimitAddHom

L2582 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.injective_iwasawaGlobalProdiscreteLimitAddHom

Documentation

The specified map is injective: Function.Injective (iwasawaGlobalProdiscreteLimitAddHom F hpi).

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

theorem injective_iwasawaGlobalProdiscreteLimitAddHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    Function.Injective (iwasawaGlobalProdiscreteLimitAddHom F hpi)

def

iwasawaGlobalProdiscreteLimitAddEquiv

L2601 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGlobalProdiscreteLimitAddEquiv

Documentation

The equal-characteristic Iwasawa isomorphism, with the prodiscrete topology fixed in its codomain type. In the local-field case this topology is profinite.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaGlobalProdiscreteLimitAddEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    iwasawaDomain F ≃+ PrincipalUnitProdiscreteLimit F.toCompleteDVF

def

iwasawaGlobalProdiscreteLimitContinuousAddEquiv

L2613 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGlobalProdiscreteLimitContinuousAddEquiv

Documentation

The Iwasawa product is a homeomorphism onto the type-level prodiscrete principal-unit limit.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaGlobalProdiscreteLimitContinuousAddEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    iwasawaDomain F ≃ₜ+ PrincipalUnitProdiscreteLimit F.toCompleteDVF

def

iwasawaGlobalAdicPrincipalUnitsContinuousAddEquiv

L2627 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.iwasawaGlobalAdicPrincipalUnitsContinuousAddEquiv

Documentation

Topological form of the equal-characteristic Iwasawa isomorphism. The adic topology is part of the codomain type.

Source context 15 commands

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

noncomputable section
open scoped BigOperators
universe u v
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
noncomputable section
open scoped BigOperators
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
namespace higherPrincipalUnitGroup
open LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
open Internal
variable {K : Type u} [Field K]

Lean source · statement

def iwasawaGlobalAdicPrincipalUnitsContinuousAddEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    iwasawaDomain F ≃ₜ+ AdicPrincipalUnits F.toCompleteDVF

Module documentation

The convergent Iwasawa product for principal units

Finite-level Iwasawa generators for principal units

Reduction of p-adic exponents on one graded layer

Algebraic injectivity of each Iwasawa factor

The convergent product, constructed through finite quotients

Declarations