NYLL
Module

RayClassModulusProjection.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassModulusProjection
9 declarations indexed from sourceView source ↗

Module documentation

Projection between ray class groups

The idèle-class quotient gives the canonical map from a larger ray modulus to a smaller one. The public ray-class groups use the comparison equivalence to transport this map.

Imports4
Imported by1

Declarations

instance

ideleClassIsMulCommutative

L30 ↗
ClassFieldTheory.ideleClassIsMulCommutative
Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)
instance

rayCongruenceNormal

L34 ↗
ClassFieldTheory.rayCongruenceNormal
Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal
def

originalRayClassModulusProjection

L39 ↗
ClassFieldTheory.originalRayClassModulusProjection
Documentation

The quotient projection between the original idèle-class ray groups.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal :=
  Subgroup.normal_of_isMulCommutative _
Lean source · statement
def originalRayClassModulusProjection
    {m n : RayClass.Modulus K} (hmn : m ≤ n) :
    RayClass.RayClassGroup n →* RayClass.RayClassGroup m
theorem

originalRayClassModulusProjection_surjective

L49 ↗
ClassFieldTheory.originalRayClassModulusProjection_surjective
Documentation

The projection of the original idèle-class ray groups is onto.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal :=
  Subgroup.normal_of_isMulCommutative _
Lean source · statement
theorem originalRayClassModulusProjection_surjective
    {m n : RayClass.Modulus K} (hmn : m ≤ n) :
    Function.Surjective (originalRayClassModulusProjection K hmn)
def

rayClassModulusProjection

L60 ↗
ClassFieldTheory.rayClassModulusProjection
Documentation

For m ≤ n, the natural quotient map from the ray class group modulo n onto the ray class group modulo m.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal :=
  Subgroup.normal_of_isMulCommutative _
Lean source · statement
def rayClassModulusProjection
    {m n : RayClassModulus K} (hmn : m ≤ n) :
    RayClassGroup n →* RayClassGroup m
theorem

rayClassModulusProjection_apply

L72 ↗
ClassFieldTheory.rayClassModulusProjection_apply
Documentation

Evaluate the public projection through the original idèle-class quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal :=
  Subgroup.normal_of_isMulCommutative _
Lean source · full declaration
theorem rayClassModulusProjection_apply
    {m n : RayClassModulus K} (hmn : m ≤ n)
    (a : RayClassGroup n) :
    rayClassModulusProjection K hmn a =
      (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m).symm
        (originalRayClassModulusProjection K
          (show GlobalClassFieldComparison.rayClassModulusToOriginal K m ≤
            GlobalClassFieldComparison.rayClassModulusToOriginal K n from hmn)
          (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K n a)) :=
  rfl
theorem

rayClassModulusProjection_surjective

L84 ↗
ClassFieldTheory.rayClassModulusProjection_surjective
Documentation

The modulus-change projection is onto.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal :=
  Subgroup.normal_of_isMulCommutative _
Lean source · statement
theorem rayClassModulusProjection_surjective
    {m n : RayClassModulus K} (hmn : m ≤ n) :
    Function.Surjective (rayClassModulusProjection K hmn)
theorem

rayClassModulusProjection_prime

L117 ↗
ClassFieldTheory.rayClassModulusProjection_prime
Documentation

The image of a prime ray class under modulus change is the same prime ray class, provided the prime is outside the larger modulus.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal :=
  Subgroup.normal_of_isMulCommutative _
Lean source · full declaration
theorem rayClassModulusProjection_prime
    {m n : RayClassModulus K} (hmn : m ≤ n)
    (v : HeightOneSpectrum (𝓞 K))
    (hvn : v ∉ n.finitePart.support) :
    rayClassModulusProjection K hmn
        (rayClassOfFinitePrime n v hvn) =
      rayClassOfFinitePrime m v
        (by
          intro hvm
          exact hvn (Finsupp.support_mono hmn.1 hvm)) := by
  have hvm : v ∉ m.finitePart.support := by
    intro hv
    exact hvn (Finsupp.support_mono hmn.1 hv)
  let m' := GlobalClassFieldComparison.rayClassModulusToOriginal K m
  let n' := GlobalClassFieldComparison.rayClassModulusToOriginal K n
  have hmn' : m' ≤ n' := hmn
  apply (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m).injective
  change
    (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m)
      ((GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m).symm
        (originalRayClassModulusProjection K hmn'
          (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K n
            (rayClassOfFinitePrime n v hvn)))) =
      GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m
        (rayClassOfFinitePrime m v hvm)
  rw [(GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m).apply_symm_apply]
  rw [GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele_prime K n v hvn]
  rw [GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele_prime K m v hvm]
  rfl
theorem

chosenRayClassFieldSubfield_mono

L149 ↗
ClassFieldTheory.chosenRayClassFieldSubfield_mono
Documentation

Enlarging the public modulus gives literal containment of the selected ray class fields inside the fixed separable closure.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
variable (K : Type) [Field K] [NumberField K]
local instance ideleClassIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance rayCongruenceNormal (m : RayClass.Modulus K) :
    (RayClass.Modulus.congruenceSubgroup m).Normal :=
  Subgroup.normal_of_isMulCommutative _
Lean source · statement
theorem chosenRayClassFieldSubfield_mono
    {m n : RayClassModulus K} (hmn : m ≤ n) :
    GlobalClassFieldTheory.GlobalClassFields.rayClassFieldSubfield K
        (GlobalClassFieldComparison.rayClassModulusToOriginal K m) ≤
      GlobalClassFieldTheory.GlobalClassFields.rayClassFieldSubfield K
        (GlobalClassFieldComparison.rayClassModulusToOriginal K n)

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