Module

RayFrobeniusRigidity.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayFrobeniusRigidity

5 declarations indexed from sourceView source ↗

Module documentation

Rigidity of Frobenius-normalized ray reciprocity

An isomorphism from a ray class group to the Galois group of a finite abelian extension which sends every prime class to its genuine arithmetic Artin symbol forces the ray modulus to be defining for that extension. The proof compares the given map and genuine global reciprocity at a common multiple of the given modulus and the extension's full conductor.

Imports4

Imported by8

theorem

rayRigidity_ideleClassGroupIsMulCommutative

L31 ↗

GlobalClassFieldTheory.GlobalClassFields.rayRigidity_ideleClassGroupIsMulCommutative

Source context 4 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.GlobalClassFields

Lean source · statement

theorem rayRigidity_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem

rayModulus_isDefining_of_arithmeticPrimeArtinEquiv

L40 ↗

GlobalClassFieldTheory.GlobalClassFields.rayModulus_isDefining_of_arithmeticPrimeArtinEquiv

Documentation

Frobenius normalization on all primes away from a modulus forces that modulus to define the genuine norm subgroup of a finite abelian extension.

Source context 5 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.GlobalClassFields
attribute [local instance] rayRigidity_ideleClassGroupIsMulCommutative

Lean source · statement

theorem rayModulus_isDefining_of_arithmeticPrimeArtinEquiv
    {K L : Type} [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (m : RayClass.Modulus K)
    (e : RayClass.RayClassGroup m ≃* (L ≃ₐ[K] L))
    (hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
      (_ : v ∉ m.finitePart.support),
        e (QuotientGroup.mk' m.congruenceSubgroup
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
            (IdeleGroup.finitePrimeIdele v))) =
          arithmeticFinitePlacePrimeArtin (K := K) (L := L) v) :
    m.congruenceSubgroup ≤ (_root_.ideleClassNorm K L).range

theorem

rayModulus_normSubgroup_eq_of_arithmeticPrimeArtinEquiv

L115 ↗

GlobalClassFieldTheory.GlobalClassFields.rayModulus_normSubgroup_eq_of_arithmeticPrimeArtinEquiv

Documentation

A Frobenius-normalized ray-class isomorphism also identifies the extension's genuine norm subgroup exactly with the ray congruence subgroup. The reverse inclusion follows because the induced quotient map is a surjection between finite groups of the same order.

Source context 5 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.GlobalClassFields
attribute [local instance] rayRigidity_ideleClassGroupIsMulCommutative

Lean source · statement

theorem rayModulus_normSubgroup_eq_of_arithmeticPrimeArtinEquiv
    {K L : Type} [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (m : RayClass.Modulus K)
    (e : RayClass.RayClassGroup m ≃* (L ≃ₐ[K] L))
    (hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
      (_ : v ∉ m.finitePart.support),
        e (QuotientGroup.mk' m.congruenceSubgroup
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
            (IdeleGroup.finitePrimeIdele v))) =
          arithmeticFinitePlacePrimeArtin (K := K) (L := L) v) :
    (_root_.ideleClassNorm K L).range = m.congruenceSubgroup

theorem

rayArtin_comp_ideleClass_eq_arithmeticGlobalNormResidue

L164 ↗

GlobalClassFieldTheory.GlobalClassFields.rayArtin_comp_ideleClass_eq_arithmeticGlobalNormResidue

Documentation

Frobenius normalization away from the modulus determines the value of the ray Artin map on every idèle class, including classes supported at a ramified place. The normalization here is arithmetic Frobenius.

Source context 5 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.GlobalClassFields
attribute [local instance] rayRigidity_ideleClassGroupIsMulCommutative

Lean source · statement

theorem rayArtin_comp_ideleClass_eq_arithmeticGlobalNormResidue
    {K L : Type} [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (m : RayClass.Modulus K)
    (artin : RayClass.RayClassGroup m →* (L ≃ₐ[K] L))
    (hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
      (_ : v ∉ m.finitePart.support),
        artin (QuotientGroup.mk' m.congruenceSubgroup
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
            (IdeleGroup.finitePrimeIdele v))) =
          arithmeticFinitePlacePrimeArtin (K := K) (L := L) v)
    (x : IdeleClassGroup K) :
    artin (QuotientGroup.mk' m.congruenceSubgroup x) =
      Reciprocity.arithmeticGlobalNormResidueMonoidHom K L x

theorem

rayModulus_normSubgroup_eq_artinKer_preimage

L230 ↗

GlobalClassFieldTheory.GlobalClassFields.rayModulus_normSubgroup_eq_artinKer_preimage

Documentation

A Frobenius-normalized ray Artin homomorphism has kernel precisely the image of the genuine idèle-class norm subgroup in the ray quotient. Unlike the ray-class-field case, the homomorphism need not be injective.

Source context 5 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.GlobalClassFields
attribute [local instance] rayRigidity_ideleClassGroupIsMulCommutative

Lean source · statement

theorem rayModulus_normSubgroup_eq_artinKer_preimage
    {K L : Type} [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (m : RayClass.Modulus K)
    (artin : RayClass.RayClassGroup m →* (L ≃ₐ[K] L))
    (hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
      (_ : v ∉ m.finitePart.support),
        artin (QuotientGroup.mk' m.congruenceSubgroup
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
            (IdeleGroup.finitePrimeIdele v))) =
          arithmeticFinitePlacePrimeArtin (K := K) (L := L) v) :
    (_root_.ideleClassNorm K L).range =
      artin.ker.comap (QuotientGroup.mk' m.congruenceSubgroup)

Module documentation

Rigidity of Frobenius-normalized ray reciprocity

Declarations

rayRigidity_ideleClassGroupIsMulCommutative

rayModulus_isDefining_of_arithmeticPrimeArtinEquiv

rayModulus_normSubgroup_eq_of_arithmeticPrimeArtinEquiv

rayArtin_comp_ideleClass_eq_arithmeticGlobalNormResidue

rayModulus_normSubgroup_eq_artinKer_preimage