NYLL
Module

CompletedFrobeniusContinuity.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedFrobeniusContinuity
15 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: continuity of the standard completed Frobenius lift

For every prescribed bracket unit a, pullback of the completed-level spectral norm along the semilinear Frobenius lift is a power-multiplicative algebra norm extending the original norm of the completed maximal-unramified base. Spectral-norm uniqueness therefore makes the lift an isometry and in particular continuous. We also name the a = u⁻¹ specialization used directly in the completed theta-intertwining theorem.

Imports1
Imported by5

Declarations

instance

equalCharacteristicFrobeniusContinuityBaseAlgebra

L36 ↗
LubinTate.EqualCharacteristic.equalCharacteristicFrobeniusContinuityBaseAlgebra
Source context 7 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)
instance

equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial

L42 ↗
LubinTate.EqualCharacteristic.equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
Source context 8 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
Lean source · statement
instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial
instance

equalCharacteristicFrobeniusContinuityBaseValuationRankOne

L49 ↗
LubinTate.EqualCharacteristic.equalCharacteristicFrobeniusContinuityBaseValuationRankOne
Source context 9 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
Lean source · statement
instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne
instance

equalCharacteristicFrobeniusContinuityBaseNormedField

L57 ↗
LubinTate.EqualCharacteristic.equalCharacteristicFrobeniusContinuityBaseNormedField
Source context 10 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
Lean source · statement
instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k)
instance

equalCharacteristicFrobeniusContinuityLevelNormedField

L64 ↗
LubinTate.EqualCharacteristic.equalCharacteristicFrobeniusContinuityLevelNormedField
Source context 11 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
Lean source · statement
instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicCompletedFrobeniusBase_norm

L70 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusBase_norm
Documentation

Base arithmetic Frobenius preserves the rank-one norm.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusBase_norm
    (F : LocalField.{u, v} K)
    (b : equalCharacteristicCompletedUnramifiedField F.residueField) :
    ‖equalCharacteristicCompletedUnramifiedFrobenius F.residueField b‖ =
      ‖b‖
def

equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm

L86 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm
Documentation

Pullback of the standard completed-level spectral norm by the prescribed-bracket Frobenius lift.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · full declaration
def equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    AlgebraNorm
      (equalCharacteristicCompletedUnramifiedField F.residueField)
      (equalCharacteristicCompletedLevelField F n) where
  toFun x := ‖equalCharacteristicCompletedFrobeniusLiftEquiv F n a x‖
  map_zero' := by simp
  add_le' x y := by
    rw [map_add]
    exact norm_add_le _ _
  neg' x := by simp
  mul_le' x y := by
    rw [map_mul, norm_mul]
  eq_zero_of_map_eq_zero' x hx := by
    apply (equalCharacteristicCompletedFrobeniusLiftEquiv F n a).injective
    rw [map_zero]
    exact norm_eq_zero.mp hx
  smul' b x := by
    rw [Algebra.smul_def, map_mul,
      equalCharacteristicCompletedFrobeniusLiftEquiv_algebraMap,
      norm_mul]
    congr 1
    change spectralNorm
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)
        (algebraMap
          (equalCharacteristicCompletedUnramifiedField F.residueField)
          (equalCharacteristicCompletedLevelField F n)
          (equalCharacteristicCompletedUnramifiedFrobenius
            F.residueField b)) = ‖b‖
    rw [spectralNorm_extends,
      equalCharacteristicCompletedFrobeniusBase_norm]
theorem

equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm_isPowMul

L122 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm_isPowMul
Documentation

The pulled-back norm is power-multiplicative.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm_isPowMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    IsPowMul (equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm F n a)
theorem

equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm_eq

L135 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm_eq
Documentation

Spectral-norm uniqueness identifies the pullback norm with the original completed-level norm.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm_eq
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicCompletedFrobeniusPullbackAlgebraNorm F n a =
      spectralAlgNorm
        (equalCharacteristicCompletedUnramifiedField F.residueField)
        (equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicCompletedFrobeniusLiftEquiv_norm

L148 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftEquiv_norm
Documentation

Every prescribed-bracket standard completed Frobenius lift preserves the spectral norm.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLiftEquiv_norm
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ)
    (x : equalCharacteristicCompletedLevelField F n) :
    ‖equalCharacteristicCompletedFrobeniusLiftEquiv F n a x‖ = ‖x‖
theorem

equalCharacteristicCompletedFrobeniusLiftEquiv_isometry

L164 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftEquiv_isometry
Documentation

Every prescribed-bracket standard completed Frobenius lift is an isometry.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLiftEquiv_isometry
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    Isometry (equalCharacteristicCompletedFrobeniusLiftEquiv F n a)
theorem

equalCharacteristicCompletedFrobeniusLiftEquiv_continuous

L175 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLiftEquiv_continuous
Documentation

Every prescribed-bracket standard completed Frobenius lift is continuous for the spectral-norm topology.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLiftEquiv_continuous
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    Continuous (equalCharacteristicCompletedFrobeniusLiftEquiv F n a)
theorem

equalCharacteristicCompletedFrobeniusLift_norm

L183 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLift_norm
Documentation

The completed theta-intertwining theorem specialization preserves the spectral norm.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLift_norm
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x : equalCharacteristicCompletedLevelField F n) :
    ‖equalCharacteristicCompletedFrobeniusLiftEquiv F n u⁻¹ x‖ = ‖x‖
theorem

equalCharacteristicCompletedFrobeniusLift_isometry

L192 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLift_isometry
Documentation

The completed theta-intertwining theorem specialization is an isometry.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLift_isometry
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Isometry (equalCharacteristicCompletedFrobeniusLiftEquiv F n u⁻¹)
theorem

equalCharacteristicCompletedFrobeniusLift_continuous

L202 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedFrobeniusLift_continuous
Documentation

The completed theta-intertwining theorem specialization is continuous for the standard completed-level spectral-norm topology.

Source context 12 commands

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

noncomputable section
open scoped LaurentSeries NNReal Polynomial PowerSeries Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationIsNontrivial
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).IsNontrivial :=
  equalCharacteristicCompletedBaseValuationIsNontrivial k
noncomputable local instance
    equalCharacteristicFrobeniusContinuityBaseValuationRankOne
    (k : Type v) [Field k] :
    (Valued.v : Valuation
      (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰).RankOne :=
  equalCharacteristicCompletedBaseValuationRankOne k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityBaseNormedField
    (k : Type v) [Field k] :
    NontriviallyNormedField
      (equalCharacteristicCompletedUnramifiedField k) :=
  equalCharacteristicCompletedBaseNormedField k
@[reducible]
noncomputable local instance equalCharacteristicFrobeniusContinuityLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
theorem equalCharacteristicCompletedFrobeniusLift_continuous
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Continuous (equalCharacteristicCompletedFrobeniusLiftEquiv F n u⁻¹)

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