Module

CompletedUnramifiedField.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.CompletedUnramifiedField

46 declarations indexed from sourceView source ↗

Module documentation

The equal-characteristic completed-unramified construction: the completed maximal-unramified

field in equal characteristic

For a finite field k, the equal-characteristic model of the completion of the maximal unramified extension of k((T)) is (AlgebraicClosure k)((T)). This file equips that field with the genuine coefficientwise arithmetic Frobenius over k((T)).

This is the equal-characteristic specialization of the completed-unramified source in the equal-characteristic completed-unramified construction. In particular, the Frobenius below is an actual algebra equivalence; it is not a theorem-shaped replacement for later theta evaluation or norm-subgroup arguments.

Imports4

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.CoefficientFrobenius
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Existence.LaurentLocalField
Mathlib.RingTheory.PowerSeries.Evaluation

Imported by5

theorem

valuedInteger_hasBasis_ltIdeal

L44 ↗

LubinTate.EqualCharacteristic.valuedInteger_hasBasis_ltIdeal

Documentation

The valuation balls in a valued integer ring, expressed as genuine ideals, form its neighbourhood basis at zero.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]

Lean source · full declaration

theorem valuedInteger_hasBasis_ltIdeal
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    (𝓝 (0 : Valued.integer K)).HasBasis
      (fun _ : (MonoidWithZeroHom.ValueGroup₀
        ((Valued.v : Valuation K Γ) : K →*₀ Γ))ˣ ↦ True)
      (fun γ ↦ (Valuation.ltIdeal (Valued.v : Valuation K Γ)
        (Units.map (MonoidWithZeroHom.ValueGroup₀.embedding
          (f := ((Valued.v : Valuation K Γ) : K →*₀ Γ))) γ) :
        Set (Valued.integer K))) := by
  rw [nhds_subtype]
  refine ((Valued.hasBasis_nhds_zero K Γ).comap
    ((↑) : Valued.integer K → K)).congr (fun _ ↦ Iff.rfl) ?_
  intro γ _
  ext x
  change (Valued.v : Valuation K Γ).restrict x < (γ.1 :
      MonoidWithZeroHom.ValueGroup₀
        ((Valued.v : Valuation K Γ) : K →*₀ Γ)) ↔
    (Valued.v : Valuation K Γ) (x : K) <
      ((Units.map (MonoidWithZeroHom.ValueGroup₀.embedding
        (f := ((Valued.v : Valuation K Γ) : K →*₀ Γ))) γ : Γˣ) : Γ)
  rw [Valuation.restrict_lt_iff_lt_embedding]
  simp

theorem

valuedIntegerLinearTopology

L70 ↗

LubinTate.EqualCharacteristic.valuedIntegerLinearTopology

Documentation

The native topology on a valued integer ring is linear: its valuation balls are ideals.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]

Lean source · statement

theorem valuedIntegerLinearTopology
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K)

theorem

valuedIntegerCompleteSpace

L79 ↗

LubinTate.EqualCharacteristic.valuedIntegerCompleteSpace

Documentation

A closed valued integer ring inherits completeness from its fraction field.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]

Lean source · statement

theorem valuedIntegerCompleteSpace
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K)

theorem

valuedIntegerIsUniformAddGroup

L87 ↗

LubinTate.EqualCharacteristic.valuedIntegerIsUniformAddGroup

Documentation

The induced uniformity on a valued integer ring is compatible with its additive group.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]

Lean source · statement

theorem valuedIntegerIsUniformAddGroup
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K)

instance

valuedIntegerLinearTopologyInstance

L93 ↗

LubinTate.EqualCharacteristic.valuedIntegerLinearTopologyInstance

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]

Lean source · statement

instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K)

instance

valuedIntegerCompleteSpaceInstance

L99 ↗

LubinTate.EqualCharacteristic.valuedIntegerCompleteSpaceInstance

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology

Lean source · statement

instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K)

instance

valuedIntegerIsUniformAddGroupInstance

L105 ↗

LubinTate.EqualCharacteristic.valuedIntegerIsUniformAddGroupInstance

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace

Lean source · statement

instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K)

instance

equalCharacteristicCoefficientUniformSpace

L112 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCoefficientUniformSpace

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
omit [Finite k] in

Lean source · statement

instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k)

theorem

equalCharacteristicCoefficientFrobenius_fixed_iff

L117 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCoefficientFrobenius_fixed_iff

