Module

CompletedUnramifiedField.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedUnramifiedField

20 declarations indexed from sourceView source ↗

Module documentation

The p-adic completed-unramified coefficient field

The coefficient ring used by the mixed-characteristic changed-uniformizer construction is

W(AlgebraicClosure (ZMod p)).

Its fraction field is the completed maximal-unramified coefficient field. This file equips that existing mathlib fraction field with its canonical ℚ_[p]-algebra structure. Mathlib's fraction-field Frobenius then becomes an actual ℚ_[p]-algebra automorphism. No second Witt ring, p-adic field, or Frobenius is introduced.

Imports4

Imported by4

abbrev

padicCompletedUnramifiedField

L40 ↗

LubinTate.padicCompletedUnramifiedField

Documentation

The fraction field of the completed-unramified Witt integer ring.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

abbrev padicCompletedUnramifiedField (p : ℕ) [Fact p.Prime]

theorem

padicCompletedUnramifiedWittRing_maximalIdeal

L45 ↗

LubinTate.padicCompletedUnramifiedWittRing_maximalIdeal

Documentation

The maximal ideal of the completed-unramified Witt integer ring is generated by the canonical prime p.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedWittRing_maximalIdeal
    (p : ℕ) [Fact p.Prime] :
    IsLocalRing.maximalIdeal (padicCompletedUnramifiedWittRing p) =
      Ideal.span
        ({(p : padicCompletedUnramifiedWittRing p)} : Set
          (padicCompletedUnramifiedWittRing p))

abbrev

padicCompletedUnramifiedValuation

L61 ↗

LubinTate.padicCompletedUnramifiedValuation

Documentation

The canonical DVR valuation on the fraction field of the completed-unramified Witt integer ring.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

abbrev padicCompletedUnramifiedValuation
    (p : ℕ) [Fact p.Prime] :
    Valuation (padicCompletedUnramifiedField p) ℤᵐ⁰

instance

padicCompletedUnramifiedFieldValued

L70 ↗

LubinTate.padicCompletedUnramifiedFieldValued

Documentation

The valued-field structure induced by the canonical Witt DVR valuation.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

instance padicCompletedUnramifiedFieldValued
    (p : ℕ) [Fact p.Prime] :
    Valued (padicCompletedUnramifiedField p) ℤᵐ⁰

def

padicCompletedUnramifiedWittRingEquivValuationSubring

L77 ↗

LubinTate.padicCompletedUnramifiedWittRingEquivValuationSubring

Documentation

The original Witt integer ring is the valuation ring of its fraction field with the canonical DVR valuation.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

def
    padicCompletedUnramifiedWittRingEquivValuationSubring
    (p : ℕ) [Fact p.Prime] :
    padicCompletedUnramifiedWittRing p ≃+*
      (padicCompletedUnramifiedValuation p).valuationSubring

theorem

padicCompletedUnramifiedValuation_isAdicComplete

L90 ↗

LubinTate.padicCompletedUnramifiedValuation_isAdicComplete

Documentation

The valuation ring of the completed-unramified coefficient field is complete for its maximal-ideal adic topology. This transports mathlib's p-adic completeness of Witt vectors across the canonical valuation-ring equivalence.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedValuation_isAdicComplete
    (p : ℕ) [Fact p.Prime] :
    IsAdicComplete
      (IsLocalRing.maximalIdeal
        (padicCompletedUnramifiedValuation p).valuationSubring)
      (padicCompletedUnramifiedValuation p).valuationSubring

def

padicCompletedUnramifiedCompleteDVF

L141 ↗

LubinTate.padicCompletedUnramifiedCompleteDVF

Documentation

The completed-unramified Witt fraction field, packaged with its actual complete rank-one discrete valuation.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · full declaration

