NYLL
Module

FiniteCoefficientLaurent.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FiniteCoefficientLaurent
20 declarations indexed from sourceView source ↗

Module documentation

Coefficient-field descent for Laurent series

This file starts the remaining equal-characteristic descent in the local-field structure classification: a finite coefficient field k of characteristic p gives a canonical coefficientwise map from F_p((X)) to k((X)).

Imports9
  • Mathlib.Algebra.Algebra.ZMod
  • Mathlib.Algebra.Field.ZMod
  • Mathlib.LinearAlgebra.Basis.Basic
  • Mathlib.LinearAlgebra.Dimension.Free
  • Mathlib.LinearAlgebra.FiniteDimensional.Defs
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.RingTheory.LaurentSeries
  • Mathlib.RingTheory.Localization.Away.Basic
  • Mathlib.RingTheory.RingHom.Finite
Imported by2

Declarations

theorem

powerSeries_moduleFinite_of_finiteDimensional

L43 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.powerSeries_moduleFinite_of_finiteDimensional
Documentation

If the coefficient field extension A/R is finite-dimensional, then A⟦X⟧ is finitely generated over R⟦X⟧. A finite R-basis of A gives generators by embedding basis vectors as constant power series.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
section PowerSeriesFinite
variable {R : Type u} {A : Type v} [Field R] [Field A] [Algebra R A]
Lean source · statement
theorem powerSeries_moduleFinite_of_finiteDimensional
    [FiniteDimensional R A] :
    Module.Finite R⟦X⟧ A⟦X⟧
theorem

zmod_finiteDimensional_of_finite

L85 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmod_finiteDimensional_of_finite
Documentation

A finite field of characteristic p is finite-dimensional over its prime field ZMod p.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · full declaration
theorem zmod_finiteDimensional_of_finite [Finite k] :
    letI : Algebra (ZMod p) k := ZMod.algebra k p
    FiniteDimensional (ZMod p) k := by
  let : Algebra (ZMod p) k := ZMod.algebra k p
  have : Fintype k := Fintype.ofFinite k
  exact Module.finite_def.2 <| by
    simpa using
    (Submodule.fg_span (R := ZMod p) (M := k)
      (s := Set.univ) (Set.finite_univ : (Set.univ : Set k).Finite))
theorem

zmodPowerSeries_moduleFinite

L97 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodPowerSeries_moduleFinite
Documentation

Finite generation of k⟦X⟧ over F_p⟦X⟧, for a finite coefficient field k of characteristic p.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · full declaration
theorem zmodPowerSeries_moduleFinite [Finite k] :
    letI : Algebra (ZMod p) k := ZMod.algebra k p
    Module.Finite (ZMod p)⟦X⟧ k⟦X⟧ := by
  let : Algebra (ZMod p) k := ZMod.algebra k p
  have : FiniteDimensional (ZMod p) k :=
    zmod_finiteDimensional_of_finite p k
  exact powerSeries_moduleFinite_of_finiteDimensional (R := ZMod p) (A := k)
def

zmodPowerSeriesCoeffMap

L107 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodPowerSeriesCoeffMap
Documentation

Coefficientwise map on power series induced by the prime-field embedding ZMod p -> k.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
def zmodPowerSeriesCoeffMap :
    (ZMod p)⟦X⟧ →+* k⟦X⟧
theorem

zmodPowerSeriesCoeffMap_C

L117 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodPowerSeriesCoeffMap_C
Documentation

Establishes the identity zmodPowerSeriesCoeffMap p k (PowerSeries.C a) = PowerSeries.C ((ZMod.castHom (m := p) dvd_rfl k) a).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodPowerSeriesCoeffMap_C (a : ZMod p) :
    zmodPowerSeriesCoeffMap p k (PowerSeries.C a) =
      PowerSeries.C ((ZMod.castHom (m := p) dvd_rfl k) a)
theorem

zmodPowerSeriesCoeffMap_X

L128 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodPowerSeriesCoeffMap_X
Documentation

Establishes the identity zmodPowerSeriesCoeffMap p k PowerSeries.X = PowerSeries.X.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodPowerSeriesCoeffMap_X :
    zmodPowerSeriesCoeffMap p k PowerSeries.X = PowerSeries.X
theorem

zmodPowerSeriesCoeffMap_finite

L135 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodPowerSeriesCoeffMap_finite
Documentation

The coefficientwise power-series map is finite when the coefficient field extension k / F_p is finite.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodPowerSeriesCoeffMap_finite [Finite k] :
    (zmodPowerSeriesCoeffMap p k).Finite
theorem

zmodPowerSeriesCoeffMap_X_isUnit

L143 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodPowerSeriesCoeffMap_X_isUnit
Documentation

