Module

RationalPrincipalLocalUnit.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.RationalPrincipalLocalUnit

16 declarations indexed from sourceView source ↗

Module documentation

The ramified local unit of a rational principal idele

For a nonzero rational number x and a rational prime p, removing the p-power from x produces an actual p-adic unit. This file identifies that unit simultaneously in the height-one completion used by global reciprocity, in the standard field ℚ_[p], and in the valuation subring used by the multiplicative Lubin--Tate construction.

Imports13

Imported by2

instance

(anonymous instance)

L43 ↗

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp

Lean source · statement

instance (p : Nat.Primes) : Fact p.1.Prime

theorem

rationalPrimeUnit_heightOneValuation_eq_one

L48 ↗

GlobalClassFieldTheory.Reciprocity.rationalPrimeUnit_heightOneValuation_eq_one

Documentation

The rational p-unit has value one for the height-one valuation corresponding to p.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem rationalPrimeUnit_heightOneValuation_eq_one
    (x : ℚˣ) (p : Nat.Primes) :
    (RayClass.rationalPrime p).valuation ℚ
        (rationalPrimeUnit x p : ℚ) =
      1

def

rationalPrimeUnitValuationSubringUnit

L72 ↗

GlobalClassFieldTheory.Reciprocity.rationalPrimeUnitValuationSubringUnit

Documentation

The rational p-unit, expressed as a unit of the valuation subring of the standard local field ℚ_[p].

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

def rationalPrimeUnitValuationSubringUnit
    (x : ℚˣ) (p : Nat.Primes) :
    (padicLocalField p.1).valuationSubringˣ

theorem

rationalPrimeUnitValuationSubringUnit_coe

L86 ↗

GlobalClassFieldTheory.Reciprocity.rationalPrimeUnitValuationSubringUnit_coe

Documentation

Forgetting the integrality proof from the standard valuation-subring unit recovers the rational p-unit in ℚ_[p].

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem rationalPrimeUnitValuationSubringUnit_coe
    (x : ℚˣ) (p : Nat.Primes) :
    ((rationalPrimeUnitValuationSubringUnit x p :
        (padicLocalField p.1).valuationSubring) :
      ℚ_[p.1]) =
        ((rationalPrimeUnit x p : ℚ) : ℚ_[p.1])

theorem

standardLubinTateUnitFactorFieldUnit_rationalPrimeUnit

L107 ↗

GlobalClassFieldTheory.Reciprocity.standardLubinTateUnitFactorFieldUnit_rationalPrimeUnit

Documentation

The Lubin--Tate field-unit inclusion of the rational p-unit is the ordinary embedding of that rational unit into ℚ_[p].

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem standardLubinTateUnitFactorFieldUnit_rationalPrimeUnit
    (x : ℚˣ) (p : Nat.Primes) :
    LubinTate.standardLubinTateUnitFactorFieldUnit
        (padicLocalField p.1)
        (rationalPrimeUnitValuationSubringUnit x p) =
      Units.map (algebraMap ℚ ℚ_[p.1]).toMonoidHom
        (rationalPrimeUnit x p)

theorem

standardLubinTateBaseUniformizerUnit_eq_rationalPrimeGenerator

L124 ↗

GlobalClassFieldTheory.Reciprocity.standardLubinTateBaseUniformizerUnit_eq_rationalPrimeGenerator

Documentation

The standard multiplicative Lubin--Tate base uniformizer is exactly the image of the positive rational prime generator in ℚ_[p]ˣ.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · full declaration

