Module

FreeRankOne.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.FreeRankOne

39 declarations indexed from sourceView source ↗

Module documentation

The primitive-division-module equivalence: equal-characteristic division points are free of

rank one

For the standard equal-characteristic Lubin--Tate series, the points killed by the (n + 1)-st iterate form a free rank-one module over κ⟦T⟧/(T^(n+1)). The shift is intentional: the existing division-tower The primitive polynomial is indexed by n, while its roots lie at division level n + 1.

Imports6

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.AmbientDivisionTorsion
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.FiniteParameters
Mathlib.Algebra.Module.RingHom
Mathlib.Data.Fintype.EquivFin
Mathlib.LinearAlgebra.FreeModule.Basic

Imported by4

structure

equalCharacteristicLubinTateParameter

L44 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameter

Documentation

All coefficients visible at division level n + 1. In contrast with the unit parameters used for the primitive roots in the uniformizer norm identity, the constant coefficient is allowed to vanish; this is necessary to parametrize every division point.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

structure equalCharacteristicLubinTateParameter
    (F : LocalField.{u, v} K) (n : ℕ) where
  /-- The coefficients in degrees `0` through `n` of the represented truncated series. -/
  coeff : Fin (n + 1) → F.residueField

instance

equalCharacteristicLubinTateParameter_coeFun

L50 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameter_coeFun

Documentation

A Lubin–Tate parameter evaluates to its finite coefficient function.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

instance equalCharacteristicLubinTateParameter_coeFun
    (F : LocalField.{u, v} K) (n : ℕ) :
    CoeFun (equalCharacteristicLubinTateParameter F n)
      (fun _ => Fin (n + 1) → F.residueField) :=
  ⟨equalCharacteristicLubinTateParameter.coeff⟩

def

equalCharacteristicLubinTateParameterOfFunction

L57 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameterOfFunction

Documentation

Construct a finite parameter from its coefficient function.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateParameterOfFunction
    (F : LocalField.{u, v} K) (n : ℕ)
    (coeff : Fin (n + 1) → F.residueField) :
    equalCharacteristicLubinTateParameter F n

def

equalCharacteristicLubinTateParameterEquiv

L64 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameterEquiv

Documentation

Comparison with the raw finite coefficient function.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

def equalCharacteristicLubinTateParameterEquiv
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTateParameter F n ≃
      (Fin (n + 1) → F.residueField) where
  toFun := equalCharacteristicLubinTateParameter.coeff
  invFun := equalCharacteristicLubinTateParameterOfFunction F n
  left_inv a := by cases a; rfl
  right_inv _ := rfl

theorem

equalCharacteristicLubinTateParameter_ext

L75 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameter_ext

Documentation

Lubin–Tate parameters are equal when all their coefficients agree.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateParameter_ext
    (F : LocalField.{u, v} K) (n : ℕ)
    {a b : equalCharacteristicLubinTateParameter F n}
    (hcoeff : a.coeff = b.coeff) :
    a = b

instance

equalCharacteristicLubinTateParameter_finite

L86 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameter_finite

Documentation

The finite coefficient parameter space is finite.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

instance equalCharacteristicLubinTateParameter_finite
    (F : LocalField.{u, v} K) (n : ℕ) :
    Finite (equalCharacteristicLubinTateParameter F n)

def

equalCharacteristicLubinTateParameterSeries

L93 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameterSeries

Documentation

The canonical polynomial representative of a finite parameter.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateParameterSeries
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateParameter F n) :
    F.residueField⟦X⟧

theorem

equalCharacteristicLubinTateParameterSeries_coeff

L102 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameterSeries_coeff

Documentation

The parameter power series recovers each stored finite coefficient.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateParameterSeries_coeff
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateParameter F n)
    (i : Fin (n + 1)) :
    PowerSeries.coeff i
        (equalCharacteristicLubinTateParameterSeries F n a) = a i

def

