Module

LaurentSeriesFrobenius.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Frobenius.LaurentSeriesFrobenius

42 declarations indexed from sourceView source ↗

Module documentation

The equal-characteristic completed-unramified construction: finite unramified coefficient

extensions in equal characteristic

For a finite extension l / k of finite fields, coefficientwise extension makes l((T)) a finite extension of k((T)) of the same degree. Every automorphism of l / k extends coefficientwise, and these extensions exhaust the Galois group of l((T)) / k((T)). In particular, arithmetic Frobenius on l gives the genuine Frobenius automorphism of this finite Laurent-series base change and fixes T.

This is the finite unramified source used to model the completed maximal unramified field in the equal-characteristic completed-unramified construction. The construction is coefficientwise and does not postulate an abstract unramified extension.

Imports6

Mathlib.SetTheory.Cardinal.Finite
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FiniteCoefficientLaurent
Mathlib.FieldTheory.Finite.Extension
Mathlib.FieldTheory.Galois.Profinite
Mathlib.LinearAlgebra.Basis.Basic
Mathlib.LinearAlgebra.Dimension.Free

Imported by5

def

laurentSeriesCoefficientMap

L47 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientMap

Documentation

The coefficientwise map k((T)) -> l((T)) induced by a ring map k -> l.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}

Lean source · full declaration

def laurentSeriesCoefficientMap
    {k : Type u} {l : Type v} [Field k] [Field l]
    (f : k →+* l) : k⸨X⸩ →+* l⸨X⸩ where
  toFun x := HahnSeries.map x f
  map_zero' := by
    change HahnSeries.map (0 : k⸨X⸩) f.toZeroHom = 0
    exact HahnSeries.map_zero (Γ := ℤ) f.toZeroHom
  map_one' := by
    change HahnSeries.map (1 : k⸨X⸩) f.toMonoidWithZeroHom = 1
    exact HahnSeries.map_one (Γ := ℤ) f.toMonoidWithZeroHom
  map_add' x y := by
    change HahnSeries.map (x + y) f.toAddMonoidHom =
      HahnSeries.map x f.toAddMonoidHom + HahnSeries.map y f.toAddMonoidHom
    exact HahnSeries.map_add (Γ := ℤ) f.toAddMonoidHom
  map_mul' x y := by
    change HahnSeries.map (x * y) f.toNonUnitalRingHom =
      HahnSeries.map x f.toNonUnitalRingHom * HahnSeries.map y f.toNonUnitalRingHom
    exact HahnSeries.map_mul (Γ := ℤ) f.toNonUnitalRingHom

theorem

laurentSeriesCoefficientMap_coeff

L68 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientMap_coeff

Documentation

Mapping Laurent-series coefficients applies the ring homomorphism coefficientwise.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}

Lean source · statement

theorem laurentSeriesCoefficientMap_coeff
    [Field k] [Field l] (f : k →+* l) (x : k⸨X⸩) (m : ℤ) :
    (laurentSeriesCoefficientMap f x).coeff m = f (x.coeff m)

theorem

laurentSeriesCoefficientMap_C

L75 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientMap_C

Documentation

The coefficient map sends a constant series to the mapped constant series.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}

Lean source · statement

theorem laurentSeriesCoefficientMap_C
    [Field k] [Field l] (f : k →+* l) (a : k) :
    laurentSeriesCoefficientMap f (HahnSeries.C (Γ := ℤ) a) =
      HahnSeries.C (Γ := ℤ) (f a)

theorem

laurentSeriesCoefficientMap_single_one

L84 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientMap_single_one

Documentation

The coefficient map fixes the Laurent uniformizer monomial.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}

Lean source · statement

theorem laurentSeriesCoefficientMap_single_one
    [Field k] [Field l] (f : k →+* l) :
    laurentSeriesCoefficientMap f (HahnSeries.single (1 : ℤ) 1) =
      (HahnSeries.single (1 : ℤ) 1 : l⸨X⸩)

def

laurentSeriesCoefficientAlgebra

L96 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientAlgebra

Documentation

The induced k((T))-algebra structure on l((T)).

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}

