NYLL
Module

GlobalNormResidueAbelianization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalNormResidueAbelianization
30 declarations indexed from sourceView source ↗

Module documentation

The global norm-residue symbol for finite Galois extensions

For an arbitrary finite Galois extension of number fields, the global norm-residue quotient is the abelianization of the genuine Galois group:

C_K / N_{L/K} C_L ≃ Gal(L / K)ᵃᵇ.

The abelian specialization in GlobalNormResidue identifies this target further with Gal(L / K). This file retains the abelianization and therefore states global reciprocity at its full finite-Galois generality.

Imports1
Imported by3

Declarations

instance

globalNormResidueAbelianization_ideleClassGroupIsMulCommutative

L43 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianization_ideleClassGroupIsMulCommutative
Documentation

Idèle classes are commutative. Keeping the mixin as a named local instance lets norm-range quotient types elaborate before entering a declaration body.

Source context 8 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
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
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)
def

numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization

L50 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization
Documentation

The abelianization of the compatible abstract extension quotient is the abelianization of the actual Galois group.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization :
    Additive
        (Abelianization
          (ClassFormation.FiniteGaloisSubextension.extensionQuotient
            (numberFieldTowerFiniteGaloisSubextension K L))) ≃+
      Additive (Abelianization (Gal(L / K)))
theorem

numberFieldTowerAbelianizationCongr_of

L61 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbelianizationCongr_of
Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem numberFieldTowerAbelianizationCongr_of
    (q :
      ClassFormation.FiniteGaloisSubextension.extensionQuotient
        (numberFieldTowerFiniteGaloisSubextension K L)) :
    MulEquiv.abelianizationCongr
        (numberFieldTowerExtensionQuotientEquivGaloisGroup K L)
        (Abelianization.of q) =
      Abelianization.of
        (numberFieldTowerExtensionQuotientEquivGaloisGroup K L q)
theorem

numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization_of

L76 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization_of
Documentation

The comparison on abelianizations sends the class of an abstract automorphism to the class of its actual restriction to L.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization_of
    (q :
      ClassFormation.FiniteGaloisSubextension.extensionQuotient
        (numberFieldTowerFiniteGaloisSubextension K L)) :
    numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization
        K L (Additive.ofMul (Abelianization.of q)) =
      Additive.ofMul
        (Abelianization.of
          (numberFieldTowerExtensionQuotientEquivGaloisGroup K L q))
def

numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv

L93 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv
Documentation

The abstract norm-residue symbol followed by the concrete Galois comparison. This declaration boundary keeps the dependent quotient indices and their instance packages from being reconstructed at each evaluation.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv :
    FiniteNormQuotient rationalIdeleClassRepresentation
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L) ≃+
      Additive (Abelianization (Gal(L / K)))
def

globalNormResidueAbelianizationEquiv

L144 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationEquiv
Documentation

The actual global norm-residue equivalence for a finite Galois number-field extension:

C_K / N_{L/K} C_L ≃ Gal(L / K)ᵃᵇ.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def globalNormResidueAbelianizationEquiv :
    Additive
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) ≃+
      Additive (Abelianization (Gal(L / K)))
theorem

numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv_apply