equalCharacteristicLubinTateParameterRoot

L114 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameterRoot

Documentation

Evaluation of a finite parameter at the chosen primitive division-level n + 1 point.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateParameterRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateParameter F n) :
    equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
      (equalCharacteristicSeparableUniformizer F) (n + 1)

theorem

equalCharacteristicLubinTateParameterRoot_injective

L133 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameterRoot_injective

Documentation

The primitive point detects every coefficient modulo T^(n+1).

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateParameterRoot_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Injective (equalCharacteristicLubinTateParameterRoot F n)

theorem

equalCharacteristicLubinTateParameter_natCard

L153 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameter_natCard

Documentation

The full finite parameter type has q^(n+1) elements.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateParameter_natCard
    (F : LocalField.{u, v} K) (n : ℕ) :
    Nat.card (equalCharacteristicLubinTateParameter F n) =
      Nat.card F.residueField ^ (n + 1)

def

equalCharacteristicLubinTateTorsionEquivRootSet

L162 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTorsionEquivRootSet

Documentation

Level n + 1 torsion is exactly the root set of the corresponding division polynomial.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

def equalCharacteristicLubinTateTorsionEquivRootSet
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
        (equalCharacteristicSeparableUniformizer F) (n + 1) ≃
      (equalCharacteristicLubinTatePiPolynomialIterate F (n + 1)).rootSet
        (SeparableClosure F.residueField⸨X⸩) where
  toFun x := ⟨x.1, by
    have hP : equalCharacteristicLubinTatePiPolynomialIterate F (n + 1) ≠ 0 := by
      apply Polynomial.ne_zero_of_natDegree_gt
      · rw [equalCharacteristicLubinTatePiPolynomialIterate_natDegree]
        exact Nat.pow_pos Nat.card_pos
    rw [Polynomial.mem_rootSet_of_ne hP, Polynomial.aeval_def,
      ← equalCharacteristicSeparableBaseHom_eq_algebraMap,
      equalCharacteristicLubinTatePiPolynomialIterate_eval₂]
    exact x.2⟩
  invFun x := ⟨x.1, by
    have hP : equalCharacteristicLubinTatePiPolynomialIterate F (n + 1) ≠ 0 := by
      apply Polynomial.ne_zero_of_natDegree_gt
      · rw [equalCharacteristicLubinTatePiPolynomialIterate_natDegree]
        exact Nat.pow_pos Nat.card_pos
    have hx := (Polynomial.mem_rootSet_of_ne hP).mp x.2
    rw [Polynomial.aeval_def,
      ← equalCharacteristicSeparableBaseHom_eq_algebraMap,
      equalCharacteristicLubinTatePiPolynomialIterate_eval₂] at hx
    exact hx⟩
  left_inv x := rfl
  right_inv x := rfl

instance

equalCharacteristicLubinTateAmbientTorsion_finite

L193 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientTorsion_finite

Documentation

The ambient Lubin–Tate torsion module at finite level is finite.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

instance equalCharacteristicLubinTateAmbientTorsion_finite
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Finite
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
        (equalCharacteristicSeparableUniformizer F) (n + 1))

theorem

equalCharacteristicLubinTateAmbientTorsion_natCard

L205 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientTorsion_natCard

Documentation

The level n + 1 division group has q^(n+1) elements.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateAmbientTorsion_natCard
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Nat.card
        (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1)) =
      Nat.card F.residueField ^ (n + 1)

theorem

equalCharacteristicLubinTateParameterRoot_bijective

L225 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateParameterRoot_bijective

Documentation

Every division-level n + 1 division point is obtained uniquely by applying one truncated coefficient series to the chosen primitive point.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateParameterRoot_bijective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Bijective (equalCharacteristicLubinTateParameterRoot F n)

def

equalCharacteristicLubinTateTruncatedRing

L253 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRing

Documentation

