NYLL
Module

EqualCharacteristicLaurent.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.EqualCharacteristicLaurent
47 declarations indexed from sourceView source ↗

Module documentation

Equal-characteristic Laurent-series input for the local-field structure classification

This file starts the equal-characteristic branch of the local-field structure classification, the local-field structure classification. Given the Teichmuller coefficient-field section κ -> O_K -> K and a uniformizer π, it constructs the induced evaluation map κ((X)) -> K by first evaluating κ⟦X⟧ at X = π, then using the localization description κ((X)) = κ⟦X⟧[X⁻¹].

Imports21
Imported by2

Declarations

abbrev

coeffSubringHom

L60 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.coeffSubringHom
Documentation

The Teichmuller coefficient-field section κ -> O_K used before passing to the fraction field.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
abbrev coeffSubringHom [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ)) :
    F.residueField →+* F.valuationSubring
abbrev

coeffHom

L69 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.coeffHom
Documentation

The Teichmuller coefficient-field embedding κ -> K used in the equal-characteristic Laurent-series branch.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
abbrev coeffHom [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ)) :
    F.residueField →+* K
def

teichmullerRepresentativeSystem

L77 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.teichmullerRepresentativeSystem
Documentation

The Teichmuller section is a representative system for the residue field.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
def teichmullerRepresentativeSystem [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ)) :
    LubinTate.Valuations.residueRepresentativeSystem F where
  repr := coeffSubringHom (F := F) p hcard
  residue_repr := by
    intro a
    have hcomp :=
      higherPrincipalUnitGroup.residueMap_comp_residueTeichmullerRingHomOfCharP
        (F := F) p hcard
    simpa [coeffSubringHom, RingHom.comp_apply] using
      congrFun (congrArg DFunLike.coe hcomp) a
  repr_zero := by
    simp [coeffSubringHom]
theorem

coeffHom_apply

L94 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.coeffHom_apply
Documentation

