Module

GlobalArtinCompatibility.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalArtinCompatibility

12 declarations indexed from sourceView source ↗

Module documentation

Compatibility of the global Artin map with global reciprocity

For a finite abelian extension of number fields, the preliminary global Artin map is the product of the chosen local Artin maps. The finite-place and infinite-place compatibility theorems identify every one-place factor with the canonical global norm-residue map.

Only finitely many finite local Artin factors of an idele are nontrivial. The finite-support approximation theorem replaces an arbitrary idele by the product of those one-place ideles modulo an actual relative-idele norm. It follows that the preliminary global Artin map is exactly the pullback of the canonical norm-residue map along I_K → C_K.

In particular, the local product is trivial on every principal idele. The global Artin map therefore descends to the idele class group, where it is the canonical surjective reciprocity homomorphism and has the genuine idele-class norm range as its kernel.

Imports7

Imported by5

theorem

globalNormResidueMonoidHom_comp_ideleClassQuotient_eq_globalArtin

L55 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_comp_ideleClassQuotient_eq_globalArtin

Documentation

Pulling the canonical global norm-residue homomorphism back from idele classes to ideles gives exactly the product of the chosen local Artin homomorphisms.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    globalNormResidueMonoidHom_comp_ideleClassQuotient_eq_globalArtin :
    (globalNormResidueMonoidHom K L).comp
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)) =
      globalArtinMonoidHom (K := K) (L := L)

theorem

globalArtinMonoidHom_principalIdele

L151 ↗

GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_principalIdele

Documentation

The chosen local Artin product is trivial on every principal idele. This is the global Artin product formula with the arithmetic Frobenius normalization used by the local maps.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalArtinMonoidHom_principalIdele
    (x : Kˣ) :
    globalArtinMonoidHom
        (K := K) (L := L)
        (IdeleGroup.principalIdele K x) =
      1

theorem

chosenLocalArtin_product_principalIdele

L180 ↗

GlobalClassFieldTheory.Reciprocity.chosenLocalArtin_product_principalIdele

Documentation

Expanded form of the global product formula: the product of all chosen infinite local symbols and the finite-support product of all chosen finite local symbols of a principal idele is one.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem chosenLocalArtin_product_principalIdele
    (x : Kˣ) :
    (∏ v : InfinitePlace K,
        chosenInfinitePlaceArtinMonoidHom
          (K := K) (L := L) v
          (IdeleGroup.infiniteComponent v
            (IdeleGroup.principalIdele K x))) *
      ∏ᶠ v : HeightOneSpectrum (𝓞 K),
        chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v
          (IdeleGroup.finiteComponent v
            (IdeleGroup.principalIdele K x)) =
      1

def

globalIdeleClassArtinMonoidHom

L200 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinMonoidHom

Documentation

The genuine idele-class Artin homomorphism obtained by descending the local-product global Artin map through the principal ideles.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

def globalIdeleClassArtinMonoidHom :
    IdeleClassGroup K →* (L ≃ₐ[K] L)

theorem

globalIdeleClassArtinMonoidHom_mk

L217 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinMonoidHom_mk

Documentation

Evaluation of the descended Artin homomorphism on an idele representative recovers the chosen-local-factor product.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalIdeleClassArtinMonoidHom_mk
    (a : IdeleGroup K) :
    globalIdeleClassArtinMonoidHom
        (K := K) (L := L)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a) =
      globalArtinMonoidHom (K := K) (L := L) a

theorem

globalIdeleClassArtinMonoidHom_continuous

L229 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinMonoidHom_continuous

Documentation

The descended global Artin homomorphism is continuous for the ordinary quotient topology on the idele class group.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalIdeleClassArtinMonoidHom_continuous :
    Continuous
      (globalIdeleClassArtinMonoidHom
        (K := K) (L := L))

def

globalIdeleClassArtinContinuousMonoidHom

L246 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinContinuousMonoidHom

Documentation

The descended global Artin map, retaining its ordinary topological group structure.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · full declaration

def globalIdeleClassArtinContinuousMonoidHom :
    IdeleClassGroup K →ₜ* (L ≃ₐ[K] L) where
  toMonoidHom :=
    globalIdeleClassArtinMonoidHom
      (K := K) (L := L)
  continuous_toFun :=
    globalIdeleClassArtinMonoidHom_continuous
      (K := K) (L := L)

theorem

globalIdeleClassArtinMonoidHom_eq_globalNormResidueMonoidHom

L257 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinMonoidHom_eq_globalNormResidueMonoidHom

Documentation

The descended local-product Artin homomorphism is the canonical global norm-residue homomorphism.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    globalIdeleClassArtinMonoidHom_eq_globalNormResidueMonoidHom :
    globalIdeleClassArtinMonoidHom
        (K := K) (L := L) =
      globalNormResidueMonoidHom K L

theorem

globalIdeleClassArtinContinuousMonoidHom_eq_globalNormResidueContinuousMonoidHom

L282 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinContinuousMonoidHom_eq_globalNormResidueContinuousMonoidHom

Documentation

The independently descended continuous local-product Artin map is the canonical topological global norm-residue map.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem
    globalIdeleClassArtinContinuousMonoidHom_eq_globalNormResidueContinuousMonoidHom :
    globalIdeleClassArtinContinuousMonoidHom
        (K := K) (L := L) =
      globalNormResidueContinuousMonoidHom K L

theorem

globalIdeleClassArtinMonoidHom_surjective

L299 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinMonoidHom_surjective

Documentation

The descended global Artin homomorphism is surjective.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalIdeleClassArtinMonoidHom_surjective :
    Function.Surjective
      (globalIdeleClassArtinMonoidHom
        (K := K) (L := L))

theorem

globalIdeleClassArtinMonoidHom_ker

L310 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinMonoidHom_ker

Documentation

The kernel of the descended global Artin homomorphism is exactly the genuine idele-class norm range.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalIdeleClassArtinMonoidHom_ker :
    (globalIdeleClassArtinMonoidHom
      (K := K) (L := L)).ker =
      (_root_.ideleClassNorm K L).range

theorem

globalIdeleClassArtinMonoidHom_eq_one_iff

L321 ↗

GlobalClassFieldTheory.Reciprocity.globalIdeleClassArtinMonoidHom_eq_one_iff

Documentation

An idele class has trivial global Artin symbol exactly when it is the norm of an idele class from the extension.

Source context 7 commands

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

open scoped NumberField BigOperators IsMulCommutative
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem globalIdeleClassArtinMonoidHom_eq_one_iff
    (c : IdeleClassGroup K) :
    globalIdeleClassArtinMonoidHom
        (K := K) (L := L) c = 1 ↔
      c ∈ (_root_.ideleClassNorm K L).range

Module documentation

Compatibility of the global Artin map with global reciprocity

Declarations