Module

CompletedChangedUniformizerThetaFixed.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedChangedUniformizerThetaFixed

8 declarations indexed from sourceView source ↗

Module documentation

Fixedness of completed p-adic changed-uniformizer theta values

The Frobenius lift whose primitive-point action is indexed by the inverse unit is the genuine diagonal action relevant to change of uniformizer. Semilinear evaluation changes theta coefficients by Witt Frobenius, while the first changed-uniformizer identity changes the evaluation point by the unit itself. The unit and inverse-unit actions cancel, so the actual convergent theta value is fixed.

Imports1

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedFrobeniusEvaluation

Imported by2

instance

padicCompletedThetaFixedWittUniformSpace

L29 ↗

LubinTate.padicCompletedThetaFixedWittUniformSpace

Source context 4 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp

Lean source · statement

instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p)

instance

padicCompletedThetaFixedTargetWithIdeal

L35 ↗

LubinTate.padicCompletedThetaFixedTargetWithIdeal

Source context 5 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥

Lean source · full declaration

instance
    padicCompletedThetaFixedTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal

instance

padicCompletedThetaFixedTargetCompleteSpace

L42 ↗

LubinTate.padicCompletedThetaFixedTargetCompleteSpace

Source context 6 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedThetaFixedTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal

Lean source · statement

instance
    padicCompletedThetaFixedTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring

instance

padicCompletedThetaFixedTargetT2Space

L51 ↗

LubinTate.padicCompletedThetaFixedTargetT2Space

Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedThetaFixedTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedThetaFixedTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1

Lean source · statement

instance
    padicCompletedThetaFixedTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring

theorem

padicCompletedThetaFixedEvaluation_eq_of_point_eq

L60 ↗

LubinTate.padicCompletedThetaFixedEvaluation_eq_of_point_eq

Source context 8 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedThetaFixedTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedThetaFixedTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedThetaFixedTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2

Lean source · statement

theorem padicCompletedThetaFixedEvaluation_eq_of_point_eq
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x y : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) (hy : PowerSeries.HasEval y)
    (hxy : x = y) :
    padicCompletedLevelPowerSeriesEval p n x hx =
      padicCompletedLevelPowerSeriesEval p n y hy

theorem

padicCompletedDiagonalFrobenius_multiplicativeUnitAction

L73 ↗

LubinTate.padicCompletedDiagonalFrobenius_multiplicativeUnitAction

Documentation

On the genuine multiplicative primitive point, the multiplicative unit action cancels the inverse-unit action prescribed by the diagonal completed Frobenius lift.

Source context 8 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedThetaFixedTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedThetaFixedTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedThetaFixedTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2

Lean source · full declaration

theorem padicCompletedDiagonalFrobenius_multiplicativeUnitAction
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    let r :=
      padicCompletedUnitFrobeniusIntegerEquiv p n u⁻¹
    let x := padicCompletedMultiplicativePrimitivePoint p n
    let hx := padicCompletedMultiplicativePrimitivePoint_hasEval p n
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        (r x)
        (padicCompletedUnitFrobeniusIntegerEquiv_hasEval
          p n u⁻¹ x hx)
        (u : (padicLocalField p).valuationSubring) =
      x := by
  let r :=
    padicCompletedUnitFrobeniusIntegerEquiv p n u⁻¹
  let x := padicCompletedMultiplicativePrimitivePoint p n
  let hx := padicCompletedMultiplicativePrimitivePoint_hasEval p n
  have hpoint :
      r x =
        padicCompletedMultiplicativePrimitivePointUnitAction p u⁻¹ n := by
    simpa only [r, x] using
      padicCompletedUnitFrobeniusIntegerEquiv_multiplicativePrimitivePoint
        p n u⁻¹
  have htransport :=
    DFunLike.congr_fun
      (padicCompletedThetaFixedEvaluation_eq_of_point_eq p n
        (r x)
        (padicCompletedMultiplicativePrimitivePointUnitAction p u⁻¹ n)
        (padicCompletedUnitFrobeniusIntegerEquiv_hasEval
          p n u⁻¹ x hx)
        (padicCompletedMultiplicativePrimitivePointUnitAction_hasEval
          p u⁻¹ n)
        hpoint)
      (padicCompletedMultiplicativeUnitEndomorphism p u)
  calc
    padicCompletedMultiplicativeScalarEndomorphismValue p n
        (r x)
        (padicCompletedUnitFrobeniusIntegerEquiv_hasEval
          p n u⁻¹ x hx)
        (u : (padicLocalField p).valuationSubring) =
      padicCompletedMultiplicativeScalarEndomorphismValue p n
        (padicCompletedMultiplicativePrimitivePointUnitAction p u⁻¹ n)
        (padicCompletedMultiplicativePrimitivePointUnitAction_hasEval
          p u⁻¹ n)
        (u : (padicLocalField p).valuationSubring) := by
      simpa only [padicCompletedMultiplicativeUnitEndomorphism,
        padicCompletedMultiplicativeScalarEndomorphismValue] using
        htransport
    _ = x := by
      simpa only [x, hx,
        padicCompletedMultiplicativePrimitivePointUnitAction,
        padicCompletedMultiplicativeUnitEndomorphism,
        padicCompletedMultiplicativeScalarEndomorphismValue] using
        (padicCompletedMultiplicativeScalarEndomorphismValue_unit_after_inverse
          p n
          (padicCompletedMultiplicativePrimitivePoint p n)
          (padicCompletedMultiplicativePrimitivePoint_hasEval p n) u)

theorem

padicCompletedChangedUniformizerThetaValue_fixed_by_diagonalFrobeniusInteger

L133 ↗

LubinTate.padicCompletedChangedUniformizerThetaValue_fixed_by_diagonalFrobeniusInteger

Documentation

The inverse-unit diagonal completed Frobenius fixes the genuine changed-uniformizer theta value in the completed-level valuation ring.

Source context 8 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedThetaFixedTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedThetaFixedTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedThetaFixedTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2

Lean source · statement

theorem
    padicCompletedChangedUniformizerThetaValue_fixed_by_diagonalFrobeniusInteger
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedUnitFrobeniusIntegerEquiv p n u⁻¹
        (padicChangedUniformizerThetaValue p u n) =
      padicChangedUniformizerThetaValue p u n

theorem

padicCompletedChangedUniformizerThetaValue_fixed_by_diagonalFrobenius

L189 ↗

LubinTate.padicCompletedChangedUniformizerThetaValue_fixed_by_diagonalFrobenius

Documentation

The inverse-unit diagonal completed Frobenius field automorphism fixes the genuine changed-uniformizer theta value.

Source context 8 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
private noncomputable local instance (priority := 50)
    padicCompletedThetaFixedWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedThetaFixedTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedThetaFixedTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).1
private noncomputable local instance
    padicCompletedThetaFixedTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2

Lean source · statement

theorem
    padicCompletedChangedUniformizerThetaValue_fixed_by_diagonalFrobenius
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) (n : ℕ) :
    padicCompletedUnitFrobeniusLiftEquiv p n u⁻¹
        ((padicChangedUniformizerThetaValue p u n :
            (padicCompletedLevelCompleteDVF p n).valuationSubring) :
          padicCompletedLevelField p n) =
      ((padicChangedUniformizerThetaValue p u n :
          (padicCompletedLevelCompleteDVF p n).valuationSubring) :
        padicCompletedLevelField p n)

Module documentation

Fixedness of completed p-adic changed-uniformizer theta values

Declarations