NYLL
Module

PrimitiveAction.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveAction
32 declarations indexed from sourceView source ↗

Module documentation

The standard Lubin--Tate action on primitive division points

The formal scalar endomorphism [a] is in general an infinite power series. It is therefore evaluated on the primitive point only after that point has been placed in the complete integral closure constructed in PrimitiveUniformizer. Unit scalars preserve the exact torsion level, so their analytic values are again roots of the primitive division polynomial.

The action is faithful precisely modulo the higher principal-unit subgroup U^(n + 1). This is the finite-level congruence needed to descend the action from valuation-ring units to the standard finite unit parameters.

Imports5
Imported by4

Declarations

theorem

standardLubinTateSeries_hasLinearTerm

L50 ↗
LubinTate.SameUniformizer.standardLubinTateSeries_hasLinearTerm
Documentation

The standard Lubin--Tate series itself has the prescribed linear term π X.

Source context 10 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
namespace SameUniformizer
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
Lean source · full declaration
theorem standardLubinTateSeries_hasLinearTerm
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    HasLinearTerm (standardLubinTateSeries hπ).toPowerSeries
      (fun _ : Unit => π) := by
  have hlinear :
      (standardLubinTateSeries hπ).toPowerSeries -
          linearForm (fun _ : Unit => π) =
        (PowerSeries.X : PowerSeries F.valuationSubring) ^
          Nat.card F.residueField := by
    rw [LubinTateSeries.standardLubinTateSeries_toPowerSeries]
    dsimp only [standardLubinTatePowerSeries, linearForm]
    rw [Fintype.sum_unique, PowerSeries.C_apply, PowerSeries.X_apply]
    ring
  rw [HasLinearTerm, hlinear, ← PowerSeries.order_eq_order,
    PowerSeries.order_X_pow]
  exact_mod_cast (Finite.one_lt_card : 1 < Nat.card F.residueField)
theorem

standardLubinTateEndomorphism_uniformizer

L69 ↗
LubinTate.SameUniformizer.standardLubinTateEndomorphism_uniformizer
Documentation

The scalar endomorphism attached to the uniformizer is the defining standard Lubin--Tate series.

Source context 10 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
namespace SameUniformizer
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
Lean source · statement
theorem standardLubinTateEndomorphism_uniformizer
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    standardLubinTateEndomorphism hπ π =
      (standardLubinTateSeries hπ).toPowerSeries
instance

standardLubinTatePrimitiveActionCoefficientUniformSpace

L103 ↗
LubinTate.standardLubinTatePrimitiveActionCoefficientUniformSpace
Source context 10 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
Lean source · statement
instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring
instance

standardLubinTatePrimitiveActionTargetWithIdeal

L108 ↗
LubinTate.standardLubinTatePrimitiveActionTargetWithIdeal
Source context 11 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
Lean source · full declaration
instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
instance

standardLubinTatePrimitiveActionTargetCompleteSpace

L115 ↗
LubinTate.standardLubinTatePrimitiveActionTargetCompleteSpace
Source context 12 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
Lean source · statement
instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
instance

standardLubinTatePrimitiveActionTargetT2Space

L124 ↗
LubinTate.standardLubinTatePrimitiveActionTargetT2Space
Source context 13 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
Lean source · statement
instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
instance

standardLubinTatePrimitiveActionAlgebra

L133 ↗
LubinTate.standardLubinTatePrimitiveActionAlgebra
Source context 14 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
def

standardLubinTateFormalAdd

L142 ↗
LubinTate.standardLubinTateFormalAdd
Documentation

Analytic addition in the standard formal group on the integer ring of a finite level.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
def standardLubinTateFormalAdd
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x y :
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

standardLubinTateEndomorphismEvalAt_add

L153 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_add
Documentation

Analytic evaluation of scalar addition is addition in the standard formal group.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_add
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (a b : F.valuationSubring) :
    standardLubinTateEndomorphismEvalAt hπ n x hx (a + b) =
      standardLubinTateFormalAdd hπ n
        (standardLubinTateEndomorphismEvalAt hπ n x hx a)
        (standardLubinTateEndomorphismEvalAt hπ n x hx b)
