NYLL
Module

TopologicalGlobalNormResidueAbelianization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.TopologicalGlobalNormResidueAbelianization
14 declarations indexed from sourceView source ↗

Module documentation

Topological global reciprocity for finite Galois extensions

For a finite Galois extension L / K, global norm-residue reciprocity identifies the native idele-class norm quotient with the abelianization of the finite Krull Galois group. This file records the identification as a ContinuousMulEquiv in both mathematical directions:

  • norm-residue: C_K / N_{L/K}(C_L) ≃ₜ* Gal(L / K)ᵃᵇ;
  • reciprocity: Gal(L / K)ᵃᵇ ≃ₜ* C_K / N_{L/K}(C_L).

The evaluation lemmas below ensure that these are the already constructed actual global symbols, rather than unrelated abstract isomorphisms between finite groups.

Imports4
Imported by3

Declarations

instance

topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative

L44 ↗
GlobalClassFieldTheory.Reciprocity.topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative
Documentation

Keep quotient normality out of every exported declaration type.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)
instance

topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology

L51 ↗
GlobalClassFieldTheory.Reciprocity.topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology
Documentation

Abelianization is an opaque quotient alias, so install its native quotient topology explicitly before asking for topological properties.

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K)))
theorem

ideleClassNormAbelianizationQuotient_discreteTopology

L62 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassNormAbelianizationQuotient_discreteTopology
Documentation

The native topology on the actual idele-class norm quotient is discrete. The openness used here is the genuine ordinary norm-range theorem for the given finite Galois extension.

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
theorem ideleClassNormAbelianizationQuotient_discreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
theorem

finiteGaloisAbelianization_discreteTopology

L74 ↗
GlobalClassFieldTheory.Reciprocity.finiteGaloisAbelianization_discreteTopology
Documentation

The abelianization of a finite Krull Galois group carries the discrete quotient topology.

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
omit [NumberField K] [NumberField L] [IsGalois K L] in
Lean source · statement
theorem finiteGaloisAbelianization_discreteTopology :
    DiscreteTopology
      (Abelianization (Gal(L / K)))
instance

topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology

L84 ↗
GlobalClassFieldTheory.Reciprocity.topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology
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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
Lean source · statement
instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
instance

topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology

L91 ↗
GlobalClassFieldTheory.Reciprocity.topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology
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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
Lean source · statement
instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K)))
def

globalNormResidueAbelianizationContinuousMulEquiv

L100 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationContinuousMulEquiv
Documentation

The full finite-Galois norm-residue isomorphism with its native topologies:

C_K / N_{L/K}(C_L) ≃ₜ* Gal(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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
def globalNormResidueAbelianizationContinuousMulEquiv :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃ₜ*
      Abelianization (Gal(L / K))
theorem

globalNormResidueAbelianizationContinuousMulEquiv_apply

L119 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationContinuousMulEquiv_apply
Documentation

Evaluation of the topological finite-Galois norm-residue equivalence is the previously constructed actual 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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
theorem globalNormResidueAbelianizationContinuousMulEquiv_apply
    (c :
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :
    globalNormResidueAbelianizationContinuousMulEquiv K L c =
      Additive.toMul
        (globalNormResidueAbelianizationEquiv K L
          (Additive.ofMul c))
def

globalReciprocityAbelianizationContinuousMulEquiv

L133 ↗
GlobalClassFieldTheory.Reciprocity.globalReciprocityAbelianizationContinuousMulEquiv
Documentation

Global reciprocity for a finite Galois extension in the direction used by the class-field correspondence:

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
def globalReciprocityAbelianizationContinuousMulEquiv :
    Abelianization (Gal(L / K)) ≃ₜ*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
theorem

globalReciprocityAbelianizationContinuousMulEquiv_apply

L142 ↗
GlobalClassFieldTheory.Reciprocity.globalReciprocityAbelianizationContinuousMulEquiv_apply
Documentation

Evaluation in the reciprocity direction is exactly the inverse actual finite-Galois norm-residue map.

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
theorem globalReciprocityAbelianizationContinuousMulEquiv_apply
    (σ : Abelianization (Gal(L/K))) :
    globalReciprocityAbelianizationContinuousMulEquiv K L σ =
      Additive.toMul
        ((globalNormResidueAbelianizationEquiv K L).symm
          (Additive.ofMul σ))
def

ideleClassNormAbelianizationQuotientContinuousMonoidHom

L152 ↗
GlobalClassFieldTheory.Reciprocity.ideleClassNormAbelianizationQuotientContinuousMonoidHom
Documentation

The native quotient projection C_K → C_K / N_{L/K}(C_L) as a continuous homomorphism.

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
def
    ideleClassNormAbelianizationQuotientContinuousMonoidHom :
    IdeleClassGroup K →ₜ*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)
def

globalNormResidueAbelianizationContinuousMonoidHom

L164 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationContinuousMonoidHom
Documentation

The global norm-residue symbol C_K → Gal(L / K)ᵃᵇ as a continuous homomorphism in the natural idele-class and finite Krull quotient topologies.

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
def
    globalNormResidueAbelianizationContinuousMonoidHom :
    IdeleClassGroup K →ₜ*
      Abelianization (Gal(L / K))
theorem

globalNormResidueAbelianizationContinuousMonoidHom_apply

L175 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationContinuousMonoidHom_apply
Documentation

Forgetting continuity from the topological finite-Galois norm-residue map recovers the previously constructed actual 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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
theorem globalNormResidueAbelianizationContinuousMonoidHom_apply
    (c : IdeleClassGroup K) :
    globalNormResidueAbelianizationContinuousMonoidHom K L c =
      globalNormResidueAbelianizationMonoidHom K L c
theorem

globalNormResidueAbelianizationMonoidHom_continuous

L182 ↗
GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianizationMonoidHom_continuous
Documentation

The actual finite-Galois norm-residue symbol is continuous.

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
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep quotient normality out of every exported declaration type. -/
local instance
    topologicalGlobalNormResidueAbelianization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
/-- `Abelianization` is an opaque quotient alias, so install its native
quotient topology explicitly before asking for topological properties. -/
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationTopology :
    TopologicalSpace (Abelianization (Gal(L / K))) := by
  change
    TopologicalSpace
      (Gal(L / K) ⧸ commutator (Gal(L / K)))
  infer_instance
local instance
    topologicalGlobalNormResidueAbelianization_normQuotientDiscreteTopology :
    DiscreteTopology
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) :=
  ideleClassNormAbelianizationQuotient_discreteTopology K L
local instance
    topologicalGlobalNormResidueAbelianization_galoisAbelianizationDiscreteTopology :
    DiscreteTopology (Abelianization (Gal(L / K))) :=
  finiteGaloisAbelianization_discreteTopology K L
Lean source · statement
theorem globalNormResidueAbelianizationMonoidHom_continuous :
    Continuous
      (globalNormResidueAbelianizationMonoidHom K L)

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