Module

RayClassSubgroupRealizationEq.lean

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.RayClassSubgroupRealizationEq

1 declaration indexed from sourceView source ↗

Module documentation

Uniqueness of a ray-class subgroup field inside the fixed closure

The class field is independent of the Frobenius-normalized realization as an actual intermediate field, not just up to abstract isomorphism. This does not assert uniqueness of the embedding or of the Artin map.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.ConductorsAndRayClassFields.All

theorem

rayClassSubgroupRealizations_eq

L22 ↗

ClassFieldTheory.rayClassSubgroupRealizations_eq

Documentation

Two realizations for the same modulus and subgroup have the same intermediate field in the chosen separable closure.

Source context 1 command

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

namespace ClassFieldTheory

Lean source · statement

theorem rayClassSubgroupRealizations_eq
    (K : Type) [Field K] [NumberField K]
    (m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
    (R₁ R₂ : RayClassSubgroupRealization K m H) :
    R₁.extension.1 = R₂.extension.1

Module documentation

Uniqueness of a ray-class subgroup field inside the fixed closure

Declarations

rayClassSubgroupRealizations_eq