NYLL
Module

ThetaLocalInverse.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.ThetaLocalInverse
21 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: local injectivity of theta

The theta series has a unit linear coefficient and integral higher coefficients. This file records the resulting nonarchimedean local isometry on the maximal ideal.

Imports2
Imported by4

Declarations

theorem

norm_finset_sum_le_of_norm_le

L34 ↗
LubinTate.EqualCharacteristic.norm_finset_sum_le_of_norm_le
Source context 7 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
Lean source · statement
theorem norm_finset_sum_le_of_norm_le
    [SeminormedAddCommGroup E] [IsUltrametricDist E]
    {f : ι → E} (t : Finset ι) {C : ℝ}
    (hC : 0 ≤ C) (hf : ∀ i ∈ t, ‖f i‖ ≤ C) :
    ‖∑ i ∈ t, f i‖ ≤ C
theorem

norm_le_of_hasSum_of_norm_le

L50 ↗
LubinTate.EqualCharacteristic.norm_le_of_hasSum_of_norm_le
Documentation

A convergent series in an ultrametric group has norm bounded by any common bound for all its terms.

Source context 7 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
Lean source · statement
theorem norm_le_of_hasSum_of_norm_le
    [SeminormedAddCommGroup E] [IsUltrametricDist E]
    {f : ι → E} {s : E} {C : ℝ}
    (hC : 0 ≤ C) (hf : ∀ i, ‖f i‖ ≤ C) (hs : HasSum f s) :
    ‖s‖ ≤ C
theorem

norm_geomSum₂_le_max

L67 ↗
LubinTate.EqualCharacteristic.norm_geomSum₂_le_max
Documentation

The two-variable geometric factor in x^n-y^n is bounded by the larger of ‖x‖ and ‖y‖ on the open unit ball, once n ≥ 2.

Source context 7 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
Lean source · statement
theorem norm_geomSum₂_le_max
    {L : Type*} [NontriviallyNormedField L] [IsUltrametricDist L]
    (x y : Valued.integer L) (n : ℕ) (hn : 2 ≤ n)
    (hx : ‖x‖ < 1) (hy : ‖y‖ < 1) :
    ‖∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)‖ ≤
      max ‖x‖ ‖y‖
theorem

norm_pow_sub_pow_le_max_mul_norm_sub

L99 ↗
LubinTate.EqualCharacteristic.norm_pow_sub_pow_le_max_mul_norm_sub
Documentation

Higher power differences contract strictly relative to x-y on the open unit ball.

Source context 7 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
Lean source · statement
theorem norm_pow_sub_pow_le_max_mul_norm_sub
    {L : Type*} [NontriviallyNormedField L] [IsUltrametricDist L]
    (x y : Valued.integer L) (n : ℕ) (hn : 2 ≤ n)
    (hx : ‖x‖ < 1) (hy : ‖y‖ < 1) :
    ‖x ^ n - y ^ n‖ ≤ max ‖x‖ ‖y‖ * ‖x - y‖
theorem

integralPowerSeriesEvaluation_norm_sub

L113 ↗
LubinTate.EqualCharacteristic.integralPowerSeriesEvaluation_norm_sub
Documentation

Nonarchimedean inverse-function estimate for an integral power series.

The coefficient sequence is valued in the valuation ring. A unit linear coefficient makes any two convergent evaluations on the open unit ball an isometry. No characteristic assumption is needed.

