Module

RayClassSubgroupRealizationEquiv.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassSubgroupRealizationEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Independence of the realization of a ray-class subgroup

The field attached to a fixed modulus and subgroup is well-defined up to K-algebra equivalence. The equivalence is not claimed to be unique.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

rayClassSubgroupRealizations_equiv

L26 ↗

ClassFieldTheory.rayClassSubgroupRealizations_equiv

Documentation

Two Frobenius-normalized class-field realizations for the same modulus and ray-class subgroup are isomorphic over the base number field.

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 rayClassSubgroupRealizations_equiv
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
    (R₁ R₂ : RayClassSubgroupRealization K m H) :
    Nonempty (R₁.extension ≃ₐ[K] R₂.extension)

Module documentation

Independence of the realization of a ray-class subgroup

Declarations

rayClassSubgroupRealizations_equiv