NYLL
Module

CompletedChangedUniformizerFixedField.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedUniformizerFixedField
21 declarations indexed from sourceView source ↗

Module documentation

The changed p-adic Lubin--Tate level as a completed Frobenius fixed field

The completed Frobenius lift whose action on the standard primitive point is indexed by u⁻¹ is an actual ℚ_[p]-automorphism. Its fixed field is exactly the finite changed-uniformizer Lubin--Tate level generated by the genuine theta value.

The key reverse inclusion is coefficient descent in the theta power basis: fixedness makes every completed-unramified coefficient Frobenius-fixed, and the fixed-field theorem for Witt Frobenius puts that coefficient in ℚ_[p]. The final norm formula is therefore transported from the actual finite changed level, with no comparison hypothesis.

Imports4
Imported by2

Declarations

def

padicCompletedChangedUniformizerFrobeniusAlgEquiv

L40 ↗
LubinTate.padicCompletedChangedUniformizerFrobeniusAlgEquiv
Documentation

The inverse-unit completed Frobenius lift, regarded as an actual automorphism over ℚ_[p].

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
def padicCompletedChangedUniformizerFrobeniusAlgEquiv
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedLevelField p n ≃ₐ[ℚ_[p]]
      padicCompletedLevelField p n
theorem

padicCompletedChangedUniformizerFrobeniusAlgEquiv_apply

L63 ↗
LubinTate.padicCompletedChangedUniformizerFrobeniusAlgEquiv_apply
Documentation

The underlying action of the changed-uniformizer Frobenius automorphism is the actual completed inverse-unit lift.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicCompletedChangedUniformizerFrobeniusAlgEquiv_apply
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : padicCompletedLevelField p n) :
    padicCompletedChangedUniformizerFrobeniusAlgEquiv p u n x =
      padicCompletedUnitFrobeniusLiftEquiv p n u⁻¹ x
def

padicCompletedChangedUniformizerFrobeniusSubgroup

L73 ↗
LubinTate.padicCompletedChangedUniformizerFrobeniusSubgroup
Documentation

The cyclic subgroup generated by the completed changed-uniformizer Frobenius automorphism.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
def padicCompletedChangedUniformizerFrobeniusSubgroup
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Subgroup
      (padicCompletedLevelField p n ≃ₐ[ℚ_[p]]
        padicCompletedLevelField p n)
def

padicCompletedChangedUniformizerFixedField

L83 ↗
LubinTate.padicCompletedChangedUniformizerFixedField
Documentation

The field fixed by the actual inverse-unit completed Frobenius lift.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
def padicCompletedChangedUniformizerFixedField
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IntermediateField ℚ_[p] (padicCompletedLevelField p n)
theorem

padicChangedUniformizerThetaValue_mem_completedFixedField

L91 ↗
LubinTate.padicChangedUniformizerThetaValue_mem_completedFixedField
Documentation

The genuine theta value belongs to the completed Frobenius fixed field.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicChangedUniformizerThetaValue_mem_completedFixedField
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    ((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n) ∈
      padicCompletedChangedUniformizerFixedField p u n
theorem

padicChangedUniformizerLevelEmbedding_mem_completedFixedField

L124 ↗
LubinTate.padicChangedUniformizerLevelEmbedding_mem_completedFixedField
Documentation

The completed changed-level embedding is pointwise fixed by the inverse-unit Frobenius lift.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicChangedUniformizerLevelEmbedding_mem_completedFixedField
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x :
      standardLubinTateChangedLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u n) :
    padicChangedUniformizerLevelEmbedding p u n x ∈
      padicCompletedChangedUniformizerFixedField p u n
def

padicChangedUniformizerLevelToCompletedFixedField

L167 ↗
LubinTate.padicChangedUniformizerLevelToCompletedFixedField
Documentation

The finite changed Lubin--Tate level embedded directly into the completed Frobenius fixed field.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
def padicChangedUniformizerLevelToCompletedFixedField
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    standardLubinTateChangedLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u n
      →ₐ[ℚ_[p]]
        padicCompletedChangedUniformizerFixedField p u n
theorem

