Module

UnitQuotientCard.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.NormSubgroup.UnitQuotientCard

10 declarations indexed from sourceView source ↗

Module documentation

LubinTate the explicit norm-subgroup computation: cardinality of the standard Lubin--Tate quotient

At repository level n, reduction modulo T^(n+1) identifies the quotient of the power-series unit group by its explicit higher-unit kernel with the units of the truncated power-series ring. Its elements are parametrized by one nonzero constant coefficient and n arbitrary further coefficients, so the quotient has cardinality (q - 1) q^n.

The power-series/integer-ring equivalence, the light quotient equivalence from the unramified norm-index formula, and the normalized Laurent uniformizer then give the same cardinality for K^x / (<T^-1> U^(n+1)).

Imports5

Imported by4

def

unitParameterReduction

L47 ↗

LubinTate.EqualCharacteristic.unitParameterReduction

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

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

theorem

unitParameterReduction_injective

L54 ↗

LubinTate.EqualCharacteristic.unitParameterReduction_injective

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 unitParameterReduction_injective
    (F : LocalField.{u, v} K) (n : ℕ) :
    Function.Injective (unitParameterReduction F n)

theorem

unitParameterReduction_surjective

L76 ↗

LubinTate.EqualCharacteristic.unitParameterReduction_surjective

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 unitParameterReduction_surjective
    (F : LocalField.{u, v} K) (n : ℕ) :
    Function.Surjective (unitParameterReduction F n)

def

unitParameterReductionEquiv

L117 ↗

LubinTate.EqualCharacteristic.unitParameterReductionEquiv

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

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

theorem

truncatedUnitsFinite

L125 ↗

LubinTate.EqualCharacteristic.truncatedUnitsFinite

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 truncatedUnitsFinite
    (F : LocalField.{u, v} K) (n : ℕ) :
    Finite (equalCharacteristicLubinTateTruncatedRing F n)ˣ

theorem

unitQuotientFinite

L131 ↗

LubinTate.EqualCharacteristic.unitQuotientFinite

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 unitQuotientFinite
    (F : LocalField.{u, v} K) (n : ℕ) :
    Finite
      (F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n)

theorem

equalCharacteristicLubinTateUnitQuotient_natCard

L145 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitQuotient_natCard

Documentation

