Module

HigherUnits.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.HigherUnits

9 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: higher units in the Laurent-series model

The power-series coefficient ring k[[T]] is the canonical integer ring of k((T)). The induced equivalence on units carries the explicit kernel used in the Lubin--Tate construction to the canonical principal-unit filtration. The construction uses index n, while the corresponding division-level unit group is U^(n+1).

Imports3

Imported by6

theorem

ringEquiv_map_maximalIdeal

L40 ↗

LubinTate.EqualCharacteristic.ringEquiv_map_maximalIdeal

Source context 10 commands

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

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

Lean source · statement

theorem ringEquiv_map_maximalIdeal
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) :
    Ideal.map e.toRingHom (IsLocalRing.maximalIdeal R) =
      IsLocalRing.maximalIdeal S

theorem

ringEquiv_map_maximalIdeal_pow

L60 ↗

LubinTate.EqualCharacteristic.ringEquiv_map_maximalIdeal_pow

Source context 10 commands

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

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

Lean source · statement

theorem ringEquiv_map_maximalIdeal_pow
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) (n : ℕ) :
    Ideal.map e.toRingHom (IsLocalRing.maximalIdeal R ^ n) =
      IsLocalRing.maximalIdeal S ^ n

theorem

ringEquiv_mem_maximalIdeal_pow_iff

L67 ↗

LubinTate.EqualCharacteristic.ringEquiv_mem_maximalIdeal_pow_iff

Source context 10 commands

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

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

Lean source · statement

theorem ringEquiv_mem_maximalIdeal_pow_iff
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) (n : ℕ) (x : R) :
    e x ∈ IsLocalRing.maximalIdeal S ^ n ↔
      x ∈ IsLocalRing.maximalIdeal R ^ n

def

equalCharacteristicPowerSeriesUnitsEquivLaurentInteger

L82 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesUnitsEquivLaurentInteger

Documentation

The genuine equivalence between power-series units and the units of the canonical integer ring of the Laurent-series field.

Source context 10 commands

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

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

Lean source · full declaration