padicChangedUniformizerLevelToCompletedFixedField_apply_gen

L182 ↗
LubinTate.padicChangedUniformizerLevelToCompletedFixedField_apply_gen
Documentation

The fixed-field embedding sends the finite changed-level generator to the genuine theta value.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · full declaration
theorem padicChangedUniformizerLevelToCompletedFixedField_apply_gen
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    let hπ :=
      standardLubinTateChangedUniformizer_isUniformizer
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u
    padicChangedUniformizerLevelToCompletedFixedField p u n
        (standardLubinTateLevelPowerBasis hπ n).gen =
      ⟨((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n),
        padicChangedUniformizerThetaValue_mem_completedFixedField
          p u n⟩ := by
  apply Subtype.ext
  exact padicChangedUniformizerLevelEmbedding_apply_gen p u n
theorem

padicCompletedChangedUniformizerFrobenius_fixed_mem_adjoin_theta

L200 ↗
LubinTate.padicCompletedChangedUniformizerFrobenius_fixed_mem_adjoin_theta
Documentation

A Frobenius-fixed element of the completed level belongs to the ℚ_[p]-field generated by the theta value.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicCompletedChangedUniformizerFrobenius_fixed_mem_adjoin_theta
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ)
    (x : padicCompletedLevelField p n)
    (hx :
      padicCompletedChangedUniformizerFrobeniusAlgEquiv p u n x = x) :
    x ∈ IntermediateField.adjoin ℚ_[p]
      ({((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n)} :
        Set (padicCompletedLevelField p n))
theorem

padicCompletedChangedUniformizerFixedField_eq_adjoin_theta

L292 ↗
LubinTate.padicCompletedChangedUniformizerFixedField_eq_adjoin_theta
Documentation

The completed inverse-unit Frobenius fixed field is exactly the ℚ_[p]-field generated by the theta value.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicCompletedChangedUniformizerFixedField_eq_adjoin_theta
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedChangedUniformizerFixedField p u n =
      IntermediateField.adjoin ℚ_[p]
        ({((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n)} :
          Set (padicCompletedLevelField p n))
theorem

padicChangedUniformizerThetaValue_isIntegral_padicBase

L322 ↗
LubinTate.padicChangedUniformizerThetaValue_isIntegral_padicBase
Documentation

The theta value is integral over ℚ_[p].

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicChangedUniformizerThetaValue_isIntegral_padicBase
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    IsIntegral ℚ_[p]
      ((padicChangedUniformizerThetaValue p u n :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n)
theorem

padicChangedUniformizerThetaValue_minpoly_padicBase

L343 ↗
LubinTate.padicChangedUniformizerThetaValue_minpoly_padicBase
Documentation

Over ℚ_[p], the theta value has the actual changed Lubin--Tate primitive polynomial as its minimal polynomial.

Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
theorem padicChangedUniformizerThetaValue_minpoly_padicBase
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    minpoly ℚ_[p]
        ((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n) =
      standardLubinTatePrimitivePolynomialOverField
        (padicLocalField p)
        (standardLubinTateChangedUniformizer
          (padicLocalField p)
          (padicIntEquivValuationSubring p (p : ℤ_[p])) u) n
instance

padicCompletedChangedUniformizerFixedFieldAlgebra

L384 ↗
LubinTate.padicCompletedChangedUniformizerFixedFieldAlgebra
Source context 5 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
Lean source · statement
instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n)
instance

padicCompletedChangedUniformizerFixedFieldSMul

L393 ↗
LubinTate.padicCompletedChangedUniformizerFixedFieldSMul
Source context 6 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
Lean source · statement
instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n)
instance

padicCompletedChangedUniformizerFixedFieldModule

L402 ↗
LubinTate.padicCompletedChangedUniformizerFixedFieldModule
Source context 7 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toSMul _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
Lean source · statement
instance
    padicCompletedChangedUniformizerFixedFieldModule
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n)
theorem

padicCompletedChangedUniformizerFixedField_finrank

L413 ↗
LubinTate.padicCompletedChangedUniformizerFixedField_finrank
Documentation

The completed changed-uniformizer fixed field has degree (p - 1) * p ^ n over ℚ_[p].

Source context 8 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toSMul _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldModule
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toModule _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
Lean source · statement
theorem padicCompletedChangedUniformizerFixedField_finrank
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module.finrank ℚ_[p]
        (padicCompletedChangedUniformizerFixedField p u n) =
      (p - 1) * p ^ n
def

padicChangedUniformizerLevelEquivCompletedFixedField

L454 ↗
LubinTate.padicChangedUniformizerLevelEquivCompletedFixedField
Documentation

The actual finite changed Lubin--Tate level is algebraically equivalent to the completed inverse-unit Frobenius fixed field.

Source context 8 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toSMul _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldModule
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toModule _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
Lean source · statement
def padicChangedUniformizerLevelEquivCompletedFixedField
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    standardLubinTateChangedLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) u n
      ≃ₐ[ℚ_[p]]
        padicCompletedChangedUniformizerFixedField p u n
