NYLL
Module

CompletedPrimitiveAction.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedPrimitiveAction
38 declarations indexed from sourceView source ↗

Module documentation

Primitive unit action on a completed p-adic Lubin--Tate level

The completed level is defined as the splitting field of the standard primitive Lubin--Tate polynomial over the completed maximal-unramified field. This file identifies all of its roots with the genuine finite unit-parameter quotient of the original p-adic field.

The construction first embeds the ordinary standard Lubin--Tate level into the completed splitting field by sending its canonical primitive generator to the chosen completed root. The already constructed finite-level unit-parameter automorphisms then give every completed root. Comparing cardinalities proves that these are all the roots, and hence that each one generates the completed splitting field.

Imports5
Imported by3

Declarations

instance

padicCompletedActionTargetWithIdeal

L40 ↗
LubinTate.padicCompletedActionTargetWithIdeal
Source context 5 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · full declaration
instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
instance

padicCompletedActionTargetCompleteSpace

L47 ↗
LubinTate.padicCompletedActionTargetCompleteSpace
Source context 6 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
Lean source · statement
instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring
instance

padicCompletedActionTargetT2Space

L56 ↗
LubinTate.padicCompletedActionTargetT2Space
Source context 7 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
Lean source · statement
instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedPrimitiveRoot_aeval_standardPrimitivePolynomial

L67 ↗
LubinTate.padicCompletedPrimitiveRoot_aeval_standardPrimitivePolynomial
Documentation

The chosen completed primitive root annihilates the original standard primitive polynomial over ℚ_[p].

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_aeval_standardPrimitivePolynomial
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Polynomial.aeval (padicCompletedPrimitiveRoot p n)
        (standardLubinTatePrimitivePolynomialOverField
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) n) =
      0
def

padicStandardLevelEmbedding

L85 ↗
LubinTate.padicStandardLevelEmbedding
Documentation

The ordinary standard Lubin--Tate level embeds into the completed splitting field by sending its canonical generator to the chosen completed root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · full declaration
def padicStandardLevelEmbedding
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let hπ :=
      padicMultiplicativeLubinTateSeries_isUniformizer p
    standardLubinTateLevelField hπ n →ₐ[ℚ_[p]]
      padicCompletedLevelField p n := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  exact
    (standardLubinTateLevelPowerBasis hπ n).lift
      (padicCompletedPrimitiveRoot p n) (by
        exact (congrArg
          (fun f : Polynomial ℚ_[p] =>
            Polynomial.aeval (padicCompletedPrimitiveRoot p n) f)
          (standardLubinTateLevelPowerBasis_minpoly
            (F := padicLocalField p)
            (π := padicIntEquivValuationSubring p (p : ℤ_[p])) hπ n)).trans
          (padicCompletedPrimitiveRoot_aeval_standardPrimitivePolynomial p n))
theorem

padicStandardLevelEmbedding_apply_gen

L106 ↗
LubinTate.padicStandardLevelEmbedding_apply_gen
Documentation

The standard-level embedding has the prescribed value on the canonical primitive generator.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · full declaration
theorem padicStandardLevelEmbedding_apply_gen
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let hπ :=
      padicMultiplicativeLubinTateSeries_isUniformizer p
    padicStandardLevelEmbedding p n
        (standardLubinTateLevelPowerBasis hπ n).gen =
      padicCompletedPrimitiveRoot p n := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  simp only [padicStandardLevelEmbedding, PowerBasis.lift_gen]
def

padicCompletedUnitParameterRoot

L118 ↗
LubinTate.padicCompletedUnitParameterRoot
Documentation

A finite unit parameter, realized as a root in the completed splitting field.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedUnitParameterRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    padicCompletedLevelField p n
theorem

padicCompletedUnitParameterRoot_one

L130 ↗
LubinTate.padicCompletedUnitParameterRoot_one
Documentation

The identity unit parameter gives the chosen completed primitive root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRoot_one
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedUnitParameterRoot p n 1 =
      padicCompletedPrimitiveRoot p n
theorem

padicCompletedUnitParameterRoot_injective

L142 ↗
LubinTate.padicCompletedUnitParameterRoot_injective
Documentation

Distinct finite unit parameters give distinct roots in the completed level.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRoot_injective
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Function.Injective (padicCompletedUnitParameterRoot p n)
theorem