Source context 7 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
Lean source · full declaration
theorem integralPowerSeriesEvaluation_norm_sub
    {L : Type*} [NontriviallyNormedField L] [IsUltrametricDist L]
    (c : ℕ → Valued.integer L) (hc₁ : IsUnit (c 1))
    (x y fx fy : Valued.integer L)
    (hx : ‖x‖ < 1) (hy : ‖y‖ < 1)
    (hfx : HasSum (fun m : ℕ ↦ c m * x ^ m) fx)
    (hfy : HasSum (fun m : ℕ ↦ c m * y ^ m) fy) :
    ‖fx - fy‖ = ‖x - y‖ := by
  by_cases hxy : x = y
  · subst y
    have hvalue : fx = fy := hfx.unique hfy
    subst fy
    simp
  let term : ℕ → Valued.integer L :=
    fun m ↦ c m * x ^ m - c m * y ^ m
  let linear : Valued.integer L := c 1 * (x - y)
  let remainder : Valued.integer L := (fx - fy) - linear
  let r : ℝ := max ‖x‖ ‖y‖
  have hr0 : 0 ≤ r := le_trans (norm_nonneg x) (le_max_left _ _)
  have hr1 : r < 1 := max_lt hx hy
  have hdiff : HasSum term (fx - fy) := by
    simpa only [term] using hfx.sub hfy
  have hprefix : ∑ i ∈ Finset.range 2, term i = linear := by
    simp only [Finset.sum_range_succ, Finset.sum_range_zero, zero_add]
    dsimp only [term, linear]
    ring
  have htail : HasSum (fun m : ℕ ↦ term (m + 2)) remainder := by
    have h := (hasSum_nat_add_iff' (f := term) 2).2 hdiff
    rwa [hprefix] at h
  have htermBound : ∀ m : ℕ,
      ‖term (m + 2)‖ ≤ r * ‖x - y‖ := by
    intro m
    change ‖c (m + 2) * x ^ (m + 2) -
      c (m + 2) * y ^ (m + 2)‖ ≤ r * ‖x - y‖
    rw [← mul_sub, norm_mul]
    calc
      ‖c (m + 2)‖ * ‖x ^ (m + 2) - y ^ (m + 2)‖ ≤
          1 * (r * ‖x - y‖) :=
        mul_le_mul (Valued.integer.norm_le_one _) (by
          simpa only [r] using
            norm_pow_sub_pow_le_max_mul_norm_sub x y (m + 2) (by omega) hx hy)
          (norm_nonneg _) zero_le_one
      _ = r * ‖x - y‖ := one_mul _
  have hremainder_le : ‖remainder‖ ≤ r * ‖x - y‖ :=
    norm_le_of_hasSum_of_norm_le
      (mul_nonneg hr0 (norm_nonneg (x - y))) htermBound htail
  have hsubpos : 0 < ‖x - y‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hxy)
  have hremainder_lt : ‖remainder‖ < ‖x - y‖ :=
    hremainder_le.trans_lt (by
      simpa only [one_mul] using mul_lt_mul_of_pos_right hr1 hsubpos)
  have hlinear : ‖linear‖ = ‖x - y‖ := by
    change ‖c 1 * (x - y)‖ = ‖x - y‖
    rw [norm_mul,
      (Valued.integer.isUnit_iff_norm_eq_one.mp hc₁), one_mul]
  have hdecomp : fx - fy = linear + remainder := by
    simp [remainder]
  rw [hdecomp]
  calc
    ‖linear + remainder‖ = max ‖linear‖ ‖remainder‖ :=
      IsUltrametricDist.norm_add_eq_max_of_norm_ne_norm
        (hlinear.trans_ne hremainder_lt.ne')
    _ = ‖x - y‖ := by
      rw [hlinear, max_eq_left hremainder_lt.le]
theorem

integralPowerSeriesEvaluation_injectiveOn

L179 ↗
LubinTate.EqualCharacteristic.integralPowerSeriesEvaluation_injectiveOn
Documentation

Consequently, any analytic evaluation with integral coefficients and unit linear coefficient is injective on the open unit ball.

Source context 7 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
Lean source · full declaration
theorem integralPowerSeriesEvaluation_injectiveOn
    {L : Type*} [NontriviallyNormedField L] [IsUltrametricDist L]
    (c : ℕ → Valued.integer L) (hc₁ : IsUnit (c 1))
    (eval : Valued.integer L → Valued.integer L)
    (hsum : ∀ x : Valued.integer L, ‖x‖ < 1 →
      HasSum (fun m : ℕ ↦ c m * x ^ m) (eval x)) :
    Set.InjOn eval {x | ‖x‖ < 1} := by
  intro x hx y hy hxy
  have hnorm := integralPowerSeriesEvaluation_norm_sub c hc₁ x y
    (eval x) (eval y) hx hy (hsum x hx) (hsum y hy)
  rw [hxy, sub_self, norm_zero] at hnorm
  exact sub_eq_zero.mp (norm_eq_zero.mp hnorm.symm)
instance

equalCharacteristicThetaInverseLevelNormedField

L196 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseLevelNormedField
Source context 9 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n)
instance