The image of X under the coefficientwise power-series map is invertible after passing to Laurent series.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodPowerSeriesCoeffMap_X_isUnit :
    IsUnit
      ((algebraMap k⟦X⟧ k⸨X⸩).comp (zmodPowerSeriesCoeffMap p k)
        (PowerSeries.X : (ZMod p)⟦X⟧))
def

zmodLaurentCoeffMap

L151 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffMap
Documentation

Coefficientwise Laurent-series map induced from ZMod p -> k.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
def zmodLaurentCoeffMap :
    (ZMod p)⸨X⸩ →+* k⸨X⸩
theorem

zmodLaurentCoeffMap_coeff

L189 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffMap_coeff
Documentation

Establishes the identity (zmodLaurentCoeffMap p k f).coeff n = (ZMod.castHom (m := p) dvd_rfl k) (f.coeff n).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodLaurentCoeffMap_coeff (f : (ZMod p)⸨X⸩) (n : ℤ) :
    (zmodLaurentCoeffMap p k f).coeff n =
      (ZMod.castHom (m := p) dvd_rfl k) (f.coeff n)
theorem

zmodLaurentCoeffMap_C

L205 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffMap_C
Documentation

Establishes the identity zmodLaurentCoeffMap p k (HahnSeries.C (Γ := ℤ) a : (ZMod p)⸨X⸩) = (HahnSeries.C (Γ := ℤ) ((ZMod.castHom (m := p) dvd_rfl k) a) : k⸨X⸩).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodLaurentCoeffMap_C (a : ZMod p) :
    zmodLaurentCoeffMap p k (HahnSeries.C (Γ := ℤ) a : (ZMod p)⸨X⸩) =
      (HahnSeries.C (Γ := ℤ) ((ZMod.castHom (m := p) dvd_rfl k) a) :
        k⸨X⸩)
theorem

zmodLaurentCoeffMap_comp_powerSeries

L225 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffMap_comp_powerSeries
Documentation

Establishes the identity (zmodLaurentCoeffMap p k).comp (algebraMap (ZMod p)⟦X⟧ (ZMod p)⸨X⸩) = (algebraMap k⟦X⟧ k⸨X⸩).comp (zmodPowerSeriesCoeffMap p k).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodLaurentCoeffMap_comp_powerSeries :
    (zmodLaurentCoeffMap p k).comp
        (algebraMap (ZMod p)⟦X⟧ (ZMod p)⸨X⸩) =
      (algebraMap k⟦X⟧ k⸨X⸩).comp
        (zmodPowerSeriesCoeffMap p k)
theorem

zmodLaurentCoeffMap_powerSeries_X

L245 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffMap_powerSeries_X
Documentation

Establishes the identity zmodLaurentCoeffMap p k ((algebraMap (ZMod p)⟦X⟧ (ZMod p)⸨X⸩) (PowerSeries.X : (ZMod p)⟦X⟧)) = (algebraMap k⟦X⟧ k⸨X⸩) (PowerSeries.X : k⟦X⟧).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodLaurentCoeffMap_powerSeries_X :
    zmodLaurentCoeffMap p k
        ((algebraMap (ZMod p)⟦X⟧ (ZMod p)⸨X⸩)
          (PowerSeries.X : (ZMod p)⟦X⟧)) =
      (algebraMap k⟦X⟧ k⸨X⸩) (PowerSeries.X : k⟦X⟧)
def

zmodLaurentCoeffAlgebra

L260 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffAlgebra
Documentation

The induced algebra structure of k((X)) over F_p((X)).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
def zmodLaurentCoeffAlgebra :
    Algebra ((ZMod p)⸨X⸩) (k⸨X⸩)
theorem

zmodLaurentCoeffAlgebra_algebraMap

L265 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffAlgebra_algebraMap
Documentation

The algebra map from F_p((X)) to k((X)) is the coefficientwise extension map.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · full declaration
theorem zmodLaurentCoeffAlgebra_algebraMap :
    letI : Algebra ((ZMod p)⸨X⸩) (k⸨X⸩) :=
      zmodLaurentCoeffAlgebra p k
    algebraMap ((ZMod p)⸨X⸩) (k⸨X⸩) =
      zmodLaurentCoeffMap p k := by
  rfl
def

zmodLaurentCoeffCoord

L274 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffCoord
Documentation

The Laurent series whose coefficients are one coordinate of the coefficients of f with respect to a fixed ZMod p-basis of k.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
def zmodLaurentCoeffCoord {ι : Type*} [Algebra (ZMod p) k]
    (b : Module.Basis ι (ZMod p) k) (f : k⸨X⸩) (i : ι) :
    (ZMod p)⸨X⸩
theorem

zmodLaurentCoeffCoord_coeff

L293 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffCoord_coeff
Documentation

Establishes the identity (zmodLaurentCoeffCoord (p := p) (k := k) b f i).coeff n = b.repr (f.coeff n) i.

