NYLL
Module

ArithmeticNormalization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ArithmeticNormalization
34 declarations indexed from sourceView source ↗

Module documentation

Arithmetic normalization of global reciprocity

The valuation used by the local class-formation implementation is the logarithm of the multiplicative absolute value. Consequently its distinguished element of value 1 is the inverse of a DVR uniformizer. The resulting field-facing reciprocity map sends a usual uniformizer to geometric Frobenius.

The arithmetic global norm-residue symbol uses the opposite normalization: a DVR uniformizer maps to arithmetic Frobenius and a ramified cyclotomic unit u acts by u⁻¹. For an abelian target the two normalizations differ by the canonical inversion automorphism. This file records that normalization explicitly, including its topology and its local-global compatibility. Thus no sign convention is hidden in an unbundled equality.

Imports2
Imported by14

Declarations

theorem

arithmeticNormIdeleClassIsMulCommutative

L39 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticNormIdeleClassIsMulCommutative
Source context 6 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
Lean source · statement
theorem arithmeticNormIdeleClassIsMulCommutative
    (K : Type) [Field K] [NumberField K] :
    IsMulCommutative (IdeleClassGroup K)
def

commutativeGroupInversionContinuousMulEquiv

L48 ↗
GlobalClassFieldTheory.Reciprocity.commutativeGroupInversionContinuousMulEquiv
Documentation

Inversion as a topological multiplicative automorphism of a commutative topological group.

Source context 7 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
Lean source · statement
def commutativeGroupInversionContinuousMulEquiv
    (G : Type*) [CommGroup G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    G ≃ₜ* G
instance

arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology

L64 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology
Documentation

Reuse the quotient topology chosen by topological global reciprocity.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K)))
instance

arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup

L72 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup
Documentation

The quotient topology above carries the quotient topological-group structure.

Source context 10 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
Lean source · statement
instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K)))
def

arithmeticGlobalNormResidueAbelianizationMonoidHom

L82 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianizationMonoidHom
Documentation

The global norm-residue homomorphism with arithmetic Frobenius normalization, for an arbitrary finite Galois extension.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
def arithmeticGlobalNormResidueAbelianizationMonoidHom :
    IdeleClassGroup K →*
      Abelianization (Gal(L / K))
theorem

arithmeticGlobalNormResidueAbelianizationMonoidHom_apply

L92 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianizationMonoidHom_apply
Documentation

Arithmetic normalization evaluates by inverting the geometric norm-residue symbol.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
theorem arithmeticGlobalNormResidueAbelianizationMonoidHom_apply
    (c : IdeleClassGroup K) :
    arithmeticGlobalNormResidueAbelianizationMonoidHom K L c =
      (globalNormResidueAbelianizationMonoidHom K L c)⁻¹
theorem

arithmeticGlobalNormResidueAbelianizationMonoidHom_ker

L100 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianizationMonoidHom_ker
Documentation

Arithmetic normalization does not change the genuine norm kernel.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
theorem arithmeticGlobalNormResidueAbelianizationMonoidHom_ker :
    (arithmeticGlobalNormResidueAbelianizationMonoidHom K L).ker =
      (_root_.ideleClassNorm K L).range
theorem

arithmeticGlobalNormResidueAbelianizationMonoidHom_surjective

L110 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianizationMonoidHom_surjective
Documentation

The arithmetic global norm-residue homomorphism is surjective.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
theorem arithmeticGlobalNormResidueAbelianizationMonoidHom_surjective :
    Function.Surjective
      (arithmeticGlobalNormResidueAbelianizationMonoidHom K L)
def

arithmeticGlobalNormResidueAbelianizationContinuousMulEquiv

L120 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianizationContinuousMulEquiv
Documentation

The arithmetic finite-Galois norm-residue isomorphism, with the native idèle-class quotient topology and the finite Krull quotient topology on the Galois abelianization.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
def
    arithmeticGlobalNormResidueAbelianizationContinuousMulEquiv :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃ₜ*
      Abelianization (Gal(L / K))
theorem

arithmeticGlobalNormResidueAbelianizationContinuousMulEquiv_apply

