ClassFieldTheory.rayClassIdealArtinKer_eq_normRange_sup_principal
Before passing to ray classes, the Artin kernel is the product of the genuine ideal-norm subgroup and the principal ray-ideal subgroup.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem rayClassIdealArtinKer_eq_normRange_sup_principal
(K L : Type)
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
(D : FiniteAbelianReciprocityData K L) :
(D.artin.comp
(QuotientGroup.mk' (rayPrincipalIdealSubgroupInPrimeTo D.modulus))).ker =
(rayClassPrimeToIdealNorm K L D.modulus).range ⊔
rayPrincipalIdealSubgroupInPrimeTo D.modulus