The field-valued coefficient embedding is the valuation-ring coefficient section followed by the valuation-subring inclusion.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem coeffHom_apply [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (a : F.residueField) :
    coeffHom (F := F) p hcard a =
      (coeffSubringHom (F := F) p hcard a : K)
theorem

continuous_coeffHom_of_discrete

L104 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.continuous_coeffHom_of_discrete
Documentation

The Teichmuller coefficient-field embedding is continuous when the finite residue field is given the discrete uniformity.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem continuous_coeffHom_of_discrete [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    [UniformSpace F.residueField] [DiscreteUniformity F.residueField]
    [TopologicalSpace K] :
    Continuous (coeffHom (F := F) p hcard)
theorem

continuous_coeffSubringHom_of_discrete

L114 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.continuous_coeffSubringHom_of_discrete
Documentation

The valuation-ring Teichmuller coefficient section is continuous from the discrete residue-field topology to any topology on the valuation ring.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem continuous_coeffSubringHom_of_discrete [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    [UniformSpace F.residueField] [DiscreteUniformity F.residueField]
    [TopologicalSpace F.valuationSubring] :
    Continuous (coeffSubringHom (F := F) p hcard)
theorem

uniformizer_hasEval_mrangeRestrict

L124 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.uniformizer_hasEval_mrangeRestrict
Documentation

A complete-DVF uniformizer is topologically nilpotent for the range-restricted valued topology.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
theorem uniformizer_hasEval_mrangeRestrict
    {π : F.valuationSubring}
    (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.valuation.toMonoidWithZeroHom) :=
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued F)
    PowerSeries.HasEval (π : K) := by
  let Γ : Type v :=
    MonoidHom.mrange F.valuation.toMonoidWithZeroHom
  let : Valued K Γ := (mrangeRestrictValued F)
  have : IsCyclic Γˣ := by
    simpa [Γ] using
      _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_units_isCyclic F
  have : MulArchimedean Γ :=
    _root_.LocalFieldTheory.DiscreteValuationField.WithZeroValuation.units_isCyclic_mulArchimedean Γ
  have hπ_lt :
      (Valued.v : _root_.Valuation K Γ) (π : K) < 1 := by
    change mrangeRestrict F (π : K) < (1 : Γ)
    rw [← Subtype.coe_lt_coe]
    simpa [Γ, mrangeRestrict] using hπ.val_lt_one
  exact Valued.tendsto_zero_pow_of_v_lt_one hπ_lt
theorem

valuationSubring_isLinearTopology_adic

L147 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.valuationSubring_isLinearTopology_adic
Documentation

The maximal-ideal adic topology on the valuation ring is linear.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
theorem valuationSubring_isLinearTopology_adic :
    letI : TopologicalSpace F.valuationSubring := F.maximalIdeal.adicTopology
    IsLinearTopology F.valuationSubring F.valuationSubring := by
  let : TopologicalSpace F.valuationSubring := F.maximalIdeal.adicTopology
  exact
    IsLinearTopology.mk_of_hasBasis F.valuationSubring
      (Ideal.hasBasis_nhds_zero_adic F.maximalIdeal)
theorem

valuationSubring_isLinearTopology_withIdeal

L156 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.valuationSubring_isLinearTopology_withIdeal
Documentation

The WithIdeal adic topology on the valuation ring is linear.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
theorem valuationSubring_isLinearTopology_withIdeal :
    letI : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
    IsLinearTopology F.valuationSubring F.valuationSubring := by
  let : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
  exact valuationSubring_isLinearTopology_adic (F := F)
theorem

valuationSubring_completeSpace_withIdeal

L163 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.valuationSubring_completeSpace_withIdeal
Documentation

The valuation ring is complete for its maximal-ideal adic topology.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
theorem valuationSubring_completeSpace_withIdeal :
    letI : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
    CompleteSpace F.valuationSubring := by
  let : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
  have hadic : IsAdic F.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp F.isAdicComplete).1
theorem

valuationSubring_t2Space_withIdeal

L171 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.valuationSubring_t2Space_withIdeal
Documentation

The valuation ring is Hausdorff for its maximal-ideal adic topology.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
theorem valuationSubring_t2Space_withIdeal :
    letI : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
    T2Space F.valuationSubring := by
  let : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
  have hadic : IsAdic F.maximalIdeal := rfl
  exact (hadic.isAdicComplete_iff.mp F.isAdicComplete).2
theorem

uniformizer_hasEval_valuationSubring_withIdeal

L180 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.uniformizer_hasEval_valuationSubring_withIdeal
Documentation

A complete-DVF uniformizer is topologically nilpotent in the valuation ring for the maximal-ideal adic topology.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
theorem uniformizer_hasEval_valuationSubring_withIdeal
    {π : F.valuationSubring}
    (hπ : F.valuation.IsUniformizer (π : K)) :
    letI : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
    PowerSeries.HasEval π := by
  let : WithIdeal F.valuationSubring := { i := F.maximalIdeal }
  change Filter.Tendsto (fun m : ℕ => π ^ m) Filter.atTop
    (nhds (0 : F.valuationSubring))
  refine (F.maximalIdeal.hasBasis_nhds_zero_adic).tendsto_right_iff.2 ?_
  intro n _
  refine Filter.eventually_atTop.2 ⟨n, fun m hm => ?_⟩
  have hπmem : π ∈ F.maximalIdeal :=
    F.uniformizer_mem_maximalIdeal hπ
  have hpow : π ^ m ∈ F.maximalIdeal ^ m :=
    Ideal.pow_mem_pow hπmem m
  exact Ideal.pow_le_pow_right hm hpow
def

powerSeriesEvalSubringHom

L199 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.powerSeriesEvalSubringHom
Documentation

Evaluation of power series into the valuation ring through the Teichmuller coefficient section, sending X to a chosen uniformizer.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
def powerSeriesEvalSubringHom [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    F.residueField⟦X⟧ →+* F.valuationSubring
theorem

powerSeriesEvalSubringHom_C

L218 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.powerSeriesEvalSubringHom_C
Documentation

Establishes the identity powerSeriesEvalSubringHom (F := F) p hcard π hcoeff hπeval (PowerSeries.C a) = coeffSubringHom (F := F) p hcard a.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem powerSeriesEvalSubringHom_C [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) (a : F.residueField) :
    powerSeriesEvalSubringHom (F := F) p hcard π hcoeff hπeval
        (PowerSeries.C a) =
      coeffSubringHom (F := F) p hcard a
theorem

powerSeriesEvalSubringHom_X

L244 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.powerSeriesEvalSubringHom_X
Documentation

Establishes the identity powerSeriesEvalSubringHom (F := F) p hcard π hcoeff hπeval PowerSeries.X = π.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem powerSeriesEvalSubringHom_X [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    powerSeriesEvalSubringHom (F := F) p hcard π hcoeff hπeval
        PowerSeries.X =
      π
def

powerSeriesEvalHom

L267 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.powerSeriesEvalHom
Documentation

The valuation-ring evaluation composed with the inclusion O_K -> K.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
def powerSeriesEvalHom [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    F.residueField⟦X⟧ →+* K
theorem

powerSeriesEvalHom_C

L287 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.powerSeriesEvalHom_C
Documentation

Establishes the identity powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval (PowerSeries.C a) = coeffHom (F := F) p hcard a.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem powerSeriesEvalHom_C [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) (a : F.residueField) :
    powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval
        (PowerSeries.C a) =
      coeffHom (F := F) p hcard a
theorem

powerSeriesEvalHom_X

L311 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.powerSeriesEvalHom_X
Documentation

Establishes the identity powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval PowerSeries.X = (π : K).

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem powerSeriesEvalHom_X [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval
        PowerSeries.X =
      (π : K)
theorem

powerSeriesEvalHom_X_isUnit

L335 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.powerSeriesEvalHom_X_isUnit
Documentation

Proves that the specified element is a unit: IsUnit (powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval PowerSeries.X).

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem powerSeriesEvalHom_X_isUnit [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K))
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    IsUnit
      (powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval
        PowerSeries.X)
def

laurentSeriesEvalHom

L356 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.laurentSeriesEvalHom
Documentation

The Laurent-series evaluation map κ((X)) -> K attached to the Teichmuller coefficient field and the chosen uniformizer.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
def laurentSeriesEvalHom [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K))
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    F.residueField⸨X⸩ →+* K
theorem

laurentSeriesEvalHom_comp_powerSeries

L383 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.laurentSeriesEvalHom_comp_powerSeries
Documentation

Establishes the identity (laurentSeriesEvalHom (F := F) p hcard π hπ hcoeff hπeval).comp (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) = powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem laurentSeriesEvalHom_comp_powerSeries [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K))
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    (laurentSeriesEvalHom (F := F) p hcard π hπ hcoeff hπeval).comp
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) =
      powerSeriesEvalHom (F := F) p hcard π hcoeff hπeval
theorem

laurentSeriesEvalHom_algebraMap_C

L412 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.laurentSeriesEvalHom_algebraMap_C
Documentation

Establishes the identity laurentSeriesEvalHom (F := F) p hcard π hπ hcoeff hπeval (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩ (PowerSeries.C a)) = coeffHom (F := F) p hcard a.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem laurentSeriesEvalHom_algebraMap_C
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K))
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) (a : F.residueField) :
    laurentSeriesEvalHom (F := F) p hcard π hπ hcoeff hπeval
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.C a)) =
      coeffHom (F := F) p hcard a