L154 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv_apply
Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · full declaration
theorem
    numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv_apply
    (x :
      FiniteNormQuotient rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :
    letI :=
      (numberFieldTowerReciprocityFiniteAbstractField K L).finite
    letI :=
      numberFieldTowerExtensionSubgroup_normal K L
    letI :=
      (numberFieldTowerFiniteGaloisSubextension K L).finite
    numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv K L x =
      numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization
        K L
        (rationalCyclotomicDegreeData.normResidueSymbol
          rationalIdeleClassRepresentation
          rationalCyclotomicIdeleClassValuationData
          rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
          (numberFieldTowerReciprocityFiniteAbstractField K L)
          (numberFieldTowerFiniteGaloisSubextension K L) x) := by
  let hBaseFinite :=
    (numberFieldTowerReciprocityFiniteAbstractField K L).finite
  let hExtensionNormal :=
    numberFieldTowerExtensionSubgroup_normal K L
  let hRelativeFinite :=
    (numberFieldTowerFiniteGaloisSubextension K L).finite
  rfl
theorem

globalNormResidueAbelianizationEquiv_transport_apply

L184 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationEquiv_transport_apply
Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationEquiv_transport_apply
    (x :
      FiniteNormQuotient rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :
    globalNormResidueAbelianizationEquiv K L
        (numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
          K L x) =
      numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv K L x
theorem

globalNormResidueAbelianizationEquiv_finiteNormClass

L198 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationEquiv_finiteNormClass
Documentation

The abelianized global norm-residue equivalence on a finite norm class.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · full declaration
theorem globalNormResidueAbelianizationEquiv_finiteNormClass
    (x : FiniteNormQuotient rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :
    letI := (numberFieldTowerReciprocityFiniteAbstractField K L).finite
    letI := numberFieldTowerExtensionSubgroup_normal K L
    letI := (numberFieldTowerFiniteGaloisSubextension K L).finite
    globalNormResidueAbelianizationEquiv K L
        (numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
          K L x) =
      numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization
        K L
        (rationalCyclotomicDegreeData.normResidueSymbol
          rationalIdeleClassRepresentation
          rationalCyclotomicIdeleClassValuationData
          rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
          (numberFieldTowerReciprocityFiniteAbstractField K L)
          (numberFieldTowerFiniteGaloisSubextension K L) x) := by
  exact (globalNormResidueAbelianizationEquiv_transport_apply K L x).trans
    (numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv_apply K L x)
theorem

globalNormResidueAbelianizationEquiv_finiteReciprocityHom

L224 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationEquiv_finiteReciprocityHom
Documentation

On the genuine finite-reciprocity class of an abstract extension automorphism, the finite-Galois norm-residue equivalence gives the class of the corresponding actual automorphism in the Galois abelianization.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · full declaration
theorem globalNormResidueAbelianizationEquiv_finiteReciprocityHom
    (q :
      ClassFormation.FiniteGaloisSubextension.extensionQuotient
        (numberFieldTowerFiniteGaloisSubextension K L)) :
    letI :=
      (numberFieldTowerReciprocityFiniteAbstractField K L).finite
    letI :=
      numberFieldTowerExtensionSubgroup_normal K L
    letI :=
      (numberFieldTowerFiniteGaloisSubextension K L).finite
    globalNormResidueAbelianizationEquiv K L
        (numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
          K L
          (rationalCyclotomicDegreeData.finiteReciprocityHom
            rationalIdeleClassRepresentation
            rationalCyclotomicIdeleClassValuationData
            (
          rationalCyclotomicIdeleClassValuationData.classFieldAxiom_implies_unramifiedUnitCohomology
                rationalIdeleClassRepresentation_satisfiesClassFieldAxiom)
            (numberFieldTowerReciprocityFiniteAbstractField K L)
            (numberFieldTowerFiniteGaloisSubextension K L).field
            (numberFieldTowerFiniteGaloisSubextension K L).below
            (hLnormal :=
              (numberFieldTowerFiniteGaloisSubextension K L).normal)
            (hLfinite :=
              (numberFieldTowerFiniteGaloisSubextension K L).finite)
            (Additive.ofMul q))) =
      Additive.ofMul
        (Abelianization.of
          (numberFieldTowerExtensionQuotientEquivGaloisGroup K L q)) := by
  let hBaseFinite :=
    (numberFieldTowerReciprocityFiniteAbstractField K L).finite
  let hExtensionNormal :=
    numberFieldTowerExtensionSubgroup_normal K L
  let hRelativeFinite :=
    (numberFieldTowerFiniteGaloisSubextension K L).finite
  let x :=
    rationalCyclotomicDegreeData.finiteReciprocityHom
      rationalIdeleClassRepresentation
      rationalCyclotomicIdeleClassValuationData
      (rationalCyclotomicIdeleClassValuationData.classFieldAxiom_implies_unramifiedUnitCohomology
        rationalIdeleClassRepresentation_satisfiesClassFieldAxiom)
      (numberFieldTowerReciprocityFiniteAbstractField K L)
      (numberFieldTowerFiniteGaloisSubextension K L).field
      (numberFieldTowerFiniteGaloisSubextension K L).below
      (hLnormal :=
        (numberFieldTowerFiniteGaloisSubextension K L).normal)
      (hLfinite :=
        (numberFieldTowerFiniteGaloisSubextension K L).finite)
      (Additive.ofMul q)
  have hxNorm :
      rationalCyclotomicDegreeData.normResidueSymbol
          rationalIdeleClassRepresentation
          rationalCyclotomicIdeleClassValuationData
          rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
          (numberFieldTowerReciprocityFiniteAbstractField K L)
          (numberFieldTowerFiniteGaloisSubextension K L) x =
        Additive.ofMul (Abelianization.of q) :=
    rationalCyclotomicDegreeData.normResidueSymbol_finiteReciprocityHom
      rationalIdeleClassRepresentation
      rationalCyclotomicIdeleClassValuationData
      rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
      (numberFieldTowerReciprocityFiniteAbstractField K L)
      (numberFieldTowerFiniteGaloisSubextension K L) q
  exact
    (globalNormResidueAbelianizationEquiv_transport_apply K L x).trans
      ((numberFieldTowerAbstractNormResidueGaloisAbelianizationEquiv_apply
          K L x).trans
        ((congrArg
            (numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization
              K L)
            hxNorm).trans
          (numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization_of
            K L q)))
def

globalReciprocityAbelianizationEquiv

L301 ↗
GlobalClassFieldTheory.Reciprocity.globalReciprocityAbelianizationEquiv
Documentation

The inverse global reciprocity equivalence for an arbitrary finite Galois extension.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def globalReciprocityAbelianizationEquiv :
    Additive (Abelianization (Gal(L / K))) ≃+
      Additive
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range)
def

globalNormResidueAbelianizationMonoidHom

L310 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom
Documentation

The genuine global norm-residue homomorphism with target the abelianization of the actual Galois group.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def globalNormResidueAbelianizationMonoidHom :
    IdeleClassGroup K →*
      Abelianization (Gal(L / K))
theorem

globalNormResidueAbelianizationMonoidHom_apply

L327 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_apply
Documentation

Evaluation of the finite-Galois global norm-residue homomorphism is the global equivalence applied to the genuine norm quotient class.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationMonoidHom_apply
    (c : IdeleClassGroup K) :
    globalNormResidueAbelianizationMonoidHom K L c =
      Additive.toMul
        (globalNormResidueAbelianizationEquiv K L
          (Additive.ofMul
            (QuotientGroup.mk'
              (_root_.ideleClassNorm K L).range c)))
theorem

globalNormResidueAbelianizationMonoidHom_finiteNormClass

L338 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_finiteNormClass
Documentation

Evaluate the finite-Galois symbol on the norm class of an idèle class.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · full declaration
theorem globalNormResidueAbelianizationMonoidHom_finiteNormClass
    (c : IdeleClassGroup K) :
    letI := (numberFieldTowerReciprocityFiniteAbstractField K L).finite
    letI := numberFieldTowerExtensionSubgroup_normal K L
    letI := (numberFieldTowerFiniteGaloisSubextension K L).finite
    globalNormResidueAbelianizationMonoidHom K L c =
      Additive.toMul
        (numberFieldTowerAbelianizedExtensionQuotientEquivGaloisAbelianization
          K L
          (rationalCyclotomicDegreeData.normResidueSymbol
            rationalIdeleClassRepresentation
            rationalCyclotomicIdeleClassValuationData
            rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
            (numberFieldTowerReciprocityFiniteAbstractField K L)
            (numberFieldTowerFiniteGaloisSubextension K L)
            (finiteNormClass rationalIdeleClassRepresentation
              (numberFieldTowerBaseSubgroup K L)
              (numberFieldTowerTopSubgroup L)
              (numberFieldTowerTopSubgroup_le_baseSubgroup K L)
              (numberFieldTowerIdeleClassEquivAmbientFixed K L
                (Additive.ofMul c))))) := by
  let x : FiniteNormQuotient rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L) :=
    finiteNormClass rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)
      (numberFieldTowerIdeleClassEquivAmbientFixed K L (Additive.ofMul c))
  have hclass :=
    numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient_ideleClass
      K L c
  calc
    _ = Additive.toMul
        (globalNormResidueAbelianizationEquiv K L
          (Additive.ofMul
            (QuotientGroup.mk' (_root_.ideleClassNorm K L).range c))) :=
      globalNormResidueAbelianizationMonoidHom_apply K L c
    _ = Additive.toMul
        (globalNormResidueAbelianizationEquiv K L
          (numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
            K L x)) :=
      congrArg (fun q => Additive.toMul
        (globalNormResidueAbelianizationEquiv K L q)) hclass.symm
    _ = _ := congrArg Additive.toMul
      (globalNormResidueAbelianizationEquiv_finiteNormClass K L x)
theorem

globalNormResidueAbelianizationMonoidHom_eq_one_iff

L389 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_eq_one_iff
Documentation

An idele class has trivial finite-Galois norm-residue symbol exactly when it is an actual idele-class norm from L.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationMonoidHom_eq_one_iff
    (c : IdeleClassGroup K) :
    globalNormResidueAbelianizationMonoidHom K L c = 1 ↔
      c ∈ (_root_.ideleClassNorm K L).range
theorem

globalNormResidueAbelianizationMonoidHom_surjective

L423 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_surjective
Documentation

The finite-Galois global norm-residue homomorphism is surjective onto the actual Galois abelianization.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationMonoidHom_surjective :
    Function.Surjective
      (globalNormResidueAbelianizationMonoidHom K L)
def

globalNormResidueAbelianizationIdeleMonoidHom

L453 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationIdeleMonoidHom
Documentation

The finite-Galois global norm-residue symbol viewed on the idele group.

This is the genuine idele-class symbol pulled back along I_K → C_K; in particular it is not a separately chosen map.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def globalNormResidueAbelianizationIdeleMonoidHom :
    IdeleGroup K →*
      Abelianization (Gal(L / K))
theorem

globalNormResidueAbelianizationIdeleMonoidHom_apply

L463 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationIdeleMonoidHom_apply
Documentation

Evaluation of the finite-Galois norm-residue symbol on an idele is evaluation of the class symbol on its genuine idele class.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationIdeleMonoidHom_apply
    (a : IdeleGroup K) :
    globalNormResidueAbelianizationIdeleMonoidHom K L a =
      globalNormResidueAbelianizationMonoidHom K L
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a)
theorem

globalNormResidueAbelianizationIdeleMonoidHom_principalIdele

L474 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationIdeleMonoidHom_principalIdele
Documentation

The finite-Galois norm-residue symbol on ideles is trivial on every principal idele.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationIdeleMonoidHom_principalIdele
    (x : Kˣ) :
    globalNormResidueAbelianizationIdeleMonoidHom K L
        (IdeleGroup.principalIdele K x) =
      1
theorem

globalNormResidueAbelianizationIdeleMonoidHom_surjective

L503 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationIdeleMonoidHom_surjective
Documentation

The finite-Galois norm-residue symbol remains surjective when viewed on ideles.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationIdeleMonoidHom_surjective :
    Function.Surjective
      (globalNormResidueAbelianizationIdeleMonoidHom K L)
theorem

globalNormResidueAbelianizationIdeleMonoidHom_eq_one_iff

L513 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationIdeleMonoidHom_eq_one_iff
Documentation

An idele has trivial finite-Galois norm-residue symbol exactly when its idele class is an actual norm from L.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationIdeleMonoidHom_eq_one_iff
    (a : IdeleGroup K) :
    globalNormResidueAbelianizationIdeleMonoidHom K L a = 1 ↔
      QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K) a ∈
        (_root_.ideleClassNorm K L).range
theorem

globalNormResidueAbelianizationIdeleMonoidHom_ker

L528 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationIdeleMonoidHom_ker
Documentation

The kernel of the idele-level finite-Galois norm-residue symbol is the full inverse image of the genuine idele-class norm range.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationIdeleMonoidHom_ker :
    (globalNormResidueAbelianizationIdeleMonoidHom K L).ker =
      (_root_.ideleClassNorm K L).range.comap
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup K))
theorem