Lean source · statement

def laurentSeriesCoefficientAlgebra
    [Field k] [Field l] [Algebra k l] : Algebra k⸨X⸩ l⸨X⸩

theorem

laurentSeriesCoefficientAlgebra_algebraMap

L102 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientAlgebra_algebraMap

Documentation

The induced Laurent-series algebra map is the coefficientwise scalar map.

Source context 6 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}

Lean source · full declaration

theorem laurentSeriesCoefficientAlgebra_algebraMap
    [Field k] [Field l] [Algebra k l] :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    algebraMap k⸨X⸩ l⸨X⸩ =
      laurentSeriesCoefficientMap (algebraMap k l) :=
  rfl

def

laurentSeriesCoefficientCoord

L113 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientCoord

Documentation

One coefficient coordinate of a Laurent series with respect to a basis of the coefficient extension.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · statement

def laurentSeriesCoefficientCoord
    [Field k] [Field l] [Algebra k l]
    {ι : Type*} (b : Module.Basis ι k l)
    (x : l⸨X⸩) (i : ι) : k⸨X⸩

theorem

laurentSeriesCoefficientCoord_coeff

L129 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientCoord_coeff

Documentation

A Laurent coordinate series records the corresponding basis coordinate coefficientwise.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · statement

theorem laurentSeriesCoefficientCoord_coeff
    [Field k] [Field l] [Algebra k l]
    {ι : Type*} (b : Module.Basis ι k l)
    (x : l⸨X⸩) (i : ι) (m : ℤ) :
    (laurentSeriesCoefficientCoord b x i).coeff m =
      b.repr (x.coeff m) i

theorem

laurentSeriesCoefficientBasis_linearIndependent

L143 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientBasis_linearIndependent

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteBasis
variable [Field k] [Field l] [Algebra k l]
  {ι : Type*} [Fintype ι]
omit [Fintype ι] in

Lean source · full declaration

theorem laurentSeriesCoefficientBasis_linearIndependent
    [Finite ι]
    (b : Module.Basis ι k l) :
    LinearIndependent k⸨X⸩
      (fun i : ι ↦ (HahnSeries.C (Γ := ℤ) (b i) : l⸨X⸩)) := by
  let : Fintype ι := Fintype.ofFinite ι
  let : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
  classical
  rw [Fintype.linearIndependent_iff]
  intro g hg i
  ext m
  have hcoeff := congrArg (fun x : l⸨X⸩ ↦ x.coeff m) hg
  have halgebraMap_coeff (x : k⸨X⸩) :
      (algebraMap k⸨X⸩ l⸨X⸩ x).coeff m =
        algebraMap k l (x.coeff m) := by
    change
      (laurentSeriesCoefficientMap (algebraMap k l) x).coeff m =
        algebraMap k l (x.coeff m)
    exact laurentSeriesCoefficientMap_coeff (algebraMap k l) x m
  have hsum :
      ∑ j : ι, algebraMap k l ((g j).coeff m) * b j = 0 := by
    simpa [Algebra.smul_def, laurentSeriesCoefficientAlgebra,
      laurentSeriesCoefficientMap, halgebraMap_coeff, mul_comm] using hcoeff
  have hrepr : ∀ j : ι, (g j).coeff m = 0 := by
    intro j
    have hb := Fintype.linearIndependent_iff.mp b.linearIndependent
      (fun t : ι ↦ (g t).coeff m) (by
        simpa [Algebra.smul_def] using hsum) j
    exact hb
  exact hrepr i

theorem

laurentSeriesCoefficientBasis_span

L175 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientBasis_span

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteBasis
variable [Field k] [Field l] [Algebra k l]
  {ι : Type*} [Fintype ι]
omit [Fintype ι] in

Lean source · full declaration

