Module

SmallHilbertClassFieldMathlibArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldMathlibArtin

6 declarations indexed from sourceView source ↗

Module documentation

Arithmetic Artin reciprocity for any small Hilbert class field

The intrinsic small Hilbert class field is unique up to a base-field equivalence. Therefore its actual idèle-class norm subgroup is the same as that of the selected class field. Arithmetic global reciprocity then gives the Artin map, with its prime normalization obtained from the prime idèle.

Imports8

Imported by2

instance

smallHilbertArtinIdeleClassGroupIsMulCommutative

L34 ↗

ClassFieldTheory.SmallHilbertClassFieldComparison.smallHilbertArtinIdeleClassGroupIsMulCommutative

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.SmallHilbertClassFieldComparison
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance smallHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)

theorem

smallHilbertClassField_ideleClassNorm_range_of_isSmall

L40 ↗

ClassFieldTheory.SmallHilbertClassFieldComparison.smallHilbertClassField_ideleClassNorm_range_of_isSmall

Documentation

All intrinsic small Hilbert class fields have the selected field's actual 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.SmallHilbertClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance smallHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem smallHilbertClassField_ideleClassNorm_range_of_isSmall
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E) :
    (_root_.ideleClassNorm K E).range =
      GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup
        (K := K)

def

arithmeticHilbertClassGroupEquivOfNormRange

L61 ↗

ClassFieldTheory.SmallHilbertClassFieldComparison.arithmeticHilbertClassGroupEquivOfNormRange

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.SmallHilbertClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance smallHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def arithmeticHilbertClassGroupEquivOfNormRange
    (E : FiniteAbelianExtension K)
    (hNorm : (_root_.ideleClassNorm K E).range =
      GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup
        (K := K)) :
    (E ≃ₐ[K] E) ≃* ClassGroup (𝓞 K)

def

arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_of_isSmall

L84 ↗

ClassFieldTheory.SmallHilbertClassFieldComparison.arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_of_isSmall

Documentation

Arithmetic reciprocity identifies the Galois group of any intrinsic small Hilbert class field with the ordinary 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.SmallHilbertClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance smallHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_of_isSmall
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E) :
    (E ≃ₐ[K] E) ≃* ClassGroup (𝓞 K)

theorem

arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_globalNormResidue

L92 ↗

ClassFieldTheory.SmallHilbertClassFieldComparison.arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_globalNormResidue

Documentation

Intrinsic arithmetic reciprocity sends a global norm-residue symbol to its represented class in the small-Hilbert norm quotient.

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.SmallHilbertClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance smallHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_globalNormResidue
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E)
    (c : IdeleClassGroup K) :
    arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_of_isSmall E hE
      (GlobalClassFieldTheory.Reciprocity.arithmeticGlobalNormResidueMonoidHom
        K E c) =
      GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientEquivClassGroup
        (K := K)
        (QuotientGroup.mk'
          (GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup
            (K := K)) c)

theorem

arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_prime

L133 ↗

ClassFieldTheory.SmallHilbertClassFieldComparison.arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_prime

Documentation

At every finite prime, the arithmetic Artin symbol has the usual prime ideal class under the intrinsic Hilbert reciprocity equivalence.

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.SmallHilbertClassFieldComparison
variable {K : Type} [Field K] [NumberField K]
local instance smallHilbertArtinIdeleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_prime
    (E : FiniteAbelianExtension K) (hE : IsSmallHilbertClassField E)
    (v : HeightOneSpectrum (𝓞 K)) :
    arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_of_isSmall E hE
      (GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := E) v) =
      ClassGroup.mk K (finitePrimeFractionalIdeal v)

Module documentation

Arithmetic Artin reciprocity for any small Hilbert class field

Declarations

smallHilbertArtinIdeleClassGroupIsMulCommutative

smallHilbertClassField_ideleClassNorm_range_of_isSmall

arithmeticHilbertClassGroupEquivOfNormRange

arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_of_isSmall

arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_globalNormResidue

arithmeticSmallHilbertClassFieldGaloisEquivClassGroup_prime