Module

FiniteAbelianGlobalReciprocityQuotient.lean

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.FiniteAbelianGlobalReciprocityQuotient

1 declaration indexed from sourceView source ↗

Module documentation

Quotient form of finite abelian global reciprocity

The kernel of a finite ray-class Artin map is exactly the relation that must be divided out to obtain the Galois group. The modulus and Frobenius normalization are carried by FiniteAbelianReciprocityData.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.All

theorem

finiteAbelianGlobalReciprocity_quotient

L28 ↗

ClassFieldTheory.finiteAbelianGlobalReciprocity_quotient

Documentation

A finite Artin map induces an isomorphism from its ray-class quotient to the finite abelian Galois group.

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

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

Module documentation

Quotient form of finite abelian global reciprocity

Declarations

finiteAbelianGlobalReciprocity_quotient