NYLL
Module

DivisionModuleEndomorphisms.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FormalModule.DivisionModuleEndomorphisms
21 declarations indexed from sourceView source ↗

Module documentation

The endomorphism-ring equivalence: endomorphisms and automorphisms of division modules

For the standard equal-characteristic Lubin--Tate module, scalar brackets identify the endomorphism ring of the level-m division module with κ⟦T⟧/(T^m), and its automorphism group with the quotient of κ⟦T⟧ˣ by the m-th higher unit subgroup. The division-tower sources use a primitive polynomial indexed by n for division level m = n + 1; every statement below keeps this shift explicit.

Imports3
Imported by4

Declarations

theorem

scalarConjRingEquiv_apply

L42 ↗
LubinTate.EqualCharacteristic.scalarConjRingEquiv_apply
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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem scalarConjRingEquiv_apply
    {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
    (e : R ≃ₗ[R] M) (a : R) (x : M) :
    (((RingEquiv.toOpposite R).trans (RingEquiv.moduleEndSelf R)).trans
      e.conjRingEquiv) a x = a • x
def

equalCharacteristicLubinTateScalarEndomorphismRingEquiv

L57 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateScalarEndomorphismRingEquiv
Documentation

The public ring isomorphism a ↦ [a]_F of the endomorphism-ring equivalence.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateScalarEndomorphismRingEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateTruncatedRing F n ≃+*
      Module.End (equalCharacteristicLubinTateTruncatedRing F n)
        (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1))
def

equalCharacteristicLubinTateEndomorphismRingEquiv

L73 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateEndomorphismRingEquiv
Documentation

The orientation printed in the endomorphism-ring equivalence: End_{κ⟦T⟧}(F[n+1]) ≃ κ⟦T⟧/(T^(n+1)).

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateEndomorphismRingEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Module.End (equalCharacteristicLubinTateTruncatedRing F n)
        (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1)) ≃+*
      equalCharacteristicLubinTateTruncatedRing F n
theorem

equalCharacteristicLubinTateScalarEndomorphismRingEquiv_apply

L85 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateScalarEndomorphismRingEquiv_apply
Documentation

The scalar-endomorphism equivalence sends a truncated scalar to its action map.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateScalarEndomorphismRingEquiv_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateTruncatedRing F n)
    (x : equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
      (equalCharacteristicSeparableUniformizer F) (n + 1)) :
    equalCharacteristicLubinTateScalarEndomorphismRingEquiv F n a x = a • x
theorem

equalCharacteristicLubinTateScalarEndomorphismRingEquiv_mk_apply

L97 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateScalarEndomorphismRingEquiv_mk_apply
Documentation

On a power-series representative, the scalar endomorphism is the genuine finite Lubin--Tate bracket.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateScalarEndomorphismRingEquiv_mk_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧)
    (x : equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
      (equalCharacteristicSeparableUniformizer F) (n + 1)) :
    (equalCharacteristicLubinTateScalarEndomorphismRingEquiv F n
        (equalCharacteristicLubinTateTruncatedRingMk F n a)
        x).1 =
      equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) (n + 1) a x.1
def

equalCharacteristicLubinTateTruncatedUnitsAutomorphismEquiv

L114 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedUnitsAutomorphismEquiv
Documentation

Units of κ⟦T⟧/(T^(n+1)) are precisely the linear automorphisms of the division-level n + 1 division module.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateTruncatedUnitsAutomorphismEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTateTruncatedRing F n)ˣ ≃*
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1) ≃ₗ[
        equalCharacteristicLubinTateTruncatedRing F n]
        equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1))
theorem

equalCharacteristicLubinTateTruncatedUnitsAutomorphismEquiv_apply

L133 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedUnitsAutomorphismEquiv_apply
Documentation

A truncated unit acts on the division module by scalar multiplication.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateTruncatedUnitsAutomorphismEquiv_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : (equalCharacteristicLubinTateTruncatedRing F n)ˣ)
    (x : equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
      (equalCharacteristicSeparableUniformizer F) (n + 1)) :
    equalCharacteristicLubinTateTruncatedUnitsAutomorphismEquiv F n a x =
      (a : equalCharacteristicLubinTateTruncatedRing F n) • x
def

equalCharacteristicLubinTateTruncatedQuotientMap

L145 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedQuotientMap
Documentation

Reduction of integral coefficients modulo T^(n+1).

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateTruncatedQuotientMap
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.residueField⟦X⟧ →+* equalCharacteristicLubinTateTruncatedRing F n
def

equalCharacteristicLubinTateUnitReduction

L151 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitReduction
Documentation

Reduction of integral units modulo T^(n+1).

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateUnitReduction
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.residueField⟦X⟧ˣ →*
      (equalCharacteristicLubinTateTruncatedRing F n)ˣ
theorem

equalCharacteristicLubinTateUnitReduction_val

L159 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitReduction_val
Documentation

