NYLL
Module

GlobalNormResidue.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalNormResidue
19 declarations indexed from sourceView source ↗

Module documentation

The global norm-residue symbol

For a finite abelian Galois extension L / K, the rational absolute idele-class formation realizes the abstract finite norm quotient as the actual quotient

C_K / N_{L/K} C_L.

The concrete cyclotomic valuation supplies the valuation data required by abstract reciprocity. Composing the inverse of the fixed-field comparison, the abstract norm-residue symbol, and the compatible Galois-group comparison gives the actual equivalence

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

The homomorphism on C_K is obtained from the genuine quotient map. Consequently it is surjective and its kernel is exactly the range of the actual ordinary idele-class norm.

Imports5
Imported by12

Declarations

def

globalNormResidueIdeleClassCommGroup

L49 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueIdeleClassCommGroup
Documentation

Fix the canonical class-group dictionary before forming norm quotients.

Source context 7 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
Lean source · statement
def globalNormResidueIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)
theorem

globalNormResidueIdeleClassIsMulCommutative

L56 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueIdeleClassIsMulCommutative
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
attribute [local instance] globalNormResidueIdeleClassCommGroup
Lean source · statement
theorem globalNormResidueIdeleClassIsMulCommutative
    (F : Type) [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
abbrev

numberFieldTowerReciprocityFiniteAbstractField

L71 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerReciprocityFiniteAbstractField
Documentation

A reducible presentation of the compatible finite abstract field. Its field projection is definitionally the concrete tower subgroup, so dependent norm-quotient types do not require opaque unfolding.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · full declaration
abbrev numberFieldTowerReciprocityFiniteAbstractField :
    FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ) where
  field := numberFieldTowerBaseSubgroup K L
  finite := numberFieldTowerBaseSubgroupAbsoluteQuotientFinite K L
def

numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup

L79 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup
Documentation

The abelianization of the compatible abstract extension quotient is the actual abelian Galois group of L / K.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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
    numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup :
    Additive
        (Abelianization
          (ClassFormation.FiniteGaloisSubextension.extensionQuotient
            (numberFieldTowerFiniteGaloisSubextension K L))) ≃+
      Additive (Gal(L / K))
theorem

numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup_of

L98 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup_of
Documentation

The compatible abelianized extension-quotient comparison sends the class of an abstract automorphism to the corresponding actual automorphism of L / K.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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
    numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup_of
    (q :
      ClassFormation.FiniteGaloisSubextension.extensionQuotient
        (numberFieldTowerFiniteGaloisSubextension K L)) :
    numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup K L
        (Additive.ofMul (Abelianization.of q)) =
      Additive.ofMul
        (numberFieldTowerExtensionQuotientEquivGaloisGroup K L q)
def

numberFieldTowerAbstractNormResidueGaloisEquiv

L126 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractNormResidueGaloisEquiv
Documentation

The abstract norm-residue map followed by the compatible actual Galois-group comparison. Keeping this composition behind a typed boundary prevents the finite norm quotient from being reconstructed while composing with the concrete quotient comparison.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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
    numberFieldTowerAbstractNormResidueGaloisEquiv :
    FiniteNormQuotient rationalIdeleClassRepresentation
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L) ≃+
      Additive (Gal(L / K))
theorem

numberFieldTowerAbstractNormResidueGaloisEquiv_apply

L163 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerAbstractNormResidueGaloisEquiv_apply
Documentation

Evaluation of the typed abstract norm-residue/Galois comparison.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 numberFieldTowerAbstractNormResidueGaloisEquiv_apply
    (x : FiniteNormQuotient rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :
    numberFieldTowerAbstractNormResidueGaloisEquiv K L x =
      numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup K L
        (rationalCyclotomicDegreeData.normResidueSymbol
          rationalIdeleClassRepresentation
          rationalCyclotomicIdeleClassValuationData
          rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
          (numberFieldTowerReciprocityFiniteAbstractField K L)
          (numberFieldTowerFiniteGaloisSubextension K L) x)
def

globalNormResidueEquiv

L185 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueEquiv
Documentation

The actual global norm-residue equivalence

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

Its three factors are respectively the actual fixed-field norm comparison, the abstract norm-residue symbol built from the concrete cyclotomic valuation, and the compatible Galois-group comparison.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueEquiv :
    Additive
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) ≃+
      Additive (Gal(L / K))
theorem

globalNormResidueEquiv_transport_apply

L197 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueEquiv_transport_apply
Documentation