theorem

laurentSeriesEvalHom_algebraMap_X

L441 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.laurentSeriesEvalHom_algebraMap_X
Documentation

Establishes the identity laurentSeriesEvalHom (F := F) p hcard π hπ hcoeff hπeval (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩ (PowerSeries.X : F.residueField⟦X⟧)) = (π : K).

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem laurentSeriesEvalHom_algebraMap_X
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K))
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    laurentSeriesEvalHom (F := F) p hcard π hπ hcoeff hπeval
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.X : F.residueField⟦X⟧)) =
      (π : K)
def

laurentSeriesAlgebra

L468 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.laurentSeriesAlgebra
Documentation

The algebra structure on K induced by the Laurent-series evaluation map. This is the base algebra for the remaining finite-dimensionality step.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
def laurentSeriesAlgebra [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K))
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) :
    Algebra F.residueField⸨X⸩ K
theorem

algebraMap_laurentSeriesAlgebra_apply

L489 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.algebraMap_laurentSeriesAlgebra_apply
Documentation

Under the Laurent-series algebra structure, the algebra map evaluates a series through laurentSeriesEvalHom.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · full declaration
theorem algebraMap_laurentSeriesAlgebra_apply
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K))
    [UniformSpace F.residueField] [IsUniformAddGroup F.residueField]
    [IsTopologicalSemiring F.residueField]
    [UniformSpace F.valuationSubring] [IsUniformAddGroup F.valuationSubring]
    [T2Space F.valuationSubring] [CompleteSpace F.valuationSubring]
    [IsTopologicalRing F.valuationSubring]
    [IsLinearTopology F.valuationSubring F.valuationSubring]
    (hcoeff : Continuous (coeffSubringHom (F := F) p hcard))
    (hπeval : PowerSeries.HasEval π) (x : F.residueField⸨X⸩) :
    letI : Algebra F.residueField⸨X⸩ K :=
      laurentSeriesAlgebra
        (F := F) p hcard π hπ hcoeff hπeval
    algebraMap F.residueField⸨X⸩ K x =
      laurentSeriesEvalHom (F := F) p hcard π hπ hcoeff hπeval x := by
  rfl