def equalCharacteristicPowerSeriesUnitsEquivLaurentInteger
    (k : Type u) [Field k] :
    letI : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
      (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
    k⟦X⟧ˣ ≃* 𝒪[k⸨X⸩]ˣ := by
  letI : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
    (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
  exact Units.mapEquiv
    (powerSeriesEquivLaurentValuativeInteger k).toMulEquiv

theorem

equalCharacteristicPowerSeriesUnitsEquivLaurentInteger_mem_iff

L93 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesUnitsEquivLaurentInteger_mem_iff

Documentation

States the theorem equalCharacteristicPowerSeriesUnitsEquivLaurentInteger_mem_iff.

Source context 10 commands

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

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

Lean source · full declaration

theorem equalCharacteristicPowerSeriesUnitsEquivLaurentInteger_mem_iff
    (k : Type u) [Field k] (n : ℕ) (a : k⟦X⟧ˣ) :
    letI : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
      (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
    equalCharacteristicPowerSeriesUnitsEquivLaurentInteger k a ∈
        principalUnits k⸨X⸩ n ↔
      (a : k⟦X⟧) - 1 ∈
        Ideal.span ({PowerSeries.X ^ n} : Set k⟦X⟧) := by
  let : ValuativeRel k⸨X⸩ := ValuativeRel.ofValuation
    (Valued.v : Valuation k⸨X⸩ ℤᵐ⁰)
  rw [mem_principalUnits_iff]
  change powerSeriesEquivLaurentValuativeInteger k
      (a : k⟦X⟧) - 1 ∈
        IsLocalRing.maximalIdeal 𝒪[k⸨X⸩] ^ n ↔ _
  simpa [PowerSeries.maximalIdeal_eq_span_X,
    Ideal.span_singleton_pow] using
    (ringEquiv_mem_maximalIdeal_pow_iff
      (powerSeriesEquivLaurentValuativeInteger k) n
      ((a : k⟦X⟧) - 1))

theorem

equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_principalUnits

L115 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_principalUnits

Documentation

The explicit Lubin--Tate higher-unit kernel is exactly the canonical principal-unit group U^(n+1) under the integer-unit equivalence.

Source context 10 commands

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

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

Lean source · full declaration

theorem equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_principalUnits
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    (equalCharacteristicLubinTateHigherUnitSubgroup F n).map
        (equalCharacteristicPowerSeriesUnitsEquivLaurentInteger
          F.residueField).toMonoidHom =
      principalUnits F.residueField⸨X⸩ (n + 1) := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  let E := equalCharacteristicPowerSeriesUnitsEquivLaurentInteger
    F.residueField
  ext u
  constructor
  · rintro ⟨a, ha, rfl⟩
    apply
      (equalCharacteristicPowerSeriesUnitsEquivLaurentInteger_mem_iff
        F.residueField (n + 1) a).2
    exact (mem_equalCharacteristicLubinTateHigherUnitSubgroup F n a).1 ha
  · intro hu
    refine ⟨E.symm u, ?_, ?_⟩
    · apply
        (mem_equalCharacteristicLubinTateHigherUnitSubgroup F n
          (E.symm u)).2
      apply
        (equalCharacteristicPowerSeriesUnitsEquivLaurentInteger_mem_iff
          F.residueField (n + 1) (E.symm u)).1
      simpa [E] using hu
    · exact E.apply_symm_apply u

theorem

equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_fieldPrincipalUnits

L147 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_fieldPrincipalUnits

Documentation

After inclusion of integer units into field units, the explicit higher unit kernel is the canonical field subgroup U^(n+1).

Source context 10 commands

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

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

Lean source · full declaration

theorem equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_fieldPrincipalUnits
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    ((equalCharacteristicLubinTateHigherUnitSubgroup F n).map
        (equalCharacteristicPowerSeriesUnitsEquivLaurentInteger
          F.residueField).toMonoidHom).map
        (integerUnitsToFieldUnits F.residueField⸨X⸩) =
      LocalFieldTheory.fieldPrincipalUnits F.residueField⸨X⸩ (n + 1) := by
  let : ValuativeRel F.residueField⸨X⸩ :=
    equalCharacteristicLaurentValuativeRel F
  rw [equalCharacteristicLubinTateHigherUnitSubgroup_map_eq_principalUnits]
  rfl

theorem

equalCharacteristicLubinTateAmbientBracket_primitiveRoot_eq_iff_mem_higherUnitSubgroup

L161 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_primitiveRoot_eq_iff_mem_higherUnitSubgroup

Source context 10 commands

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

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

Lean source · statement

theorem
  equalCharacteristicLubinTateAmbientBracket_primitiveRoot_eq_iff_mem_higherUnitSubgroup
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (u : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) (n + 1)
        (u : F.residueField⟦X⟧)
        (chosenEqualCharacteristicLubinTatePrimitiveRoot F n) =
      chosenEqualCharacteristicLubinTatePrimitiveRoot F n ↔
        u ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n

theorem

equalCharacteristicLubinTateAmbientBracket_inv_primitiveRoot_eq_iff_mem_higherUnitSubgroup

L233 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_inv_primitiveRoot_eq_iff_mem_higherUnitSubgroup

Documentation

The [u⁻¹] action occurring in the completed theta-intertwining theorem fixes the standard primitive division-level n + 1 division point exactly when u is an (n + 1)-st higher unit. This is the faithful-action kernel needed in the proof of the explicit norm-subgroup computation.

Source context 10 commands

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

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

Lean source · statement

theorem equalCharacteristicLubinTateAmbientBracket_inv_primitiveRoot_eq_iff_mem_higherUnitSubgroup
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (u : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) (n + 1)
        ((u⁻¹ : F.residueField⟦X⟧ˣ) : F.residueField⟦X⟧)
        (chosenEqualCharacteristicLubinTatePrimitiveRoot F n) =
      chosenEqualCharacteristicLubinTatePrimitiveRoot F n ↔
        u ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n

Module documentation

LubinTate the explicit norm-subgroup computation: higher units in the Laurent-series model

Declarations