The explicit unit quotient at repository level n has order (q - 1) q^n, where q is the residue-field cardinality.

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 equalCharacteristicLubinTateUnitQuotient_natCard
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : Finite
        (F.residueField⟦X⟧ˣ ⧸
          equalCharacteristicLubinTateHigherUnitSubgroup F n) :=
      unitQuotientFinite F n
    Nat.card
        (F.residueField⟦X⟧ˣ ⧸
          equalCharacteristicLubinTateHigherUnitSubgroup F n) =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n := by
  let : Finite
      (F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n) :=
    unitQuotientFinite F n
  let : Finite (equalCharacteristicLubinTateTruncatedRing F n)ˣ :=
    truncatedUnitsFinite F n
  calc
    Nat.card
        (F.residueField⟦X⟧ˣ ⧸
          equalCharacteristicLubinTateHigherUnitSubgroup F n) =
        Nat.card (equalCharacteristicLubinTateTruncatedRing F n)ˣ :=
      Nat.card_congr
        (equalCharacteristicLubinTateUnitQuotientEquivTruncatedUnits
          F n).toEquiv
    _ = Nat.card (equalCharacteristicLubinTateUnitParameter F n) :=
      Nat.card_congr
        (unitParameterReductionEquiv F n).symm
    _ = (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n :=
      equalCharacteristicLubinTateUnitParameter_natCard F n

def

unitQuotientCard_powerSeriesQuotientEquivLaurentIntegerQuotient

L179 ↗

LubinTate.EqualCharacteristic.unitQuotientCard_powerSeriesQuotientEquivLaurentIntegerQuotient

Documentation

The canonical power-series unit quotient is the integer-unit quotient of the Laurent valuation ring at the same depth.

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
    unitQuotientCard_powerSeriesQuotientEquivLaurentIntegerQuotient
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n ≃*
      IntegerUnitsPrincipalQuot F.residueField⸨X⸩ (n + 1) := by
  let B := F.residueField⸨X⸩
  letI : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
  let e := equalCharacteristicPowerSeriesUnitsEquivLaurentInteger
    F.residueField
  let phi : F.residueField⟦X⟧ˣ →*
      IntegerUnitsPrincipalQuot B (n + 1) :=
    (integerUnitsPrincipalQuotMk B (n + 1)).comp e.toMonoidHom
  have hsurjective : Function.Surjective phi := by
    intro q
    obtain ⟨a, rfl⟩ :=
      integerUnitsPrincipalQuotMk_surjective B (n + 1) q
    refine ⟨e.symm a, ?_⟩
    change integerUnitsPrincipalQuotMk B (n + 1)
      (e (e.symm a)) = integerUnitsPrincipalQuotMk B (n + 1) a
    rw [e.apply_symm_apply]
  have hker : MonoidHom.ker phi =
      equalCharacteristicLubinTateHigherUnitSubgroup F n := by
    ext a
    change integerUnitsPrincipalQuotMk B (n + 1) (e a) = 1 ↔
      a ∈ equalCharacteristicLubinTateHigherUnitSubgroup F n
    rw [integerUnitsPrincipalQuotMk_eq_one_iff]
    exact
      (equalCharacteristicPowerSeriesUnitsEquivLaurentInteger_mem_iff
        F.residueField (n + 1) a).trans
        (mem_equalCharacteristicLubinTateHigherUnitSubgroup F n a).symm
  exact
    (QuotientGroup.quotientMulEquivOfEq hker.symm).trans
      (QuotientGroup.quotientKerEquivOfSurjective phi hsurjective)

theorem

uniformizerPrincipalQuotientFinite

L216 ↗

LubinTate.EqualCharacteristic.uniformizerPrincipalQuotientFinite

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 uniformizerPrincipalQuotientFinite
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    letI : IsNonarchimedeanLocalField F.residueField⸨X⸩ :=
      equalCharacteristicLaurentIsNonarchimedeanLocalField F
    Finite
      (F.residueField⸨X⸩ˣ ⧸
        LocalFieldTheory.uniformizerPrincipalSubgroup F.residueField⸨X⸩
          (equalCharacteristicLaurentUniformizerUnit F)⁻¹ 1 (n + 1)) := by
  let B := F.residueField⸨X⸩
  let pi : Bˣ := (equalCharacteristicLaurentUniformizerUnit F)⁻¹
  let : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
  let : IsNonarchimedeanLocalField B :=
    equalCharacteristicLaurentIsNonarchimedeanLocalField F
  let : Finite
      (F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n) :=
    unitQuotientFinite F n
  let : Finite (IntegerUnitsPrincipalQuot B (n + 1)) :=
    Finite.of_equiv
      (F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n)
      (unitQuotientCard_powerSeriesQuotientEquivLaurentIntegerQuotient
        F n).toEquiv
  have hpi : valuationMap B (Additive.ofMul pi) = 1 := by
    simpa [B, pi] using
      equalCharacteristicLaurentUniformizerUnit_inv_valuationMap F
  exact Finite.of_equiv (IntegerUnitsPrincipalQuot B (n + 1))
    (LocalFieldTheory.uniformizerPrincipalQuotientEquivIntegerUnitsPrincipalQuotient
      B pi hpi (n + 1)).symm.toEquiv

theorem

equalCharacteristicLubinTateUniformizerPrincipalQuotient_natCard

L250 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUniformizerPrincipalQuotient_natCard

Documentation

The standard subgroup generated by the normalized Laurent uniformizer and U^(n+1) has quotient cardinality (q - 1) q^n.

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 equalCharacteristicLubinTateUniformizerPrincipalQuotient_natCard
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    letI : IsNonarchimedeanLocalField F.residueField⸨X⸩ :=
      equalCharacteristicLaurentIsNonarchimedeanLocalField F
    letI : Finite
        (F.residueField⸨X⸩ˣ ⧸
          LocalFieldTheory.uniformizerPrincipalSubgroup F.residueField⸨X⸩
            (equalCharacteristicLaurentUniformizerUnit F)⁻¹ 1 (n + 1)) :=
      uniformizerPrincipalQuotientFinite F n
    Nat.card
        (F.residueField⸨X⸩ˣ ⧸
          LocalFieldTheory.uniformizerPrincipalSubgroup F.residueField⸨X⸩
            (equalCharacteristicLaurentUniformizerUnit F)⁻¹ 1 (n + 1)) =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n := by
  let B := F.residueField⸨X⸩
  let pi : Bˣ := (equalCharacteristicLaurentUniformizerUnit F)⁻¹
  let : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
  let : IsNonarchimedeanLocalField B :=
    equalCharacteristicLaurentIsNonarchimedeanLocalField F
  let : Finite
      (Bˣ ⧸
        LocalFieldTheory.uniformizerPrincipalSubgroup B pi 1 (n + 1)) := by
    simpa [B, pi] using uniformizerPrincipalQuotientFinite F n
  let : Finite
      (F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n) :=
    unitQuotientFinite F n
  let : Finite (IntegerUnitsPrincipalQuot B (n + 1)) :=
    Finite.of_equiv
      (F.residueField⟦X⟧ˣ ⧸
        equalCharacteristicLubinTateHigherUnitSubgroup F n)
      (unitQuotientCard_powerSeriesQuotientEquivLaurentIntegerQuotient
        F n).toEquiv
  have hpi : valuationMap B (Additive.ofMul pi) = 1 := by
    simpa [B, pi] using
      equalCharacteristicLaurentUniformizerUnit_inv_valuationMap F
  calc
    Nat.card
        (Bˣ ⧸ LocalFieldTheory.uniformizerPrincipalSubgroup B pi 1 (n + 1)) =
        Nat.card (IntegerUnitsPrincipalQuot B (n + 1)) :=
      Nat.card_congr
        (LocalFieldTheory.uniformizerPrincipalQuotientEquivIntegerUnitsPrincipalQuotient
          B pi hpi (n + 1)).toEquiv
    _ = Nat.card
        (F.residueField⟦X⟧ˣ ⧸
          equalCharacteristicLubinTateHigherUnitSubgroup F n) :=
      Nat.card_congr
        (unitQuotientCard_powerSeriesQuotientEquivLaurentIntegerQuotient
          F n).symm.toEquiv
    _ = (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n :=
      equalCharacteristicLubinTateUnitQuotient_natCard F n

Module documentation

LubinTate the explicit norm-subgroup computation: cardinality of the standard Lubin--Tate quotient

Declarations