theorem

padicChangedUniformizerLevelEquivCompletedFixedField_apply_generator

L496 ↗
LubinTate.padicChangedUniformizerLevelEquivCompletedFixedField_apply_generator
Documentation

The fixed-field equivalence sends the changed finite-level generator to the genuine theta value.

Source context 8 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toSMul _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldModule
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toModule _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
Lean source · statement
theorem
    padicChangedUniformizerLevelEquivCompletedFixedField_apply_generator
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicChangedUniformizerLevelEquivCompletedFixedField p u n
        (standardLubinTateChangedLevelGenerator
          (padicMultiplicativeLubinTateSeries_isUniformizer p) u n) =
      ⟨((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
            padicCompletedLevelField p n),
        padicChangedUniformizerThetaValue_mem_completedFixedField
          p u n⟩
def

padicCompletedChangedUniformizerPrimeElement

L514 ↗
LubinTate.padicCompletedChangedUniformizerPrimeElement
Documentation

The theta value, regarded as an element of the completed Frobenius fixed field.

Source context 8 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toSMul _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldModule
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toModule _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
Lean source · statement
def padicCompletedChangedUniformizerPrimeElement
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedChangedUniformizerFixedField p u n
theorem

padicCompletedChangedUniformizerPrimeElement_eq_equiv_generator

L526 ↗
LubinTate.padicCompletedChangedUniformizerPrimeElement_eq_equiv_generator
Documentation

The fixed-field prime element is the image of the changed finite-level generator.

Source context 8 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toSMul _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldModule
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toModule _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
Lean source · statement
theorem
    padicCompletedChangedUniformizerPrimeElement_eq_equiv_generator
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedChangedUniformizerPrimeElement p u n =
      padicChangedUniformizerLevelEquivCompletedFixedField p u n
        (standardLubinTateChangedLevelGenerator
          (padicMultiplicativeLubinTateSeries_isUniformizer p) u n)
theorem

padicCompletedChangedUniformizer_norm_neg_primeElement

L540 ↗
LubinTate.padicCompletedChangedUniformizer_norm_neg_primeElement
Documentation

The completed changed-uniformizer norm formula: N(-theta) = u * p.

Source context 8 commands

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

noncomputable section
open scoped Polynomial
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldAlgebra
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  Subalgebra.algebra
    (padicCompletedChangedUniformizerFixedField p u n).toSubalgebra
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldSMul
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    SMul ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toSMul _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
noncomputable local instance
    padicCompletedChangedUniformizerFixedFieldModule
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Module ℚ_[p]
      (padicCompletedChangedUniformizerFixedField p u n) :=
  @Algebra.toModule _ _ _ _
    (padicCompletedChangedUniformizerFixedFieldAlgebra p u n)
Lean source · statement
theorem padicCompletedChangedUniformizer_norm_neg_primeElement
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    Algebra.norm ℚ_[p]
        (-padicCompletedChangedUniformizerPrimeElement p u n) =
      (standardLubinTateChangedUniformizer
        (padicLocalField p)
        (padicIntEquivValuationSubring p (p : ℤ_[p])) u :
          ℚ_[p])

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