NYLL
Module

InfiniteGlobalArtinDescent.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.InfiniteGlobalArtinDescent
7 declarations indexed from sourceView source ↗

Module documentation

Descent of the infinite global Artin homomorphism

The finite global Artin product formula at every finite Galois intermediate field shows that the infinite global Artin homomorphism kills principal ideles. This file descends that homomorphism to the idele class group and retains its ordinary quotient topology.

Imports2
Imported by3

Declarations

theorem

continuousMulEquivToLimit_infiniteGlobalArtinMonoidHom_apply

L33 ↗
GlobalClassFieldTheory.Reciprocity.continuousMulEquivToLimit_infiniteGlobalArtinMonoidHom_apply
Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
Lean source · statement
theorem
    continuousMulEquivToLimit_infiniteGlobalArtinMonoidHom_apply
    (a : IdeleGroup K) :
    InfiniteGalois.continuousMulEquivToLimit K Ω
        (infiniteGlobalArtinMonoidHom K Ω a) =
      infiniteGlobalArtinToLimit K Ω a
theorem

infiniteGlobalArtinMonoidHom_principalIdele

L45 ↗
GlobalClassFieldTheory.Reciprocity.infiniteGlobalArtinMonoidHom_principalIdele
Documentation

The infinite global Artin homomorphism is trivial on every principal idele.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
Lean source · statement
theorem infiniteGlobalArtinMonoidHom_principalIdele
    (x : Kˣ) :
    infiniteGlobalArtinMonoidHom K Ω
        (IdeleGroup.principalIdele K x) =
      1
def

infiniteGlobalIdeleClassArtinMonoidHom

L66 ↗
GlobalClassFieldTheory.Reciprocity.infiniteGlobalIdeleClassArtinMonoidHom
Documentation

The infinite global Artin homomorphism descended through the subgroup of principal ideles.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
Lean source · statement
def infiniteGlobalIdeleClassArtinMonoidHom :
    IdeleClassGroup K →* (Ω ≃ₐ[K] Ω)
theorem

infiniteGlobalIdeleClassArtinMonoidHom_mk

L82 ↗
GlobalClassFieldTheory.Reciprocity.infiniteGlobalIdeleClassArtinMonoidHom_mk
Documentation

Evaluation of the descended infinite global Artin homomorphism on an idele representative recovers the original infinite Artin homomorphism.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
Lean source · statement
theorem infiniteGlobalIdeleClassArtinMonoidHom_mk
    (a : IdeleGroup K) :
    infiniteGlobalIdeleClassArtinMonoidHom
        (K := K) (Ω := Ω)
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a) =
      infiniteGlobalArtinMonoidHom K Ω a
theorem

infiniteGlobalIdeleClassArtinMonoidHom_continuous

L92 ↗
GlobalClassFieldTheory.Reciprocity.infiniteGlobalIdeleClassArtinMonoidHom_continuous
Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
Lean source · statement
theorem infiniteGlobalIdeleClassArtinMonoidHom_continuous :
    Continuous
      (infiniteGlobalIdeleClassArtinMonoidHom
        (K := K) (Ω := Ω))
def

infiniteGlobalIdeleClassArtinContinuousMonoidHom

L109 ↗
GlobalClassFieldTheory.Reciprocity.infiniteGlobalIdeleClassArtinContinuousMonoidHom
Documentation

The descended infinite global Artin homomorphism, retaining the ordinary quotient topology on the idele class group.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
Lean source · full declaration
def infiniteGlobalIdeleClassArtinContinuousMonoidHom :
    IdeleClassGroup K →ₜ* (Ω ≃ₐ[K] Ω) where
  toMonoidHom :=
    infiniteGlobalIdeleClassArtinMonoidHom
      (K := K) (Ω := Ω)
  continuous_toFun :=
    infiniteGlobalIdeleClassArtinMonoidHom_continuous
      (K := K) (Ω := Ω)
theorem

infiniteGlobalIdeleClassArtinContinuousMonoidHom_denseRange

L120 ↗
GlobalClassFieldTheory.Reciprocity.infiniteGlobalIdeleClassArtinContinuousMonoidHom_denseRange
Documentation

The descended infinite global Artin homomorphism has dense image in the Krull topology.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K Ω : Type}
    [Field K] [NumberField K]
    [Field Ω] [Algebra K Ω] [IsAbelianGalois K Ω]
Lean source · statement
theorem infiniteGlobalIdeleClassArtinContinuousMonoidHom_denseRange :
    DenseRange
      (infiniteGlobalIdeleClassArtinContinuousMonoidHom
        (K := K) (Ω := Ω))

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