equalCharacteristicThetaInverseLevelIsUltrametric

L201 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseLevelIsUltrametric
Source context 10 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
Lean source · statement
instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n)
instance

equalCharacteristicThetaInverseLevelCompleteSpace

L206 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseLevelCompleteSpace
Source context 11 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
Lean source · statement
instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n)
instance

equalCharacteristicThetaInverseLevelValued

L211 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseLevelValued
Source context 12 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
Lean source · statement
instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0
instance

equalCharacteristicThetaInverseIntegerLinearTopology

L216 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseIntegerLinearTopology
Source context 13 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
Lean source · statement
instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
instance

equalCharacteristicThetaInverseIntegerCompleteSpace

L223 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseIntegerCompleteSpace
Source context 14 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
Lean source · statement
instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
instance

equalCharacteristicThetaInverseIntegerUniformAddGroup

L229 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseIntegerUniformAddGroup
Source context 15 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
Lean source · statement
instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
instance

equalCharacteristicThetaInverseCoefficientUniformSpace

L235 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseCoefficientUniformSpace
Source context 16 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
Lean source · statement
instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧)
theorem

equalCharacteristicThetaInverseCoefficientHom_continuous

L239 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaInverseCoefficientHom_continuous
Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
Lean source · statement
theorem equalCharacteristicThetaInverseCoefficientHom_continuous
    (F : LocalField.{u, v} K) (n : ℕ) :
    Continuous (equalCharacteristicCompletedLevelCoefficientHom F n)
theorem

equalCharacteristicCompletedLevel_hasEval_of_norm_lt_one

L246 ↗
LubinTate.EqualCharacteristic.equalCharacteristicCompletedLevel_hasEval_of_norm_lt_one
Documentation

Norm < 1 supplies the analytic evaluation hypothesis for a point in the completed-level valuation ring.

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
Lean source · statement
theorem equalCharacteristicCompletedLevel_hasEval_of_norm_lt_one
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : Valued.integer (equalCharacteristicCompletedLevelField F n))
    (hx : ‖x‖ < 1) :
    PowerSeries.HasEval x
theorem

equalCharacteristicThetaCompletedCoefficientOne_isUnit

L256 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaCompletedCoefficientOne_isUnit
Documentation

The linear coefficient of theta stays a unit after inclusion into any completed level valuation ring.

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
Lean source · statement
theorem equalCharacteristicThetaCompletedCoefficientOne_isUnit
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    IsUnit
      (equalCharacteristicCompletedLevelCoefficientHom F n
        (PowerSeries.coeff 1 (equalCharacteristicThetaSeries u)))
def

equalCharacteristicThetaOnCompletedLevelMaximalIdeal

L277 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaOnCompletedLevelMaximalIdeal
Documentation

Theta evaluated at an arbitrary point of the completed-level maximal ideal.

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
Lean source · statement
def equalCharacteristicThetaOnCompletedLevelMaximalIdeal
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x : {x : Valued.integer (equalCharacteristicCompletedLevelField F n) //
      ‖x‖ < 1}) :
    Valued.integer (equalCharacteristicCompletedLevelField F n)
theorem

equalCharacteristicThetaOnCompletedLevelMaximalIdeal_hasSum

L287 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaOnCompletedLevelMaximalIdeal_hasSum
Documentation