Documentation

The fixed elements of arithmetic Frobenius in the algebraic closure are exactly the embedded elements of the finite coefficient field.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCoefficientFrobenius_fixed_iff
    (x : AlgebraicClosure k) :
    equalCharacteristicCoefficientFrobenius k x = x ↔
      x ∈ (algebraMap k (AlgebraicClosure k)).range

def

equalCharacteristicCompletedUnramifiedField

L151 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedField

Documentation

The equal-characteristic model of the completed maximal unramified extension of k((T)).

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedField

instance

equalCharacteristicCompletedUnramifiedField_field

L155 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedField_field

Documentation

The completed unramified Laurent-series model is a field.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicCompletedUnramifiedField_field :
    Field (equalCharacteristicCompletedUnramifiedField k)

instance

equalCharacteristicCompletedUnramifiedField_valued

L161 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedField_valued

Documentation

The completed unramified field carries its Laurent-series valuation.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicCompletedUnramifiedField_valued :
    Valued (equalCharacteristicCompletedUnramifiedField k) ℤᵐ⁰

instance

equalCharacteristicCompletedUnramifiedField_completeSpace

L167 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedField_completeSpace

Documentation

The completed unramified Laurent-series field is complete.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicCompletedUnramifiedField_completeSpace :
    CompleteSpace (equalCharacteristicCompletedUnramifiedField k)

def

equalCharacteristicCompletedUnramifiedFieldEquivLaurentSeries

L174 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldEquivLaurentSeries

Documentation

Comparison with the Laurent-series model underlying the completed unramified field.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFieldEquivLaurentSeries :
    equalCharacteristicCompletedUnramifiedField k ≃+*
      (AlgebraicClosure k)⸨X⸩

def

equalCharacteristicCompletedUnramifiedFieldOfLaurentSeries

L180 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldOfLaurentSeries

Documentation

Embed a Laurent series into the named completed-unramified field.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFieldOfLaurentSeries :
    (AlgebraicClosure k)⸨X⸩ →+*
      equalCharacteristicCompletedUnramifiedField k

def

equalCharacteristicCompletedUnramifiedFieldToLaurentSeries

L186 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldToLaurentSeries

Documentation

Read a named completed-unramified element in its Laurent-series model.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFieldToLaurentSeries :
    equalCharacteristicCompletedUnramifiedField k →+*
      (AlgebraicClosure k)⸨X⸩

theorem

equalCharacteristicCompletedUnramifiedFieldToLaurentSeries_ofLaurentSeries

L194 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldToLaurentSeries_ofLaurentSeries

Documentation

Converting a Laurent series into the named field and back returns the series.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFieldToLaurentSeries_ofLaurentSeries
    (x : (AlgebraicClosure k)⸨X⸩) :
    equalCharacteristicCompletedUnramifiedFieldToLaurentSeries k
        (equalCharacteristicCompletedUnramifiedFieldOfLaurentSeries k x) = x

def

equalCharacteristicCompletedUnramifiedFieldSingle

L201 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldSingle

Documentation

A single Laurent monomial in the named completed-unramified field.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFieldSingle
    (m : ℤ) (a : AlgebraicClosure k) :
    equalCharacteristicCompletedUnramifiedField k

def

equalCharacteristicCompletedUnramifiedFieldCoeff

L208 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldCoeff

Documentation

The coefficient of a named completed-unramified Laurent element.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFieldCoeff
    (x : equalCharacteristicCompletedUnramifiedField k) (m : ℤ) :
    AlgebraicClosure k

theorem

equalCharacteristicCompletedUnramifiedFieldCoeff_ofLaurentSeries

L216 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldCoeff_ofLaurentSeries

Documentation

Coefficients of an imported Laurent series agree with its original coefficients.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFieldCoeff_ofLaurentSeries
    (x : (AlgebraicClosure k)⸨X⸩) (m : ℤ) :
    equalCharacteristicCompletedUnramifiedFieldCoeff k
        (equalCharacteristicCompletedUnramifiedFieldOfLaurentSeries k x) m =
      x.coeff m

theorem

equalCharacteristicCompletedUnramifiedField_ext

L227 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedField_ext

Documentation

Two named completed-unramified elements are equal when all Laurent coefficients agree.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedField_ext
    {x y : equalCharacteristicCompletedUnramifiedField k}
    (h : ∀ m, equalCharacteristicCompletedUnramifiedFieldCoeff k x m =
      equalCharacteristicCompletedUnramifiedFieldCoeff k y m) :
    x = y

