ClassFieldTheory.finiteAbelianReciprocityQuotientEquiv_mk
The quotient isomorphism evaluates to the original 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 vLean source · statement
theorem finiteAbelianReciprocityQuotientEquiv_mk
(K : Type u) (L : Type v)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
[IsAbelianGalois K L]
(D : FiniteAbelianReciprocityData K L)
(x : RayClassGroup D.modulus) :
finiteAbelianReciprocityQuotientEquiv K L D
(QuotientGroup.mk' D.artin.ker x) = D.artin x