Module

EmbedsInRayClassFieldIffConductorLe.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.EmbedsInRayClassFieldIffConductorLe

1 declaration indexed from sourceView source ↗

Module documentation

The full conductor as a minimal modulus

Let L/K be finite abelian. Its conductor is the least modulus whose ray class field contains L. Since the public interface makes no global choice of ray class fields, the theorem asserts existence of this least modulus.

Imports2

Imported by4

theorem

embedsInRayClassField_iff_conductor_le

L27 ↗

ClassFieldTheory.embedsInRayClassField_iff_conductor_le

Documentation

A finite abelian extension has a conductor characterized by containment in ray class fields.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory

Lean source · statement

theorem embedsInRayClassField_iff_conductor_le
    (K : Type) [Field K] [NumberField K]
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L] :
    ∃ c : RayClassModulus K, IsAbelianConductor K L c

Module documentation

The full conductor as a minimal modulus

Declarations

embedsInRayClassField_iff_conductor_le