Module

FiniteAbelianReciprocityQuotientEquiv.lean

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.FiniteAbelianReciprocityQuotientEquiv

1 declaration indexed from sourceView source ↗

Module documentation

The quotient induced by a finite Artin map

This is the specific isomorphism induced by the Artin map in FiniteAbelianReciprocityData, not an arbitrarily chosen isomorphism.

Imports2

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.FiniteAbelianReciprocityData
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by3

def

finiteAbelianReciprocityQuotientEquiv

L26 ↗

ClassFieldTheory.finiteAbelianReciprocityQuotientEquiv

Documentation

The first-isomorphism-theorem map induced by a finite Artin map.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def finiteAbelianReciprocityQuotientEquiv
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsAbelianGalois K L]
    (D : FiniteAbelianReciprocityData K L) :
    (RayClassGroup D.modulus ⧸ D.artin.ker) ≃* (L ≃ₐ[K] L)

Module documentation

The quotient induced by a finite Artin map

Declarations

finiteAbelianReciprocityQuotientEquiv