Module

RayClassFieldModulusMonotone.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassFieldModulusMonotone

1 declaration indexed from sourceView source ↗

Module documentation

Ray class fields increase with the modulus

The modulus projection produces an embedding of realizations. Normality upgrades that embedding to literal inclusion in the fixed separable closure.

Imports2

Imported by2

theorem

rayClassFieldRealization_mono_modulus

L26 ↗

ClassFieldTheory.rayClassFieldRealization_mono_modulus

Documentation

For m ≤ n, every realization of the ray class field of m is a subfield of every realization of the ray class field of n in the fixed separable closure.

Source context 3 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem rayClassFieldRealization_mono_modulus
    {K : Type} [Field K] [NumberField K]
    {m n : RayClassModulus K} (hmn : m ≤ n)
    (Rm : RayClassFieldRealization K m)
    (Rn : RayClassFieldRealization K n) :
    Rm.extension.1 ≤ Rn.extension.1

Module documentation

Ray class fields increase with the modulus

Declarations

rayClassFieldRealization_mono_modulus