NYLL
Module

CompletedStandardLevelTransport.lean

Nyll.ClassFieldTheory.LubinTate.Padic.CompletedStandardLevelTransport
22 declarations indexed from sourceView source ↗

Module documentation

Transporting a finite p-adic Lubin--Tate level to the completed level

The ordinary standard Lubin--Tate level embeds in the completed level by sending its primitive generator to the chosen completed primitive point. This file proves that the embedding also preserves the integral analytic action. In particular, the direct completed action of a p-adic unit is the image of the finite action with the same unit-parameter class.

This fixes the parameter orientation before the completed Frobenius is used in the changed-uniformizer norm argument.

Imports2
Imported by2

Declarations

instance

padicStandardLevelTransportCoefficientUniformSpace

L36 ↗
LubinTate.padicStandardLevelTransportCoefficientUniformSpace
Source context 7 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
Lean source · statement
instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring
instance

padicStandardLevelTransportCoefficientTopologicalSpace

L42 ↗
LubinTate.padicStandardLevelTransportCoefficientTopologicalSpace
Source context 8 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
Lean source · statement
instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring
instance

padicStandardLevelTransportWittUniformSpace

L48 ↗
LubinTate.padicStandardLevelTransportWittUniformSpace
Source context 9 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
Lean source · statement
instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p)
instance

padicStandardLevelTransportSourceWithIdeal

L54 ↗
LubinTate.padicStandardLevelTransportSourceWithIdeal
Source context 10 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
Lean source · full declaration
instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
instance

padicStandardLevelTransportTargetWithIdeal

L66 ↗
LubinTate.padicStandardLevelTransportTargetWithIdeal
Source context 11 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
Lean source · full declaration
instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
instance

padicStandardLevelTransportSourceCompleteSpace

L73 ↗
LubinTate.padicStandardLevelTransportSourceCompleteSpace
Source context 12 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
Lean source · statement
instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring
instance

padicStandardLevelTransportSourceT2Space

L86 ↗
LubinTate.padicStandardLevelTransportSourceT2Space
Source context 13 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
Lean source · statement
instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring
instance

padicStandardLevelTransportTargetCompleteSpace

L99 ↗
LubinTate.padicStandardLevelTransportTargetCompleteSpace
Source context 14 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
Lean source · statement
instance
    padicStandardLevelTransportTargetCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (padicCompletedLevelCompleteDVF p n).valuationSubring
instance

padicStandardLevelTransportTargetT2Space

L108 ↗
LubinTate.padicStandardLevelTransportTargetT2Space
Source context 15 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring
def

padicStandardLevelIntegerEmbedding

L119 ↗
LubinTate.padicStandardLevelIntegerEmbedding
Documentation

The standard finite-level embedding restricted to the actual valuation rings.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicStandardLevelIntegerEmbedding
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    (standardLubinTateLevelCompleteDVF hπ n).valuationSubring →+*
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let F := padicLocalField p
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let source := standardLubinTateLevelCompleteDVF hπ n
  let A := padicCompletedUnramifiedCompleteDVF p
  let E := padicCompletedLevelField p n
  let target := padicCompletedLevelCompleteDVF p n
  let ι : L →ₐ[ℚ_[p]] E := padicStandardLevelEmbedding p n
  letI : F.valuation.HasExtension source.valuation :=
    standardLubinTateLevelCompleteDVF_hasExtension
      (F := padicLocalField p)
      (π := padicIntEquivValuationSubring p (p : ℤ_[p])) hπ n
  letI : Algebra F.valuationSubring source.valuationSubring :=
    Valuation.HasExtension.instAlgebra_valuationSubring
      (padicLocalField p).valuation
      (standardLubinTateLevelCompleteDVF
        (F := padicLocalField p)
        (π := padicIntEquivValuationSubring p (p : ℤ_[p])) hπ n).valuation
  letI : IsScalarTower F.valuationSubring source.valuationSubring L :=
    IsScalarTower.of_algebraMap_eq' rfl
  letI : IsIntegralClosure
      source.valuationSubring F.valuationSubring L :=
    standardLubinTateLevelCompleteDVF_isIntegralClosure hπ n
  letI : IsScalarTower A.valuationSubring target.valuationSubring E :=
    IsScalarTower.of_algebraMap_eq' rfl
  letI : IsIntegralClosure
      target.valuationSubring A.valuationSubring E :=
    padicCompletedLevelCompleteDVF_isIntegralClosure p n
  let f : source.valuationSubring →+* E :=
    ι.toRingHom.comp source.valuation.valuationSubring.subtype
  apply RingHom.codRestrict f target.valuation.valuationSubring
  intro x
  have hxIntegral :
      IsIntegral F.valuationSubring (x.val : L) :=
    (IsIntegralClosure.isIntegral_iff
      (A := source.valuationSubring)
      (R := F.valuationSubring)
      (B := L)).2 ⟨x, rfl⟩
  have hcomp :
      (algebraMap A.valuationSubring E).comp
          (padicCompletedUnramifiedIntegerMap p) =
        ι.toRingHom.comp (algebraMap F.valuationSubring L) := by
    ext a
    simp only [RingHom.comp_apply]
    change
      algebraMap (padicCompletedUnramifiedField p) E
          ((padicCompletedUnramifiedIntegerMap p a :
            A.valuationSubring) :
              padicCompletedUnramifiedField p) =
        ι (algebraMap ℚ_[p] L (a : ℚ_[p]))
    rw [padicCompletedUnramifiedIntegerMap_coe]
    calc
      algebraMap (padicCompletedUnramifiedField p) E
          (algebraMap ℚ_[p]
            (padicCompletedUnramifiedField p) (a : ℚ_[p])) =
          algebraMap ℚ_[p] E (a : ℚ_[p]) :=
        (IsScalarTower.algebraMap_apply ℚ_[p]
          (padicCompletedUnramifiedField p) E (a : ℚ_[p])).symm
      _ = ι (algebraMap ℚ_[p] L (a : ℚ_[p])) :=
        (ι.commutes (a : ℚ_[p])).symm
  have hxMappedIntegral :
      IsIntegral A.valuationSubring (ι (x.val : L)) :=
    IsIntegral.map_of_comp_eq
      (padicCompletedUnramifiedIntegerMap p)
      ι.toRingHom hcomp hxIntegral
  rcases
      (IsIntegralClosure.isIntegral_iff
        (A := target.valuationSubring)
        (R := A.valuationSubring)
        (B := E)).1 hxMappedIntegral with
    ⟨z, hz⟩
  change target.valuation (ι (x.val : L)) ≤ 1
  rw [← hz]
  exact z.property