theorem standardLubinTateBaseUniformizerUnit_eq_rationalPrimeGenerator
    (p : Nat.Primes) :
    LubinTate.standardLubinTateBaseUniformizerUnit
        (LubinTate.padicMultiplicativeLubinTateSeries_isUniformizer
          p.1) =
      Units.map (algebraMap ℚ ℚ_[p.1]).toMonoidHom
        (Units.mk0 (p.1 : ℚ) (by
          exact_mod_cast p.2.ne_zero)) := by
  apply Units.ext
  change
    ((padicIntEquivValuationSubring
        p.1 (p.1 : ℤ_[p.1]) :
      (padicLocalField p.1).valuationSubring) :
        ℚ_[p.1]) =
      algebraMap ℚ ℚ_[p.1] (p.1 : ℚ)
  rw [padicIntEquivValuationSubring_coe]
  simp

theorem

rationalPrimeUnit_mul_primeGenerator_zpow

L144 ↗

GlobalClassFieldTheory.Reciprocity.rationalPrimeUnit_mul_primeGenerator_zpow

Documentation

Restoring the removed p-power recovers the original rational field unit. This is the multiplicative factorization used after completion.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · full declaration

theorem rationalPrimeUnit_mul_primeGenerator_zpow
    (x : ℚˣ) (p : Nat.Primes) :
    rationalPrimeUnit x p *
        (Units.mk0 (p.1 : ℚ) (by
          exact_mod_cast p.2.ne_zero)) ^
          padicValRat p.1 (x : ℚ) =
      x := by
  rw [rationalPrimeUnit]
  calc
    ((Units.mk0 (p.1 : ℚ) (by
          exact_mod_cast p.2.ne_zero)) ^
        (-padicValRat p.1 (x : ℚ)) * x) *
          (Units.mk0 (p.1 : ℚ) (by
            exact_mod_cast p.2.ne_zero)) ^
            padicValRat p.1 (x : ℚ) =
        x * ((Units.mk0 (p.1 : ℚ) (by
              exact_mod_cast p.2.ne_zero)) ^
            (-padicValRat p.1 (x : ℚ)) *
          (Units.mk0 (p.1 : ℚ) (by
              exact_mod_cast p.2.ne_zero)) ^
            padicValRat p.1 (x : ℚ)) := by
      ac_rfl
    _ = x := by
      rw [← zpow_add]
      simp

theorem

rationalPadicFieldUnit_eq_unitFactor_mul_baseUniformizer_zpow

L173 ↗

GlobalClassFieldTheory.Reciprocity.rationalPadicFieldUnit_eq_unitFactor_mul_baseUniformizer_zpow

Documentation

In ℚ_[p]ˣ, a rational field unit is its actual integral rationalPrimeUnit factor times the corresponding power of the standard multiplicative Lubin--Tate uniformizer.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem rationalPadicFieldUnit_eq_unitFactor_mul_baseUniformizer_zpow
    (x : ℚˣ) (p : Nat.Primes) :
    Units.map (algebraMap ℚ ℚ_[p.1]).toMonoidHom x =
      LubinTate.standardLubinTateUnitFactorFieldUnit
          (padicLocalField p.1)
          (rationalPrimeUnitValuationSubringUnit x p) *
        LubinTate.standardLubinTateBaseUniformizerUnit
            (LubinTate.padicMultiplicativeLubinTateSeries_isUniformizer
              p.1) ^
          padicValRat p.1 (x : ℚ)

theorem

rationalPadicFieldUnit_uniformizerValueExponent

L197 ↗

GlobalClassFieldTheory.Reciprocity.rationalPadicFieldUnit_uniformizerValueExponent

Documentation

The exponent selected by the complete-DVF uniformizer decomposition of a rational element is its ordinary p-adic valuation.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  multiplicativeIntegerValuationOfUniformizer_isUniformizer
  multiplicativeIntegerValuationOfUniformizer_zeroSubgroup_eq_unitGroup
  valuationSubringUnitsToFieldUnits_mem_unitGroup
) in

Lean source · statement