Evaluation after transporting an abstract finite norm class to the ordinary idele-class norm quotient.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueEquiv_transport_apply
    (x : FiniteNormQuotient rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :
    globalNormResidueEquiv K L
        (numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
          K L x) =
      numberFieldTowerAbstractNormResidueGaloisEquiv K L x
theorem

globalNormResidueEquiv_finiteNormClass

L211 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueEquiv_finiteNormClass
Documentation

The global norm-residue equivalence on a finite abstract norm class, after transport to the ordinary idele-class norm quotient.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueEquiv_finiteNormClass
    (x : FiniteNormQuotient rationalIdeleClassRepresentation
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :
    globalNormResidueEquiv K L
        (numberFieldTowerFiniteNormQuotientEquivIdeleClassNormQuotient
          K L x) =
      numberFieldTowerAbelianizedExtensionQuotientEquivGaloisGroup K L
        (rationalCyclotomicDegreeData.normResidueSymbol
          rationalIdeleClassRepresentation
          rationalCyclotomicIdeleClassValuationData
          rationalIdeleClassRepresentation_satisfiesClassFieldAxiom
          (numberFieldTowerReciprocityFiniteAbstractField K L)
          (numberFieldTowerFiniteGaloisSubextension K L) x)
theorem

globalNormResidueEquiv_finiteReciprocityHom

L233 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueEquiv_finiteReciprocityHom
Documentation

On the genuine finite-reciprocity class of an abstract extension automorphism, the global norm-residue equivalence is the corresponding actual automorphism of L / K.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueEquiv_finiteReciprocityHom
    (q :
      ClassFormation.FiniteGaloisSubextension.extensionQuotient
        (numberFieldTowerFiniteGaloisSubextension K L)) :
    globalNormResidueEquiv 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
        (numberFieldTowerExtensionQuotientEquivGaloisGroup K L q)
def

globalReciprocityEquiv

L309 ↗
GlobalClassFieldTheory.Reciprocity.globalReciprocityEquiv
Documentation

The inverse global reciprocity equivalence

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

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalReciprocityEquiv :
    Additive (Gal(L / K)) ≃+
      Additive
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range)
def

globalNormResidueMonoidHom

L319 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom
Documentation

The actual global norm-residue homomorphism on the idele class group, obtained by composing the genuine quotient map with the global norm-residue equivalence.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueMonoidHom :
    IdeleClassGroup K →* Gal(L / K)
theorem

globalNormResidueMonoidHom_apply

L335 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_apply
Documentation

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

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueMonoidHom_apply
    (c : IdeleClassGroup K) :
    globalNormResidueMonoidHom K L c =
      Additive.toMul
        (globalNormResidueEquiv K L
          (Additive.ofMul
            (QuotientGroup.mk'
          (_root_.ideleClassNorm K L).range c)))
theorem

globalNormResidueMonoidHom_eq_maximalUnramifiedRestriction

L349 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_eq_maximalUnramifiedRestriction
Documentation

For a finite extension whose compatible abstract realization is unramified for the cyclotomic degree datum, the actual global norm-residue symbol is the finite restriction of the maximal-unramified valuation symbol.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueMonoidHom_eq_maximalUnramifiedRestriction
    (hUnramified :
      (numberFieldTowerFiniteGaloisSubextension K L).IsUnramified
        rationalCyclotomicDegreeData)
    (c : IdeleClassGroup K) :
    globalNormResidueMonoidHom K L c =
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
        (DegreeData.finiteUnramifiedRestriction
          rationalCyclotomicDegreeData
          (ClassFormation.FiniteAbstractField.toFiniteResidueAbstractField
            (numberFieldTowerReciprocityFiniteAbstractField K L)
            rationalCyclotomicDegreeData)
          (numberFieldTowerFiniteGaloisSubextension K L)
          hUnramified
          (ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol
            rationalCyclotomicIdeleClassValuationData
            (numberFieldTowerReciprocityFiniteAbstractField K L)
            (numberFieldTowerIdeleClassEquivAmbientFixed K L
              (Additive.ofMul c))).toMul)
theorem

globalNormResidueMonoidHom_eq_one_iff

L430 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_eq_one_iff
Documentation

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

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueMonoidHom_eq_one_iff
    (c : IdeleClassGroup K) :
    globalNormResidueMonoidHom K L c = 1 ↔
      c ∈ (_root_.ideleClassNorm K L).range
theorem

globalNormResidueMonoidHom_surjective

L466 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_surjective
Documentation

The actual global norm-residue homomorphism is surjective.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueMonoidHom_surjective :
    Function.Surjective
      (globalNormResidueMonoidHom K L)
theorem

ideleClassNorm_index_eq_finrank_abelian

L483 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassNorm_index_eq_finrank_abelian
Documentation

The index of the actual idele-class norm subgroup of a finite abelian extension is its field degree.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 ideleClassNorm_index_eq_finrank_abelian :
    (_root_.ideleClassNorm K L).range.index =
      Module.finrank K L
theorem

globalNormResidueMonoidHom_ker

L506 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHom_ker
Documentation

The kernel of the actual global norm-residue homomorphism is exactly the range of the ordinary idele-class norm.

Source context 10 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
attribute [local instance] globalNormResidueIdeleClassCommGroup
attribute [local instance] globalNormResidueIdeleClassIsMulCommutative
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 globalNormResidueMonoidHom_ker :
    (globalNormResidueMonoidHom K L).ker =
      (_root_.ideleClassNorm K L).range

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