def

adicPowerSeriesEvalSubringHom

L512 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.adicPowerSeriesEvalSubringHom
Documentation

The adic valuation-ring power-series evaluation with all topology instances supplied from the complete-DVF structure.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
def adicPowerSeriesEvalSubringHom
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K)) :
    F.residueField⟦X⟧ →+* F.valuationSubring
theorem

adicPowerSeriesEvalSubringHom_surjective

L538 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.adicPowerSeriesEvalSubringHom_surjective
Documentation

The π-adic power-series evaluation onto the valuation ring is surjective. This is the complete-DVR coefficient expansion, using the Teichmuller representatives as digits.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem adicPowerSeriesEvalSubringHom_surjective
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K)) :
    Function.Surjective
      (adicPowerSeriesEvalSubringHom (F := F) p hcard π hπ)
def

adicLaurentSeriesEvalHom

L622 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom
Documentation

The adic Laurent-series evaluation with all topology instances supplied from the complete-DVF structure.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
def adicLaurentSeriesEvalHom
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K)) :
    F.residueField⸨X⸩ →+* K
theorem

adicLaurentSeriesEvalHom_algebraMap_C

L649 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom_algebraMap_C
Documentation

Establishes the identity adicLaurentSeriesEvalHom (F := F) p hcard π hπ (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩ (PowerSeries.C a)) = coeffHom (F := F) p hcard a.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem adicLaurentSeriesEvalHom_algebraMap_C
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K)) (a : F.residueField) :
    adicLaurentSeriesEvalHom (F := F) p hcard π hπ
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.C a)) =
      coeffHom (F := F) p hcard a
theorem

adicLaurentSeriesEvalHom_algebraMap_X

L680 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom_algebraMap_X
Documentation

Establishes the identity adicLaurentSeriesEvalHom (F := F) p hcard π hπ (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩ (PowerSeries.X : F.residueField⟦X⟧)) = (π : K).

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem adicLaurentSeriesEvalHom_algebraMap_X
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K)) :
    adicLaurentSeriesEvalHom (F := F) p hcard π hπ
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.X : F.residueField⟦X⟧)) =
      (π : K)
theorem

adicLaurentSeriesEvalHom_comp_powerSeries