theorem rationalPadicFieldUnit_uniformizerValueExponent
    (x : ℚˣ) (p : Nat.Primes) :
    (LocalFieldTheory.DiscreteValuationField.CompleteDVF.uniformizerValueExponent
        (padicLocalField p.1).toCompleteDVF)
        (LubinTate.padicMultiplicativeLubinTateSeries_isUniformizer
          p.1)
        (Units.map (algebraMap ℚ ℚ_[p.1]).toMonoidHom x) =
      padicValRat p.1 (x : ℚ)

theorem

rationalPadicFieldUnit_uniformizerUnitPart

L283 ↗

GlobalClassFieldTheory.Reciprocity.rationalPadicFieldUnit_uniformizerUnitPart

Documentation

The actual unit part chosen by the standard multiplicative Lubin--Tate uniformizer decomposition of a rational p-adic field unit is precisely rationalPrimeUnitValuationSubringUnit.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  fieldUnitUniformizerUnitPart
  valuationSubringUnitFieldUnitHom_fieldUnitUniformizerUnitPart
  valuationSubringUnitFieldUnitHom_injective
) in

Lean source · statement

theorem rationalPadicFieldUnit_uniformizerUnitPart
    (x : ℚˣ) (p : Nat.Primes) :
    fieldUnitUniformizerUnitPart
        (padicLocalField p.1).toCompleteDVF
        (LubinTate.padicMultiplicativeLubinTateSeries_isUniformizer
          p.1)
        (Units.map (algebraMap ℚ ℚ_[p.1]).toMonoidHom x) =
      rationalPrimeUnitValuationSubringUnit x p

theorem

padicCompletionEquiv_principalFiniteComponent_rationalPrimeUnit

L331 ↗

GlobalClassFieldTheory.Reciprocity.padicCompletionEquiv_principalFiniteComponent_rationalPrimeUnit

Documentation

Under the canonical equivalence between ℚ_[p] and the height-one completion at p, the principal finite component of the rational p-unit is its ordinary image in ℚ_[p].

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem padicCompletionEquiv_principalFiniteComponent_rationalPrimeUnit
    (x : ℚˣ) (p : Nat.Primes) :
    Units.map
        (Padic.adicCompletionEquiv (𝓞 ℚ) p).symm.toMonoidHom
        (IdeleGroup.finiteComponent
          (RayClass.rationalPrime p)
          (IdeleGroup.principalIdele ℚ
            (rationalPrimeUnit x p))) =
      Units.map (algebraMap ℚ ℚ_[p.1]).toMonoidHom
        (rationalPrimeUnit x p)

theorem

padicCompletionEquiv_principalFiniteComponent

L359 ↗

GlobalClassFieldTheory.Reciprocity.padicCompletionEquiv_principalFiniteComponent

Documentation

Transporting an arbitrary rational principal finite component through the canonical p-adic completion equivalence gives its ordinary image in ℚ_[p]ˣ.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem padicCompletionEquiv_principalFiniteComponent
    (x : ℚˣ) (p : Nat.Primes) :
    Units.map
        (Padic.adicCompletionEquiv (𝓞 ℚ) p).symm.toMonoidHom
        (IdeleGroup.finiteComponent
          (RayClass.rationalPrime p)
          (IdeleGroup.principalIdele ℚ x)) =
      Units.map (algebraMap ℚ ℚ_[p.1]).toMonoidHom x

theorem

padicCompletionEquiv_principalFiniteComponent_factorization

L383 ↗

GlobalClassFieldTheory.Reciprocity.padicCompletionEquiv_principalFiniteComponent_factorization

Documentation

The transported rational principal finite component has the explicit standard Lubin--Tate uniformizer/unit factorization.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem padicCompletionEquiv_principalFiniteComponent_factorization
    (x : ℚˣ) (p : Nat.Primes) :
    Units.map
        (Padic.adicCompletionEquiv (𝓞 ℚ) p).symm.toMonoidHom
        (IdeleGroup.finiteComponent
          (RayClass.rationalPrime p)
          (IdeleGroup.principalIdele ℚ x)) =
      LubinTate.standardLubinTateUnitFactorFieldUnit
          (padicLocalField p.1)
          (rationalPrimeUnitValuationSubringUnit x p) *
        LubinTate.standardLubinTateBaseUniformizerUnit
            (LubinTate.padicMultiplicativeLubinTateSeries_isUniformizer
              p.1) ^
          padicValRat p.1 (x : ℚ)