theorem

padicStandardLevelIntegerEmbedding_coe

L202 ↗
LubinTate.padicStandardLevelIntegerEmbedding_coe
Documentation

Coercing the integral standard-level embedding to the completed field recovers the field embedding.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicStandardLevelIntegerEmbedding_coe
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x :
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring) :
    ((padicStandardLevelIntegerEmbedding p n x :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
      padicCompletedLevelField p n) =
        padicStandardLevelEmbedding p n
          (x.val :
            standardLubinTateLevelField
              (padicMultiplicativeLubinTateSeries_isUniformizer p) n)
theorem

padicStandardLevelIntegerEmbedding_apply_primitivePoint

L219 ↗
LubinTate.padicStandardLevelIntegerEmbedding_apply_primitivePoint
Documentation

The integral embedding sends the finite primitive point to the chosen completed primitive point.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicStandardLevelIntegerEmbedding_apply_primitivePoint
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    padicStandardLevelIntegerEmbedding p n
        (standardLubinTatePrimitivePointInteger hπ n) =
      padicCompletedPrimitiveRootInteger p n := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  apply Subtype.ext
  rw [padicStandardLevelIntegerEmbedding_coe,
    padicCompletedPrimitiveRootInteger_coe]
  have hpoint := congrArg (padicStandardLevelEmbedding p n)
    (standardLubinTatePrimitivePointInteger_coe
      (F := padicLocalField p) hπ n)
  exact hpoint.trans (padicStandardLevelEmbedding_apply_gen p n)
theorem

padicStandardLevelIntegerEmbedding_continuous

L236 ↗
LubinTate.padicStandardLevelIntegerEmbedding_continuous
Documentation

The integral standard-level embedding is continuous for the two maximal-ideal adic topologies.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicStandardLevelIntegerEmbedding_continuous
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    Continuous (padicStandardLevelIntegerEmbedding p n)
theorem

padicStandardLevelIntegerEmbedding_comp_coefficientHom

L263 ↗
LubinTate.padicStandardLevelIntegerEmbedding_comp_coefficientHom
Documentation

The integral embedding commutes with the canonical maps of p-adic integer coefficients.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicStandardLevelIntegerEmbedding_comp_coefficientHom
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    (padicStandardLevelIntegerEmbedding p n).comp
        (standardLubinTateLevelCoefficientHom hπ n) =
      padicCompletedLevelPadicIntegerCoefficientHom p n := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  let L := standardLubinTateLevelField hπ n
  let E := padicCompletedLevelField p n
  ext a
  simp only [RingHom.comp_apply,
    padicStandardLevelIntegerEmbedding_coe,
    padicCompletedLevelPadicIntegerCoefficientHom_coe]
  change
    padicStandardLevelEmbedding p n
        (algebraMap ℚ_[p] L (a : ℚ_[p])) =
      algebraMap (padicCompletedUnramifiedField p) E
        (algebraMap ℚ_[p]
          (padicCompletedUnramifiedField p) (a : ℚ_[p]))
  rw [(padicStandardLevelEmbedding p n).commutes,
    ← IsScalarTower.algebraMap_apply ℚ_[p]
      (padicCompletedUnramifiedField p) E]
theorem

padicCompletedLevelPowerSeriesEval_map_padicCoefficients

L288 ↗
LubinTate.padicCompletedLevelPowerSeriesEval_map_padicCoefficients
Documentation

Evaluation after extending p-adic coefficients to the completed Witt ring is evaluation through the direct p-adic coefficient map.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicCompletedLevelPowerSeriesEval_map_padicCoefficients
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x : (padicCompletedLevelCompleteDVF p n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (f : PowerSeries (padicLocalField p).valuationSubring) :
    padicCompletedLevelPowerSeriesEval p n x hx
        (PowerSeries.map
          (padicValuationSubringToCompletedUnramifiedWittRing p) f) =
      PowerSeries.eval₂
        (padicCompletedLevelPadicIntegerCoefficientHom p n) x f
theorem

padicStandardLevelIntegerEmbedding_powerSeriesEval

L313 ↗
LubinTate.padicStandardLevelIntegerEmbedding_powerSeriesEval
Documentation

Analytic evaluation in the finite standard level commutes with its integral embedding into the completed level.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicStandardLevelIntegerEmbedding_powerSeriesEval
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (x :
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n).valuationSubring)
    (hx : PowerSeries.HasEval x)
    (f : PowerSeries (padicLocalField p).valuationSubring) :
    padicStandardLevelIntegerEmbedding p n
        (standardLubinTateLevelPowerSeriesEval
          (padicMultiplicativeLubinTateSeries_isUniformizer p)
          n x hx f) =
      padicCompletedLevelPowerSeriesEval p n
        (padicStandardLevelIntegerEmbedding p n x)
        (hx.map (padicStandardLevelIntegerEmbedding_continuous p n))
        (PowerSeries.map
          (padicValuationSubringToCompletedUnramifiedWittRing p) f)
theorem

padicStandardLevelIntegerEmbedding_apply_primitivePointUnitAction

L367 ↗
LubinTate.padicStandardLevelIntegerEmbedding_apply_primitivePointUnitAction
Documentation

The integral embedding carries the finite analytic unit action to the direct completed analytic unit action with the same unit.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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
    padicStandardLevelIntegerEmbedding_apply_primitivePointUnitAction
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    padicStandardLevelIntegerEmbedding p n
        (standardLubinTatePrimitivePointIntegerAction hπ n u) =
      padicCompletedStandardPrimitivePointUnitAction p n u := by
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  have h :=
    padicStandardLevelIntegerEmbedding_powerSeriesEval p n
      (standardLubinTatePrimitivePointInteger hπ n)
      (standardLubinTatePrimitivePointInteger_hasEval hπ n)
      (standardLubinTateEndomorphism hπ
        (u : (padicLocalField p).valuationSubring))
  simpa only [
    standardLubinTatePrimitivePointIntegerAction,
    standardLubinTateEndomorphismValue,
    standardLubinTateEndomorphismEvalAt,
    padicCompletedStandardPrimitivePointUnitAction,
    padicCompletedStandardScalarEndomorphismValue,
    padicCompletedStandardScalarEndomorphism,
    padicStandardLevelIntegerEmbedding_apply_primitivePoint] using h
theorem

padicStandardUnitParameterLevelRoot_class

L393 ↗
LubinTate.padicStandardUnitParameterLevelRoot_class
Documentation

At the finite p-adic level, the parameter class of a unit realizes exactly its direct analytic action.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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 padicStandardUnitParameterLevelRoot_class
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    let F := padicLocalField p
    let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
    standardLubinTateUnitParameterLevelRoot F hπ n
        (standardLubinTateUnitParameterClass F n u) =
      standardLubinTatePrimitiveLevelAction hπ n u := by
  let F := padicLocalField p
  let hπ := padicMultiplicativeLubinTateSeries_isUniformizer p
  apply Subtype.ext
  exact (standardLubinTateUnitParameterLevelRoot_coe F hπ n
    (standardLubinTateUnitParameterClass F n u)).trans
      ((standardLubinTateUnitParameterRoot_class F hπ n u).trans
        (standardLubinTatePrimitiveLevelAction_coe
          (F := F) hπ n u).symm)
theorem

padicCompletedStandardPrimitivePointUnitAction_eq_unitParameterRoot

L413 ↗
LubinTate.padicCompletedStandardPrimitivePointUnitAction_eq_unitParameterRoot
Documentation

The direct completed unit action is the completed realization of the same finite unit-parameter class.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (padicCompletedLevelCompleteDVF p n).valuationSubring := by
  let target := padicCompletedLevelCompleteDVF p n
  have hadic : IsAdic target.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp target.isAdicComplete).2