L712 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom_comp_powerSeries
Documentation

Establishes the identity (adicLaurentSeriesEvalHom (F := F) p hcard π hπ).comp (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) = F.valuation.valuationSubring.subtype.comp (adicPowerSeriesEvalSubringHom (F := F) p hcard π hπ).

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem adicLaurentSeriesEvalHom_comp_powerSeries
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K)) :
    (adicLaurentSeriesEvalHom (F := F) p hcard π hπ).comp
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) =
      F.valuation.valuationSubring.subtype.comp
        (adicPowerSeriesEvalSubringHom (F := F) p hcard π hπ)
theorem

adicLaurentSeriesEvalHom_surjective

L740 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom_surjective
Documentation

The equal-characteristic Laurent-series evaluation is onto the field.

Source context 10 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace CompleteDVF
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
open Filter
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
namespace EqualCharacteristicLaurent
Lean source · statement
theorem adicLaurentSeriesEvalHom_surjective
    [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.valuation.IsUniformizer (π : K)) :
    Function.Surjective
      (adicLaurentSeriesEvalHom (F := F) p hcard π hπ)
theorem

finiteDimensional_of_surjective_algebraMap

L800 ↗
LocalFieldTheory.DiscreteValuationField.finiteDimensional_of_surjective_algebraMap
Documentation

If the structure map of an algebra over a field is onto, the algebra is one-dimensional as a vector space over the base.

Source context 4 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
Lean source · statement
theorem finiteDimensional_of_surjective_algebraMap
    (E L : Type u) [Field E] [Field L] [Algebra E L]
    (hsurj : Function.Surjective (algebraMap E L)) :
    FiniteDimensional E L
def

laurentImageSubfield

L818 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentImageSubfield
Documentation

The image in K of the equal-characteristic Laurent-series evaluation. This is the candidate base field for the converse direction of the local-field structure classification.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
def laurentImageSubfield
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    Subfield K
theorem

adicLaurentSeriesEval_mem_laurentImageSubfield

L832 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.adicLaurentSeriesEval_mem_laurentImageSubfield
Documentation

Establishes the membership statement CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom (F := F.toCompleteDVF) p hcard π hπ x ∈ F.laurentImageSubfield p hcard π hπ.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
theorem adicLaurentSeriesEval_mem_laurentImageSubfield
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (x : F.residueField⸨X⸩) :
    CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom
        (F := F.toCompleteDVF) p hcard π hπ x ∈
      F.laurentImageSubfield p hcard π hπ
theorem

laurentImageSubfield_eq_top

L846 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentImageSubfield_eq_top
Documentation

Establishes the identity F.laurentImageSubfield p hcard π hπ = ⊤.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
theorem laurentImageSubfield_eq_top
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    F.laurentImageSubfield p hcard π hπ = ⊤
def

laurentSeriesEquivLaurentImageSubfield

L863 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentSeriesEquivLaurentImageSubfield
Documentation

The Laurent-series field is identified with its image in K.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
def laurentSeriesEquivLaurentImageSubfield
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    F.residueField⸨X⸩ ≃+*
      F.laurentImageSubfield p hcard π hπ
theorem

laurentSeriesEquivLaurentImageSubfield_apply_coe

L880 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentSeriesEquivLaurentImageSubfield_apply_coe
Documentation

Establishes the identity ((F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ x : F.laurentImageSubfield p hcard π hπ) : K) = CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom (F := F.toCompleteDVF) p hcard π hπ x.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
theorem laurentSeriesEquivLaurentImageSubfield_apply_coe
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (x : F.residueField⸨X⸩) :
    ((F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ x :
        F.laurentImageSubfield p hcard π hπ) : K) =
      CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom
        (F := F.toCompleteDVF) p hcard π hπ x
theorem

laurentSeriesEquivLaurentImageSubfield_algebraMap_C

L897 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentSeriesEquivLaurentImageSubfield_algebraMap_C
Documentation