theorem laurentSeriesCoefficientBasis_span
    [Finite ι]
    (b : Module.Basis ι k l) :
    Submodule.span k⸨X⸩
        (Set.range (fun i : ι ↦
          (HahnSeries.C (Γ := ℤ) (b i) : l⸨X⸩))) = ⊤ := by
  let : Fintype ι := Fintype.ofFinite ι
  let : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
  classical
  rw [eq_top_iff]
  intro x _hx
  let coord : ι → k⸨X⸩ := fun i ↦ laurentSeriesCoefficientCoord b x i
  have hsum :
      (∑ i : ι, coord i •
        (HahnSeries.C (Γ := ℤ) (b i) : l⸨X⸩)) = x := by
    ext m
    rw [HahnSeries.coeff_sum]
    calc
      (∑ i : ι, (coord i •
          (HahnSeries.C (Γ := ℤ) (b i) : l⸨X⸩) : l⸨X⸩).coeff m) =
          ∑ i : ι, algebraMap k l (b.repr (x.coeff m) i) * b i := by
        apply Finset.sum_congr rfl
        intro i _
        change
          ((HahnSeries.map (coord i) (algebraMap k l)) *
            (HahnSeries.C (Γ := ℤ) (b i) : l⸨X⸩)).coeff m = _
        rw [mul_comm]
        simp [coord, mul_comm]
      _ = x.coeff m := by
        simpa [Algebra.smul_def] using b.sum_repr (x.coeff m)
  rw [← hsum]
  exact Submodule.sum_mem _ fun i _ ↦
    Submodule.smul_mem _ (coord i)
      (Submodule.subset_span ⟨i, rfl⟩)

def

laurentSeriesCoefficientBasis

L212 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientBasis

Documentation

A finite coefficient basis extends coefficientwise to a Laurent-series basis.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteBasis
variable [Field k] [Field l] [Algebra k l]
  {ι : Type*} [Fintype ι]

Lean source · statement

def laurentSeriesCoefficientBasis
    (b : Module.Basis ι k l) : Module.Basis ι k⸨X⸩ l⸨X⸩

theorem

laurentSeriesCoefficientBasis_apply

L221 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientBasis_apply

Documentation

The induced Laurent-series basis consists of constant images of the coefficient basis.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteBasis
variable [Field k] [Field l] [Algebra k l]
  {ι : Type*} [Fintype ι]

Lean source · full declaration

theorem laurentSeriesCoefficientBasis_apply
    (b : Module.Basis ι k l) (i : ι) :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    laurentSeriesCoefficientBasis b i =
      (HahnSeries.C (Γ := ℤ) (b i) : l⸨X⸩) := by
  let : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
  exact Module.Basis.mk_apply _ _ _

theorem

laurentSeriesCoefficient_finiteDimensional

L233 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficient_finiteDimensional

Documentation

Finite-dimensionality is preserved by coefficientwise Laurent-series extension.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · full declaration

theorem laurentSeriesCoefficient_finiteDimensional
    [Field k] [Field l] [Algebra k l] [FiniteDimensional k l] :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    FiniteDimensional k⸨X⸩ l⸨X⸩ := by
  let : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
  let b : Module.Basis (Fin (Module.finrank k l)) k l := Module.finBasis k l
  exact (laurentSeriesCoefficientBasis b).finiteDimensional_of_finite

theorem

laurentSeriesCoefficient_finrank

L242 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficient_finrank

Documentation

Coefficient extension does not change the finite extension degree.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · full declaration

theorem laurentSeriesCoefficient_finrank
    [Field k] [Field l] [Algebra k l] [FiniteDimensional k l] :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    Module.finrank k⸨X⸩ l⸨X⸩ = Module.finrank k l := by
  let : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
  let b : Module.Basis (Fin (Module.finrank k l)) k l := Module.finBasis k l
  let B := laurentSeriesCoefficientBasis b
  let : FiniteDimensional k⸨X⸩ l⸨X⸩ :=
    B.finiteDimensional_of_finite
  simpa [B] using Module.finrank_eq_card_basis B

def

laurentSeriesCoefficientRingEquiv

L255 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientRingEquiv

Documentation

A coefficient-field ring equivalence extends coefficientwise to Laurent series.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · full declaration

