Module

FiniteLocalFamily.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.FiniteLocalFamily

5 declarations indexed from sourceView source ↗

Module documentation

Finite local families of ideles

A finite family of local elements, extended by 1, is the product of its one-place ideles. Applying the global norm-quotient map gives the finite product identity. The quotient map itself factors through idele classes and therefore kills principal ideles.

Imports2

Imported by3

theorem

prod_finitePlaceIdele_eq_ideleOfFiniteLocalFamily

L33 ↗

GlobalClassFieldTheory.Reciprocity.prod_finitePlaceIdele_eq_ideleOfFiniteLocalFamily

Documentation

A finite local family is the product of its one-place ideles.

Source context 7 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem prod_finitePlaceIdele_eq_ideleOfFiniteLocalFamily
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ) :
    (∏ v : ↥S, finitePlaceIdele v.1 (a v)) =
      IdeleGroup.ideleOfFiniteLocalFamily S a

theorem

map_ideleOfFiniteLocalFamily_eq_prod_local

L107 ↗

GlobalClassFieldTheory.Reciprocity.map_ideleOfFiniteLocalFamily_eq_prod_local

Documentation

Applying any multiplicative global symbol to a finite local family gives the product of the one-place symbols.

Source context 7 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem map_ideleOfFiniteLocalFamily_eq_prod_local
    {A : Type*} [CommGroup A]
    (f : IdeleGroup K →* A)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ) :
    f (IdeleGroup.ideleOfFiniteLocalFamily S a) =
      ∏ v : ↥S, f (finitePlaceIdele v.1 (a v))

instance

finiteLocalFamilyIdeleClassGroupIsMulCommutative

L123 ↗

GlobalClassFieldTheory.Reciprocity.finiteLocalFamilyIdeleClassGroupIsMulCommutative

Source context 9 commands

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

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

Lean source · statement

instance finiteLocalFamilyIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)

instance

finiteLocalFamilyIdeleClassGroupCommGroup

L127 ↗

GlobalClassFieldTheory.Reciprocity.finiteLocalFamilyIdeleClassGroupCommGroup

Source context 10 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K : Type*} [Field K] [NumberField K]
section NormQuotient
variable
    (L : Type*) [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
local instance finiteLocalFamilyIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

instance finiteLocalFamilyIdeleClassGroupCommGroup :
    CommGroup (IdeleClassGroup K)

theorem

globalNormClass_finiteLocalFamily

L135 ↗

GlobalClassFieldTheory.Reciprocity.globalNormClass_finiteLocalFamily

Documentation

The finite-support product formula for the global norm-quotient symbol.

Source context 12 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable {K : Type*} [Field K] [NumberField K]
section NormQuotient
variable
    (L : Type*) [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
local instance finiteLocalFamilyIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance finiteLocalFamilyIdeleClassGroupCommGroup :
    CommGroup (IdeleClassGroup K) :=
  open scoped IsMulCommutative in
  inferInstance
omit [FiniteDimensional K L] in

Lean source · statement

theorem globalNormClass_finiteLocalFamily
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ) :
    globalNormClassFromIdele K L
        (IdeleGroup.ideleOfFiniteLocalFamily S a) =
      ∏ v : ↥S,
        globalNormClassFromIdele K L
          (finitePlaceIdele v.1 (a v))

Module documentation

Finite local families of ideles

Declarations

prod_finitePlaceIdele_eq_ideleOfFiniteLocalFamily

map_ideleOfFiniteLocalFamily_eq_prod_local

finiteLocalFamilyIdeleClassGroupIsMulCommutative

finiteLocalFamilyIdeleClassGroupCommGroup

globalNormClass_finiteLocalFamily