Establishes the identity ((F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩ (PowerSeries.C a)) : F.laurentImageSubfield p hcard π hπ) : K) = CompleteDVF.EqualCharacteristicLaurent.coeffHom (F := F.toCompleteDVF) p hcard a.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
theorem laurentSeriesEquivLaurentImageSubfield_algebraMap_C
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (a : F.residueField) :
    ((F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.C a)) :
        F.laurentImageSubfield p hcard π hπ) : K) =
      _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.EqualCharacteristicLaurent.coeffHom
        (F := F.toCompleteDVF) p hcard a
theorem

laurentSeriesEquivLaurentImageSubfield_algebraMap_X

L918 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentSeriesEquivLaurentImageSubfield_algebraMap_X
Documentation

Establishes the identity ((F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩ (PowerSeries.X : F.residueField⟦X⟧)) : F.laurentImageSubfield p hcard π hπ) : K) = (π : K).

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
theorem laurentSeriesEquivLaurentImageSubfield_algebraMap_X
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    ((F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.X : F.residueField⟦X⟧)) :
        F.laurentImageSubfield p hcard π hπ) : K) =
      (π : K)
def

laurentImageSubfield_nontriviallyNormedField

L935 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentImageSubfield_nontriviallyNormedField
Documentation

The image base field is nontrivially normed by the norm induced from the range-restricted valuation topology on K.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · full declaration
def laurentImageSubfield_nontriviallyNormedField
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.toCompleteDVF.valuation.toMonoidWithZeroHom) :=
      ((CompleteDVF.mrangeRestrictValued F.toCompleteDVF))
    letI : NontriviallyNormedField K :=
      CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    NontriviallyNormedField
      (F.laurentImageSubfield p hcard π hπ) := by
  let Γ : Type v :=
    MonoidHom.mrange F.toCompleteDVF.valuation.toMonoidWithZeroHom
  letI : Valued K Γ := ((CompleteDVF.mrangeRestrictValued F.toCompleteDVF))
  haveI : (Valued.v : _root_.Valuation K Γ).RankOne := by
    change
      (_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict
        F.toCompleteDVF).RankOne
    exact
      _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_rankOne
        F.toCompleteDVF
  letI : NontriviallyNormedField K :=
    CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  let piSub : F.laurentImageSubfield p hcard π hπ :=
    F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ
      (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
        (PowerSeries.X : F.residueField⟦X⟧))
  have hpiSub_coe : (piSub : K) = (π : K) := by
    simpa [piSub] using
      F.laurentSeriesEquivLaurentImageSubfield_algebraMap_X
        p hcard π hπ
  refine NontriviallyNormedField.ofNormNeOne ?_
  refine ⟨piSub, ?_, ?_⟩
  · intro hzero
    have hzeroK : (piSub : K) = 0 := by
      simpa using congrArg Subtype.val hzero
    rw [hpiSub_coe] at hzeroK
    exact hπ.ne_zero hzeroK
  · have hπ_lt_one :
        CompleteDVF.mrangeRestrict F.toCompleteDVF (π : K) < 1 := by
      rw [← Subtype.coe_lt_coe]
      simpa [Γ, CompleteDVF.mrangeRestrict_apply] using hπ.val_lt_one
    have hπ_norm_lt_one_K : ‖(π : K)‖ < 1 := by
      simpa [_root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrictValued] using
        (Valued.toNormedField.norm_lt_one_iff
          (x := (π : K))).2 hπ_lt_one
    have hπ_norm_lt_one : ‖piSub‖ < 1 := by
      change ‖(piSub : K)‖ < 1
      simpa [hpiSub_coe] using hπ_norm_lt_one_K
    exact ne_of_lt hπ_norm_lt_one
def

laurentImageSubfield_normedAlgebra

L989 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentImageSubfield_normedAlgebra
Documentation

