Module

PublicIdealArtinKernelComparison.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.PublicIdealArtinKernelComparison

4 declarations indexed from sourceView source ↗

Module documentation

Comparing the public and ideal-theoretic Artin kernels

The public finite ray-class Artin map is normalized on all primes away from its modulus. Frobenius rigidity identifies its kernel with the genuine idèle-class norm kernel. We then compare that kernel with the established ideal-theoretic Artin map on the same ray modulus.

Imports4

Imported by2

theorem

finiteAbelianReciprocity_primeArtin_eq_original

L28 ↗

ClassFieldTheory.GlobalClassFieldComparison.finiteAbelianReciprocity_primeArtin_eq_original

Source context 4 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison

Lean source · statement

theorem finiteAbelianReciprocity_primeArtin_eq_original
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (D : FiniteAbelianReciprocityData K L)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ D.modulus.finitePart.support) :
    D.artin (rayClassOfFinitePrime D.modulus v hv) =
      GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
        (K := K) (L := L) v

theorem

finiteAbelianReciprocity_originalPrimeNormalization

L55 ↗

ClassFieldTheory.GlobalClassFieldComparison.finiteAbelianReciprocity_originalPrimeNormalization

Source context 4 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison

Lean source · full declaration

theorem finiteAbelianReciprocity_originalPrimeNormalization
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (D : FiniteAbelianReciprocityData K L) :
    let m := rayClassModulusToOriginal K D.modulus
    let e := rayClassGroupEquivOriginalIdele K D.modulus
    let a : RayClass.RayClassGroup m →* (L ≃ₐ[K] L) :=
      D.artin.comp e.symm.toMonoidHom
    ∀ (v : HeightOneSpectrum (𝓞 K))
      (_hv : v ∉ m.finitePart.support),
      a (QuotientGroup.mk' m.congruenceSubgroup
        (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
          (IdeleGroup.finitePrimeIdele v))) =
        GlobalClassFieldTheory.GlobalClassFields.arithmeticFinitePlacePrimeArtin
          (K := K) (L := L) v := by
  intro m e a v hv
  have hvm : v ∉ D.modulus.finitePart.support := hv
  change D.artin (e.symm (QuotientGroup.mk' m.congruenceSubgroup
    (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
      (IdeleGroup.finitePrimeIdele v)))) = _
  rw [← rayClassGroupEquivOriginalIdele_prime K D.modulus v hvm]
  simpa only [e, MulEquiv.symm_apply_apply] using
    finiteAbelianReciprocity_primeArtin_eq_original K L D v hvm

theorem

finiteAbelianReciprocity_modulus_isDefining

L84 ↗

ClassFieldTheory.GlobalClassFieldComparison.finiteAbelianReciprocity_modulus_isDefining

Documentation

The modulus of public finite abelian reciprocity data defines the extension's genuine idèle-class norm subgroup. This follows from prime normalization, rather than being an additional field of the data.

Source context 4 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison

Lean source · statement

theorem finiteAbelianReciprocity_modulus_isDefining
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (D : FiniteAbelianReciprocityData K L) :
    (rayClassModulusToOriginal K D.modulus).congruenceSubgroup ≤
      (_root_.ideleClassNorm K L).range

theorem

publicArtinKer_iff_idealArtinKernel

L110 ↗

ClassFieldTheory.GlobalClassFieldComparison.publicArtinKer_iff_idealArtinKernel

Documentation

On a fractional ideal prime to the modulus, the public Artin map is trivial exactly when the original ideal Artin map is trivial.

Source context 4 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory.GlobalClassFieldComparison

Lean source · statement

theorem publicArtinKer_iff_idealArtinKernel
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (D : FiniteAbelianReciprocityData K L)
    (I : rayClassPrimeToIdeals D.modulus) :
    (QuotientGroup.mk' (rayPrincipalIdealSubgroupInPrimeTo D.modulus) I) ∈
        D.artin.ker ↔
      I ∈ GlobalClassFieldTheory.IdealClassFieldTheory.idealArtinKernel
        (rayClassModulusToOriginal K D.modulus)
        (_root_.ideleClassNorm K L).range
        (finiteAbelianReciprocity_modulus_isDefining K L D)

Module documentation

Comparing the public and ideal-theoretic Artin kernels

Declarations

finiteAbelianReciprocity_primeArtin_eq_original

finiteAbelianReciprocity_originalPrimeNormalization

finiteAbelianReciprocity_modulus_isDefining

publicArtinKer_iff_idealArtinKernel