def laurentSeriesCoefficientRingEquiv
    [Field k] [Field l] (e : k ≃+* l) : k⸨X⸩ ≃+* l⸨X⸩ where
  toFun := laurentSeriesCoefficientMap e.toRingHom
  invFun := laurentSeriesCoefficientMap e.symm.toRingHom
  left_inv x := by
    ext m
    simp
  right_inv x := by
    ext m
    simp
  map_add' := map_add (laurentSeriesCoefficientMap e.toRingHom)
  map_mul' := map_mul (laurentSeriesCoefficientMap e.toRingHom)

theorem

laurentSeriesCoefficientRingEquiv_coeff

L270 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientRingEquiv_coeff

Documentation

A coefficientwise ring equivalence applies the base equivalence at every exponent.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · statement

theorem laurentSeriesCoefficientRingEquiv_coeff
    [Field k] [Field l] (e : k ≃+* l) (x : k⸨X⸩) (m : ℤ) :
    (laurentSeriesCoefficientRingEquiv e x).coeff m = e (x.coeff m)

def

laurentSeriesCoefficientAlgEquiv

L277 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientAlgEquiv

Documentation

An automorphism of the coefficient extension acts coefficientwise as an automorphism over the Laurent-series base.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · statement

def laurentSeriesCoefficientAlgEquiv
    [Field k] [Field l] [Algebra k l]
    (e : l ≃ₐ[k] l) : l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩

theorem

laurentSeriesCoefficientAlgEquiv_coeff

L294 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientAlgEquiv_coeff

Documentation

A coefficientwise algebra equivalence applies the base automorphism at every exponent.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · full declaration

theorem laurentSeriesCoefficientAlgEquiv_coeff
    [Field k] [Field l] [Algebra k l]
    (e : l ≃ₐ[k] l) (x : l⸨X⸩) (m : ℤ) :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    (laurentSeriesCoefficientAlgEquiv e x).coeff m = e (x.coeff m) :=
  rfl

theorem

laurentSeriesCoefficientAlgEquiv_injective

L302 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientAlgEquiv_injective

Documentation

Coefficientwise extension is faithful on automorphisms.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · full declaration

theorem laurentSeriesCoefficientAlgEquiv_injective
    [Field k] [Field l] [Algebra k l] :
    Function.Injective
      (fun e : l ≃ₐ[k] l ↦
        letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
        laurentSeriesCoefficientAlgEquiv e) := by
  intro e f hef
  apply AlgEquiv.ext
  intro x
  have h := DFunLike.congr_fun hef (HahnSeries.C (Γ := ℤ) x : l⸨X⸩)
  have hc := congrArg (fun y : l⸨X⸩ ↦ y.coeff 0) h
  simpa using hc

def

laurentSeriesCoefficientGalHom

L317 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientGalHom

Documentation

Coefficientwise extension as a homomorphism between the two Galois groups.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · statement

def laurentSeriesCoefficientGalHom
    [Field k] [Field l] [Algebra k l] :
    (l ≃ₐ[k] l) →* (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩)

theorem

laurentSeriesCoefficientGalHom_apply

L337 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientGalHom_apply

Documentation

The Galois homomorphism sends an automorphism to its coefficientwise Laurent action.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · full declaration

theorem laurentSeriesCoefficientGalHom_apply
    [Field k] [Field l] [Algebra k l]
    (e : l ≃ₐ[k] l) :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    laurentSeriesCoefficientGalHom e = laurentSeriesCoefficientAlgEquiv e :=
  rfl

theorem

laurentSeriesCoefficientGalHom_injective

L345 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientGalHom_injective

Documentation

Distinct coefficient automorphisms induce distinct Laurent-series automorphisms.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra

Lean source · full declaration

theorem laurentSeriesCoefficientGalHom_injective
    [Field k] [Field l] [Algebra k l] :
    Function.Injective
      (letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
       laurentSeriesCoefficientGalHom :
        (l ≃ₐ[k] l) → (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩)) :=
  laurentSeriesCoefficientAlgEquiv_injective

theorem

laurentSeriesCoefficientGalHom_surjective

L360 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficientGalHom_surjective

Documentation

For finite coefficient fields, all Laurent-series automorphisms come from coefficient automorphisms.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteFields
variable [Field k] [Finite k] [Field l] [Finite l] [Algebra k l]
omit [Finite k] in