Lean source · statement
theorem
    padicCompletedStandardPrimitivePointUnitAction_eq_unitParameterRoot
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ) :
    ((padicCompletedStandardPrimitivePointUnitAction p n u :
        (padicCompletedLevelCompleteDVF p n).valuationSubring) :
      padicCompletedLevelField p n) =
        padicCompletedUnitParameterRoot p n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u)
theorem

padicCompletedUnitFrobeniusLiftEquiv_standardLevelEmbedding

L463 ↗
LubinTate.padicCompletedUnitFrobeniusLiftEquiv_standardLevelEmbedding
Documentation

The completed unit-indexed Frobenius lift restricts to the finite standard-level automorphism with the same unit-parameter class.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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_standardLevelEmbedding
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x :
      standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n) :
    padicCompletedUnitFrobeniusLiftEquiv p n u
        (padicStandardLevelEmbedding p n x) =
      padicStandardLevelEmbedding p n
        (standardLubinTateUnitParameterAlgEquiv
          (padicLocalField p)
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u) x)
theorem

padicCompletedUnitFrobeniusLiftEquiv_symm_standardLevelEmbedding

L525 ↗
LubinTate.padicCompletedUnitFrobeniusLiftEquiv_symm_standardLevelEmbedding
Documentation

The inverse completed unit-indexed Frobenius lift restricts to the inverse finite unit-parameter automorphism.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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_standardLevelEmbedding
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x :
      standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n) :
    (padicCompletedUnitFrobeniusLiftEquiv p n u).symm
        (padicStandardLevelEmbedding p n x) =
      padicStandardLevelEmbedding p n
        ((standardLubinTateUnitParameterAlgEquiv
          (padicLocalField p)
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u)).symm x)
theorem

