Module

RayClassSubgroupExistence.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassSubgroupExistence

1 declaration indexed from sourceView source ↗

Module documentation

Existence of the class field of a ray-class subgroup

Every subgroup of an ideal-theoretic ray class group is the kernel of the Frobenius-normalized Artin map of a finite abelian extension. The statement uses ideal classes; the proof transports the existing idelic reciprocity construction to that interface.

Imports3

Imported by2

theorem

rayClassSubgroup_existence

L27 ↗

ClassFieldTheory.rayClassSubgroup_existence

Documentation

Every ray-class subgroup has a finite abelian class-field realization.

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 rayClassSubgroup_existence
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K) (H : Subgroup (RayClassGroup m)) :
    Nonempty (RayClassSubgroupRealization K m H)

Module documentation

Existence of the class field of a ray-class subgroup

Declarations

rayClassSubgroup_existence