padicCompletedUnitParameterRoot_aeval_standardPrimitivePolynomial

L154 ↗
LubinTate.padicCompletedUnitParameterRoot_aeval_standardPrimitivePolynomial
Documentation

A completed parameter root annihilates the original primitive polynomial over ℚ_[p].

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRoot_aeval_standardPrimitivePolynomial
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    Polynomial.aeval (padicCompletedUnitParameterRoot p n a)
        (standardLubinTatePrimitivePolynomialOverField
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) n) =
      0
theorem

padicCompletedUnitParameterRoot_isRoot

L178 ↗
LubinTate.padicCompletedUnitParameterRoot_isRoot
Documentation

Every completed finite-parameter point is a root of the genuine completed primitive polynomial.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRoot_isRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    ((padicCompletedPrimitivePolynomial p n).map
      (algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n))).IsRoot
      (padicCompletedUnitParameterRoot p n a)
theorem

padicCompletedStandardScalarEndomorphismValue_congr_point

L195 ↗
LubinTate.padicCompletedStandardScalarEndomorphismValue_congr_point
Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicCompletedStandardScalarEndomorphismValue_congr_point
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    {x y : (padicCompletedLevelCompleteDVF p n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy : x = y) (a : (padicLocalField p).valuationSubring) :
    padicCompletedStandardScalarEndomorphismValue p n x hx a =
      padicCompletedStandardScalarEndomorphismValue p n y hy a
def

padicCompletedStandardPrimitivePointUnitAction

L208 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction
Documentation

The direct completed standard Lubin--Tate action of a p-adic unit on the chosen integral primitive point.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedStandardPrimitivePointUnitAction
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedStandardPrimitivePointUnitAction_hasEval

L219 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction_hasEval
Documentation

A direct completed standard unit translate remains a convergent evaluation point.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedStandardPrimitivePointUnitAction_hasEval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.HasEval
      (padicCompletedStandardPrimitivePointUnitAction p n u)
theorem

padicCompletedStandardPrimitivePointUnitAction_one

L231 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction_one
Documentation

The identity unit fixes the chosen completed standard primitive point.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedStandardPrimitivePointUnitAction_one
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    padicCompletedStandardPrimitivePointUnitAction p n 1 =
      padicCompletedPrimitiveRootInteger p n
theorem

padicCompletedStandardPrimitivePointUnitAction_iterate_succ_eq_zero

L239 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction_iterate_succ_eq_zero
Documentation

A direct completed standard unit translate is killed at level n + 1.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicCompletedStandardPrimitivePointUnitAction_iterate_succ_eq_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n)
        (padicCompletedStandardPrimitivePointUnitAction p n u)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) (n + 1)) =
      0
theorem

padicCompletedStandardPrimitivePointUnitAction_iterate_ne_zero

L310 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction_iterate_ne_zero
Documentation

A direct completed standard unit translate is not killed one level early.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicCompletedStandardPrimitivePointUnitAction_iterate_ne_zero
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    Polynomial.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n)
        (padicCompletedStandardPrimitivePointUnitAction p n u)
        (standardLubinTatePolynomialIterate
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) n) ≠
      0
theorem

padicCompletedStandardPrimitivePointUnitAction_isRoot

L378 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction_isRoot
Documentation