The ambient local field is a normed algebra over the Laurent image base.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · full declaration
def laurentImageSubfield_normedAlgebra
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.toCompleteDVF.valuation.toMonoidWithZeroHom) :=
      ((CompleteDVF.mrangeRestrictValued F.toCompleteDVF))
    letI : NontriviallyNormedField K :=
      CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    letI : NontriviallyNormedField
        (F.laurentImageSubfield p hcard π hπ) :=
      F.laurentImageSubfield_nontriviallyNormedField p hcard π hπ
    NormedAlgebra (F.laurentImageSubfield p hcard π hπ) K := by
  let Γ : Type v :=
    MonoidHom.mrange F.toCompleteDVF.valuation.toMonoidWithZeroHom
  letI : Valued K Γ := ((CompleteDVF.mrangeRestrictValued F.toCompleteDVF))
  letI : NontriviallyNormedField K :=
    CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  letI : NontriviallyNormedField
      (F.laurentImageSubfield p hcard π hπ) :=
    F.laurentImageSubfield_nontriviallyNormedField p hcard π hπ
  exact
    { (inferInstance :
        Algebra (F.laurentImageSubfield p hcard π hπ) K) with
      norm_smul_le := fun a x => by
        change ‖(a : K) * x‖ ≤ ‖(a : K)‖ * ‖x‖
        exact norm_mul_le (a : K) x }
theorem

finiteDimensional_over_laurentImageSubfield

L1020 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.finiteDimensional_over_laurentImageSubfield
Documentation

The local field is finite-dimensional over the image of the Laurent-series base field.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · full declaration
theorem finiteDimensional_over_laurentImageSubfield
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    letI : Valued K
        (MonoidHom.mrange F.toCompleteDVF.valuation.toMonoidWithZeroHom) :=
      ((CompleteDVF.mrangeRestrictValued F.toCompleteDVF))
    letI : NontriviallyNormedField K :=
      CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
    letI : NontriviallyNormedField
        (F.laurentImageSubfield p hcard π hπ) :=
      F.laurentImageSubfield_nontriviallyNormedField p hcard π hπ
    letI : NormedAlgebra
        (F.laurentImageSubfield p hcard π hπ) K :=
      F.laurentImageSubfield_normedAlgebra p hcard π hπ
    FiniteDimensional (F.laurentImageSubfield p hcard π hπ) K := by
  let Γ : Type v :=
    MonoidHom.mrange F.toCompleteDVF.valuation.toMonoidWithZeroHom
  let : Valued K Γ := ((CompleteDVF.mrangeRestrictValued F.toCompleteDVF))
  let : NontriviallyNormedField K :=
    CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  let : NontriviallyNormedField
      (F.laurentImageSubfield p hcard π hπ) :=
    F.laurentImageSubfield_nontriviallyNormedField p hcard π hπ
  let : NormedAlgebra
      (F.laurentImageSubfield p hcard π hπ) K :=
    F.laurentImageSubfield_normedAlgebra p hcard π hπ
  have htop : F.laurentImageSubfield p hcard π hπ = ⊤ :=
    F.laurentImageSubfield_eq_top p hcard π hπ
  have hsurj :
      Function.Surjective
        (algebraMap (F.laurentImageSubfield p hcard π hπ) K) := by
    intro x
    have hxmem : x ∈ F.laurentImageSubfield p hcard π hπ := by
      rw [htop]
      trivial
    exact ⟨⟨x, hxmem⟩, rfl⟩
  exact
    finiteDimensional_of_surjective_algebraMap
      (F.laurentImageSubfield p hcard π hπ) K hsurj
def

laurentSeriesAlgebra

L1063 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentSeriesAlgebra
Documentation

The actual Laurent-series base acts on K through the image subfield.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · statement
def laurentSeriesAlgebra
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    Algebra F.residueField⸨X⸩ K
theorem

laurentSeriesAlgebra_algebraMap

L1079 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.laurentSeriesAlgebra_algebraMap
Documentation