L132 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueAbelianizationContinuousMulEquiv_apply
Documentation

The arithmetic abelianized norm-residue equivalence is pointwise the inverse of the geometric equivalence.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
theorem
    arithmeticGlobalNormResidueAbelianizationContinuousMulEquiv_apply
    (q :
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :
    arithmeticGlobalNormResidueAbelianizationContinuousMulEquiv K L q =
      (globalNormResidueAbelianizationContinuousMulEquiv K L q)⁻¹
def

arithmeticGlobalReciprocityAbelianizationContinuousMulEquiv

L154 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalReciprocityAbelianizationContinuousMulEquiv
Documentation

The canonical reciprocity isomorphism Gal(L/K)ᵃᵇ ≃ₜ* C_K / N_{L/K}(C_L), in the direction stated in the global reciprocity theorem.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
def
    arithmeticGlobalReciprocityAbelianizationContinuousMulEquiv :
    Abelianization (Gal(L / K)) ≃ₜ*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
theorem

arithmeticGlobalReciprocityAbelianizationContinuousMulEquiv_symm_mk

L165 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalReciprocityAbelianizationContinuousMulEquiv_symm_mk
Documentation

The inverse of arithmetic reciprocity is literally the arithmetic global norm-residue symbol on every idèle class.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteGalois
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Reuse the quotient topology chosen by topological global reciprocity. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) :=
  topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
    K L
/-- The quotient topology above carries the quotient topological-group
structure. -/
local instance
    arithmeticGlobalNormResidueAbelianization_galoisAbelianizationIsTopologicalGroup :
    IsTopologicalGroup (Abelianization (Gal(L / K))) := by
  change
    IsTopologicalGroup
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
theorem
    arithmeticGlobalReciprocityAbelianizationContinuousMulEquiv_symm_mk
    (c : IdeleClassGroup K) :
    (arithmeticGlobalReciprocityAbelianizationContinuousMulEquiv
        K L).symm
      (QuotientGroup.mk'
        (_root_.ideleClassNorm K L).range c) =
      arithmeticGlobalNormResidueAbelianizationMonoidHom K L c
def

arithmeticGlobalNormResidueMonoidHom

L206 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom
Documentation

The global norm-residue homomorphism in arithmetic Frobenius normalization for a finite abelian extension.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalNormResidueMonoidHom :
    IdeleClassGroup K →* Gal(L / K)
theorem

arithmeticGlobalNormResidueMonoidHom_apply

L214 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom_apply
Documentation

Arithmetic normalization evaluates by inverting the geometric global norm-residue symbol.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalNormResidueMonoidHom_apply
    (c : IdeleClassGroup K) :
    arithmeticGlobalNormResidueMonoidHom K L c =
      (globalNormResidueMonoidHom K L c)⁻¹
theorem

arithmeticGlobalNormResidueMonoidHom_ker

L222 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom_ker
Documentation

Arithmetic normalization leaves the global norm kernel unchanged.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalNormResidueMonoidHom_ker :
    (arithmeticGlobalNormResidueMonoidHom K L).ker =
      (_root_.ideleClassNorm K L).range
theorem

arithmeticGlobalNormResidueMonoidHom_surjective

L231 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom_surjective
Documentation

The arithmetic global norm-residue homomorphism is surjective.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalNormResidueMonoidHom_surjective :
    Function.Surjective
      (arithmeticGlobalNormResidueMonoidHom K L)
theorem

arithmeticGlobalNormResidueMonoidHom_continuous

L239 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom_continuous
Documentation

The arithmetic global norm-residue map is continuous for the ordinary idèle-class topology and the finite Krull topology.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalNormResidueMonoidHom_continuous :
    Continuous (arithmeticGlobalNormResidueMonoidHom K L)
def

arithmeticGlobalNormResidueContinuousMulEquiv

L247 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueContinuousMulEquiv
Documentation

Arithmetic global norm-residue as a homeomorphic multiplicative equivalence of the native norm quotient with the finite Krull Galois group.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalNormResidueContinuousMulEquiv :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃ₜ*
      Gal(L / K)
theorem

