NYLL
Module

GlobalArtinFiniteSupportApproximation.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalArtinFiniteSupportApproximation
12 declarations indexed from sourceView source ↗

Module documentation

Finite-support reduction for the global Artin map

For a finite abelian extension L / K, only finitely many finite local Artin factors of an idele are nontrivial. Keeping precisely those finite components, together with every infinite component, gives an idele with finite one-place support. The quotient of the original idele by this approximation is an actual relative-idele norm: outside the retained finite set this follows from the local Artin kernel theorem, and at the retained and infinite places it follows because the quotient component is one.

Consequently both the preliminary global Artin map and the canonical idele-class norm quotient may be evaluated on this finite-support approximation.

Imports3
Imported by2

Declarations

theorem

artinFiniteSupportIdeleClassIsMulCommutative

L40 ↗
GlobalClassFieldTheory.Reciprocity.artinFiniteSupportIdeleClassIsMulCommutative
Documentation

Supply the canonical commutativity used by the finite-support norm quotient.

Source context 6 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
Lean source · statement
theorem artinFiniteSupportIdeleClassIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

globalArtinFiniteSupport

L55 ↗
GlobalClassFieldTheory.Reciprocity.globalArtinFiniteSupport
Documentation

The finite places at which the local Artin factor of a is nontrivial.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
def globalArtinFiniteSupport
    (a : IdeleGroup K) :
    Finset (HeightOneSpectrum (𝓞 K))
theorem

mem_globalArtinFiniteSupport_iff

L64 ↗
GlobalClassFieldTheory.Reciprocity.mem_globalArtinFiniteSupport_iff
Documentation

