Module

UnitQuotientGalois.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.UnitQuotientGalois

18 declarations indexed from sourceView source ↗

Module documentation

Equal-characteristic Lubin--Tate unit quotients and Galois groups

This file constructs the finite-level Galois action of a power-series unit with the local-Artin orientation: a sends the chosen primitive generator to [a⁻¹]. Its kernel is the (n + 1)-st higher-unit subgroup, so the action descends to a multiplicative equivalence from the finite unit quotient to the Galois group.

Imports72

Imported by3

def

equalCharacteristicLubinTateArtinUnitLevelRoot

L106 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitLevelRoot

Documentation

The finite-level root obtained from the Artin-oriented bracket [a⁻¹].

Source context 7 commands

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

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

Lean source · statement

def equalCharacteristicLubinTateArtinUnitLevelRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateLevelField F n

theorem

equalCharacteristicLubinTateArtinUnitLevelRoot_aeval_minpoly

L117 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitLevelRoot_aeval_minpoly

Documentation

The Artin-oriented unit root annihilates the generator's minimal polynomial.

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitLevelRoot_aeval_minpoly
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    Polynomial.aeval
        (equalCharacteristicLubinTateArtinUnitLevelRoot F n a)
        (minpoly F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen) = 0

def

equalCharacteristicLubinTateArtinUnitAlgHom

L149 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitAlgHom

Documentation

The finite-level algebra endomorphism with Artin orientation.

Source context 7 commands

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

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

Lean source · statement

def equalCharacteristicLubinTateArtinUnitAlgHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateLevelField F n →ₐ[F.residueField⸨X⸩]
      equalCharacteristicLubinTateLevelField F n

theorem

equalCharacteristicLubinTateArtinUnitAlgHom_apply_gen

L160 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitAlgHom_apply_gen

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitAlgHom_apply_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitAlgHom F n a
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTateArtinUnitLevelRoot F n a

def

equalCharacteristicLubinTateArtinUnitAlgEquiv

L171 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitAlgEquiv

Documentation

The finite-level Galois automorphism whose generator action is [a⁻¹].

Source context 7 commands

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

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

Lean source · statement

def equalCharacteristicLubinTateArtinUnitAlgEquiv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateLevelField F n ≃ₐ[F.residueField⸨X⸩]
      equalCharacteristicLubinTateLevelField F n

theorem

equalCharacteristicLubinTateArtinUnitAlgEquiv_apply_gen

L185 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitAlgEquiv_apply_gen

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitAlgEquiv_apply_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitAlgEquiv F n a
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTateArtinUnitLevelRoot F n a

theorem

equalCharacteristicLubinTateArtinUnitAlgEquiv_one

L196 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitAlgEquiv_one

Source context 7 commands

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

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

Lean source · statement

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

theorem

equalCharacteristicLubinTateArtinUnitAlgEquiv_mul

L223 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitAlgEquiv_mul

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitAlgEquiv_mul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a b : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitAlgEquiv F n (a * b) =
      equalCharacteristicLubinTateArtinUnitAlgEquiv F n a *
        equalCharacteristicLubinTateArtinUnitAlgEquiv F n b

def

equalCharacteristicLubinTateArtinUnitToGal

L281 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitToGal

Documentation

Power-series units acting on the finite Lubin--Tate level with Artin orientation.

Source context 7 commands

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

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

Lean source · full declaration

def equalCharacteristicLubinTateArtinUnitToGal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    F.residueField⟦X⟧ˣ →*
      Gal((equalCharacteristicLubinTateLevelField F n) /
        F.residueField⸨X⸩) where
  toFun := equalCharacteristicLubinTateArtinUnitAlgEquiv F n
  map_one' := equalCharacteristicLubinTateArtinUnitAlgEquiv_one F n
  map_mul' := equalCharacteristicLubinTateArtinUnitAlgEquiv_mul F n

theorem

equalCharacteristicLubinTateArtinUnitToGal_apply_gen

L293 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitToGal_apply_gen

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitToGal_apply_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitToGal F n a
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTateArtinUnitLevelRoot F n a

theorem

equalCharacteristicLubinTateArtinUnitToGal_ker

L304 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitToGal_ker

Documentation

The kernel of the Artin-oriented explicit unit action is the level higher-unit subgroup.

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitToGal_ker
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    MonoidHom.ker (equalCharacteristicLubinTateArtinUnitToGal F n) =
      equalCharacteristicLubinTateHigherUnitSubgroup F n

theorem

equalCharacteristicLubinTateArtinUnitToGal_parameterUnit_inv

L345 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitToGal_parameterUnit_inv

Documentation

A visible finite parameter is obtained from the Artin-oriented unit action by inverting its represented power-series unit.

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitToGal_parameterUnit_inv
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (p : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateArtinUnitToGal F n
        (equalCharacteristicLubinTateUnitParameterUnit F n p)⁻¹ =
      equalCharacteristicLubinTateUnitParameterAlgEquiv F n p

theorem

equalCharacteristicLubinTateArtinUnitToGal_surjective

L368 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitToGal_surjective

Documentation

Every finite-level Galois automorphism is induced by an Artin-oriented power-series unit.

Source context 7 commands

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

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

Lean source · statement

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

def

equalCharacteristicLubinTateArtinUnitQuotientEquivGal

L383 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitQuotientEquivGal

Documentation

The Artin-oriented explicit finite-level reciprocity equivalence from the unit quotient.

Source context 7 commands

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

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

Lean source · statement

def equalCharacteristicLubinTateArtinUnitQuotientEquivGal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n ≃*
      Gal((equalCharacteristicLubinTateLevelField F n) /
        F.residueField⸨X⸩)

theorem

equalCharacteristicLubinTateArtinUnitQuotientEquivGal_mk

L398 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitQuotientEquivGal_mk

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitQuotientEquivGal_mk
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitQuotientEquivGal F n
        (QuotientGroup.mk a) =
      equalCharacteristicLubinTateArtinUnitToGal F n a

theorem

equalCharacteristicLubinTateArtinUnitQuotientEquivGal_mk_apply_gen_coe

L412 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitQuotientEquivGal_mk_apply_gen_coe

Documentation

On a representative, the quotient-to-Galois equivalence is the inverse orientation of the existing quotient action on the primitive torsion point.

Source context 7 commands

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

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

Lean source · statement

theorem
    equalCharacteristicLubinTateArtinUnitQuotientEquivGal_mk_apply_gen_coe
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    ((equalCharacteristicLubinTateArtinUnitQuotientEquivGal F n
          (QuotientGroup.mk a))
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen :
      SeparableClosure F.residueField⸨X⸩) =
      (equalCharacteristicLubinTateUnitQuotientAutomorphismEquiv F n
        (QuotientGroup.mk a⁻¹)
        (⟨chosenEqualCharacteristicLubinTatePrimitiveRoot F n,
          chosenEqualCharacteristicLubinTatePrimitiveRoot_torsion F n⟩ :
          equalCharacteristicLubinTateAmbientTorsionAddSubgroup F
            (equalCharacteristicSeparableUniformizer F) (n + 1))).1

theorem

equalCharacteristicLubinTateArtinUnitToGal_eq_one_iff

L433 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitToGal_eq_one_iff

Documentation

Kernel membership in pointwise form.

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitToGal_eq_one_iff
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitToGal F n a = 1 ↔
      a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n

theorem

equalCharacteristicLubinTateArtinUnitToGal_eq_one_iff_sub_one_mem

L443 ↗

LubinTate.equalCharacteristicLubinTateArtinUnitToGal_eq_one_iff_sub_one_mem

Documentation

The explicit congruence criterion for trivial finite-level action.

Source context 7 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateArtinUnitToGal_eq_one_iff_sub_one_mem
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitToGal F n a = 1 ↔
      (a : F.residueField⟦X⟧) - 1 ∈
        Ideal.span
          ({PowerSeries.X ^ (n + 1)} : Set F.residueField⟦X⟧)

Module documentation

Equal-characteristic Lubin--Tate unit quotients and Galois groups

Declarations