NYLL
Module

BigHilbertClassFieldMathlibArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassFieldMathlibArtin
7 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Artin reciprocity for any big Hilbert class field

The maximal finite-prime-unramified abelian extension has the same idèle-class norm subgroup as the selected big Hilbert class field. Arithmetic global reciprocity therefore gives its narrow-class-group Artin isomorphism.

Imports7
Imported by2

Declarations

instance

bigHilbertArtinIdeleClassGroupIsMulCommutative

L32 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertArtinIdeleClassGroupIsMulCommutative
Source context 5 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
instance bigHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)
def

bigHilbertClassFieldEquivOfIsBig

L38 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassFieldEquivOfIsBig
Documentation

An intrinsic big Hilbert class field is equivalent over K to the selected realization.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance bigHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def bigHilbertClassFieldEquivOfIsBig
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E) :
    E ≃ₐ[K] GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField K
theorem

bigHilbertClassField_ideleClassNorm_range_of_isBig

L57 ↗
ClassFieldTheory.GlobalClassFieldComparison.bigHilbertClassField_ideleClassNorm_range_of_isBig
Documentation

Every intrinsic big Hilbert class field has the selected field's idèle-class norm subgroup.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance bigHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigHilbertClassField_ideleClassNorm_range_of_isBig
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E) :
    (_root_.ideleClassNorm K E).range =
      GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup
        (K := K)
def

arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_of_isBig

L80 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_of_isBig
Documentation

The arithmetic Artin isomorphism for an intrinsic big Hilbert class field, with target the narrow ideal class group.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance bigHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_of_isBig
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E) :
    (E ≃ₐ[K] E) ≃* RayClass.NarrowClassGroup K
theorem

arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_globalNormResidue

L104 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_globalNormResidue
Documentation

The intrinsic arithmetic reciprocity equivalence sends a global norm-residue symbol to the represented big-Hilbert norm class.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance bigHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_globalNormResidue
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E)
    (c : IdeleClassGroup K) :
    arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_of_isBig E hE
      (GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom
        K E c) =
      GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)
        (QuotientGroup.mk'
          (GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup
            (K := K)) c)
theorem

arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_prime

L145 ↗
ClassFieldTheory.GlobalClassFieldComparison.arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_prime
Documentation

The intrinsic arithmetic Artin symbol of a finite prime is represented by its one-place prime idèle in the narrow class group.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance bigHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_prime
    (E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E)
    (v : HeightOneSpectrum (𝓞 K)) :
    arithmeticBigHilbertClassFieldGaloisEquivNarrowClassGroup_of_isBig E hE
      (GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := E) v) =
      QuotientGroup.mk' (RayClass.narrowDenominator (K := K))
        (IdeleGroup.finitePrimeIdele v)
theorem

narrowRayClassGroupEquivNarrowClassGroup_prime

L174 ↗
ClassFieldTheory.GlobalClassFieldComparison.narrowRayClassGroupEquivNarrowClassGroup_prime
Documentation

The public narrow ideal ray class of a finite prime is its normalized one-place prime idèle class.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance bigHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem narrowRayClassGroupEquivNarrowClassGroup_prime
    (v : HeightOneSpectrum (𝓞 K)) :
    narrowRayClassGroupEquivNarrowClassGroup K
      (narrowRayClassOfFinitePrime v) =
      QuotientGroup.mk' (RayClass.narrowDenominator (K := K))
        (IdeleGroup.finitePrimeIdele v)

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