arithmeticGlobalNormResidueContinuousMulEquiv_apply

L258 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueContinuousMulEquiv_apply
Documentation

The arithmetic norm-residue equivalence is pointwise the inverse of the geometric equivalence.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalNormResidueContinuousMulEquiv_apply
    (q :
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :
    arithmeticGlobalNormResidueContinuousMulEquiv K L q =
      (globalNormResidueContinuousMulEquiv K L q)⁻¹
def

arithmeticGlobalReciprocityContinuousMulEquiv

L268 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalReciprocityContinuousMulEquiv
Documentation

The canonical arithmetic reciprocity isomorphism in the direction Gal(L/K) ≃ₜ* C_K / N_{L/K}(C_L).

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalReciprocityContinuousMulEquiv :
    Gal(L / K) ≃ₜ*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
theorem

arithmeticGlobalReciprocityContinuousMulEquiv_symm_mk

L277 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalReciprocityContinuousMulEquiv_symm_mk
Documentation

Applying inverse arithmetic reciprocity to a quotient representative recovers the arithmetic norm-residue symbol.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalReciprocityContinuousMulEquiv_symm_mk
    (c : IdeleClassGroup K) :
    (arithmeticGlobalReciprocityContinuousMulEquiv K L).symm
      (QuotientGroup.mk'
        (_root_.ideleClassNorm K L).range c) =
      arithmeticGlobalNormResidueMonoidHom K L c
theorem

arithmeticGlobalReciprocityContinuousMulEquiv_globalNormResidue

L288 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalReciprocityContinuousMulEquiv_globalNormResidue
Documentation

Arithmetic reciprocity sends the arithmetic norm-residue symbol of an idèle class to its literal representative in the norm quotient.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalReciprocityContinuousMulEquiv_globalNormResidue
    (c : IdeleClassGroup K) :
    arithmeticGlobalReciprocityContinuousMulEquiv K L
        (arithmeticGlobalNormResidueMonoidHom K L c) =
      QuotientGroup.mk'
        (_root_.ideleClassNorm K L).range c
def

arithmeticChosenFinitePlaceArtinMonoidHom

L311 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticChosenFinitePlaceArtinMonoidHom
Documentation

The chosen finite-place Artin homomorphism in arithmetic normalization. A usual local uniformizer therefore maps to arithmetic Frobenius.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticChosenFinitePlaceArtinMonoidHom
    (v : HeightOneSpectrum (𝓞 K)) :
    (v.adicCompletion K)ˣ →* Gal(L / K)
theorem

arithmeticChosenFinitePlaceArtinMonoidHom_apply

L322 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticChosenFinitePlaceArtinMonoidHom_apply
Documentation

Arithmetic finite-place Artin symbols are inverses of the geometric chosen local symbols.

Source context 10 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField L] in
Lean source · statement
theorem arithmeticChosenFinitePlaceArtinMonoidHom_apply
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    arithmeticChosenFinitePlaceArtinMonoidHom K L v x =
      (chosenFinitePlaceArtinMonoidHom
        (K := K) (L := L) v x)⁻¹
theorem

arithmeticGlobalNormResidueMonoidHom_comp_finitePlaceIdeleClass

L332 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom_comp_finitePlaceIdeleClass
Documentation

Finite-place local-global compatibility in arithmetic normalization.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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
    arithmeticGlobalNormResidueMonoidHom_comp_finitePlaceIdeleClass
    (v : HeightOneSpectrum (𝓞 K)) :
    (arithmeticGlobalNormResidueMonoidHom K L).comp
        (IdeleGroup.finitePlaceIdeleClass v) =
      arithmeticChosenFinitePlaceArtinMonoidHom K L v
def

arithmeticChosenInfinitePlaceArtinMonoidHom

L353 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticChosenInfinitePlaceArtinMonoidHom
Documentation

The chosen infinite-place Artin homomorphism in arithmetic normalization.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticChosenInfinitePlaceArtinMonoidHom
    (v : InfinitePlace K) :
    v.Completionˣ →* Gal(L / K)
theorem

arithmeticChosenInfinitePlaceArtinMonoidHom_apply

