GlobalClassFieldTheory.GlobalClassFields.rayClassGroup_hom_ext_finitePrime
Two homomorphisms out of a ray class group agree if they agree on the normalized prime idèle classes away from its modulus.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.GlobalClassFields
universe u vLean source · statement
theorem rayClassGroup_hom_ext_finitePrime
{K : Type u} [Field K] [NumberField K]
(m : RayClass.Modulus K)
{G : Type v} [CommGroup G]
(f g : RayClass.RayClassGroup m →* G)
(hprime : ∀ (v : HeightOneSpectrum (𝓞 K))
(_ : v ∉ m.finitePart.support),
f (QuotientGroup.mk' m.congruenceSubgroup
(QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
(IdeleGroup.finitePrimeIdele v))) =
g (QuotientGroup.mk' m.congruenceSubgroup
(QuotientGroup.mk' (IdeleGroup.principalSubgroup K)
(IdeleGroup.finitePrimeIdele v)))) :
f = g