NYLL
Module

LaurentModel.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Existence.LaurentModel
5 declarations indexed from sourceView source ↗

Module documentation

Equal-characteristic Laurent-series model

For the positive-characteristic branch of the existence theorem, the local-field classification identifies a local field with a Laurent-series field over its residue field. The earlier complete-DVR development constructs the coefficient section and proves that Laurent series evaluation is onto. Here we package that concrete evaluation as the actual field equivalence needed by the Lubin--Tate construction; no existence or norm-subgroup statement is assumed.

Imports1
Imported by5

Declarations

def

equalCharacteristicLaurentUniformizer

L37 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentUniformizer
Documentation

The Laurent-series parameter T, written through the localization map from power series so its later transport to the local field is definitional.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLaurentUniformizer
    (F : LocalField.{u, v} K) : F.residueField⸨X⸩
def

equalCharacteristicLaurentRingEquiv

L47 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentRingEquiv
Documentation

In equal characteristic, Laurent-series evaluation at a chosen uniformizer is a field equivalence onto the local field.

Source context 8 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank
) in
Lean source · statement
def equalCharacteristicLaurentRingEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    F.residueField⸨X⸩ ≃+* K
theorem

equalCharacteristicLaurentRingEquiv_apply

L77 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentRingEquiv_apply
Documentation

States the theorem equalCharacteristicLaurentRingEquiv_apply.

Source context 8 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank
) in
Lean source · full declaration
theorem equalCharacteristicLaurentRingEquiv_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (x : F.residueField⸨X⸩) :
    equalCharacteristicLaurentRingEquiv F hpi x =
      CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom
        (F := F.toCompleteDVF) F.residueCharacteristic
        (n :=
          ⟨CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F,
            Module.finrank_pos⟩)
        (by
          simpa using
            residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank F)
        pi hpi x := by
  rfl
theorem

equalCharacteristicLaurentRingEquiv_algebraMap_C

L100 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentRingEquiv_algebraMap_C
Documentation

States the theorem equalCharacteristicLaurentRingEquiv_algebraMap_C.

Source context 8 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank
) in
Lean source · full declaration
theorem equalCharacteristicLaurentRingEquiv_algebraMap_C
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K))
    (a : F.residueField) :
    equalCharacteristicLaurentRingEquiv F hpi
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.C a)) =
      CompleteDVF.EqualCharacteristicLaurent.coeffHom
        (F := F.toCompleteDVF) F.residueCharacteristic
        (n :=
          ⟨CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F,
            Module.finrank_pos⟩)
        (by
          simpa using
            residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank F)
        a := by
  rw [equalCharacteristicLaurentRingEquiv_apply]
  exact
    CompleteDVF.EqualCharacteristicLaurent.adicLaurentSeriesEvalHom_algebraMap_C
      (F := F.toCompleteDVF) F.residueCharacteristic
      (n :=
        ⟨CompleteDVF.higherPrincipalUnitGroup.iwasawaResidueRank F,
          Module.finrank_pos⟩)
      (by
        simpa using
          residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank F)
      pi hpi a
theorem

equalCharacteristicLaurentRingEquiv_algebraMap_X

L135 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLaurentRingEquiv_algebraMap_X
Documentation

States the theorem equalCharacteristicLaurentRingEquiv_algebraMap_X.

Source context 8 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  residueField_card_eq_residueCharacteristic_pow_iwasawaResidueRank
) in
Lean source · statement
theorem equalCharacteristicLaurentRingEquiv_algebraMap_X
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {pi : F.valuationSubring}
    (hpi : F.valuation.IsUniformizer (pi : K)) :
    equalCharacteristicLaurentRingEquiv F hpi
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩
          (PowerSeries.X : F.residueField⟦X⟧)) =
      (pi : K)

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