The conductor of a subgroup of a ray class group

For a subgroup H of the ray class group of a modulus 𝔪, the conductor of H is the least modulus 𝔣 such that every ray class character trivial on H has conductor dividing 𝔣. For a divisor 𝔫 of 𝔪, the conductor of H divides 𝔫 exactly when the kernel of the transition map classMap : RayClassGroup 𝔪 →* RayClassGroup 𝔫 lies in H, that is, when the projection to RayClassGroup 𝔪 ⧸ H factors through RayClassGroup 𝔫. So the conductor of H is the least modulus through which H is defined, and it divides 𝔪.

This is the conductor of an abelian extension in its ideal-theoretic form: if the Artin map of an abelian extension factors through RayClassGroup 𝔪, the conductor of its kernel is the least modulus through which the Artin map factors.

Main definitions

• Subgroup.rayClassConductor: the conductor of a subgroup of a ray class group.

Main results

• Subgroup.rayClassConductor_dvd_iff_forall_conductor_dvd: the conductor of H divides 𝔫 exactly when the conductor of every ray class character trivial on H does.
• Subgroup.rayClassConductor_dvd_iff: for 𝔫 ∣ 𝔪, the conductor of H divides 𝔫 exactly when the kernel of classMap lies in H.
• Subgroup.rayClassConductor_dvd: the conductor of H divides 𝔪.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §6.

theorem TauCeti.GlobalNumberFields.ker_classMap_le_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔫 ∣ 𝔪) (H : Subgroup (RayClassGroup 𝔪)) : (classMap h).ker ≤ H ↔ ∀ (η : RayClassCharacter 𝔪), H ≤ MonoidHom.ker η → η.conductor ∣ 𝔫

A transition map has kernel in H exactly when the characters trivial on H come from the smaller modulus. For 𝔫 ∣ 𝔪 and a subgroup H of RayClassGroup 𝔪, the kernel of classMap : RayClassGroup 𝔪 →* RayClassGroup 𝔫 lies in H exactly when every ray class character of 𝔪 trivial on H has conductor dividing 𝔫.

noncomputable def Subgroup.rayClassConductor {K : Type u_1} [Field K] [NumberField K] {𝔪 : TauCeti.GlobalNumberFields.Modulus K} (H : Subgroup (TauCeti.GlobalNumberFields.RayClassGroup 𝔪)) : TauCeti.GlobalNumberFields.Modulus K

The conductor of a subgroup of a ray class group: the least modulus divisible by the conductor of every ray class character trivial on the subgroup (rayClassConductor_dvd_iff_forall_conductor_dvd). For 𝔫 ∣ 𝔪 it divides 𝔫 exactly when the subgroup contains the kernel of classMap : RayClassGroup 𝔪 →* RayClassGroup 𝔫 (rayClassConductor_dvd_iff).

theorem Subgroup.rayClassConductor_dvd_iff_forall_conductor_dvd {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : TauCeti.GlobalNumberFields.Modulus K} (H : Subgroup (TauCeti.GlobalNumberFields.RayClassGroup 𝔪)) : H.rayClassConductor ∣ 𝔫 ↔ ∀ (η : TauCeti.GlobalNumberFields.RayClassCharacter 𝔪), H ≤ MonoidHom.ker η → η.conductor ∣ 𝔫

The conductor of a subgroup is the least common multiple of the conductors of the characters trivial on it: it divides 𝔫 exactly when the conductor of every ray class character trivial on the subgroup divides 𝔫.

theorem Subgroup.rayClassConductor_dvd_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : TauCeti.GlobalNumberFields.Modulus K} (h : 𝔫 ∣ 𝔪) (H : Subgroup (TauCeti.GlobalNumberFields.RayClassGroup 𝔪)) : H.rayClassConductor ∣ 𝔫 ↔ (TauCeti.GlobalNumberFields.classMap h).ker ≤ H

The conductor of a subgroup is the least modulus through which it is defined: for 𝔫 ∣ 𝔪, the conductor of H divides 𝔫 exactly when the kernel of classMap : RayClassGroup 𝔪 →* RayClassGroup 𝔫 lies in H.

theorem Subgroup.rayClassConductor_dvd {K : Type u_1} [Field K] [NumberField K] {𝔪 : TauCeti.GlobalNumberFields.Modulus K} (H : Subgroup (TauCeti.GlobalNumberFields.RayClassGroup 𝔪)) : H.rayClassConductor ∣ 𝔪

The conductor of a subgroup of the ray class group of 𝔪 divides 𝔪.

theorem Subgroup.ker_classMap_rayClassConductor_le {K : Type u_1} [Field K] [NumberField K] {𝔪 : TauCeti.GlobalNumberFields.Modulus K} (H : Subgroup (TauCeti.GlobalNumberFields.RayClassGroup 𝔪)) : (TauCeti.GlobalNumberFields.classMap ⋯).ker ≤ H

The kernel of the transition map from 𝔪 to the conductor of H lies in H.

theorem Subgroup.rayClassConductor_dvd_of_le {K : Type u_1} [Field K] [NumberField K] {𝔪 : TauCeti.GlobalNumberFields.Modulus K} {H H' : Subgroup (TauCeti.GlobalNumberFields.RayClassGroup 𝔪)} (hle : H ≤ H') : H'.rayClassConductor ∣ H.rayClassConductor

A larger subgroup has a smaller conductor.

theorem TauCeti.GlobalNumberFields.RayClassCharacter.conductor_dvd_rayClassConductor {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {H : Subgroup (RayClassGroup 𝔪)} {η : RayClassCharacter 𝔪} (hη : H ≤ MonoidHom.ker η) : η.conductor ∣ H.rayClassConductor

The conductor of a ray class character trivial on H divides the conductor of H.