Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.RayClassSubgroupFieldAntitone

theorem

chosenRayClassSubgroupSubfield_antitone

ClassFieldTheory.chosenRayClassSubgroupSubfield_antitone

Documentation

For one modulus, inclusion of ray-class subgroups reverses inclusion of their selected class fields inside 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 chosenRayClassSubgroupSubfield_antitone
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K)
    {H J : Subgroup (RayClassGroup m)} (hHJ : H ≤ J) :
    GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupSubfield
        (K := K) (GlobalClassFieldComparison.rayClassModulusToOriginal K m)
        (J.map (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m).toMonoidHom) ≤
      GlobalClassFieldTheory.GlobalClassFields.rayClassSubgroupSubfield
        (K := K) (GlobalClassFieldComparison.rayClassModulusToOriginal K m)
        (H.map (GlobalClassFieldComparison.rayClassGroupEquivOriginalIdele K m).toMonoidHom)

RayClassSubgroupFieldAntitone.lean

Module documentation

Subgroup order and chosen ray class fields

chosenRayClassSubgroupSubfield_antitone

Module documentation

Subgroup order and chosen ray class fields

Declarations

chosenRayClassSubgroupSubfield_antitone