The value of a reduced unit is the truncated class of its power series.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateUnitReduction_val
    (F : LocalField.{u, v} K) (n : ℕ)
    (u : F.residueField⟦X⟧ˣ) :
    (equalCharacteristicLubinTateUnitReduction F n u :
        equalCharacteristicLubinTateTruncatedRing F n) =
      equalCharacteristicLubinTateTruncatedRingMk F n
        (u : F.residueField⟦X⟧)
def

equalCharacteristicLubinTateHigherUnitSubgroup

L170 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateHigherUnitSubgroup
Documentation

The equal-characteristic realization of the higher unit group U_K^(n+1): units congruent to one modulo T^(n+1).

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateHigherUnitSubgroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    Subgroup F.residueField⟦X⟧ˣ
theorem

mem_equalCharacteristicLubinTateHigherUnitSubgroup

L176 ↗
LubinTate.EqualCharacteristic.mem_equalCharacteristicLubinTateHigherUnitSubgroup
Documentation

A unit is in the higher-unit kernel exactly when it is one modulo X ^ (n + 1).

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem mem_equalCharacteristicLubinTateHigherUnitSubgroup
    (F : LocalField.{u, v} K) (n : ℕ)
    (u : F.residueField⟦X⟧ˣ) :
    u ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n ↔
      (u : F.residueField⟦X⟧) - 1 ∈
        Ideal.span ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧)
theorem

equalCharacteristicLubinTateTruncationIdeal_le_constantCoeff_ker

L198 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncationIdeal_le_constantCoeff_ker
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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateTruncationIdeal_le_constantCoeff_ker
    (F : LocalField.{u, v} K) (n : ℕ) :
    Ideal.span ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧) ≤
      RingHom.ker (PowerSeries.constantCoeff (R := F.residueField))
def

equalCharacteristicLubinTateTruncatedConstantCoeff

L211 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedConstantCoeff
Documentation

Constant coefficient descends to every positive truncated power-series ring.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateTruncatedConstantCoeff
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTateTruncatedRing F n →+* F.residueField
theorem

equalCharacteristicLubinTateTruncatedConstantCoeff_mk

L221 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateTruncatedConstantCoeff_mk
Documentation

The descended constant-coefficient map evaluates any truncated representative.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateTruncatedConstantCoeff_mk
    (F : LocalField.{u, v} K) (n : ℕ) (f : F.residueField⟦X⟧) :
    equalCharacteristicLubinTateTruncatedConstantCoeff F n
        (equalCharacteristicLubinTateTruncatedRingMk F n f) =
      PowerSeries.constantCoeff f
theorem

equalCharacteristicLubinTateUnitReduction_surjective

L229 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitReduction_surjective
Documentation

Every unit modulo T^(n+1) has a power-series unit lift.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateUnitReduction_surjective
    (F : LocalField.{u, v} K) (n : ℕ) :
    Function.Surjective (equalCharacteristicLubinTateUnitReduction F n)
def

equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits

L255 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits
Documentation

The canonical first-isomorphism-theorem identification U_K/U_K^(n+1) ≃ (κ⟦T⟧/(T^(n+1)))ˣ.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n ≃*
      (equalCharacteristicLubinTateTruncatedRing F n)ˣ
theorem

equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits_mk

L266 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits_mk
Documentation

The higher-unit quotient equivalence sends a unit class to its truncation.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits_mk
    (F : LocalField.{u, v} K) (n : ℕ)
    (u : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits F n
        (QuotientGroup.mk u) =
      equalCharacteristicLubinTateUnitReduction F n u
def

equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv

L276 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv
Documentation

The canonical the endomorphism-ring equivalence map from the higher-unit quotient to linear automorphisms, induced by a ↦ [a]_F.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n ≃*
      (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1) ≃ₗ[
        equalCharacteristicLubinTateTruncatedRing F n]
        equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1))
def

equalCharacteristicLubinTateAutomorphismEquivUnitQuotient

L292 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAutomorphismEquivUnitQuotient
Documentation

The orientation printed in the endomorphism-ring equivalence: Aut_{κ⟦T⟧}(F[n+1]) ≃ U_K/U_K^(n+1).

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
def equalCharacteristicLubinTateAutomorphismEquivUnitQuotient
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    (equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1) ≃ₗ[
        equalCharacteristicLubinTateTruncatedRing F n]
        equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
          (equalCharacteristicSeparableUniformizer F) (n + 1)) ≃*
      F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n
theorem

equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv_mk_apply

L307 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv_mk_apply
Documentation

A representative unit acts through the actual Lubin--Tate bracket, so the preceding automorphism isomorphism is the canonical one.

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]
attribute [local instance]
  equalCharacteristicLubinTateTruncatedSelfSMul
  equalCharacteristicLubinTateTruncatedSelfModule
Lean source · statement
theorem equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv_mk_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (u : F.residueField⟦X⟧ˣ)
    (x : equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
      (equalCharacteristicSeparableUniformizer F) (n + 1)) :
    (equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv F n
        (QuotientGroup.mk u) x).1 =
      equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) (n + 1)
        (u : F.residueField⟦X⟧) x.1

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