L364 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticChosenInfinitePlaceArtinMonoidHom_apply
Documentation

Arithmetic infinite-place Artin symbols are inverses of the geometric chosen local symbols.

Source context 10 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [NumberField K] [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem arithmeticChosenInfinitePlaceArtinMonoidHom_apply
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    arithmeticChosenInfinitePlaceArtinMonoidHom K L v x =
      (chosenInfinitePlaceArtinMonoidHom
        (K := K) (L := L) v x)⁻¹
theorem

arithmeticGlobalNormResidueMonoidHom_comp_infinitePlaceIdeleClass

L374 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom_comp_infinitePlaceIdeleClass
Documentation

Infinite-place local-global compatibility in arithmetic normalization.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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
    arithmeticGlobalNormResidueMonoidHom_comp_infinitePlaceIdeleClass
    (v : InfinitePlace K) :
    (arithmeticGlobalNormResidueMonoidHom K L).comp
        (IdeleGroup.infinitePlaceIdeleClass v) =
      arithmeticChosenInfinitePlaceArtinMonoidHom K L v
def

arithmeticGlobalArtinMonoidHom

L394 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalArtinMonoidHom
Documentation

The idèle-level global Artin product in arithmetic normalization.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalArtinMonoidHom :
    IdeleGroup K →* Gal(L / K)
theorem

arithmeticGlobalArtinMonoidHom_apply

L403 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalArtinMonoidHom_apply
Documentation

The arithmetic global Artin symbol is the inverse of the geometric global Artin symbol.

Source context 10 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem arithmeticGlobalArtinMonoidHom_apply
    (a : IdeleGroup K) :
    arithmeticGlobalArtinMonoidHom K L a =
      (globalArtinMonoidHom (K := K) (L := L) a)⁻¹
theorem

arithmeticGlobalArtinMonoidHom_finitePlaceIdele

L412 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalArtinMonoidHom_finitePlaceIdele
Documentation

The arithmetic global Artin symbol of a finite one-place idèle is literally the arithmetic chosen local Artin symbol.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalArtinMonoidHom_finitePlaceIdele
    (v : HeightOneSpectrum (𝓞 K))
    (x : (v.adicCompletion K)ˣ) :
    arithmeticGlobalArtinMonoidHom K L
        (finitePlaceIdele v x) =
      arithmeticChosenFinitePlaceArtinMonoidHom K L v x
theorem

arithmeticGlobalArtinMonoidHom_infinitePlaceIdele

L426 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalArtinMonoidHom_infinitePlaceIdele
Documentation

The arithmetic global Artin symbol of an infinite one-place idèle is literally the arithmetic chosen local Artin symbol.

Source context 10 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem arithmeticGlobalArtinMonoidHom_infinitePlaceIdele
    (v : InfinitePlace K)
    (x : v.Completionˣ) :
    arithmeticGlobalArtinMonoidHom K L
        (infinitePlaceIdele v x) =
      arithmeticChosenInfinitePlaceArtinMonoidHom K L v x
theorem

arithmeticGlobalArtinMonoidHom_principalIdele

L438 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalArtinMonoidHom_principalIdele
Documentation

Arithmetic global Artin kills every principal idèle.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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 arithmeticGlobalArtinMonoidHom_principalIdele
    (x : Kˣ) :
    arithmeticGlobalArtinMonoidHom K L
        (IdeleGroup.principalIdele K x) =
      1
theorem

arithmeticGlobalNormResidueMonoidHom_comp_ideleClassQuotient_eq_globalArtin

L448 ↗
GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom_comp_ideleClassQuotient_eq_globalArtin
Documentation

Descending the arithmetic local-product Artin map through principal idèles gives the arithmetic global norm-residue homomorphism literally.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField IsDedekindDomain
open IdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] arithmeticNormIdeleClassIsMulCommutative
section FiniteAbelian
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
    arithmeticGlobalNormResidueMonoidHom_comp_ideleClassQuotient_eq_globalArtin :
    (arithmeticGlobalNormResidueMonoidHom K L).comp
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K)) =
      arithmeticGlobalArtinMonoidHom K L

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