Module

RayClassIdealModulusProjectionPrime.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassIdealModulusProjectionPrime

1 declaration indexed from sourceView source ↗

Module documentation

Prime classes and reduction of a ray modulus

An ideal prime to the larger modulus represents the same prime ideal after projection to the ray class group of the smaller modulus.

Imports3

Imported by3

theorem

rayClassIdealModulusProjection_prime

L29 ↗

ClassFieldTheory.rayClassIdealModulusProjection_prime

Documentation

Modulus reduction preserves the class of every prime outside the larger modulus.

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 · full declaration

theorem rayClassIdealModulusProjection_prime
    (K : Type u) [Field K] [NumberField K]
    {m n : RayClassModulus K} (hmn : m ≤ n)
    (v : HeightOneSpectrum (𝓞 K))
    (hvn : v ∉ n.finitePart.support) :
    rayClassIdealModulusProjection K hmn
        (rayClassOfFinitePrime n v hvn) =
      rayClassOfFinitePrime m v
        (by
          intro hvm
          exact hvn (Finsupp.support_mono hmn.1 hvm)) := by
  rfl

Module documentation

Prime classes and reduction of a ray modulus

Declarations

rayClassIdealModulusProjection_prime