The direct completed standard action of every p-adic unit is a root of the genuine completed primitive polynomial.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedStandardPrimitivePointUnitAction_isRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    ((padicCompletedPrimitivePolynomial p n).map
      (algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n))).IsRoot
      ((padicCompletedStandardPrimitivePointUnitAction p n u :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n)
def

padicCompletedUnitParameterRootSet

L427 ↗
LubinTate.padicCompletedUnitParameterRootSet
Documentation

A finite unit parameter, regarded as an element of the full root set in the completed splitting field.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedUnitParameterRootSet
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    (padicCompletedPrimitivePolynomial p n).rootSet
      (padicCompletedLevelField p n)
theorem

padicCompletedUnitParameterRootSet_injective

L440 ↗
LubinTate.padicCompletedUnitParameterRootSet_injective
Documentation

The root-set realization of finite unit parameters is injective.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRootSet_injective
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Function.Injective (padicCompletedUnitParameterRootSet p n)
theorem

padicCompletedPrimitiveRootSet_natCard

L449 ↗
LubinTate.padicCompletedPrimitiveRootSet_natCard
Documentation

The completed primitive polynomial has exactly its degree many roots in the completed splitting field.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRootSet_natCard
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Nat.card
        ((padicCompletedPrimitivePolynomial p n).rootSet
          (padicCompletedLevelField p n)) =
      (p - 1) * p ^ n
theorem

padicStandardUnitParameter_natCard

L463 ↗
LubinTate.padicStandardUnitParameter_natCard
Documentation

The finite p-adic unit-parameter quotient has the degree of the completed primitive polynomial.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicStandardUnitParameter_natCard
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Nat.card (standardLubinTateUnitParameter (padicLocalField p) n) =
      (p - 1) * p ^ n
theorem

padicCompletedUnitParameterRootSet_bijective

L475 ↗
LubinTate.padicCompletedUnitParameterRootSet_bijective
Documentation

Finite p-adic unit parameters enumerate every root of the completed primitive polynomial.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRootSet_bijective
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Function.Bijective (padicCompletedUnitParameterRootSet p n)
def

padicStandardLevelUnitParameterPowerBasis

L488 ↗
LubinTate.padicStandardLevelUnitParameterPowerBasis
Documentation

A parameter root is itself a power-basis generator of the ordinary standard level.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · full declaration
def padicStandardLevelUnitParameterPowerBasis
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    let hπ :=
      padicMultiplicativeLubinTateSeries_isUniformizer p
    PowerBasis ℚ_[p] (standardLubinTateLevelField hπ n) := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  exact
    (standardLubinTateLevelPowerBasis hπ n).map
      (standardLubinTateUnitParameterAlgEquiv
        (padicLocalField p) hπ n a)
theorem

padicStandardLevelUnitParameterPowerBasis_gen

L503 ↗
LubinTate.padicStandardLevelUnitParameterPowerBasis_gen
Documentation

The generator of the parameter power basis is the corresponding finite-level parameter root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · full declaration
theorem padicStandardLevelUnitParameterPowerBasis_gen
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    let hπ :=
      padicMultiplicativeLubinTateSeries_isUniformizer p
    (padicStandardLevelUnitParameterPowerBasis p n a).gen =
      standardLubinTateUnitParameterLevelRoot
        (padicLocalField p) hπ n a := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  simp only [padicStandardLevelUnitParameterPowerBasis,
    PowerBasis.map_gen]
  exact standardLubinTateUnitParameterAlgEquiv_apply_gen
    (padicLocalField p)
    (π := padicIntEquivValuationSubring p (p : ℤ_[p])) hπ n a
theorem

padicPolynomialAeval_mem_completedUnramifiedAdjoin

L518 ↗
LubinTate.padicPolynomialAeval_mem_completedUnramifiedAdjoin
Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicPolynomialAeval_mem_completedUnramifiedAdjoin
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : padicCompletedLevelField p n) (f : Polynomial ℚ_[p]) :
    Polynomial.aeval x f ∈
      Algebra.adjoin (padicCompletedUnramifiedField p)
        ({x} : Set (padicCompletedLevelField p n))
theorem

padicCompletedUnitParameterRoot_mem_adjoin

L537 ↗
LubinTate.padicCompletedUnitParameterRoot_mem_adjoin
Documentation

Every completed parameter root is a polynomial expression in any other completed parameter root, with coefficients in the completed-unramified base.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRoot_mem_adjoin
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a b : standardLubinTateUnitParameter (padicLocalField p) n) :
    padicCompletedUnitParameterRoot p n b ∈
      Algebra.adjoin (padicCompletedUnramifiedField p)
        ({padicCompletedUnitParameterRoot p n a} :
          Set (padicCompletedLevelField p n))
theorem

padicCompletedPrimitiveRootSet_subset_adjoin_parameter

L583 ↗
LubinTate.padicCompletedPrimitiveRootSet_subset_adjoin_parameter
Documentation

All roots of the completed primitive polynomial lie in the field generated by any chosen parameter root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRootSet_subset_adjoin_parameter
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    ((padicCompletedPrimitivePolynomial p n).rootSet
        (padicCompletedLevelField p n) :
      Set (padicCompletedLevelField p n)) ⊆
      Algebra.adjoin (padicCompletedUnramifiedField p)
        ({padicCompletedUnitParameterRoot p n a} :
          Set (padicCompletedLevelField p n))
