Module

Core.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.Core

7 declarations indexed from sourceView source ↗

Module documentation

The ordinary ideal class group as an idele quotient

This file proves that quotienting the idele group by the ideles integral at every finite place and by the principal ideles gives the ordinary ideal class group.

Imports3

Imported by10

theorem

count_toPrincipalIdeal

L33 ↗

IdeleGroup.count_toPrincipalIdeal

Documentation

The exponent of a prime in a principal fractional ideal is the additive form of the corresponding normalized finite-place valuation.

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 count_toPrincipalIdeal (x : Kˣ)
    (v : HeightOneSpectrum (𝓞 K)) :
    FractionalIdeal.count K v
        ((toPrincipalIdeal (𝓞 K) K x : FractionalIdealGroup K) :
          FractionalIdeal (nonZeroDivisors (𝓞 K)) K) =
      -WithZero.log (v.valuation K (x : K))

theorem

fractionalIdeal_principalIdele

L71 ↗

IdeleGroup.fractionalIdeal_principalIdele

Documentation

The fractional ideal map sends a principal idele to the corresponding principal 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 IdeleGroup

Lean source · statement

theorem fractionalIdeal_principalIdele (x : Kˣ) :
    fractionalIdeal (principalIdele K x) =
      toPrincipalIdeal (𝓞 K) K x

theorem

classGroup_mk_eq_one_iff

L92 ↗

IdeleGroup.classGroup_mk_eq_one_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 IdeleGroup

Lean source · statement

theorem classGroup_mk_eq_one_iff
    (I : FractionalIdealGroup K) :
    ClassGroup.mk K I = 1 ↔
      I ∈ (toPrincipalIdeal (𝓞 K) K).range

theorem

idealClass_principalIdele

L105 ↗

IdeleGroup.idealClass_principalIdele

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_principalIdele (x : Kˣ) :
    idealClass (principalIdele K x) = 1

def

ordinaryIdealClassSubgroup

L114 ↗

IdeleGroup.ordinaryIdealClassSubgroup

Documentation

The subgroup I_K^{S∞} Kˣ defining the ordinary ideal class quotient.

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 ordinaryIdealClassSubgroup : Subgroup (IdeleGroup K)

theorem

ordinaryIdealClassSubgroup_eq_ker

L119 ↗

IdeleGroup.ordinaryIdealClassSubgroup_eq_ker

Documentation

The kernel of the map from ideles to the ordinary ideal class group is exactly 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

theorem ordinaryIdealClassSubgroup_eq_ker :
    ordinaryIdealClassSubgroup (K := K) =
      (idealClass (K := K)).ker

def

quotientIntegralSupPrincipalEquiv

L155 ↗

IdeleGroup.quotientIntegralSupPrincipalEquiv

Documentation

The ordinary ideal class group is the quotient of the ideles by the ideles integral at all finite places and the principal 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 IdeleGroup

Lean source · statement

def quotientIntegralSupPrincipalEquiv :
    IdeleGroup K ⧸
        (integralAtFinitePlaces (K := K) ⊔ principalSubgroup K) ≃*
      ClassGroup (𝓞 K)

Module documentation

The ordinary ideal class group as an idele quotient

Declarations

count_toPrincipalIdeal

fractionalIdeal_principalIdele

classGroup_mk_eq_one_iff

idealClass_principalIdele

ordinaryIdealClassSubgroup

ordinaryIdealClassSubgroup_eq_ker

quotientIntegralSupPrincipalEquiv