Module

RayClassSubgroupQuotientEquiv.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassSubgroupQuotientEquiv

1 declaration indexed from sourceView source ↗

Module documentation

The quotient induced by a ray-class Artin map

The prescribed subgroup is identified with the Artin kernel before applying the first isomorphism theorem.

Imports2

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassSubgroupRealization
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by5

def

rayClassSubgroupQuotientEquiv

L26 ↗

ClassFieldTheory.rayClassSubgroupQuotientEquiv

Documentation

The isomorphism induced by the Artin map of a ray-class realization.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

def rayClassSubgroupQuotientEquiv
    (K : Type u) [Field K] [NumberField K]
    (m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
    (R : RayClassSubgroupRealization K m H) :
    (RayClassGroup m ⧸ H) ≃* (R.extension ≃ₐ[K] R.extension)

Module documentation

The quotient induced by a ray-class Artin map

Declarations

rayClassSubgroupQuotientEquiv