Module

RayClassSubgroupFieldAntitone.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassSubgroupFieldAntitone

1 declaration indexed from sourceView source ↗

Module documentation

Inclusion of ray-class subgroup class fields

The fields are intermediate fields of one fixed separable closure, so the conclusion is literal inclusion rather than merely an abstract embedding.

Imports2

Imported by2

theorem

rayClassSubgroupField_antitone

L26 ↗

ClassFieldTheory.rayClassSubgroupField_antitone

Documentation

For one modulus, a larger ray-class subgroup gives a smaller class field inside the fixed separable closure. This holds for any choices of Frobenius-normalized realizations.

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 rayClassSubgroupField_antitone
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K)
    {H J : Subgroup (RayClassGroup m)} (hHJ : H ≤ J)
    (RH : RayClassSubgroupRealization K m H)
    (RJ : RayClassSubgroupRealization K m J) :
    RJ.extension.1 ≤ RH.extension.1

Module documentation

Inclusion of ray-class subgroup class fields

Declarations

rayClassSubgroupField_antitone