theorem

standardLubinTateEndomorphismValue_add

L219 ↗
LubinTate.standardLubinTateEndomorphismValue_add
Documentation

At the primitive point, addition of scalars is analytic formal-group addition of their values.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismValue_add
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (a b : F.valuationSubring) :
    standardLubinTateEndomorphismValue hπ n (a + b) =
      standardLubinTateFormalAdd hπ n
        (standardLubinTateEndomorphismValue hπ n a)
        (standardLubinTateEndomorphismValue hπ n b)
theorem

standardLubinTateEndomorphismEvalAt_eq_of_point_eq

L230 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_eq_of_point_eq
Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_eq_of_point_eq
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x y : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy : x = y) (a : F.valuationSubring) :
    standardLubinTateEndomorphismEvalAt hπ n x hx a =
      standardLubinTateEndomorphismEvalAt hπ n y hy a
theorem

standardLubinTateEndomorphismEvalAt_zero_point

L241 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_zero_point
Documentation

Every standard scalar endomorphism fixes the zero point.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_zero_point
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (a : F.valuationSubring) :
    standardLubinTateEndomorphismEvalAt hπ n 0
        PowerSeries.HasEval.zero a = 0
theorem

standardLubinTateEndomorphismEvalAt_unit_injective

L253 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_unit_injective
Documentation

A unit scalar acts injectively on the topologically nilpotent elements of a finite-level integer ring.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_unit_injective
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ)
    {x y : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring}
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy :
      standardLubinTateEndomorphismEvalAt hπ n x hx
          (u : F.valuationSubring) =
        standardLubinTateEndomorphismEvalAt hπ n y hy
          (u : F.valuationSubring)) :
    x = y
theorem

standardLubinTateEndomorphismEvalAt_uniformizer_pow

L305 ↗
LubinTate.standardLubinTateEndomorphismEvalAt_uniformizer_pow
Documentation

Evaluating [π ^ r] is the same as evaluating the r-fold standard division-polynomial iterate.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismEvalAt_uniformizer_pow
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (x : (standardLubinTateLevelCompleteDVF hπ n).valuationSubring)
    (hx : PowerSeries.HasEval x) (r : ℕ) :
    standardLubinTateEndomorphismEvalAt hπ n x hx (π ^ r) =
      Polynomial.eval₂
        (standardLubinTateLevelCoefficientHom hπ n) x
        (standardLubinTatePolynomialIterate F π r)
def

standardLubinTatePrimitivePointIntegerAction

L328 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction
Documentation

A valuation-ring unit acts on the chosen primitive point by analytic evaluation of its standard scalar endomorphism.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
def standardLubinTatePrimitivePointIntegerAction
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
theorem

standardLubinTatePrimitivePointIntegerAction_hasEval

L337 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_hasEval
Documentation

A unit translate of the primitive point is still topologically nilpotent.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitivePointIntegerAction_hasEval
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ) :
    PowerSeries.HasEval
      (standardLubinTatePrimitivePointIntegerAction hπ n u)
theorem

standardLubinTatePrimitivePointIntegerAction_one

L347 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_one
Documentation

The unit 1 fixes the chosen primitive point.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitivePointIntegerAction_one
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTatePrimitivePointIntegerAction hπ n 1 =
      standardLubinTatePrimitivePointInteger hπ n
theorem

standardLubinTatePrimitivePointIntegerAction_mul

L355 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_mul
Documentation

Multiplication of unit parameters is composition of their analytic actions.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitivePointIntegerAction_mul
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u w : F.valuationSubringˣ) :
    standardLubinTatePrimitivePointIntegerAction hπ n (u * w) =
      standardLubinTateEndomorphismEvalAt hπ n
        (standardLubinTatePrimitivePointIntegerAction hπ n w)
        (standardLubinTatePrimitivePointIntegerAction_hasEval hπ n w)
        (u : F.valuationSubring)
theorem

standardLubinTateEndomorphismValue_eq_zero_iff_mem_maximalIdeal_pow