theorem

padicCompletedUnitParameterRoot_adjoin_eq_top

L607 ↗
LubinTate.padicCompletedUnitParameterRoot_adjoin_eq_top
Documentation

Every completed parameter root generates the completed splitting field over the completed maximal-unramified base.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRoot_adjoin_eq_top
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    Algebra.adjoin (padicCompletedUnramifiedField p)
        ({padicCompletedUnitParameterRoot p n a} :
          Set (padicCompletedLevelField p n)) =
      ⊤
theorem

padicCompletedStandardPrimitivePointUnitAction_adjoin_eq_top

L629 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction_adjoin_eq_top
Documentation

Every direct completed standard unit translate generates the completed splitting field over the completed maximal-unramified base.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicCompletedStandardPrimitivePointUnitAction_adjoin_eq_top
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    Algebra.adjoin (padicCompletedUnramifiedField p)
        ({((padicCompletedStandardPrimitivePointUnitAction p n u :
              (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n)} :
          Set (padicCompletedLevelField p n)) =
      ⊤
theorem

padicCompletedPrimitiveRoot_adjoin_eq_top

L667 ↗
LubinTate.padicCompletedPrimitiveRoot_adjoin_eq_top
Documentation

The chosen completed primitive root generates the completed splitting field.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_adjoin_eq_top
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Algebra.adjoin (padicCompletedUnramifiedField p)
        ({padicCompletedPrimitiveRoot p n} :
          Set (padicCompletedLevelField p n)) =
      ⊤
theorem

padicCompletedPrimitiveRoot_minpoly

L679 ↗
LubinTate.padicCompletedPrimitiveRoot_minpoly
Documentation

The completed primitive polynomial is the minimal polynomial of the chosen completed root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_minpoly
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    minpoly (padicCompletedUnramifiedField p)
        (padicCompletedPrimitiveRoot p n) =
      padicCompletedPrimitivePolynomial p n
theorem

padicCompletedPrimitiveRoot_isIntegral_over_completedUnramified

L698 ↗
LubinTate.padicCompletedPrimitiveRoot_isIntegral_over_completedUnramified
Documentation

The chosen primitive root is integral over the completed-unramified field.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitiveRoot_isIntegral_over_completedUnramified
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    IsIntegral (padicCompletedUnramifiedField p)
      (padicCompletedPrimitiveRoot p n)
def

padicCompletedPrimitivePowerBasis

L711 ↗
LubinTate.padicCompletedPrimitivePowerBasis
Documentation

The power basis of the completed level generated by the chosen primitive root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedPrimitivePowerBasis
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    PowerBasis (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
theorem

padicCompletedPrimitivePowerBasis_gen

L722 ↗
LubinTate.padicCompletedPrimitivePowerBasis_gen
Documentation

The generator of the completed primitive power basis is the chosen completed root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedPrimitivePowerBasis_gen
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    (padicCompletedPrimitivePowerBasis p n).gen =
      padicCompletedPrimitiveRoot p n
theorem

padicCompletedUnitParameterRoot_isIntegral

L729 ↗
LubinTate.padicCompletedUnitParameterRoot_isIntegral
Documentation

Every parameter root is integral over the completed-unramified base.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterRoot_isIntegral
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    IsIntegral (padicCompletedUnramifiedField p)
      (padicCompletedUnitParameterRoot p n a)
def

padicCompletedUnitParameterPowerBasis

L743 ↗
LubinTate.padicCompletedUnitParameterPowerBasis
Documentation

The power basis of the completed level generated by a prescribed finite unit parameter.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedUnitParameterPowerBasis
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    PowerBasis (padicCompletedUnramifiedField p)
      (padicCompletedLevelField p n)
theorem

padicCompletedUnitParameterPowerBasis_gen

L755 ↗
LubinTate.padicCompletedUnitParameterPowerBasis_gen
Documentation

The generator of a completed unit-parameter power basis is the corresponding completed root.

Source context 8 commands

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

noncomputable section
open scoped Polynomial PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance
    padicCompletedActionTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedActionTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedActionTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem padicCompletedUnitParameterPowerBasis_gen
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (a : standardLubinTateUnitParameter (padicLocalField p) n) :
    (padicCompletedUnitParameterPowerBasis p n a).gen =
      padicCompletedUnitParameterRoot p n a

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