Lean source · full declaration

theorem laurentSeriesCoefficientGalHom_surjective :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    Function.Surjective (laurentSeriesCoefficientGalHom :
      (l ≃ₐ[k] l) → (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩)) := by
  let : Module.Finite k l := Module.Finite.of_finite
  let : FiniteDimensional k⸨X⸩ l⸨X⸩ :=
    laurentSeriesCoefficient_finiteDimensional
  have hcard :
      Nat.card (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩) ≤ Nat.card (l ≃ₐ[k] l) := by
    calc
      Nat.card (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩) ≤
          Module.finrank k⸨X⸩ l⸨X⸩ := by
        simpa only [Nat.card_eq_fintype_card] using
          (AlgEquiv.card_le (F := k⸨X⸩) (K := l⸨X⸩))
      _ = Module.finrank k l := laurentSeriesCoefficient_finrank
      _ = Nat.card (l ≃ₐ[k] l) :=
        (IsGalois.card_aut_eq_finrank k l).symm
  have hbijective : Function.Bijective
      (laurentSeriesCoefficientGalHom :
        (l ≃ₐ[k] l) → (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩)) :=
    Function.Injective.bijective_of_nat_card_le
      laurentSeriesCoefficientGalHom_injective hcard
  exact hbijective.2

theorem

laurentSeriesCoefficient_isGalois

L386 ↗

LubinTate.EqualCharacteristic.laurentSeriesCoefficient_isGalois

Documentation

The coefficient Laurent-series extension is Galois.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteFields
variable [Field k] [Finite k] [Field l] [Finite l] [Algebra k l]
omit [Finite k] in

Lean source · full declaration

theorem laurentSeriesCoefficient_isGalois :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    IsGalois k⸨X⸩ l⸨X⸩ := by
  let : Module.Finite k l := Module.Finite.of_finite
  let : FiniteDimensional k⸨X⸩ l⸨X⸩ :=
    laurentSeriesCoefficient_finiteDimensional
  apply IsGalois.of_card_aut_eq_finrank
  apply Nat.le_antisymm
  · simpa only [Nat.card_eq_fintype_card] using
      (AlgEquiv.card_le (F := k⸨X⸩) (K := l⸨X⸩))
  · calc
      Module.finrank k⸨X⸩ l⸨X⸩ = Nat.card (l ≃ₐ[k] l) := by
        exact laurentSeriesCoefficient_finrank.trans
          (IsGalois.card_aut_eq_finrank k l).symm
      _ ≤ Nat.card (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩) :=
        Nat.card_le_card_of_injective
          (laurentSeriesCoefficientGalHom :
            (l ≃ₐ[k] l) → (l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩))
          laurentSeriesCoefficientGalHom_injective

def

equalCharacteristicLaurentFrobenius

L408 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLaurentFrobenius

Documentation

Arithmetic Frobenius on the coefficient field, extended to Laurent series.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteFields
variable [Field k] [Finite k] [Field l] [Finite l] [Algebra k l]

Lean source · full declaration

def equalCharacteristicLaurentFrobenius :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    l⸨X⸩ ≃ₐ[k⸨X⸩] l⸨X⸩ := by
  letI : Fintype k := Fintype.ofFinite k
  exact laurentSeriesCoefficientAlgEquiv
    (k := k) (l := l)
    (FiniteField.frobeniusAlgEquivOfAlgebraic k l)

theorem

equalCharacteristicLaurentFrobenius_coeff

L418 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLaurentFrobenius_coeff

Documentation

Laurent Frobenius raises each coefficient to the residue-field cardinality.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteFields
variable [Field k] [Finite k] [Field l] [Finite l] [Algebra k l]

Lean source · full declaration

theorem equalCharacteristicLaurentFrobenius_coeff
    (x : l⸨X⸩) (m : ℤ) :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    (equalCharacteristicLaurentFrobenius (k := k) (l := l) x).coeff m =
      (x.coeff m) ^ Nat.card k := by
  let : Fintype k := Fintype.ofFinite k
  simp [equalCharacteristicLaurentFrobenius,
    Nat.card_eq_fintype_card]