L369 ↗
LubinTate.standardLubinTateEndomorphismValue_eq_zero_iff_mem_maximalIdeal_pow
Documentation

The primitive level-n + 1 point has exact scalar annihilator m^(n + 1).

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateEndomorphismValue_eq_zero_iff_mem_maximalIdeal_pow
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (a : F.valuationSubring) :
    standardLubinTateEndomorphismValue hπ n a = 0 ↔
      a ∈ F.toCompleteDVF.maximalIdeal ^ (n + 1)
theorem

standardLubinTatePrimitivePointIntegerAction_eq_self_iff_mem_higherPrincipalUnitGroup

L475 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_eq_self_iff_mem_higherPrincipalUnitGroup
Documentation

A unit fixes the primitive level-n + 1 point exactly when it belongs to U^(n + 1).

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerAction_eq_self_iff_mem_higherPrincipalUnitGroup
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ) :
    standardLubinTatePrimitivePointIntegerAction hπ n u =
        standardLubinTatePrimitivePointInteger hπ n ↔
      u ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF
        (n + 1)
theorem

standardLubinTatePrimitivePointIntegerAction_eq_iff_div_mem_higherPrincipalUnitGroup

L554 ↗
LubinTate.standardLubinTatePrimitivePointIntegerAction_eq_iff_div_mem_higherPrincipalUnitGroup
Documentation

Two unit actions give the same primitive integer point exactly when their quotient lies in U^(n + 1).

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTatePrimitivePointIntegerAction_eq_iff_div_mem_higherPrincipalUnitGroup
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u w : F.valuationSubringˣ) :
    standardLubinTatePrimitivePointIntegerAction hπ n u =
        standardLubinTatePrimitivePointIntegerAction hπ n w ↔
      u / w ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF
        (n + 1)
def

standardLubinTatePrimitiveLevelAction

L622 ↗
LubinTate.standardLubinTatePrimitiveLevelAction
Documentation

The analytic unit action, viewed in the finite-level field.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
def standardLubinTatePrimitiveLevelAction
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ) :
    standardLubinTateLevelField hπ n
def

standardLubinTateLevelIntegerToSeparableClosure

L630 ↗
LubinTate.standardLubinTateLevelIntegerToSeparableClosure
Documentation

The natural embedding of the finite-level integer ring into the fixed separable closure.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
def standardLubinTateLevelIntegerToSeparableClosure
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring →+*
      SeparableClosure K
theorem

standardLubinTateLevelIntegerToSeparableClosure_injective

L639 ↗
LubinTate.standardLubinTateLevelIntegerToSeparableClosure_injective
Documentation

The natural embedding of the finite-level integer ring into the fixed separable closure is injective.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateLevelIntegerToSeparableClosure_injective
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Function.Injective
      (standardLubinTateLevelIntegerToSeparableClosure hπ n)
theorem

standardLubinTateLevelIntegerToSeparableClosure_comp_coefficientHom

L654 ↗
LubinTate.standardLubinTateLevelIntegerToSeparableClosure_comp_coefficientHom
Documentation

On base coefficients, the level-integer embedding is the fixed embedding of the base field into its separable closure.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTateLevelIntegerToSeparableClosure_comp_coefficientHom
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTateLevelIntegerToSeparableClosure hπ n).comp
        (standardLubinTateLevelCoefficientHom hπ n) =
      (algebraMap K (SeparableClosure K)).comp
        (algebraMap F.valuationSubring K)
def

standardLubinTatePrimitiveRootAction

L675 ↗
LubinTate.standardLubinTatePrimitiveRootAction
Documentation

The analytic unit action, transported from the level integer ring to the chosen finite-level field.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
def standardLubinTatePrimitiveRootAction
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ) :
    SeparableClosure K
theorem

standardLubinTatePrimitiveLevelAction_coe

L685 ↗
LubinTate.standardLubinTatePrimitiveLevelAction_coe
Documentation

