Module

RayClassIdealModulusProjection.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassIdealModulusProjection

7 declarations indexed from sourceView source ↗

Module documentation

Projection between ideal-theoretic ray class groups

Enlarging a modulus strengthens its finite congruences and real positivity conditions. The induced inclusions of prime-to-modulus ideals and ray-principal ideals give the canonical quotient map from the larger modulus to the smaller.

Imports4

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.IsRayCongruent
Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassGroup
Mathlib.Data.Finsupp.Order
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by5

def

rayLocalIntegralValue

L29 ↗

ClassFieldTheory.rayLocalIntegralValue

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

def rayLocalIntegralValue
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K))
    (y : (v.adicCompletionIntegers K).units) :
    v.adicCompletionIntegers K

theorem

rayLocalHigherUnitMap_eq_one_iff

L37 ↗

ClassFieldTheory.rayLocalHigherUnitMap_eq_one_iff

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem rayLocalHigherUnitMap_eq_one_iff
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ)
    (y : (v.adicCompletionIntegers K).units) :
    rayLocalHigherUnitMap v n y = 1 ↔
      rayLocalIntegralValue v y - 1 ∈
        (IsLocalRing.maximalIdeal (v.adicCompletionIntegers K)) ^ n

theorem

rayLocalHigherUnitGroup_antitone

L55 ↗

ClassFieldTheory.rayLocalHigherUnitGroup_antitone

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem rayLocalHigherUnitGroup_antitone
    {K : Type u} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K))
    {m n : ℕ} (hmn : m ≤ n) :
    rayLocalHigherUnitGroup v n ≤ rayLocalHigherUnitGroup v m

theorem

rayCongruent_of_le

L75 ↗

ClassFieldTheory.rayCongruent_of_le

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem rayCongruent_of_le
    {K : Type u} [Field K] [NumberField K]
    {m n : RayClassModulus K} (hmn : m ≤ n)
    {x : Kˣ} (hx : IsRayCongruent n x) :
    IsRayCongruent m x

theorem

rayPrimeToIdeals_antitone

L91 ↗

ClassFieldTheory.rayPrimeToIdeals_antitone

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem rayPrimeToIdeals_antitone
    {K : Type u} [Field K] [NumberField K]
    {m n : RayClassModulus K} (hmn : m ≤ n) :
    rayClassPrimeToIdeals n ≤ rayClassPrimeToIdeals m

theorem

rayPrincipalIdeals_antitone

L98 ↗

ClassFieldTheory.rayPrincipalIdeals_antitone

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem rayPrincipalIdeals_antitone
    {K : Type u} [Field K] [NumberField K]
    {m n : RayClassModulus K} (hmn : m ≤ n) :
    rayPrincipalIdealSubgroup n ≤ rayPrincipalIdealSubgroup m

def