States the theorem equalCharacteristicThetaOnCompletedLevelMaximalIdeal_hasSum.

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
Lean source · full declaration
theorem equalCharacteristicThetaOnCompletedLevelMaximalIdeal_hasSum
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x : {x : Valued.integer (equalCharacteristicCompletedLevelField F n) //
      ‖x‖ < 1}) :
    HasSum
      (fun m : ℕ ↦
        equalCharacteristicCompletedLevelCoefficientHom F n
            (PowerSeries.coeff m (equalCharacteristicThetaSeries u)) *
          (x : Valued.integer
            (equalCharacteristicCompletedLevelField F n)) ^ m)
      (equalCharacteristicThetaOnCompletedLevelMaximalIdeal F u n x) := by
  rw [equalCharacteristicThetaOnCompletedLevelMaximalIdeal,
    equalCharacteristicCompletedLevelEvaluation,
    PowerSeries.coe_eval₂Hom]
  exact PowerSeries.hasSum_eval₂
    (equalCharacteristicThetaInverseCoefficientHom_continuous F n)
    (equalCharacteristicCompletedLevel_hasEval_of_norm_lt_one F n x x.property)
    (equalCharacteristicThetaSeries u)
theorem

equalCharacteristicThetaOnCompletedLevelMaximalIdeal_norm_sub

L308 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaOnCompletedLevelMaximalIdeal_norm_sub
Documentation

The faithful analytic conclusion used in the completed theta-intertwining theorem: theta is a local isometry, hence injective, on the completed-level maximal ideal.

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
Lean source · statement
theorem equalCharacteristicThetaOnCompletedLevelMaximalIdeal_norm_sub
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ)
    (x y : {x : Valued.integer (equalCharacteristicCompletedLevelField F n) //
      ‖x‖ < 1}) :
    ‖equalCharacteristicThetaOnCompletedLevelMaximalIdeal F u n x -
        equalCharacteristicThetaOnCompletedLevelMaximalIdeal F u n y‖ =
      ‖(x : Valued.integer (equalCharacteristicCompletedLevelField F n)) - y‖
theorem

equalCharacteristicThetaOnCompletedLevelMaximalIdeal_injective

L328 ↗
LubinTate.EqualCharacteristic.equalCharacteristicThetaOnCompletedLevelMaximalIdeal_injective
Documentation

States the theorem equalCharacteristicThetaOnCompletedLevelMaximalIdeal_injective.

Source context 17 commands

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

noncomputable section
open Filter
open scoped LaurentSeries NNReal NormedField PowerSeries
  PowerSeries.WithPiTopology Topology Valued WithZero
universe u v w
namespace LubinTate
namespace EqualCharacteristic
variable {ι E : Type*}
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicThetaInverseLevelNormedField
    (F : LocalField.{u, v} K) (n : ℕ) :
    NontriviallyNormedField (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelNormedField F n
noncomputable local instance equalCharacteristicThetaInverseLevelIsUltrametric
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUltrametricDist (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelIsUltrametric F n
noncomputable local instance equalCharacteristicThetaInverseLevelCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace (equalCharacteristicCompletedLevelField F n) :=
  equalCharacteristicCompletedLevelCompleteSpace F n
noncomputable local instance equalCharacteristicThetaInverseLevelValued
    (F : LocalField.{u, v} K) (n : ℕ) :
    Valued (equalCharacteristicCompletedLevelField F n) ℝ≥0 :=
  equalCharacteristicCompletedLevelValued F n
noncomputable local instance equalCharacteristicThetaInverseIntegerLinearTopology
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsLinearTopology
      (Valued.integer (equalCharacteristicCompletedLevelField F n))
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerLinearTopology
noncomputable local instance equalCharacteristicThetaInverseIntegerCompleteSpace
    (F : LocalField.{u, v} K) (n : ℕ) :
    CompleteSpace
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerCompleteSpace
noncomputable local instance equalCharacteristicThetaInverseIntegerUniformAddGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    IsUniformAddGroup
      (Valued.integer (equalCharacteristicCompletedLevelField F n)) :=
  valuedIntegerIsUniformAddGroup
private noncomputable local instance equalCharacteristicThetaInverseCoefficientUniformSpace
    (F : LocalField.{u, v} K) :
    UniformSpace ((AlgebraicClosure F.residueField)⟦X⟧) := ⊥
Lean source · statement
theorem equalCharacteristicThetaOnCompletedLevelMaximalIdeal_injective
    (F : LocalField.{u, v} K) (u : F.residueField⟦X⟧ˣ) (n : ℕ) :
    Function.Injective
      (equalCharacteristicThetaOnCompletedLevelMaximalIdeal F u n)

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