Module

NormQuotient.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.NormQuotient

3 declarations indexed from sourceView source ↗

Module documentation

Ideles in the ordinary idele-class norm quotient

This file supplies the useful composite from ideles to the quotient of C_K by the range of the ordinary norm C_L → C_K, used by the global norm-residue-symbol constructions.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.IdeleNorm

Imported by2

instance

normQuotientIdeleClassGroupIsMulCommutative

L31 ↗

GlobalClassFieldTheory.Reciprocity.normQuotientIdeleClassGroupIsMulCommutative

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 L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

instance normQuotientIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)

def

globalNormClassFromIdele

L37 ↗

GlobalClassFieldTheory.Reciprocity.globalNormClassFromIdele

Documentation

The composite from ideles to the canonical class norm quotient C_K / N_{L/K} C_L.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
local instance normQuotientIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def globalNormClassFromIdele :
    IdeleGroup K →*
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range

theorem

globalNormClassFromIdele_principalIdele

L50 ↗

GlobalClassFieldTheory.Reciprocity.globalNormClassFromIdele_principalIdele

Documentation

The map from ideles to the class norm quotient factors through C_K, so it kills every principal idele.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
local instance normQuotientIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [FiniteDimensional K L] in

Lean source · statement

theorem globalNormClassFromIdele_principalIdele
    (x : Kˣ) :
    globalNormClassFromIdele K L
        (IdeleGroup.principalIdele K x) = 1

Module documentation

Ideles in the ordinary idele-class norm quotient

Declarations

normQuotientIdeleClassGroupIsMulCommutative

globalNormClassFromIdele

globalNormClassFromIdele_principalIdele