Source context 7 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
omit [CharP k p] in
Lean source · statement
theorem zmodLaurentCoeffCoord_coeff {ι : Type*} [Algebra (ZMod p) k]
    (b : Module.Basis ι (ZMod p) k) (f : k⸨X⸩) (i : ι) (n : ℤ) :
    (zmodLaurentCoeffCoord (p := p) (k := k) b f i).coeff n =
      b.repr (f.coeff n) i
theorem

zmodLaurent_moduleFinite

L303 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurent_moduleFinite
Documentation

Finite generation of k((X)) as a module over F_p((X)).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · full declaration
theorem zmodLaurent_moduleFinite [Finite k] :
    letI : Algebra ((ZMod p)⸨X⸩) (k⸨X⸩) :=
      zmodLaurentCoeffAlgebra p k
    Module.Finite ((ZMod p)⸨X⸩) (k⸨X⸩) := by
  classical
  let : Algebra (ZMod p) k := ZMod.algebra k p
  have : FiniteDimensional (ZMod p) k :=
    zmod_finiteDimensional_of_finite p k
  let : Algebra ((ZMod p)⸨X⸩) (k⸨X⸩) :=
    zmodLaurentCoeffAlgebra p k
  let b : Module.Basis (Fin (Module.finrank (ZMod p) k)) (ZMod p) k :=
    Module.finBasis (ZMod p) k
  let gens : Finset k⸨X⸩ :=
    Finset.univ.image fun i : Fin (Module.finrank (ZMod p) k) =>
      (HahnSeries.C (Γ := ℤ) (b i) : k⸨X⸩)
  refine ⟨gens, ?_⟩
  rw [eq_top_iff]
  intro f _hf
  let coord : Fin (Module.finrank (ZMod p) k) → (ZMod p)⸨X⸩ :=
    fun i => zmodLaurentCoeffCoord (p := p) (k := k) b f i
  have hsum :
      (∑ i : Fin (Module.finrank (ZMod p) k),
          coord i • (HahnSeries.C (Γ := ℤ) (b i) : k⸨X⸩)) = f := by
    ext n
    rw [HahnSeries.coeff_sum]
    calc
      (∑ i : Fin (Module.finrank (ZMod p) k),
          (coord i • (HahnSeries.C (Γ := ℤ) (b i) : k⸨X⸩) :
            k⸨X⸩).coeff n) =
        ∑ i : Fin (Module.finrank (ZMod p) k),
          algebraMap (ZMod p) k (b.repr (f.coeff n) i) * b i := by
          apply Finset.sum_congr rfl
          intro i _
          change
            ((HahnSeries.map
                (zmodLaurentCoeffCoord (p := p) (k := k) b f i)
                (algebraMap (ZMod p) k)) *
              (HahnSeries.C (Γ := ℤ) (b i) : k⸨X⸩)).coeff n = _
          rw [mul_comm, HahnSeries.C_mul_eq_smul, HahnSeries.coeff_smul,
            HahnSeries.map_coeff, zmodLaurentCoeffCoord_coeff]
          exact mul_comm _ _
      _ = f.coeff n := by
        simpa [Algebra.smul_def] using (b.sum_repr (f.coeff n))
  rw [← hsum]
  exact
    Submodule.sum_mem _ fun i _ =>
      Submodule.smul_mem _ (coord i) <|
        Submodule.subset_span (by
          change (HahnSeries.C (Γ := ℤ) (b i) : k⸨X⸩) ∈
            (gens : Set k⸨X⸩)
          simp [gens])
theorem

zmodLaurentCoeffMap_finite

L357 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurentCoeffMap_finite
Documentation

The Laurent-series coefficient map F_p((X)) -> k((X)) is finite when k is finite.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · statement
theorem zmodLaurentCoeffMap_finite [Finite k] :
    (zmodLaurentCoeffMap p k).Finite
theorem

zmodLaurent_finiteDimensional

L366 ↗
LocalFieldTheory.DiscreteValuationField.FiniteCoefficientLaurent.zmodLaurent_finiteDimensional
Documentation

Finite-dimensionality of k((X)) over the literal prime-field Laurent series F_p((X)).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
namespace FiniteCoefficientLaurent
open scoped LaurentSeries PowerSeries
variable (p : ℕ) (k : Type u) [Fact p.Prime] [Field k] [CharP k p]
Lean source · full declaration
theorem zmodLaurent_finiteDimensional [Finite k] :
    letI : Algebra ((ZMod p)⸨X⸩) (k⸨X⸩) :=
      zmodLaurentCoeffAlgebra p k
    FiniteDimensional ((ZMod p)⸨X⸩) (k⸨X⸩) := by
  let : Algebra ((ZMod p)⸨X⸩) (k⸨X⸩) :=
    zmodLaurentCoeffAlgebra p k
  exact zmodLaurent_moduleFinite p k

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