The coefficient ring at division level n + 1.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateTruncatedRing
    (F : LocalField.{u, v} K) (n : ℕ)

instance

equalCharacteristicLubinTateTruncatedRing_commRing

L260 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRing_commRing

Documentation

The commutative ring structure on the named truncated coefficient ring.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

instance equalCharacteristicLubinTateTruncatedRing_commRing
    (F : LocalField.{u, v} K) (n : ℕ) :
    CommRing (equalCharacteristicLubinTateTruncatedRing F n)

def

equalCharacteristicLubinTateTruncatedRingEquiv

L270 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRingEquiv

Documentation

Comparison with the quotient-ring presentation used by the ring library.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateTruncatedRingEquiv
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTateTruncatedRing F n ≃+*
      (F.residueField⟦X⟧ ⧸
        Ideal.span ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧))

def

equalCharacteristicLubinTateTruncatedRingMk

L278 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRingMk

Documentation

The canonical projection to the named truncated coefficient ring.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateTruncatedRingMk
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.residueField⟦X⟧ →+* equalCharacteristicLubinTateTruncatedRing F n

theorem

equalCharacteristicLubinTateTruncatedRingMk_eq_iff

L286 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRingMk_eq_iff

Documentation

Two truncated classes agree exactly when their difference is divisible by X ^ (n + 1).

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateTruncatedRingMk_eq_iff
    (F : LocalField.{u, v} K) (n : ℕ) (a b : F.residueField⟦X⟧) :
    equalCharacteristicLubinTateTruncatedRingMk F n a =
        equalCharacteristicLubinTateTruncatedRingMk F n b ↔
      a - b ∈
        Ideal.span ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧)

theorem

equalCharacteristicLubinTateTruncatedRingMk_surjective

L302 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRingMk_surjective

Documentation

Every named truncated coefficient has a power-series representative.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateTruncatedRingMk_surjective
    (F : LocalField.{u, v} K) (n : ℕ) :
    Function.Surjective (equalCharacteristicLubinTateTruncatedRingMk F n)

theorem

equalCharacteristicLubinTateTruncatedRing_inductionOn₂

L312 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRing_inductionOn₂

Documentation

Eliminate two truncated coefficients simultaneously through canonical representatives.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateTruncatedRing_inductionOn₂
    (F : LocalField.{u, v} K) (n : ℕ)
    {motive : equalCharacteristicLubinTateTruncatedRing F n →
      equalCharacteristicLubinTateTruncatedRing F n → Prop}
    (q r : equalCharacteristicLubinTateTruncatedRing F n)
    (mk : ∀ a b : F.residueField⟦X⟧,
      motive (equalCharacteristicLubinTateTruncatedRingMk F n a)
        (equalCharacteristicLubinTateTruncatedRingMk F n b)) :
    motive q r

def

equalCharacteristicLubinTateTruncatedRingLift

L325 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRingLift

Documentation

Descend a ring homomorphism through the named truncated coefficient ring.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def equalCharacteristicLubinTateTruncatedRingLift
    {S : Type*} [Semiring S]
    (F : LocalField.{u, v} K) (n : ℕ)
    (f : F.residueField⟦X⟧ →+* S)
    (hf : ∀ a ∈
      Ideal.span ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧),
      f a = 0) :
    equalCharacteristicLubinTateTruncatedRing F n →+* S

theorem

equalCharacteristicLubinTateTruncatedRingLift_mk

L340 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedRingLift_mk

Documentation

A descended homomorphism evaluates a truncated representative by the original map.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateTruncatedRingLift_mk
    {S : Type*} [Semiring S]
    (F : LocalField.{u, v} K) (n : ℕ)
    (f : F.residueField⟦X⟧ →+* S)
    (hf : ∀ a ∈
      Ideal.span ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧),
      f a = 0) (a : F.residueField⟦X⟧) :
    equalCharacteristicLubinTateTruncatedRingLift F n f hf
        (equalCharacteristicLubinTateTruncatedRingMk F n a) = f a

