Module

IdealMap.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.IdealMap

40 declarations indexed from sourceView source ↗

Module documentation

The ideal attached to an idele

This file formalizes the ideal map from ideles. Its construction is explicit: local discrete valuations form a finitely supported integer vector, and unique factorization of fractional ideals identifies that vector with a nonzero fractional ideal. We prove both stages surjective and identify the kernel with the ideles integral at every finite place.

Imports3

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Basic
Mathlib.RingTheory.DedekindDomain.Factorization
Mathlib.RingTheory.ClassGroup.Basic

Imported by7

def

localOrder

L35 ↗

FiniteIdeleGroup.localOrder

Documentation

The exponent of a local multiplicative element, normalized so that a uniformizer has exponent one.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

def localOrder (v : HeightOneSpectrum (𝓞 K)) :
    (v.adicCompletion K)ˣ →* Multiplicative ℤ

theorem

localOrder_apply

L44 ↗

FiniteIdeleGroup.localOrder_apply

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem localOrder_apply (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    (localOrder v x).toAdd =
      -WithZero.log (Valued.v (x : v.adicCompletion K))

theorem

localOrder_eq_zero_iff

L51 ↗

FiniteIdeleGroup.localOrder_eq_zero_iff

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem localOrder_eq_zero_iff (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    (localOrder v x).toAdd = 0 ↔
      x ∈ (v.adicCompletionIntegers K).units

theorem

finite_nonLocalUnits

L78 ↗

FiniteIdeleGroup.finite_nonLocalUnits

Documentation

The set of finite places where a finite idele is not an integral unit is finite.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem finite_nonLocalUnits (a : FiniteIdeleGroup K) :
    {v : HeightOneSpectrum (𝓞 K) |
      a v ∉ (v.adicCompletionIntegers K).units}.Finite

def

valuationVectorAdd

L85 ↗

FiniteIdeleGroup.valuationVectorAdd

Documentation

The finitely supported family of normalized local orders of a finite idele.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

def valuationVectorAdd (a : FiniteIdeleGroup K) :
    HeightOneSpectrum (𝓞 K) →₀ ℤ

theorem

valuationVectorAdd_apply

L94 ↗

FiniteIdeleGroup.valuationVectorAdd_apply

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem valuationVectorAdd_apply (a : FiniteIdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    valuationVectorAdd a v = (localOrder v (a v)).toAdd

def

valuationVector

L101 ↗

FiniteIdeleGroup.valuationVector

Documentation

The finite valuation vector is a homomorphism from finite ideles to the free abelian group on finite places.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

def valuationVector :
    FiniteIdeleGroup K →* Multiplicative
      (HeightOneSpectrum (𝓞 K) →₀ ℤ)

theorem

valuationVector_apply

L112 ↗

FiniteIdeleGroup.valuationVector_apply

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem valuationVector_apply (a : FiniteIdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    (valuationVector a).toAdd v =
      (localOrder v (a v)).toAdd

def

chosenLocalOrderSection

L119 ↗

FiniteIdeleGroup.chosenLocalOrderSection

Documentation

A chosen local element of prescribed normalized order.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

def chosenLocalOrderSection (v : HeightOneSpectrum (𝓞 K)) (n : ℤ) :
    (v.adicCompletion K)ˣ

theorem

localOrder_chosenLocalOrderSection

L134 ↗

FiniteIdeleGroup.localOrder_chosenLocalOrderSection

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem localOrder_chosenLocalOrderSection
    (v : HeightOneSpectrum (𝓞 K)) (n : ℤ) :
    (localOrder v (chosenLocalOrderSection v n)).toAdd = n

def

valuationVectorSection

L148 ↗

FiniteIdeleGroup.valuationVectorSection

Documentation

A finite idele with a prescribed finitely supported valuation vector.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

def valuationVectorSection
    (e : HeightOneSpectrum (𝓞 K) →₀ ℤ) :
    FiniteIdeleGroup K

theorem

valuationVector_valuationVectorSection

L157 ↗

FiniteIdeleGroup.valuationVector_valuationVectorSection

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem valuationVector_valuationVectorSection
    (e : HeightOneSpectrum (𝓞 K) →₀ ℤ) :
    valuationVector (valuationVectorSection e) =
      Multiplicative.ofAdd e

theorem

valuationVector_surjective

L167 ↗

FiniteIdeleGroup.valuationVector_surjective

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem valuationVector_surjective :
    Function.Surjective (valuationVector (K := K))

abbrev

FractionalIdealGroup

L176 ↗

Documentation

The group of nonzero fractional ideals of a number field.

Source context 4 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

abbrev FractionalIdealGroup (K : Type*) [Field K] [NumberField K]

def

prime

L182 ↗

FractionalIdealGroup.prime

Documentation

The fractional ideal represented by a finite prime.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

def prime (v : HeightOneSpectrum (𝓞 K)) :
    FractionalIdealGroup K

def

primePowerHom

L189 ↗

FractionalIdealGroup.primePowerHom

Documentation

The homomorphism sending an integer exponent to the corresponding power of a finite prime.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

def primePowerHom (v : HeightOneSpectrum (𝓞 K)) :
    Multiplicative ℤ →* FractionalIdealGroup K

def

factorization

L196 ↗

FractionalIdealGroup.factorization

Documentation

Reconstruct a fractional ideal from its finitely supported vector of prime exponents.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

def factorization :
    Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ) →*
      FractionalIdealGroup K

theorem

factorization_val

L205 ↗

FractionalIdealGroup.factorization_val

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · full declaration

theorem factorization_val (exps :
    Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ)) :
    ((factorization exps : FractionalIdealGroup K) :
      FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      exps.toAdd.prod fun v n =>
        (v.asIdeal : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) ^ n := by
  classical
  simp [factorization, primePowerHom, prime, Finsupp.prod]

theorem

finite_count_support

L214 ↗

FractionalIdealGroup.finite_count_support

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

theorem finite_count_support (I : FractionalIdealGroup K) :
    {v : HeightOneSpectrum (𝓞 K) |
      FractionalIdeal.count K v
        (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) ≠ 0}.Finite

def

countVector

L224 ↗

FractionalIdealGroup.countVector

Documentation

The finitely supported vector of prime exponents of a nonzero fractional ideal.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

def countVector (I : FractionalIdealGroup K) :
    HeightOneSpectrum (𝓞 K) →₀ ℤ

theorem

countVector_apply

L234 ↗

FractionalIdealGroup.countVector_apply

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

theorem countVector_apply (I : FractionalIdealGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    countVector I v =
      FractionalIdeal.count K v
        (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K)

theorem

count_factorization

L242 ↗

FractionalIdealGroup.count_factorization

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

theorem count_factorization (exps :
    Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ))
    (v : HeightOneSpectrum (𝓞 K)) :
    FractionalIdeal.count K v
      ((factorization exps : FractionalIdealGroup K) :
        FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      exps.toAdd v

theorem

ext_count

L252 ↗

FractionalIdealGroup.ext_count

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

theorem ext_count {I J : FractionalIdealGroup K}
    (h : ∀ v : HeightOneSpectrum (𝓞 K),
      FractionalIdeal.count K v
        (I : FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      FractionalIdeal.count K v
        (J : FractionalIdeal (nonZeroDivisors (𝓞 K)) K)) :
    I = J

theorem

factorization_injective

L268 ↗

FractionalIdealGroup.factorization_injective

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

theorem factorization_injective :
    Function.Injective (factorization (K := K))

theorem

factorization_surjective

L275 ↗

FractionalIdealGroup.factorization_surjective

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

theorem factorization_surjective :
    Function.Surjective (factorization (K := K))

def

factorizationEquiv

L289 ↗

FractionalIdealGroup.factorizationEquiv

Documentation

Multiplicative unique factorization of nonzero fractional ideals by finite primes.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FractionalIdealGroup

Lean source · statement

def factorizationEquiv :
    Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ) ≃*
      FractionalIdealGroup K

def

fractionalIdeal

L300 ↗

FiniteIdeleGroup.fractionalIdeal

Documentation

The fractional ideal attached to a finite idele.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

def fractionalIdeal :
    FiniteIdeleGroup K →* FractionalIdealGroup K

theorem

fractionalIdeal_surjective

L305 ↗

FiniteIdeleGroup.fractionalIdeal_surjective

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem fractionalIdeal_surjective :
    Function.Surjective (fractionalIdeal (K := K))

def

integralSubgroup

L311 ↗

FiniteIdeleGroup.integralSubgroup

Documentation

Finite ideles integral at every finite place.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · full declaration

def integralSubgroup : Subgroup (FiniteIdeleGroup K) where
  carrier := {a | ∀ v : HeightOneSpectrum (𝓞 K),
    a v ∈ (v.adicCompletionIntegers K).units}
  one_mem' v := (v.adicCompletionIntegers K).units.one_mem
  mul_mem' ha hb v :=
    (v.adicCompletionIntegers K).units.mul_mem (ha v) (hb v)
  inv_mem' ha v :=
    (v.adicCompletionIntegers K).units.inv_mem (ha v)

theorem

mem_integralSubgroup_iff

L321 ↗

FiniteIdeleGroup.mem_integralSubgroup_iff

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem mem_integralSubgroup_iff (a : FiniteIdeleGroup K) :
    a ∈ integralSubgroup ↔
      ∀ v : HeightOneSpectrum (𝓞 K),
        a v ∈ (v.adicCompletionIntegers K).units

theorem

fractionalIdeal_ker

L327 ↗

FiniteIdeleGroup.fractionalIdeal_ker

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

theorem fractionalIdeal_ker :
    (fractionalIdeal (K := K)).ker = integralSubgroup

def

quotientIntegralEquiv

L355 ↗

FiniteIdeleGroup.quotientIntegralEquiv

Documentation

The ideal group as the quotient of finite ideles by the everywhere integral finite ideles.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroup

Lean source · statement

def quotientIntegralEquiv :
    FiniteIdeleGroup K ⧸ integralSubgroup ≃*
      FractionalIdealGroup K

def

fractionalIdeal

L368 ↗

IdeleGroup.fractionalIdeal

Documentation

The fractional ideal attached to an idele. The archimedean components do not contribute.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def fractionalIdeal :
    IdeleGroup K →* FractionalIdealGroup K

theorem

fractionalIdeal_surjective

L373 ↗

IdeleGroup.fractionalIdeal_surjective

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem fractionalIdeal_surjective :
    Function.Surjective (fractionalIdeal (K := K))

def

integralAtFinitePlaces

L382 ↗

IdeleGroup.integralAtFinitePlaces

Documentation

Ideles integral at every finite place; this is the subgroup I_K^{S∞}.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def integralAtFinitePlaces : Subgroup (IdeleGroup K)

theorem

fractionalIdeal_ker

L386 ↗

IdeleGroup.fractionalIdeal_ker

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem fractionalIdeal_ker :
    (fractionalIdeal (K := K)).ker = integralAtFinitePlaces

def

quotientIntegralEquiv

L396 ↗

IdeleGroup.quotientIntegralEquiv

Documentation

The ideal group as the quotient of all ideles by those integral at every finite place.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def quotientIntegralEquiv :
    IdeleGroup K ⧸ integralAtFinitePlaces ≃*
      FractionalIdealGroup K

def

idealClass

L405 ↗

IdeleGroup.idealClass

Documentation

The canonical surjection from ideles to the ordinary ideal class group.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def idealClass :
    IdeleGroup K →* ClassGroup (𝓞 K)

theorem

idealClass_surjective

L409 ↗

IdeleGroup.idealClass_surjective

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

theorem idealClass_surjective :
    Function.Surjective (idealClass (K := K))

def

quotientIdealClassKernelEquiv

L419 ↗

IdeleGroup.quotientIdealClassKernelEquiv

Documentation

A quotient form of the ideal-class map. The following results identify this kernel with I_K^{S∞} Kˣ.

Source context 5 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroup

Lean source · statement

def quotientIdealClassKernelEquiv :
    IdeleGroup K ⧸ (idealClass (K := K)).ker ≃*
      ClassGroup (𝓞 K)

Module documentation

The ideal attached to an idele

Declarations