instance

equalCharacteristicCompletedUnramifiedPowerSeriesAlgebra

L237 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedPowerSeriesAlgebra

Documentation

The completed unramified field is an algebra over algebraic-closure power series.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicCompletedUnramifiedPowerSeriesAlgebra :
    Algebra (AlgebraicClosure k)⟦X⟧
      (equalCharacteristicCompletedUnramifiedField k)

instance

equalCharacteristicCompletedUnramifiedCoefficientAlgebra

L244 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedCoefficientAlgebra

Documentation

The completed unramified field is an algebra over the residue base field.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicCompletedUnramifiedCoefficientAlgebra :
    Algebra k (equalCharacteristicCompletedUnramifiedField k)

instance

equalCharacteristicCompletedUnramifiedAlgebra

L250 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedAlgebra

Documentation

The completed unramified field is an algebra over the Laurent-series base.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicCompletedUnramifiedAlgebra :
    Algebra k⸨X⸩ (equalCharacteristicCompletedUnramifiedField k)

instance

equalCharacteristicCompletedUnramifiedIsFractionRing

L256 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedIsFractionRing

Documentation

The named completed-unramified Laurent field is the fraction field of its power-series integer ring.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

instance equalCharacteristicCompletedUnramifiedIsFractionRing :
    IsFractionRing (AlgebraicClosure k)⟦X⟧
      (equalCharacteristicCompletedUnramifiedField k)

theorem

equalCharacteristicCompletedUnramifiedFieldCoeff_algebraMap_powerSeries

L266 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldCoeff_algebraMap_powerSeries

Documentation

A mapped power series has its original nonnegative coefficients.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFieldCoeff_algebraMap_powerSeries
    (f : (AlgebraicClosure k)⟦X⟧) (n : ℕ) :
    equalCharacteristicCompletedUnramifiedFieldCoeff k
        (algebraMap (AlgebraicClosure k)⟦X⟧
          (equalCharacteristicCompletedUnramifiedField k) f) n =
      PowerSeries.coeff n f

theorem

equalCharacteristicCompletedUnramifiedFieldCoeff_algebraMap_laurentSeries

L279 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFieldCoeff_algebraMap_laurentSeries

Documentation

A mapped base Laurent series has coefficients embedded into the algebraic closure.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFieldCoeff_algebraMap_laurentSeries
    (f : k⸨X⸩) (m : ℤ) :
    equalCharacteristicCompletedUnramifiedFieldCoeff k
        (algebraMap k⸨X⸩
          (equalCharacteristicCompletedUnramifiedField k) f) m =
      algebraMap k (AlgebraicClosure k) (f.coeff m)

def

equalCharacteristicCompletedUnramifiedFrobenius

L293 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFrobenius

Documentation

Arithmetic Frobenius on the completed maximal-unramified Laurent field, acting coefficientwise and fixing the Laurent-series base k((T)).

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFrobenius :
    equalCharacteristicCompletedUnramifiedField k ≃ₐ[k⸨X⸩]
      equalCharacteristicCompletedUnramifiedField k

theorem

equalCharacteristicCompletedUnramifiedFrobenius_coeff

L301 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFrobenius_coeff

Documentation

Completed Frobenius applies coefficient Frobenius at every Laurent exponent.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFrobenius_coeff
    (x : equalCharacteristicCompletedUnramifiedField k) (m : ℤ) :
    equalCharacteristicCompletedUnramifiedFieldCoeff k
        (equalCharacteristicCompletedUnramifiedFrobenius k x) m =
  equalCharacteristicCompletedUnramifiedFieldCoeff k x m ^
        Nat.card k

theorem

equalCharacteristicCompletedUnramifiedFrobenius_valuation

L317 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFrobenius_valuation

Documentation

Coefficient Frobenius preserves the native Laurent valuation.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFrobenius_valuation
    (x : equalCharacteristicCompletedUnramifiedField k) :
    Valued.v (equalCharacteristicCompletedUnramifiedFrobenius k x) =
      Valued.v x

theorem

equalCharacteristicCompletedUnramifiedFrobenius_continuous

L362 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFrobenius_continuous

Documentation

Coefficient Frobenius is continuous for the Laurent valuation topology.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFrobenius_continuous :
    Continuous (equalCharacteristicCompletedUnramifiedFrobenius k)