globalNormResidueAbelianizationMonoidHom_ker

L546 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_ker
Documentation

The kernel of the finite-Galois norm-residue homomorphism is exactly the range of the ordinary idele-class norm.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem globalNormResidueAbelianizationMonoidHom_ker :
    (globalNormResidueAbelianizationMonoidHom K L).ker =
      (_root_.ideleClassNorm K L).range
theorem

ideleClassNorm_index_eq_galoisAbelianization_card

L559 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassNorm_index_eq_galoisAbelianization_card
Documentation

The index of the actual norm subgroup is the order of the abelianization of the genuine finite Galois group.

Source context 9 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem ideleClassNorm_index_eq_galoisAbelianization_card :
    (_root_.ideleClassNorm K L).range.index =
      Nat.card (Abelianization (Gal(L / K)))
theorem

globalNormResidueAbelianizationEquiv_abelianSpecialization_apply

L593 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationEquiv_abelianSpecialization_apply
Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section AbelianSpecialization
variable
    (F E : Type) [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
Lean source · statement
theorem
    globalNormResidueAbelianizationEquiv_abelianSpecialization_apply
    (q :
      Additive
        (IdeleClassGroup F ⧸
          (_root_.ideleClassNorm F E).range)) :
    MulEquiv.toAdditive
          (Abelianization.equivOfComm :
            Gal(E / F) ≃*
              Abelianization (Gal(E / F))).symm
        (globalNormResidueAbelianizationEquiv F E q) =
      globalNormResidueEquiv F E q
theorem

globalNormResidueAbelianizationEquiv_abelianSpecialization

L664 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationEquiv_abelianSpecialization
Documentation

For an abelian extension, composing the finite-Galois equivalence with the canonical equivalence from the Galois abelianization recovers the usual global norm-residue equivalence.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section AbelianSpecialization
variable
    (F E : Type) [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
Lean source · statement
theorem globalNormResidueAbelianizationEquiv_abelianSpecialization :
    (globalNormResidueAbelianizationEquiv F E).trans
        (MulEquiv.toAdditive
          (Abelianization.equivOfComm :
            Gal(E / F) ≃*
              Abelianization (Gal(E / F))).symm) =
      globalNormResidueEquiv F E
theorem

globalReciprocityAbelianizationEquiv_abelianSpecialization

L680 ↗
GlobalClassFieldTheory.Reciprocity.globalReciprocityAbelianizationEquiv_abelianSpecialization
Documentation

In the canonical direction used by the global reciprocity isomorphism, the finite-Galois construction likewise specializes to the ordinary abelian reciprocity equivalence.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section AbelianSpecialization
variable
    (F E : Type) [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
Lean source · statement
theorem globalReciprocityAbelianizationEquiv_abelianSpecialization :
    (MulEquiv.toAdditive
        (Abelianization.equivOfComm :
          Gal(E / F) ≃*
            Abelianization (Gal(E / F)))).trans
      (globalReciprocityAbelianizationEquiv F E) =
        globalReciprocityEquiv F E
theorem

globalNormResidueAbelianizationMonoidHom_abelianSpecialization_apply

L698 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_abelianSpecialization_apply
Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section AbelianSpecialization
variable
    (F E : Type) [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
Lean source · statement
theorem
    globalNormResidueAbelianizationMonoidHom_abelianSpecialization_apply
    (c : IdeleClassGroup F) :
    (Abelianization.equivOfComm :
        Gal(E / F) ≃*
          Abelianization (Gal(E / F))).symm
        (globalNormResidueAbelianizationMonoidHom F E c) =
      globalNormResidueMonoidHom F E c
theorem

globalNormResidueAbelianizationMonoidHom_abelianSpecialization

L723 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_abelianSpecialization
Documentation

The finite-Galois norm-residue homomorphism specializes to the ordinary abelian global Artin homomorphism after the canonical target identification.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section AbelianSpecialization
variable
    (F E : Type) [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
Lean source · statement
theorem
    globalNormResidueAbelianizationMonoidHom_abelianSpecialization :
    (Abelianization.equivOfComm :
        Gal(E / F) ≃*
          Abelianization (Gal(E / F))).symm.toMonoidHom.comp
        (globalNormResidueAbelianizationMonoidHom F E) =
      globalNormResidueMonoidHom F E
theorem

globalNormResidueAbelianizationIdeleMonoidHom_abelianSpecialization

L739 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationIdeleMonoidHom_abelianSpecialization
Documentation

The idele-level finite-Galois symbol has the same abelian specialization, after pulling both class symbols back along I_F → C_F.

Source context 11 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open ClassFormation
open KummerTheory
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Idèle classes are commutative.  Keeping the mixin as a named local
instance lets norm-range quotient types elaborate before entering a
declaration body. -/
local instance
    globalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
section AbelianSpecialization
variable
    (F E : Type) [Field F] [NumberField F]
    [Field E] [NumberField E] [Algebra F E]
    [FiniteDimensional F E] [IsAbelianGalois F E]
Lean source · statement
theorem
    globalNormResidueAbelianizationIdeleMonoidHom_abelianSpecialization :
    (Abelianization.equivOfComm :
        Gal(E / F) ≃*
          Abelianization (Gal(E / F))).symm.toMonoidHom.comp
        (globalNormResidueAbelianizationIdeleMonoidHom F E) =
      (globalNormResidueMonoidHom F E).comp
        (QuotientGroup.mk'
          (IdeleGroup.principalSubgroup F))

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