Membership in the finite Artin support is equivalent to nontriviality of the corresponding chosen local Artin factor.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem mem_globalArtinFiniteSupport_iff
    (a : IdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    v ∈ globalArtinFiniteSupport (K := K) (L := L) a ↔
      chosenFinitePlaceArtinMonoidHom
          (K := K) (L := L) v
          (IdeleGroup.finiteComponent v a) ≠ 1
def

artinFiniteSupportApproximation

L80 ↗
GlobalClassFieldTheory.Reciprocity.artinFiniteSupportApproximation
Documentation

The finite-support Artin approximation of an idele. It is the product of the one-place ideles carrying all infinite components and the one-place ideles carrying exactly the finite components with nontrivial local Artin factor.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
def artinFiniteSupportApproximation
    (a : IdeleGroup K) :
    IdeleGroup K
theorem

artinFiniteSupportApproximation_infiniteComponent

L94 ↗
GlobalClassFieldTheory.Reciprocity.artinFiniteSupportApproximation_infiniteComponent
Documentation

The finite-support Artin approximation retains every infinite component.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem artinFiniteSupportApproximation_infiniteComponent
    (a : IdeleGroup K)
    (w : InfinitePlace K) :
    IdeleGroup.infiniteComponent w
        (artinFiniteSupportApproximation
          (K := K) (L := L) a) =
      IdeleGroup.infiniteComponent w a
theorem

artinFiniteSupportApproximation_finiteComponent

L127 ↗
GlobalClassFieldTheory.Reciprocity.artinFiniteSupportApproximation_finiteComponent
Documentation

At a finite place, the approximation is the original component exactly on the finite Artin support and is one elsewhere.

Source context 9 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
open scoped Classical in
Lean source · full declaration
theorem artinFiniteSupportApproximation_finiteComponent
    (a : IdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    IdeleGroup.finiteComponent v
        (artinFiniteSupportApproximation
          (K := K) (L := L) a) =
      if v ∈ globalArtinFiniteSupport
          (K := K) (L := L) a then
        IdeleGroup.finiteComponent v a
      else 1 := by
  classical
  rw [artinFiniteSupportApproximation,
    prod_finitePlaceIdele_eq_ideleOfFiniteLocalFamily]
  have hinfinite :
      IdeleGroup.finiteComponent v
          (∏ w : InfinitePlace K,
            infinitePlaceIdele w
              (IdeleGroup.infiniteComponent w a)) =
        1 := by
    rw [map_prod]
    apply Finset.prod_eq_one
    intro w _
    exact
      infinitePlaceIdele_finiteComponent w v
        (IdeleGroup.infiniteComponent w a)
  rw [map_mul, hinfinite, one_mul]
  change
    IdeleGroup.finiteIdeleOfFinset
        (globalArtinFiniteSupport
          (K := K) (L := L) a)
        (fun w =>
          IdeleGroup.finiteComponent w.1 a) v =
      if v ∈ globalArtinFiniteSupport
          (K := K) (L := L) a then
        IdeleGroup.finiteComponent v a
      else 1
  by_cases hv :
      v ∈ globalArtinFiniteSupport
        (K := K) (L := L) a
  · rw [ite_eq_left hv]
    exact
      IdeleGroup.finiteIdeleOfFinset_apply_mem
        (globalArtinFiniteSupport
          (K := K) (L := L) a)
        (fun w =>
          IdeleGroup.finiteComponent w.1 a)
        ⟨v, hv⟩
  · rw [ite_eq_right hv]
    exact
      IdeleGroup.finiteIdeleOfFinset_apply_notMem
        (globalArtinFiniteSupport
          (K := K) (L := L) a)
        (fun w =>
          IdeleGroup.finiteComponent w.1 a)
        v hv
theorem

artinFiniteSupportApproximation_finiteComponent_of_mem

L186 ↗
GlobalClassFieldTheory.Reciprocity.artinFiniteSupportApproximation_finiteComponent_of_mem
Documentation

At a place in the Artin support, the finite-support approximation keeps the original finite component.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem artinFiniteSupportApproximation_finiteComponent_of_mem
    (a : IdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∈ globalArtinFiniteSupport
        (K := K) (L := L) a) :
    IdeleGroup.finiteComponent v
        (artinFiniteSupportApproximation
          (K := K) (L := L) a) =
      IdeleGroup.finiteComponent v a
theorem

artinFiniteSupportApproximation_finiteComponent_of_notMem

L203 ↗
GlobalClassFieldTheory.Reciprocity.artinFiniteSupportApproximation_finiteComponent_of_notMem
Documentation

Away from the Artin support, the finite-support approximation has trivial finite component.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem artinFiniteSupportApproximation_finiteComponent_of_notMem
    (a : IdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K))
    (hv :
      v ∉ globalArtinFiniteSupport
        (K := K) (L := L) a) :
    IdeleGroup.finiteComponent v
        (artinFiniteSupportApproximation
          (K := K) (L := L) a) =
      1
theorem

artinFiniteSupportApproximation_remainder_mem_relativeIdeleNorm_range

L222 ↗
GlobalClassFieldTheory.Reciprocity.artinFiniteSupportApproximation_remainder_mem_relativeIdeleNorm_range
Documentation

The quotient of an idele by its finite-support Artin approximation is an actual relative-idele norm.

Source context 9 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
open _root_.GlobalClassFieldTheory.ClassFieldAxiom (
  relativeIdeleNorm_range_eq_allPlaceLocalNormCondition
) in
Lean source · statement
theorem
    artinFiniteSupportApproximation_remainder_mem_relativeIdeleNorm_range
    (a : IdeleGroup K) :
    a * (artinFiniteSupportApproximation
        (K := K) (L := L) a)⁻¹ ∈
      (RelativeIdeleGroup.norm K L).range
theorem

globalNormClassFromIdele_relativeIdeleNorm_eq_one

L287 ↗
GlobalClassFieldTheory.Reciprocity.globalNormClassFromIdele_relativeIdeleNorm_eq_one
Documentation

The canonical idele-class norm quotient kills every actual relative-idele norm.

Source context 9 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
omit [IsAbelianGalois K L] in
Lean source · statement
theorem globalNormClassFromIdele_relativeIdeleNorm_eq_one
    (z : RelativeIdeleGroup K L) :
    globalNormClassFromIdele K L
        (RelativeIdeleGroup.norm K L z) =
      1
theorem

globalArtinMonoidHom_eq_artinFiniteSupportApproximation

L310 ↗
GlobalClassFieldTheory.Reciprocity.globalArtinMonoidHom_eq_artinFiniteSupportApproximation
Documentation

The global Artin value of an idele is already determined by its finite-support Artin approximation.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem globalArtinMonoidHom_eq_artinFiniteSupportApproximation
    (a : IdeleGroup K) :
    globalArtinMonoidHom (K := K) (L := L) a =
      globalArtinMonoidHom (K := K) (L := L)
        (artinFiniteSupportApproximation
          (K := K) (L := L) a)
theorem

globalNormClassFromIdele_eq_artinFiniteSupportApproximation

L339 ↗
GlobalClassFieldTheory.Reciprocity.globalNormClassFromIdele_eq_artinFiniteSupportApproximation
Documentation

The norm class of an idele is already determined by its finite-support Artin approximation.

Source context 8 commands

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

open scoped NumberField TensorProduct BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] artinFiniteSupportIdeleClassIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
Lean source · statement
theorem globalNormClassFromIdele_eq_artinFiniteSupportApproximation
    (a : IdeleGroup K) :
    globalNormClassFromIdele K L a =
      globalNormClassFromIdele K L
        (artinFiniteSupportApproximation
          (K := K) (L := L) a)

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