ClassFieldTheory.rayClassSubgroupQuotientEquiv_mk
A ray class maps to its original Artin value under the induced quotient isomorphism.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
theorem rayClassSubgroupQuotientEquiv_mk
(K : Type u) [Field K] [NumberField K]
(m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
(R : RayClassSubgroupRealization K m H)
(x : RayClassGroup m) :
rayClassSubgroupQuotientEquiv K m H R
(QuotientGroup.mk' H x) = R.artin x