NYLL
Module

CompletedFrobeniusEvaluation.lean

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

Module documentation

Semilinear evaluation for completed p-adic Frobenius lifts

The completed unit-indexed Frobenius lift preserves the actual integral closure valuation ring. Its restriction is continuous for the maximal- ideal adic topology and transports convergent Witt-coefficient power-series evaluation by Witt Frobenius on coefficients.

Applying this to the standard-to-multiplicative comparison identifies the image of the genuine completed multiplicative primitive point with its actual multiplicative unit translate.

Imports2
Imported by4

Declarations

instance

padicCompletedFrobeniusEvaluationWittUniformSpace

L34 ↗
LubinTate.padicCompletedFrobeniusEvaluationWittUniformSpace
Source context 6 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
Lean source · statement
instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p)
instance

padicCompletedFrobeniusEvaluationTargetWithIdeal

L40 ↗
LubinTate.padicCompletedFrobeniusEvaluationTargetWithIdeal
Source context 7 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
Lean source · full declaration
instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
instance

padicCompletedFrobeniusEvaluationTargetCompleteSpace

L47 ↗
LubinTate.padicCompletedFrobeniusEvaluationTargetCompleteSpace
Source context 8 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
Lean source · statement
instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring
instance

padicCompletedFrobeniusEvaluationTargetT2Space

L56 ↗
LubinTate.padicCompletedFrobeniusEvaluationTargetT2Space
Source context 9 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring
def

padicCompletedUnramifiedFrobeniusIntegerEquiv

L67 ↗
LubinTate.padicCompletedUnramifiedFrobeniusIntegerEquiv
Documentation

Arithmetic Frobenius restricted to the valuation ring of the completed maximal-unramified p-adic field.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · full declaration
def padicCompletedUnramifiedFrobeniusIntegerEquiv
    (p : ℕ) [Fact p.Prime] :
    (padicCompletedUnramifiedCompleteDVF p).valuationSubring ≃+*
      (padicCompletedUnramifiedCompleteDVF p).valuationSubring where
  toFun x :=
    ⟨padicCompletedUnramifiedFrobenius p
        (x : padicCompletedUnramifiedField p), by
      change
        padicCompletedUnramifiedValuation p
            (padicCompletedUnramifiedFrobenius p
              (x : padicCompletedUnramifiedField p)) ≤ 1
      rw [padicCompletedUnramifiedFrobenius_valuation]
      exact x.property⟩
  invFun x :=
    ⟨(padicCompletedUnramifiedFrobenius p).symm
        (x : padicCompletedUnramifiedField p), by
      change
        padicCompletedUnramifiedValuation p
            ((padicCompletedUnramifiedFrobenius p).symm
              (x : padicCompletedUnramifiedField p)) ≤ 1
      rw [← padicCompletedUnramifiedFrobenius_valuation p
          ((padicCompletedUnramifiedFrobenius p).symm
            (x : padicCompletedUnramifiedField p)),
        (padicCompletedUnramifiedFrobenius p).apply_symm_apply]
      exact x.property⟩
  left_inv x := by
    apply Subtype.ext
    exact (padicCompletedUnramifiedFrobenius p).symm_apply_apply x
  right_inv x := by
    apply Subtype.ext
    exact (padicCompletedUnramifiedFrobenius p).apply_symm_apply x
  map_mul' x y := by
    apply Subtype.ext
    exact map_mul (padicCompletedUnramifiedFrobenius p)
      (x : padicCompletedUnramifiedField p)
      (y : padicCompletedUnramifiedField p)
  map_add' x y := by
    apply Subtype.ext
    exact map_add (padicCompletedUnramifiedFrobenius p)
      (x : padicCompletedUnramifiedField p)
      (y : padicCompletedUnramifiedField p)
theorem

padicCompletedUnramifiedFrobeniusIntegerEquiv_coe

L112 ↗
LubinTate.padicCompletedUnramifiedFrobeniusIntegerEquiv_coe
Documentation