theorem

equalCharacteristicCompletedUnramifiedFrobenius_algebraMap_powerSeries

L386 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFrobenius_algebraMap_powerSeries

Documentation

On the integer ring (AlgebraicClosure k)[[T]], Laurent Frobenius is the coefficientwise power-series Frobenius constructed for theta.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFrobenius_algebraMap_powerSeries
    (f : (AlgebraicClosure k)⟦X⟧) :
    equalCharacteristicCompletedUnramifiedFrobenius k
        (algebraMap ((AlgebraicClosure k)⟦X⟧)
          (equalCharacteristicCompletedUnramifiedField k) f) =
      algebraMap ((AlgebraicClosure k)⟦X⟧)
        (equalCharacteristicCompletedUnramifiedField k)
        (equalCharacteristicPowerSeriesFrobenius k f)

theorem

equalCharacteristicCompletedUnramified_fixed_coeff_mem_range

L421 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramified_fixed_coeff_mem_range

Documentation

Every coefficient of a Frobenius-fixed completed Laurent series comes from the original finite coefficient field.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramified_fixed_coeff_mem_range
    (x : equalCharacteristicCompletedUnramifiedField k)
    (hx : equalCharacteristicCompletedUnramifiedFrobenius k x = x)
    (m : ℤ) :
    equalCharacteristicCompletedUnramifiedFieldCoeff k x m ∈
      (algebraMap k (AlgebraicClosure k)).range

def

equalCharacteristicCompletedUnramifiedFixedCoeff

L441 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFixedCoeff

Documentation

A chosen coefficient in k lifting one coefficient of a Frobenius-fixed completed Laurent series.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFixedCoeff
    (x : equalCharacteristicCompletedUnramifiedField k)
    (hx : equalCharacteristicCompletedUnramifiedFrobenius k x = x)
    (m : ℤ) : k

theorem

algebraMap_equalCharacteristicCompletedUnramifiedFixedCoeff

L450 ↗

LubinTate.EqualCharacteristic.algebraMap_equalCharacteristicCompletedUnramifiedFixedCoeff

Documentation

The chosen base coefficient embeds to the coefficient of the fixed series.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem algebraMap_equalCharacteristicCompletedUnramifiedFixedCoeff
    (x : equalCharacteristicCompletedUnramifiedField k)
    (hx : equalCharacteristicCompletedUnramifiedFrobenius k x = x)
    (m : ℤ) :
    algebraMap k (AlgebraicClosure k)
        (equalCharacteristicCompletedUnramifiedFixedCoeff k x hx m) =
      equalCharacteristicCompletedUnramifiedFieldCoeff k x m

def

equalCharacteristicCompletedUnramifiedFixedPreimage

L461 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFixedPreimage

Documentation

A Frobenius-fixed series, descended coefficientwise to k((T)).

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedUnramifiedFixedPreimage
    (x : equalCharacteristicCompletedUnramifiedField k)
    (hx : equalCharacteristicCompletedUnramifiedFrobenius k x = x) :
    k⸨X⸩

theorem

equalCharacteristicCompletedUnramifiedFixedPreimage_coeff

L483 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFixedPreimage_coeff

Documentation

The descended Laurent series has the chosen fixed coefficients.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFixedPreimage_coeff
    (x : equalCharacteristicCompletedUnramifiedField k)
    (hx : equalCharacteristicCompletedUnramifiedFrobenius k x = x)
    (m : ℤ) :
    (equalCharacteristicCompletedUnramifiedFixedPreimage k x hx).coeff m =
      equalCharacteristicCompletedUnramifiedFixedCoeff k x hx m

theorem

equalCharacteristicCompletedUnramifiedFrobenius_fixed_iff

L494 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFrobenius_fixed_iff

Documentation

The fixed field of coefficientwise Frobenius is exactly the embedded Laurent-series base k((T)).

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFrobenius_fixed_iff
    (x : equalCharacteristicCompletedUnramifiedField k) :
    equalCharacteristicCompletedUnramifiedFrobenius k x = x ↔
      x ∈ (algebraMap k⸨X⸩
        (equalCharacteristicCompletedUnramifiedField k)).range

theorem

equalCharacteristicCompletedUnramifiedFrobenius_uniformizer

L509 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedUnramifiedFrobenius_uniformizer

Documentation

The Frobenius fixes the Laurent uniformizer T.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