theorem

equalCharacteristicLaurentFrobenius_single_one

L429 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLaurentFrobenius_single_one

Documentation

Laurent Frobenius fixes the Laurent uniformizer.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section FiniteFields
variable [Field k] [Finite k] [Field l] [Finite l] [Algebra k l]

Lean source · full declaration

theorem equalCharacteristicLaurentFrobenius_single_one :
    letI : Algebra k⸨X⸩ l⸨X⸩ := laurentSeriesCoefficientAlgebra
    equalCharacteristicLaurentFrobenius (k := k) (l := l)
        (HahnSeries.single (1 : ℤ) 1 : l⸨X⸩) =
      HahnSeries.single (1 : ℤ) 1 := by
  let : Fintype k := Fintype.ofFinite k
  ext m
  by_cases h : m = 1
  · subst m
    simp
  · simp [HahnSeries.coeff_single_of_ne h]

def

equalCharacteristicFiniteUnramifiedExtension

L450 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtension

Documentation

The finite unramified Laurent-series extension obtained from the chosen degree-n extension of the residue field.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

def equalCharacteristicFiniteUnramifiedExtension

instance

equalCharacteristicFiniteUnramifiedExtension_field

L454 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtension_field

Documentation

The finite unramified Laurent-series extension is a field.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

instance equalCharacteristicFiniteUnramifiedExtension_field :
    Field (equalCharacteristicFiniteUnramifiedExtension k p n)

instance

equalCharacteristicFiniteUnramifiedAlgebra

L460 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedAlgebra

Documentation

The finite unramified extension is an algebra over the base Laurent field.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

instance equalCharacteristicFiniteUnramifiedAlgebra :
    Algebra k⸨X⸩ (equalCharacteristicFiniteUnramifiedExtension k p n)

instance

equalCharacteristicFiniteUnramifiedModule

L466 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedModule

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]
section

Lean source · statement

instance equalCharacteristicFiniteUnramifiedModule :
    @Module k⸨X⸩ (equalCharacteristicFiniteUnramifiedExtension k p n)
      (inferInstance : DivisionRing k⸨X⸩).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicFiniteUnramifiedExtension k p n)).toAddCommMonoid

instance

equalCharacteristicFiniteUnramifiedFiniteDimensional

L475 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedFiniteDimensional

Documentation

The finite unramified Laurent extension is finite-dimensional over the base.

Source context 11 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]
section
local instance equalCharacteristicFiniteUnramifiedModule :
    @Module k⸨X⸩ (equalCharacteristicFiniteUnramifiedExtension k p n)
      (inferInstance : DivisionRing k⸨X⸩).toRing.toSemiring
      (inferInstance : AddCommGroup
        (equalCharacteristicFiniteUnramifiedExtension k p n)).toAddCommMonoid :=
  @Algebra.toModule k⸨X⸩ (equalCharacteristicFiniteUnramifiedExtension k p n)
    _ _ (equalCharacteristicFiniteUnramifiedAlgebra k p n)

Lean source · statement

instance equalCharacteristicFiniteUnramifiedFiniteDimensional :
    FiniteDimensional k⸨X⸩
      (equalCharacteristicFiniteUnramifiedExtension k p n)

def

equalCharacteristicFiniteUnramifiedExtensionEquivLaurentSeries

L484 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtensionEquivLaurentSeries

Documentation

Comparison with the Laurent-series presentation over the chosen finite coefficient extension.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

def equalCharacteristicFiniteUnramifiedExtensionEquivLaurentSeries :
    equalCharacteristicFiniteUnramifiedExtension k p n ≃+*
      (FiniteField.Extension k p n)⸨X⸩

def

equalCharacteristicFiniteUnramifiedExtensionAlgEquivLaurentSeries

L491 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtensionAlgEquivLaurentSeries

Documentation

Algebra-linear comparison with the Laurent-series presentation. This is the degree-preserving bridge for the named finite unramified extension.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