Coercion of the integral Frobenius restriction agrees with arithmetic Frobenius on the completed-unramified fraction field.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnramifiedFrobeniusIntegerEquiv_coe
    (p : ℕ) [Fact p.Prime]
    (x : (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
    ((padicCompletedUnramifiedFrobeniusIntegerEquiv p x :
        (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
      padicCompletedUnramifiedField p) =
      padicCompletedUnramifiedFrobenius p
        (x : padicCompletedUnramifiedField p)
theorem

padicCompletedUnramifiedFrobeniusIntegerEquiv_symm_coe

L125 ↗
LubinTate.padicCompletedUnramifiedFrobeniusIntegerEquiv_symm_coe
Documentation

Coercion of the inverse integral Frobenius restriction agrees with inverse arithmetic Frobenius on the fraction field.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnramifiedFrobeniusIntegerEquiv_symm_coe
    (p : ℕ) [Fact p.Prime]
    (x : (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
    (((padicCompletedUnramifiedFrobeniusIntegerEquiv p).symm x :
        (padicCompletedUnramifiedCompleteDVF p).valuationSubring) :
      padicCompletedUnramifiedField p) =
      (padicCompletedUnramifiedFrobenius p).symm
        (x : padicCompletedUnramifiedField p)
theorem

padicCompletedUnitFrobeniusLiftEquiv_symm_algebraMap

L138 ↗
LubinTate.padicCompletedUnitFrobeniusLiftEquiv_symm_algebraMap
Documentation

The inverse of a unit-indexed completed Frobenius lift acts on base scalars through inverse arithmetic Frobenius.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusLiftEquiv_symm_algebraMap
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (b : padicCompletedUnramifiedField p) :
    (padicCompletedUnitFrobeniusLiftEquiv p n u).symm
        (algebraMap (padicCompletedUnramifiedField p)
          (padicCompletedLevelField p n) b) =
      algebraMap (padicCompletedUnramifiedField p)
        (padicCompletedLevelField p n)
        ((padicCompletedUnramifiedFrobenius p).symm b)
theorem

padicCompletedUnitFrobeniusLiftEquiv_mem_valuationSubring

L155 ↗
LubinTate.padicCompletedUnitFrobeniusLiftEquiv_mem_valuationSubring
Documentation

A unit-indexed completed Frobenius lift carries every element of the selected completed-level valuation ring back into that valuation ring.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusLiftEquiv_mem_valuationSubring
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x : padicCompletedLevelField p n)
    (hx :
      x ∈ (padicCompletedLevelCompleteDVF p n).valuation.valuationSubring) :
    padicCompletedUnitFrobeniusLiftEquiv p n u x ∈
      (padicCompletedLevelCompleteDVF p n).valuation.valuationSubring
theorem

padicCompletedUnitFrobeniusLiftEquiv_symm_mem_valuationSubring

L206 ↗
LubinTate.padicCompletedUnitFrobeniusLiftEquiv_symm_mem_valuationSubring
Documentation

The inverse of a unit-indexed completed Frobenius lift also preserves the selected completed-level valuation ring.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusLiftEquiv_symm_mem_valuationSubring
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x : padicCompletedLevelField p n)
    (hx :
      x ∈ (padicCompletedLevelCompleteDVF p n).valuation.valuationSubring) :
    (padicCompletedUnitFrobeniusLiftEquiv p n u).symm x ∈
      (padicCompletedLevelCompleteDVF p n).valuation.valuationSubring
theorem

padicCompletedUnitFrobeniusLiftEquiv_mem_valuationSubring_iff

L259 ↗
LubinTate.padicCompletedUnitFrobeniusLiftEquiv_mem_valuationSubring_iff
Documentation

Membership in the selected completed-level valuation ring is invariant under every unit-indexed completed Frobenius lift.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusLiftEquiv_mem_valuationSubring_iff
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x : padicCompletedLevelField p n) :
    x ∈ (padicCompletedLevelCompleteDVF p n).valuation.valuationSubring ↔
      padicCompletedUnitFrobeniusLiftEquiv p n u x ∈
        (padicCompletedLevelCompleteDVF p n).valuation.valuationSubring
def

padicCompletedUnitFrobeniusIntegerEquiv

L277 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv
Documentation

The actual valuation-ring automorphism induced by a unit-indexed completed Frobenius lift.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
def padicCompletedUnitFrobeniusIntegerEquiv
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    (padicCompletedLevelCompleteDVF p n).valuationSubring ≃+*
      (padicCompletedLevelCompleteDVF p n).valuationSubring
theorem

padicCompletedUnitFrobeniusIntegerEquiv_coe

L291 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_coe
Documentation

Coercion of the integral completed Frobenius restriction agrees with the ambient field automorphism.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusIntegerEquiv_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring) :
    ((padicCompletedUnitFrobeniusIntegerEquiv p n u x :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
      padicCompletedLevelField p n) =
      padicCompletedUnitFrobeniusLiftEquiv p n u
        (x : padicCompletedLevelField p n)
theorem

padicCompletedUnitFrobeniusIntegerEquiv_symm_coe

L305 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_symm_coe
Documentation

Coercion of the inverse integral completed Frobenius restriction agrees with the inverse ambient field automorphism.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusIntegerEquiv_symm_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring) :
    (((padicCompletedUnitFrobeniusIntegerEquiv p n u).symm x :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
      padicCompletedLevelField p n) =
      (padicCompletedUnitFrobeniusLiftEquiv p n u).symm
        (x : padicCompletedLevelField p n)
theorem

padicCompletedUnitFrobeniusIntegerEquiv_continuous

L323 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_continuous
Documentation

The integral completed Frobenius restriction is continuous for the maximal-ideal adic topology.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusIntegerEquiv_continuous
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    Continuous (padicCompletedUnitFrobeniusIntegerEquiv p n u)
theorem

padicCompletedUnitFrobeniusIntegerEquiv_wittCoefficientHom

L352 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_wittCoefficientHom
Documentation

The integral completed Frobenius restriction transports the canonical Witt coefficient map by Witt-vector Frobenius.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusIntegerEquiv_wittCoefficientHom
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (a : padicCompletedUnramifiedWittRing p) :
    padicCompletedUnitFrobeniusIntegerEquiv p n u
        (padicCompletedLevelWittCoefficientHom p n a) =
      padicCompletedLevelWittCoefficientHom p n
        (WittVector.frobenius a)
theorem

padicCompletedHasEval_map_continuous

L375 ↗
LubinTate.padicCompletedHasEval_map_continuous
Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedHasEval_map_continuous
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (r :
      (padicCompletedLevelCompleteDVF p n).valuationSubring →+*
        (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hr : Continuous r)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    PowerSeries.HasEval (r x)
theorem

padicCompletedUnitFrobeniusIntegerEquiv_hasEval

L388 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_hasEval
Documentation

A convergent completed-level evaluation point remains convergent after applying the integral completed Frobenius restriction.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusIntegerEquiv_hasEval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x) :
    PowerSeries.HasEval
      (padicCompletedUnitFrobeniusIntegerEquiv p n u x)
theorem

padicCompletedUnitFrobeniusIntegerEquiv_evaluation

L403 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_evaluation
Documentation

Convergent completed-level evaluation is semilinear for every unit-indexed completed Frobenius lift: the point is acted on by the integral lift and coefficients by Witt Frobenius.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusIntegerEquiv_evaluation
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (f : PowerSeries (padicCompletedUnramifiedWittRing p)) :
    padicCompletedUnitFrobeniusIntegerEquiv p n u
        (padicCompletedLevelPowerSeriesEval p n x hx f) =
      padicCompletedLevelPowerSeriesEval p n
        (padicCompletedUnitFrobeniusIntegerEquiv p n u x)
        (padicCompletedUnitFrobeniusIntegerEquiv_hasEval p n u x hx)
        (PowerSeries.map WittVector.frobenius f)
theorem

padicCompletedUnitFrobeniusIntegerEquiv_primitiveRoot

L452 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_primitiveRoot
Documentation

The integral completed Frobenius restriction sends the chosen primitive point to its actual completed standard unit translate.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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 padicCompletedUnitFrobeniusIntegerEquiv_primitiveRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedUnitFrobeniusIntegerEquiv p n u
        (padicCompletedPrimitiveRootInteger p n) =
      padicCompletedStandardPrimitivePointUnitAction p n u
theorem

padicCompletedUnitFrobeniusIntegerEquiv_multiplicativePrimitivePoint

L470 ↗
LubinTate.padicCompletedUnitFrobeniusIntegerEquiv_multiplicativePrimitivePoint
Documentation

The integral completed Frobenius restriction sends the genuine multiplicative primitive point to its actual multiplicative unit translate.

Source context 10 commands

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

noncomputable section
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
private noncomputable local instance (priority := 50)
    padicCompletedFrobeniusEvaluationWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicCompletedFrobeniusEvaluationTargetCompleteSpace
    (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
    padicCompletedFrobeniusEvaluationTargetT2Space
    (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
    padicCompletedUnitFrobeniusIntegerEquiv_multiplicativePrimitivePoint
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    padicCompletedUnitFrobeniusIntegerEquiv p n u
        (padicCompletedMultiplicativePrimitivePoint p n) =
      padicCompletedMultiplicativePrimitivePointUnitAction p u n

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