def padicCompletedUnramifiedCompleteDVF
    (p : ℕ) [Fact p.Prime] :
    CompleteDVF (padicCompletedUnramifiedField p) where
  ValueGroup := ℤᵐ⁰
  valuation := padicCompletedUnramifiedValuation p
  instCompleteDiscrete :=
    { isRankOneDiscrete := inferInstance
      isAdicComplete :=
        padicCompletedUnramifiedValuation_isAdicComplete p }

theorem

padicCompletedUnramifiedWittRing_intValuation_frobenius

L151 ↗

LubinTate.padicCompletedUnramifiedWittRing_intValuation_frobenius

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem
    padicCompletedUnramifiedWittRing_intValuation_frobenius
    (p : ℕ) [Fact p.Prime]
    (x : padicCompletedUnramifiedWittRing p) :
    (IsDiscreteValuationRing.maximalIdeal
        (padicCompletedUnramifiedWittRing p)).intValuation
        (WittVector.frobenius x) =
      (IsDiscreteValuationRing.maximalIdeal
        (padicCompletedUnramifiedWittRing p)).intValuation x

theorem

padicIntToCompletedUnramifiedWittRing_injective

L208 ↗

LubinTate.padicIntToCompletedUnramifiedWittRing_injective

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicIntToCompletedUnramifiedWittRing_injective
    (p : ℕ) [Fact p.Prime] :
    Function.Injective (padicIntToCompletedUnramifiedWittRing p)

instance

padicCompletedUnramifiedFieldAlgebra

L219 ↗

LubinTate.padicCompletedUnramifiedFieldAlgebra

Documentation

The canonical ℚ_[p]-algebra structure obtained by extending ℤ_[p] → W(AlgebraicClosure (ZMod p)) to fraction fields.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

instance padicCompletedUnramifiedFieldAlgebra
    (p : ℕ) [Fact p.Prime] :
    Algebra ℚ_[p] (padicCompletedUnramifiedField p)

theorem

padicCompletedUnramifiedField_algebraMap_padicInt

L236 ↗

LubinTate.padicCompletedUnramifiedField_algebraMap_padicInt

Documentation

The canonical field embedding agrees with the original Witt-ring map on p-adic integers.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedField_algebraMap_padicInt
    (p : ℕ) [Fact p.Prime] (z : ℤ_[p]) :
    algebraMap ℚ_[p] (padicCompletedUnramifiedField p)
        (algebraMap ℤ_[p] ℚ_[p] z) =
      algebraMap (padicCompletedUnramifiedWittRing p)
        (padicCompletedUnramifiedField p)
        (padicIntToCompletedUnramifiedWittRing p z)

def

padicCompletedUnramifiedIntegerMap

L248 ↗

LubinTate.padicCompletedUnramifiedIntegerMap

Documentation

The canonical map from the valuation ring of ℚ_[p] into the valuation ring of the completed-unramified field.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

def padicCompletedUnramifiedIntegerMap
    (p : ℕ) [Fact p.Prime] :
    (padicLocalField p).valuationSubring →+*
      (padicCompletedUnramifiedCompleteDVF p).valuationSubring

theorem

padicCompletedUnramifiedIntegerMap_coe

L258 ↗

LubinTate.padicCompletedUnramifiedIntegerMap_coe

Documentation