theorem

padicCompletionEquiv_principalFiniteComponent_uniformizerUnitPart

L407 ↗

GlobalClassFieldTheory.Reciprocity.padicCompletionEquiv_principalFiniteComponent_uniformizerUnitPart

Documentation

Applying the actual complete-DVF unit-part operation to a transported rational principal finite component returns the integral rationalPrimeUnit factor.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup (
  fieldUnitUniformizerUnitPart
) in

Lean source · statement

theorem
    padicCompletionEquiv_principalFiniteComponent_uniformizerUnitPart
    (x : ℚˣ) (p : Nat.Primes) :
    fieldUnitUniformizerUnitPart
        (padicLocalField p.1).toCompleteDVF
        (LubinTate.padicMultiplicativeLubinTateSeries_isUniformizer
          p.1)
        (Units.map
          (Padic.adicCompletionEquiv (𝓞 ℚ) p).symm.toMonoidHom
          (IdeleGroup.finiteComponent
            (RayClass.rationalPrime p)
            (IdeleGroup.principalIdele ℚ x))) =
      rationalPrimeUnitValuationSubringUnit x p

theorem

padicCompletionEquiv_principalFiniteComponent_rationalPrimeGenerator

L425 ↗

GlobalClassFieldTheory.Reciprocity.padicCompletionEquiv_principalFiniteComponent_rationalPrimeGenerator

Documentation

The rational prime generator at its own finite place transports to the actual standard multiplicative Lubin--Tate base uniformizer.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · full declaration

theorem
    padicCompletionEquiv_principalFiniteComponent_rationalPrimeGenerator
    (p : Nat.Primes) :
    Units.map
        (Padic.adicCompletionEquiv (𝓞 ℚ) p).symm.toMonoidHom
        (IdeleGroup.finiteComponent
          (RayClass.rationalPrime p)
          (IdeleGroup.principalIdele ℚ
            (Units.mk0 (p.1 : ℚ) (by
              exact_mod_cast p.2.ne_zero)))) =
      LubinTate.standardLubinTateBaseUniformizerUnit
        (LubinTate.padicMultiplicativeLubinTateSeries_isUniformizer
          p.1) := by
  rw [
    padicCompletionEquiv_principalFiniteComponent,
    standardLubinTateBaseUniformizerUnit_eq_rationalPrimeGenerator]

theorem

padicCompletionEquiv_principalFiniteComponent_eq_lubinTateUnitFactor

L444 ↗

GlobalClassFieldTheory.Reciprocity.padicCompletionEquiv_principalFiniteComponent_eq_lubinTateUnitFactor

Documentation

The principal finite component of the rational p-unit is transported to the exact field unit used by the multiplicative Lubin--Tate Artin map.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open LocalFieldTheory.DiscreteValuationField.Examples.Qp
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩

Lean source · statement

theorem
    padicCompletionEquiv_principalFiniteComponent_eq_lubinTateUnitFactor
    (x : ℚˣ) (p : Nat.Primes) :
    Units.map
        (Padic.adicCompletionEquiv (𝓞 ℚ) p).symm.toMonoidHom
        (IdeleGroup.finiteComponent
          (RayClass.rationalPrime p)
          (IdeleGroup.principalIdele ℚ
            (rationalPrimeUnit x p))) =
      LubinTate.standardLubinTateUnitFactorFieldUnit
        (padicLocalField p.1)
        (rationalPrimeUnitValuationSubringUnit x p)

Module documentation

The ramified local unit of a rational principal idele

Declarations