theorem equalCharacteristicCompletedUnramifiedFrobenius_uniformizer :
    equalCharacteristicCompletedUnramifiedFrobenius k
        (equalCharacteristicCompletedUnramifiedFieldSingle k 1 1) =
      equalCharacteristicCompletedUnramifiedFieldSingle k 1 1

def

equalCharacteristicPowerSeriesToCompletedInteger

L524 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesToCompletedInteger

Documentation

Evaluation of an outer power series with coefficients in (AlgebraicClosure k)[[T]] at a topologically nilpotent point of the completed-unramified integer ring. This is the analytic evaluation map needed for the theta series in the completed theta-intertwining theorem.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicPowerSeriesToCompletedInteger :
    (AlgebraicClosure k)⟦X⟧ →+*
      Valued.integer (equalCharacteristicCompletedUnramifiedField k)

theorem

equalCharacteristicPowerSeriesToCompletedInteger_continuous

L534 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesToCompletedInteger_continuous

Documentation

The embedding of power series into the completed valuation ring is continuous.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicPowerSeriesToCompletedInteger_continuous :
    Continuous (equalCharacteristicPowerSeriesToCompletedInteger k)

def

equalCharacteristicCompletedIntegerEvaluation

L541 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegerEvaluation

Documentation

Defines equalCharacteristicCompletedIntegerEvaluation.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedIntegerEvaluation
    (a : Valued.integer (equalCharacteristicCompletedUnramifiedField k))
    (ha : PowerSeries.HasEval a) :
    ((AlgebraicClosure k)⟦X⟧)⟦X⟧ →+*
      Valued.integer (equalCharacteristicCompletedUnramifiedField k)

def

equalCharacteristicCompletedIntegerUniformizer

L561 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegerUniformizer

Documentation

The Laurent uniformizer, viewed in the completed-unramified integer ring.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥

Lean source · statement

def equalCharacteristicCompletedIntegerUniformizer :
    Valued.integer (equalCharacteristicCompletedUnramifiedField k)

theorem

equalCharacteristicCompletedIntegerUniformizer_hasEval

L567 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegerUniformizer_hasEval

Documentation

The completed-unramified uniformizer is topologically nilpotent.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedIntegerUniformizer_hasEval :
    PowerSeries.HasEval
      (equalCharacteristicCompletedIntegerUniformizer k)

theorem

equalCharacteristicCompletedIntegerEvaluation_X

L579 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegerEvaluation_X

Documentation

Completed power-series evaluation sends X to the chosen integral element.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedIntegerEvaluation_X
    (a : Valued.integer (equalCharacteristicCompletedUnramifiedField k))
    (ha : PowerSeries.HasEval a) :
    equalCharacteristicCompletedIntegerEvaluation k a ha PowerSeries.X = a

theorem

equalCharacteristicCompletedIntegerEvaluation_C

L589 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegerEvaluation_C

Documentation

Completed evaluation sends a constant series to its canonical embedded value.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries PowerSeries.WithPiTopology
  Topology Valued WithZero
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable (k : Type u) [Field k] [Finite k]
noncomputable local instance valuedIntegerLinearTopologyInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsLinearTopology (Valued.integer K) (Valued.integer K) :=
  valuedIntegerLinearTopology
noncomputable local instance valuedIntegerCompleteSpaceInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] [CompleteSpace K] :
    CompleteSpace (Valued.integer K) :=
  valuedIntegerCompleteSpace
noncomputable local instance valuedIntegerIsUniformAddGroupInstance
    {K : Type u} {Γ : Type v} [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] :
    IsUniformAddGroup (Valued.integer K) :=
  valuedIntegerIsUniformAddGroup
noncomputable local instance equalCharacteristicCoefficientUniformSpace :
    UniformSpace (AlgebraicClosure k) := ⊥
omit [Finite k] in

Lean source · statement

theorem equalCharacteristicCompletedIntegerEvaluation_C
    (a : Valued.integer (equalCharacteristicCompletedUnramifiedField k))
    (ha : PowerSeries.HasEval a)
    (f : (AlgebraicClosure k)⟦X⟧) :
    equalCharacteristicCompletedIntegerEvaluation k a ha (PowerSeries.C f) =
      equalCharacteristicPowerSeriesToCompletedInteger k f

Module documentation

The equal-characteristic completed-unramified construction: the completed maximal-unramified

Declarations