NYLL
Module

MathlibComparison.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.MathlibComparison
4 declarations indexed from sourceView source ↗

Module documentation

Comparison with Mathlib's idèle class group

The restricted-product idèle group and Mathlib's adele-unit idèle group are already multiplicatively equivalent. The principal subgroups correspond, so the equivalence descends to idèle classes. The one-place map comparison needed for the public local--global reciprocity theorem is recorded below.

Imports2
Imported by3

Declarations

theorem

equivAdeleRingUnits_principalIdele

L30 ↗
IdeleGroup.equivAdeleRingUnits_principalIdele
Documentation

The algebraic idèle equivalence carries each principal idèle to Mathlib's diagonal idèle.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem equivAdeleRingUnits_principalIdele (x : Kˣ) :
    equivAdeleRingUnits (principalIdele K x) =
      NumberField.IdeleGroup.unitEmbedding (𝓞 K) K x
def

ideleClassGroupEquivMathlib

L39 ↗
IdeleGroup.ideleClassGroupEquivMathlib
Documentation

The induced multiplicative equivalence of idèle class groups.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
def ideleClassGroupEquivMathlib :
    IdeleClassGroup K ≃* NumberField.IdeleClassGroup (𝓞 K) K
theorem

equivAdeleRingUnits_finitePlaceIdele

L74 ↗
IdeleGroup.equivAdeleRingUnits_finitePlaceIdele
Documentation

The algebraic idèle comparison carries a one-place idèle to Mathlib's one-place adele-unit idèle.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem equivAdeleRingUnits_finitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K)) (x : (v.adicCompletion K)ˣ) :
    equivAdeleRingUnits (finitePlaceIdele v x) =
      NumberField.IdeleGroup.ofAdicCompletion (𝓞 K) K v x
theorem

ideleClassGroupEquivMathlib_finitePlaceIdeleClass

L102 ↗
IdeleGroup.ideleClassGroupEquivMathlib_finitePlaceIdeleClass
Documentation

The class-group comparison respects the one-place idèle-class maps.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace IdeleGroup
variable (K : Type*) [Field K] [NumberField K]
Lean source · statement
theorem ideleClassGroupEquivMathlib_finitePlaceIdeleClass
    (v : HeightOneSpectrum (𝓞 K)) (x : (v.adicCompletion K)ˣ) :
    ideleClassGroupEquivMathlib K (finitePlaceIdeleClass v x) =
      NumberField.IdeleClassGroup.ofAdicCompletion (𝓞 K) K v x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.