def equalCharacteristicFiniteUnramifiedExtensionAlgEquivLaurentSeries :
    equalCharacteristicFiniteUnramifiedExtension k p n ≃ₐ[k⸨X⸩]
      (FiniteField.Extension k p n)⸨X⸩

def

equalCharacteristicFiniteUnramifiedExtensionOfLaurentSeries

L499 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtensionOfLaurentSeries

Documentation

Construct a named finite unramified element from a Laurent series.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

def equalCharacteristicFiniteUnramifiedExtensionOfLaurentSeries :
    (FiniteField.Extension k p n)⸨X⸩ →+*
      equalCharacteristicFiniteUnramifiedExtension k p n

def

equalCharacteristicFiniteUnramifiedExtensionToLaurentSeries

L506 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtensionToLaurentSeries

Documentation

Read a named finite unramified element as a Laurent series.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

def equalCharacteristicFiniteUnramifiedExtensionToLaurentSeries :
    equalCharacteristicFiniteUnramifiedExtension k p n →+*
      (FiniteField.Extension k p n)⸨X⸩

def

equalCharacteristicFiniteUnramifiedExtensionCoeff

L513 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtensionCoeff

Documentation

The coefficient of a named finite unramified Laurent element.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

def equalCharacteristicFiniteUnramifiedExtensionCoeff
    (x : equalCharacteristicFiniteUnramifiedExtension k p n) (m : ℤ) :
    FiniteField.Extension k p n

theorem

equalCharacteristicFiniteUnramifiedExtension_finrank

L521 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtension_finrank

Documentation

The chosen coefficient extension has exactly the requested Laurent degree.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

theorem equalCharacteristicFiniteUnramifiedExtension_finrank :
    Module.finrank k⸨X⸩
      (equalCharacteristicFiniteUnramifiedExtension k p n) = n

theorem

equalCharacteristicFiniteUnramifiedExtension_isGalois

L535 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedExtension_isGalois

Documentation

The chosen finite unramified Laurent-series extension is Galois.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

theorem equalCharacteristicFiniteUnramifiedExtension_isGalois :
    IsGalois k⸨X⸩
      (equalCharacteristicFiniteUnramifiedExtension k p n)

def

equalCharacteristicFiniteUnramifiedFrobenius

L541 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedFrobenius

Documentation

Its distinguished arithmetic Frobenius.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

def equalCharacteristicFiniteUnramifiedFrobenius :
    Gal(equalCharacteristicFiniteUnramifiedExtension k p n / k⸨X⸩)

theorem

equalCharacteristicFiniteUnramifiedFrobenius_coeff

L547 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedFrobenius_coeff

Documentation

Finite unramified Frobenius applies finite-field Frobenius coefficientwise.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

theorem equalCharacteristicFiniteUnramifiedFrobenius_coeff
    (x : equalCharacteristicFiniteUnramifiedExtension k p n) (m : ℤ) :
    equalCharacteristicFiniteUnramifiedExtensionCoeff k p n
        (equalCharacteristicFiniteUnramifiedFrobenius k p n x) m =
      (equalCharacteristicFiniteUnramifiedExtensionCoeff k p n x m) ^
        Nat.card k

theorem

equalCharacteristicFiniteUnramifiedFrobenius_pow_surjective

L560 ↗

LubinTate.EqualCharacteristic.equalCharacteristicFiniteUnramifiedFrobenius_pow_surjective

Documentation

Every automorphism of the chosen unramified factor is a power of its arithmetic Frobenius.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
variable {k : Type u} {l : Type v}
attribute [local instance] laurentSeriesCoefficientAlgebra
section ChosenFiniteExtension
variable (k : Type u) [Field k] [Finite k]
  (p n : ℕ) [Fact p.Prime] [CharP k p] [NeZero n]

Lean source · statement

theorem equalCharacteristicFiniteUnramifiedFrobenius_pow_surjective
    (σ : Gal(equalCharacteristicFiniteUnramifiedExtension k p n/k⸨X⸩)) :
    ∃ i < n, equalCharacteristicFiniteUnramifiedFrobenius k p n ^ i = σ

Module documentation

The equal-characteristic completed-unramified construction: finite unramified coefficient

Declarations