The Laurent-series algebra map is the series equivalence followed by inclusion of the Laurent image subfield.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · full declaration
theorem laurentSeriesAlgebra_algebraMap
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    letI : Algebra F.residueField⸨X⸩ K :=
      F.laurentSeriesAlgebra p hcard π hπ
    algebraMap F.residueField⸨X⸩ K =
      (F.laurentImageSubfield p hcard π hπ).subtype.comp
        (F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ :
          F.residueField⸨X⸩ →+*
            F.laurentImageSubfield p hcard π hπ) := by
  rfl
theorem

finiteDimensional_over_laurentSeries

L1095 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.finiteDimensional_over_laurentSeries
Documentation

The local field is finite-dimensional over the actual Laurent-series base field.

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · full declaration
theorem finiteDimensional_over_laurentSeries
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (π : F.valuationSubring)
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    letI : Algebra F.residueField⸨X⸩ K :=
      F.laurentSeriesAlgebra p hcard π hπ
    FiniteDimensional F.residueField⸨X⸩ K := by
  let : Algebra F.residueField⸨X⸩ K :=
    F.laurentSeriesAlgebra p hcard π hπ
  let Γ : Type v :=
    MonoidHom.mrange F.toCompleteDVF.valuation.toMonoidWithZeroHom
  let : Valued K Γ := ((CompleteDVF.mrangeRestrictValued F.toCompleteDVF))
  let : NontriviallyNormedField K :=
    CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF
  let : NontriviallyNormedField
      (F.laurentImageSubfield p hcard π hπ) :=
    F.laurentImageSubfield_nontriviallyNormedField p hcard π hπ
  let : NormedAlgebra
      (F.laurentImageSubfield p hcard π hπ) K :=
    F.laurentImageSubfield_normedAlgebra p hcard π hπ
  have : FiniteDimensional
      (F.laurentImageSubfield p hcard π hπ) K :=
    F.finiteDimensional_over_laurentImageSubfield p hcard π hπ
  have hcompat :
      (algebraMap (F.laurentImageSubfield p hcard π hπ) K).comp
          (F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ :
            F.residueField⸨X⸩ →+*
              F.laurentImageSubfield p hcard π hπ) =
        (RingEquiv.refl K).toRingHom.comp
          (algebraMap F.residueField⸨X⸩ K) := by
    ext x
    rfl
  have hrank :
      Module.rank F.residueField⸨X⸩ K =
        Module.rank (F.laurentImageSubfield p hcard π hπ) K := by
    simpa using
      (Algebra.rank_eq_of_equiv_equiv
        (F.laurentSeriesEquivLaurentImageSubfield p hcard π hπ)
        (RingEquiv.refl K) hcompat)
  exact
    FiniteDimensional.of_rank_eq_nat
      (n := Module.finrank
        (F.laurentImageSubfield p hcard π hπ) K) <| by
        simpa [Module.finrank_eq_rank'] using hrank
theorem

equalCharacteristic_exists_laurent_finiteExtension

L1144 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.equalCharacteristic_exists_laurent_finiteExtension
Documentation

The local-field structure classification, equal-characteristic converse branch: after choosing a uniformizer and the finite residue field as coefficient field, K is finite-dimensional over κ((X)).

Source context 8 commands

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

noncomputable section
universe u v
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
open scoped PowerSeries LaurentSeries Filter Topology BigOperators
variable {K : Type u} [Field K]
variable (F : LocalField.{u, v} K)
Lean source · full declaration
theorem equalCharacteristic_exists_laurent_finiteExtension
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p]
    {n : ℕ+} (hcard : Nat.card F.residueField = p ^ (n : ℕ)) :
    ∃ π : F.valuationSubring,
      ∃ _hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K),
        ∃ hAlg : Algebra F.residueField⸨X⸩ K,
          letI : Algebra F.residueField⸨X⸩ K := hAlg
          FiniteDimensional F.residueField⸨X⸩ K := by
  rcases F.exists_uniformizer with ⟨π, hπ⟩
  exact
    ⟨π, hπ, F.laurentSeriesAlgebra p hcard π hπ,
      F.finiteDimensional_over_laurentSeries p hcard π hπ⟩

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