Coercing the finite-level action to the fixed separable closure gives the primitive-root action.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitiveLevelAction_coe
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ) :
    ((standardLubinTatePrimitiveLevelAction hπ n u :
        standardLubinTateLevelField hπ n) : SeparableClosure K) =
      standardLubinTatePrimitiveRootAction hπ n u
theorem

standardLubinTatePrimitiveRootAction_one

L695 ↗
LubinTate.standardLubinTatePrimitiveRootAction_one
Documentation

The identity unit fixes the chosen primitive root.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitiveRootAction_one
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTatePrimitiveRootAction hπ n 1 =
      chosenStandardLubinTatePrimitiveRoot hπ n
theorem

standardLubinTatePrimitiveRootAction_eq_iff_integerAction_eq

L712 ↗
LubinTate.standardLubinTatePrimitiveRootAction_eq_iff_integerAction_eq
Documentation

Equality of primitive-root actions can be checked already in the finite-level integer ring.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitiveRootAction_eq_iff_integerAction_eq
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u w : F.valuationSubringˣ) :
    standardLubinTatePrimitiveRootAction hπ n u =
        standardLubinTatePrimitiveRootAction hπ n w ↔
      standardLubinTatePrimitivePointIntegerAction hπ n u =
        standardLubinTatePrimitivePointIntegerAction hπ n w
theorem

standardLubinTatePrimitiveRootAction_eq_iff_div_mem_higherPrincipalUnitGroup

L734 ↗
LubinTate.standardLubinTatePrimitiveRootAction_eq_iff_div_mem_higherPrincipalUnitGroup
Documentation

Two unit actions give the same primitive root exactly when their quotient lies in U^(n + 1).

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTatePrimitiveRootAction_eq_iff_div_mem_higherPrincipalUnitGroup
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u w : F.valuationSubringˣ) :
    standardLubinTatePrimitiveRootAction hπ n u =
        standardLubinTatePrimitiveRootAction hπ n w ↔
      u / w ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF
        (n + 1)
theorem

standardLubinTatePrimitiveRootAction_eq_of_div_mem_higherPrincipalUnitGroup

L747 ↗
LubinTate.standardLubinTatePrimitiveRootAction_eq_of_div_mem_higherPrincipalUnitGroup
Documentation

Unit parameters in the same higher-principal-unit coset give the same primitive root.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem
    standardLubinTatePrimitiveRootAction_eq_of_div_mem_higherPrincipalUnitGroup
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    {u w : F.valuationSubringˣ}
    (huw :
      u / w ∈ CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF
        (n + 1)) :
    standardLubinTatePrimitiveRootAction hπ n u =
      standardLubinTatePrimitiveRootAction hπ n w
theorem

standardLubinTatePrimitiveRootAction_isRoot

L761 ↗
LubinTate.standardLubinTatePrimitiveRootAction_isRoot
Documentation

A unit translate of the chosen primitive point is again a root of the level-n + 1 primitive division polynomial.

Source context 15 commands

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

noncomputable section
open scoped Polynomial PowerSeries
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
section AnalyticAction
variable {F : LocalField.{u, v} K} {π : F.valuationSubring}
private noncomputable local instance
    standardLubinTatePrimitiveActionCoefficientUniformSpace :
    UniformSpace F.valuationSubring :=
  ⊥
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetWithIdeal
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring where
  i := (standardLubinTateLevelCompleteDVF hπ n).maximalIdeal
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetCompleteSpace
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    standardLubinTatePrimitiveActionTargetT2Space
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring := by
  let target := standardLubinTateLevelCompleteDVF hπ n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
private noncomputable local instance
    standardLubinTatePrimitiveActionAlgebra
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Algebra F.valuationSubring
      (standardLubinTateLevelCompleteDVF hπ n).valuationSubring :=
  (standardLubinTateLevelCoefficientHom hπ n).toAlgebra
Lean source · statement
theorem standardLubinTatePrimitiveRootAction_isRoot
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ)
    (u : F.valuationSubringˣ) :
    ((standardLubinTatePrimitivePolynomialOverField F π n).map
      (algebraMap K (SeparableClosure K))).IsRoot
        (standardLubinTatePrimitiveRootAction hπ n u)

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