padicCompletedInverseUnitFrobeniusLiftEquiv_standardLevelEmbedding

L553 ↗
LubinTate.padicCompletedInverseUnitFrobeniusLiftEquiv_standardLevelEmbedding
Documentation

With the inverse unit as Frobenius-lift parameter, the inverse completed lift acts on the standard finite level by the direct unit parameter. This is the orientation used by the actual local Artin map after changed-uniformizer descent.

Source context 16 commands

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

noncomputable section
open scoped PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
open ValuationTheory.DiscreteValuationField
open SameUniformizer
private noncomputable local instance
    padicStandardLevelTransportCoefficientUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportCoefficientTopologicalSpace
    (p : ℕ) [Fact p.Prime] :
    TopologicalSpace (padicLocalField p).valuationSubring :=
  ⊥
private noncomputable local instance (priority := 50)
    padicStandardLevelTransportWittUniformSpace
    (p : ℕ) [Fact p.Prime] :
    UniformSpace (padicCompletedUnramifiedWittRing p) :=
  ⊥
private noncomputable local instance
    padicStandardLevelTransportSourceWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring where
  i :=
    (standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
    ).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportTargetWithIdeal
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    WithIdeal
      (padicCompletedLevelCompleteDVF p n).valuationSubring where
  i := (padicCompletedLevelCompleteDVF p n).maximalIdeal
private noncomputable local instance
    padicStandardLevelTransportSourceCompleteSpace
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    CompleteSpace
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).1
private noncomputable local instance
    padicStandardLevelTransportSourceT2Space
    (p : ℕ) [Fact p.Prime] (n : ℕ) :
    T2Space
      (standardLubinTateLevelCompleteDVF
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n
      ).valuationSubring := by
  let source :=
    standardLubinTateLevelCompleteDVF
      (padicMultiplicativeLubinTateSeries_isUniformizer p) n
  have hadic : IsAdic source.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp source.isAdicComplete).2
private noncomputable local instance
    padicStandardLevelTransportTargetCompleteSpace
    (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
    padicStandardLevelTransportTargetT2Space
    (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
    padicCompletedInverseUnitFrobeniusLiftEquiv_standardLevelEmbedding
    (p : ℕ) [Fact p.Prime] (n : ℕ)
    (u : (padicLocalField p).valuationSubringˣ)
    (x :
      standardLubinTateLevelField
        (padicMultiplicativeLubinTateSeries_isUniformizer p) n) :
    (padicCompletedUnitFrobeniusLiftEquiv p n u⁻¹).symm
        (padicStandardLevelEmbedding p n x) =
      padicStandardLevelEmbedding p n
        (standardLubinTateUnitParameterAlgEquiv
          (padicLocalField p)
          (padicMultiplicativeLubinTateSeries_isUniformizer p) n
          (standardLubinTateUnitParameterClass
            (padicLocalField p) n u) x)

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