After coercion to fraction fields, the completed-unramified integer map is the canonical ℚ_[p]-algebra map.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedIntegerMap_coe
    (p : ℕ) [Fact p.Prime]
    (z : (padicLocalField p).valuationSubring) :
    ((padicCompletedUnramifiedIntegerMap p z :
        (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
      padicCompletedUnramifiedField p) =
      algebraMap ℚ_[p] (padicCompletedUnramifiedField p) (z : ℚ_[p])

theorem

padicCompletedUnramifiedIntegerMap_map_maximalIdeal

L298 ↗

LubinTate.padicCompletedUnramifiedIntegerMap_map_maximalIdeal

Documentation

The canonical integer map identifies the maximal ideal of ℚ_[p] with the maximal ideal of the completed-unramified valuation ring.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedIntegerMap_map_maximalIdeal
    (p : ℕ) [Fact p.Prime] :
    Ideal.map (padicCompletedUnramifiedIntegerMap p)
        (padicLocalField p).maximalIdeal =
      (padicCompletedUnramifiedCompleteDVF p).maximalIdeal

theorem

padicCompletedUnramifiedValuation_hasExtension

L368 ↗

LubinTate.padicCompletedUnramifiedValuation_hasExtension

Documentation

The canonical valuation on the completed-unramified coefficient field extends the p-adic valuation. This is obtained from the actual local map of valuation rings, rather than postulated as part of the completed field structure.

Source context 8 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero
open _root_.ValuationTheory.DiscreteValuationField.ValuedExtension (
  valuation_hasExtension_of_local_valuationSubring_map
) in

Lean source · statement

theorem padicCompletedUnramifiedValuation_hasExtension
    (p : ℕ) [Fact p.Prime] :
    (padicLocalField p).toCompleteDVF.valuation.HasExtension
      (padicCompletedUnramifiedCompleteDVF p).valuation

instance

padicCompletedUnramifiedValuation_hasExtensionInstance

L385 ↗

LubinTate.padicCompletedUnramifiedValuation_hasExtensionInstance

Documentation

Typeclass form of padicCompletedUnramifiedValuation_hasExtension.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

instance
    padicCompletedUnramifiedValuation_hasExtensionInstance
    (p : ℕ) [Fact p.Prime] :
    (padicLocalField p).toCompleteDVF.valuation.HasExtension
      (padicCompletedUnramifiedCompleteDVF p).valuation

def

padicCompletedUnramifiedFrobenius

L394 ↗

LubinTate.padicCompletedUnramifiedFrobenius

Documentation

Mathlib's Witt-vector fraction-field Frobenius, regarded over the canonical p-adic base field.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

def padicCompletedUnramifiedFrobenius
    (p : ℕ) [Fact p.Prime] :
    padicCompletedUnramifiedField p ≃ₐ[ℚ_[p]]
      padicCompletedUnramifiedField p

theorem

padicCompletedUnramifiedFrobenius_algebraMap_witt

L436 ↗

LubinTate.padicCompletedUnramifiedFrobenius_algebraMap_witt

Documentation

On the Witt integer ring, the field Frobenius is exactly mathlib's Witt-vector Frobenius.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedFrobenius_algebraMap_witt
    (p : ℕ) [Fact p.Prime]
    (x : padicCompletedUnramifiedWittRing p) :
    padicCompletedUnramifiedFrobenius p
        (algebraMap (padicCompletedUnramifiedWittRing p)
          (padicCompletedUnramifiedField p) x) =
      algebraMap (padicCompletedUnramifiedWittRing p)
        (padicCompletedUnramifiedField p)
        (WittVector.frobenius x)

theorem

padicCompletedUnramifiedFrobenius_valuation

L461 ↗

LubinTate.padicCompletedUnramifiedFrobenius_valuation

Documentation

Witt Frobenius preserves the canonical discrete valuation on the completed-unramified coefficient field.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedFrobenius_valuation
    (p : ℕ) [Fact p.Prime]
    (x : padicCompletedUnramifiedField p) :
    padicCompletedUnramifiedValuation p
        (padicCompletedUnramifiedFrobenius p x) =
      padicCompletedUnramifiedValuation p x

theorem

padicCompletedUnramifiedFrobenius_continuous

L506 ↗

LubinTate.padicCompletedUnramifiedFrobenius_continuous

Documentation

Witt Frobenius is continuous for the canonical valuation topology on the completed-unramified coefficient field.

Source context 7 commands

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

noncomputable section
namespace LubinTate
open Filter
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open scoped Topology Valued WithZero

Lean source · statement

theorem padicCompletedUnramifiedFrobenius_continuous
    (p : ℕ) [Fact p.Prime] :
    Continuous (padicCompletedUnramifiedFrobenius p)

Module documentation

The p-adic completed-unramified coefficient field

Declarations