Module

FullConductorRayClassField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FullConductorRayClassField

1 declaration indexed from sourceView source ↗

Module documentation

Full conductors and ray class field containment

This module identifies the full conductor of a finite abelian extension as the least modulus of a selected ray class field into which the extension embeds. The proof combines the ray-field embedding criterion with the minimality theorem for the full conductor.

Imports2

Imported by2

theorem

nonempty_algHom_to_rayClassField_iff_fullConductor_le

L34 ↗

GlobalClassFieldTheory.GlobalClassFields.nonempty_algHom_to_rayClassField_iff_fullConductor_le

Documentation

A finite abelian extension embeds in the selected ray class field exactly when the modulus is at least its full conductor.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem nonempty_algHom_to_rayClassField_iff_fullConductor_le
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L]
    (m : RayClass.Modulus K) :
    Nonempty (L →ₐ[K] rayClassField K m) ↔
      (ideleClassNormConductorialSubgroup
        (K := K) (L := L)).fullConductor ≤ m

Module documentation

Full conductors and ray class field containment

Declarations

nonempty_algHom_to_rayClassField_iff_fullConductor_le