instance

equalCharacteristicLubinTateTruncatedSelfSMul

L353 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedSelfSMul

Documentation

The canonical scalar multiplication of the truncated coefficient ring on itself, named to prevent typeclass search from unfolding the quotient.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)

instance

equalCharacteristicLubinTateTruncatedSelfModule

L359 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedSelfModule

Source context 8 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)

Lean source · statement

instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n)

def

equalCharacteristicLubinTateTorsionEndRingHom

L367 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTorsionEndRingHom

Documentation

Genuine Lubin--Tate brackets give a ring action of the full power-series ring on level n + 1 torsion.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · full declaration

def equalCharacteristicLubinTateTorsionEndRingHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    F.residueField⟦X⟧ →+*
      AddMonoid.End
        (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1)) where
  toFun a := equalCharacteristicLubinTateAmbientTorsionEnd F
    (equalCharacteristicSeparableCoefficientHom F)
    (equalCharacteristicSeparableUniformizer F) (n + 1) a
  map_zero' := by
    apply AddMonoidHom.ext
    intro x
    apply Subtype.ext
    exact congrArg (fun f : AddMonoid.End
        (SeparableClosure F.residueField⸨X⸩) =>
      f x.1) (equalCharacteristicLubinTateAmbientBracket_zero F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) (n + 1))
  map_one' := by
    apply AddMonoidHom.ext
    intro x
    apply Subtype.ext
    exact equalCharacteristicLubinTateAmbientBracket_one_apply_of_torsion F
      (equalCharacteristicSeparableCoefficientHom F)
      (equalCharacteristicSeparableUniformizer F) (n + 1) x.1 x.2
  map_add' a b := by
    apply AddMonoidHom.ext
    intro x
    apply Subtype.ext
    exact congrArg (fun f : AddMonoid.End
        (SeparableClosure F.residueField⸨X⸩) => f x.1)
      (equalCharacteristicLubinTateAmbientBracket_add F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) (n + 1) a b)
  map_mul' a b := by
    apply AddMonoidHom.ext
    intro x
    apply Subtype.ext
    exact equalCharacteristicLubinTateAmbientBracket_mul_apply_of_torsion F
      (equalCharacteristicSeparableCoefficientHom F)
      (equalCharacteristicSeparableUniformizer F) (n + 1) a b x.1 x.2

theorem

equalCharacteristicLubinTateTruncationIdeal_le_ker

L412 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncationIdeal_le_ker

Documentation

T^(n+1) acts trivially on division-level n + 1 division points.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

theorem equalCharacteristicLubinTateTruncationIdeal_le_ker
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Ideal.span ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧) ≤
      RingHom.ker (equalCharacteristicLubinTateTorsionEndRingHom F n)

def

equalCharacteristicLubinTateTruncatedScalarHom

L438 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedScalarHom

Documentation

The resulting action of the actual quotient κ⟦T⟧/(T^(n+1)).

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

def equalCharacteristicLubinTateTruncatedScalarHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateTruncatedRing F n →+*
      AddMonoid.End
        (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1))

instance

equalCharacteristicLubinTateTruncatedSMul

L452 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedSMul

Documentation

The quotient-ring scalar action underlying the truncated torsion module.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

instance equalCharacteristicLubinTateTruncatedSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
        (equalCharacteristicSeparableUniformizer F) (n + 1))

instance

equalCharacteristicLubinTateTruncatedModule

L466 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedModule

Documentation

The canonical κ⟦T⟧/(T^(n+1))-module structure on division-level n + 1 division points.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

instance equalCharacteristicLubinTateTruncatedModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
        (equalCharacteristicSeparableUniformizer F) (n + 1))

def

equalCharacteristicLubinTatePrimitiveTorsionPoint

L477 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitiveTorsionPoint

Documentation

The chosen primitive root, regarded as a division-level n + 1 division point.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

