Module

MaximalAbelianKernel.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.MaximalAbelianKernel

5 declarations indexed from sourceView source ↗

Module documentation

The kernel of maximal abelian global reciprocity

This module identifies the kernel of the maximal abelian global Artin map with the identity component of the idele class group. It then descends the map to the component quotient.

The separation argument is intrinsic to the compact totally disconnected component quotient. A separating open normal subgroup is pulled back to a closed finite-index idele-class subgroup, whose selected finite class field supplies the detecting finite Galois coordinate.

Imports4

Imported by5

theorem

exists_closedFiniteIndexSubgroup_not_mem_of_not_mem_identityComponent

L40 ↗

GlobalClassFieldTheory.Reciprocity.exists_closedFiniteIndexSubgroup_not_mem_of_not_mem_identityComponent

Documentation

A class outside the identity component is excluded by a closed finite-index subgroup which contains the identity component.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem exists_closedFiniteIndexSubgroup_not_mem_of_not_mem_identityComponent
    (c : IdeleClassGroup K)
    (hc : c ∉ ideleClassIdentityComponent K) :
    ∃ H : Subgroup (IdeleClassGroup K),
      IsClosed (H : Set (IdeleClassGroup K)) ∧
        H.FiniteIndex ∧
          ideleClassIdentityComponent K ≤ H ∧ c ∉ H

theorem

finiteAbelianExtensionInMaximalAbelianExtension_ideleClassNorm_range

L96 ↗

GlobalClassFieldTheory.Reciprocity.finiteAbelianExtensionInMaximalAbelianExtension_ideleClassNorm_range

Documentation

Replacing a finite abelian extension by its selected finite layer in the maximal abelian extension preserves its idele-class norm range.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · full declaration

theorem finiteAbelianExtensionInMaximalAbelianExtension_ideleClassNorm_range
    (L : Type) [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    let E := finiteAbelianExtensionInMaximalAbelianExtension K L
    letI : NumberField E := NumberField.of_module_finite K E
    (_root_.ideleClassNorm K E).range =
      (_root_.ideleClassNorm K L).range := by
  let E := finiteAbelianExtensionInMaximalAbelianExtension K L
  let e : L ≃ₐ[K] E :=
    finiteAbelianExtensionEquivInMaximalAbelianExtension K L
  let hE : NumberField E := NumberField.of_module_finite K E
  let : NumberField E := hE
  have htransport :=
    ordinaryIdeleClassNorm_range_map_congrOfAlgEquiv
      (K := K) (K' := K) (L := L) (L' := E)
      (AlgEquiv.refl : K ≃ₐ[ℚ] K)
      (e.restrictScalars ℚ)
      (fun x => e.commutes x)
  calc
    (_root_.ideleClassNorm K E).range =
        (_root_.ideleClassNorm K L).range.map
          (ideleClassCongr
            (AlgEquiv.refl : K ≃ₐ[ℚ] K)).toMonoidHom :=
      htransport.symm
    _ = (_root_.ideleClassNorm K L).range := by
      ext c
      constructor
      · rintro ⟨d, hd, rfl⟩
        simpa using hd
      · intro hc
        exact ⟨c, hc, by simp⟩

theorem

maximalAbelianGlobalArtin_ker

L131 ↗

GlobalClassFieldTheory.Reciprocity.maximalAbelianGlobalArtin_ker

Documentation

The kernel of the maximal abelian global Artin map is exactly the identity component of the idele class group.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem maximalAbelianGlobalArtin_ker :
    (maximalAbelianGlobalArtin K).ker =
      ideleClassIdentityComponent K

def

ideleClassComponentQuotientEquivMaximalAbelianGalois

L192 ↗

GlobalClassFieldTheory.Reciprocity.ideleClassComponentQuotientEquivMaximalAbelianGalois

Documentation

Maximal abelian reciprocity identifies the component quotient of the idele class group with the maximal abelian Galois group.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

def ideleClassComponentQuotientEquivMaximalAbelianGalois :
    ideleClassComponentQuotient K ≃ₜ*
      Gal(maximalAbelianExtension K / K)

theorem

ideleClassComponentQuotientEquivMaximalAbelianGalois_mk

L222 ↗

GlobalClassFieldTheory.Reciprocity.ideleClassComponentQuotientEquivMaximalAbelianGalois_mk

Documentation

Evaluation of component-quotient reciprocity on an idele class is the maximal abelian global Artin map.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem ideleClassComponentQuotientEquivMaximalAbelianGalois_mk
    (c : IdeleClassGroup K) :
    ideleClassComponentQuotientEquivMaximalAbelianGalois K
        (QuotientGroup.mk'
          (ideleClassIdentityComponent K) c) =
      maximalAbelianGlobalArtin K c

Module documentation

The kernel of maximal abelian global reciprocity

Declarations

exists_closedFiniteIndexSubgroup_not_mem_of_not_mem_identityComponent

finiteAbelianExtensionInMaximalAbelianExtension_ideleClassNorm_range

maximalAbelianGlobalArtin_ker

ideleClassComponentQuotientEquivMaximalAbelianGalois

ideleClassComponentQuotientEquivMaximalAbelianGalois_mk