def equalCharacteristicLubinTatePrimitiveTorsionPoint
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
      (equalCharacteristicSeparableUniformizer F) (n + 1)

def

equalCharacteristicLubinTatePrimitiveEvaluation

L488 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitiveEvaluation

Documentation

Evaluation at the primitive point is linear for the quotient-ring action.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

def equalCharacteristicLubinTatePrimitiveEvaluation
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateTruncatedRing F n →ₗ[
      equalCharacteristicLubinTateTruncatedRing F n]
      equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
        (equalCharacteristicSeparableUniformizer F) (n + 1)

theorem

equalCharacteristicLubinTatePrimitiveEvaluation_mk

L504 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitiveEvaluation_mk

Documentation

Primitive evaluation of a truncated class is bracket evaluation of its representative.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

theorem equalCharacteristicLubinTatePrimitiveEvaluation_mk
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧) :
    equalCharacteristicLubinTatePrimitiveEvaluation F n
        (equalCharacteristicLubinTateTruncatedRingMk F n a) =
      equalCharacteristicLubinTateAmbientTorsionEnd F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) (n + 1) a
        (equalCharacteristicLubinTatePrimitiveTorsionPoint F n)

theorem

equalCharacteristicLubinTatePrimitiveEvaluation_injective

L517 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitiveEvaluation_injective

Documentation

Evaluation at the primitive torsion point is injective on truncated coefficients.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

theorem equalCharacteristicLubinTatePrimitiveEvaluation_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Injective
      (equalCharacteristicLubinTatePrimitiveEvaluation F n)

theorem

equalCharacteristicLubinTatePrimitiveEvaluation_surjective

L561 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitiveEvaluation_surjective

Documentation

Every ambient torsion point is obtained by primitive evaluation.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

theorem equalCharacteristicLubinTatePrimitiveEvaluation_surjective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Surjective
      (equalCharacteristicLubinTatePrimitiveEvaluation F n)

def

equalCharacteristicLubinTateFreeRankOneEquiv

L587 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateFreeRankOneEquiv

Documentation

The public the primitive-division-module equivalence equivalence: at positive division level n + 1, evaluation at a primitive division point identifies κ⟦T⟧/(T^(n+1)) with the entire division module.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

def equalCharacteristicLubinTateFreeRankOneEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateTruncatedRing F n ≃ₗ[
      equalCharacteristicLubinTateTruncatedRing F n]
      equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
        (equalCharacteristicSeparableUniformizer F) (n + 1)

theorem

equalCharacteristicLubinTateFreeRankOneEquiv_apply_one

L602 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateFreeRankOneEquiv_apply_one

Documentation

The free rank-one equivalence sends one to the primitive torsion point.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

theorem equalCharacteristicLubinTateFreeRankOneEquiv_apply_one
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateFreeRankOneEquiv F n 1 =
      equalCharacteristicLubinTatePrimitiveTorsionPoint F n

instance

equalCharacteristicLubinTateDivisionModuleFree

L616 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateDivisionModuleFree

Documentation

In particular the division module of the primitive-division-module equivalence is genuinely free. The displayed linear equivalence above supplies its one-element basis.

Source context 9 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
/-- The canonical scalar multiplication of the truncated coefficient ring on
itself, named to prevent typeclass search from unfolding the quotient. -/
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfSMul
    (F : LocalField.{u, v} K) (n : ℕ) :
    SMul (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) where
  smul := (· * ·)
noncomputable local instance equalCharacteristicLubinTateTruncatedSelfModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateTruncatedRing F n) :=
  Semiring.toModule

Lean source · statement

instance equalCharacteristicLubinTateDivisionModuleFree
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Module.Free (equalCharacteristicLubinTateTruncatedRing F n)
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
        (equalCharacteristicSeparableUniformizer F) (n + 1))

Module documentation

The primitive-division-module equivalence: equal-characteristic division points are free of

Declarations