feat(NumberTheory/NumberField/Cyclotomic): cardinality of the subgroup of characters associated to an intermediate field equals its degree (#37267)

New main result : `card_intermediateFieldEquivSubgroupChar`: the cardinality of the subgroup of Dirichlet characters of level `n` associated to an intermediate field `F` of `ℚ(ζₙ)/ℚ` equals the degree `[F : ℚ]`.

Author: xroblot

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -170,6 +170,11 @@ theorem card_subtype (K : Subgroup G) (L : Subgroup K) :
     Nat.card (map K.subtype L) = Nat.card L :=
   card_map_of_injective K.subtype_injective
 
+@[to_additive]
+theorem card_mapSubgroup {G' : Type*} [Group G'] (e : G ≃* G') :
+    Nat.card (e.mapSubgroup H) = Nat.card H :=
+  Subgroup.card_map_of_injective e.injective
+
 end Subgroup
 
 namespace Subgroup

Mathlib/GroupTheory/FiniteAbelian/Duality.lean

@@ -128,6 +128,13 @@ theorem forall_monoidHom_apply_eq_one_iff (H : Subgroup G) (x : G) :
   simp only [← QuotientGroup.eq_one_iff, ← forall_apply_eq_apply_iff _ (M := M), map_one] at h ⊢
   exact fun φ ↦ h (φ.comp (QuotientGroup.mk' H)) fun y hy ↦ hy φ
 
+theorem card_restrictHom_ker (H : Subgroup G) :
+    Nat.card (restrictHom H Mˣ).ker = Nat.card (G ⧸ H) := by
+  have : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H)) :=
+    hM.of_dvd M <| Group.exponent_quotient_dvd H
+  rw [Nat.card_congr (MonoidHom.restrictHomKerEquiv Mˣ H).toEquiv,
+    card_monoidHom_of_hasEnoughRootsOfUnity]
+
 variable (G) in
 /--
 The `MulEquiv` between the double dual `(G →* Mˣ) →* Mˣ` of a finite commutative group `G`
@@ -194,4 +201,10 @@ theorem mem_subgroupOrderIsoSubgroupMonoidHom_symm_iff (Φ : Subgroup (G →* M
     Subgroup.mem_map_equiv, mem_ker, restrictHom_apply, restrict_eq_one_iff,
     monoidHomMonoidHomEquiv_symm_apply_apply]
 
+/-- The cardinality of the dual subgroup of `G →* Mˣ` associated to a subgroup `H` of `G`
+equals the index of `H` in `G`. -/
+theorem card_subgroupOrderIsoSubgroupMonoidHom (H : Subgroup G) :
+    Nat.card (subgroupOrderIsoSubgroupMonoidHom G M H).ofDual = Nat.card (G ⧸ H) :=
+  card_restrictHom_ker _ _
+
 end CommGroup

Mathlib/NumberTheory/MulChar/Duality.lean

@@ -133,4 +133,12 @@ theorem mem_subgroupOrderIsoSubgroupMulChar_symm_iff {X : Subgroup (MulChar M R)
     m ∈ (subgroupOrderIsoSubgroupMulChar M R).symm (OrderDual.toDual X) ↔ ∀ χ ∈ X, χ m = 1 := by
   simp [subgroupOrderIsoSubgroupMulChar, ← Units.val_eq_one]
 
+/-- The cardinality of the dual subgroup of `MulChar M R` associated to a subgroup `H` of `Mˣ`
+equals the index of `H` in `Mˣ`. -/
+theorem card_subgroupOrderIsoSubgroupMulChar {H : Subgroup Mˣ} :
+    Nat.card (subgroupOrderIsoSubgroupMulChar M R H).ofDual = Nat.card (Mˣ ⧸ H) := by
+  rw [subgroupOrderIsoSubgroupMulChar, OrderIso.trans_apply, OrderIso.dual_apply,
+    OrderDual.ofDual_toDual, Subgroup.card_mapSubgroup,
+    CommGroup.card_subgroupOrderIsoSubgroupMonoidHom]
+
 end MulChar

Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean

@@ -180,7 +180,12 @@ theorem mem_subgroupGalEquivSubgroupChar_symm_iff (σ : Gal(K/ℚ))
     MulEquiv.coe_mapSubgroup, Subgroup.mem_map_equiv, MulEquiv.symm_symm,
     mem_subgroupOrderIsoSubgroupMulChar_symm_iff]
 
-variable [IsGalois ℚ K]
+theorem card_subgroupGalEquivSubgroupChar [IsMulCommutative Gal(K/ℚ)] (H : Subgroup Gal(K/ℚ)) :
+    Nat.card (subgroupGalEquivSubgroupChar n K R H).ofDual = Nat.card (Gal(K/ℚ) ⧸ H) := by
+  rw [subgroupGalEquivSubgroupChar, OrderIso.trans_apply, card_subgroupOrderIsoSubgroupMulChar]
+  exact Nat.card_congr (QuotientGroup.congr _ _ (galEquivZMod n K) rfl).symm.toEquiv
+
+variable [IsAbelianGalois ℚ K]
 
 /--
 The bijection between the intermediate fields of `ℚ(ζₙ)/ℚ` and the subgroups of the group
@@ -191,6 +196,16 @@ noncomputable def intermediateFieldEquivSubgroupChar :
   IsGalois.intermediateFieldEquivSubgroup.trans <|
       (subgroupGalEquivSubgroupChar n K R).dual.trans (OrderIso.dualDual _).symm
 
+/-- The cardinality of the subgroup of Dirichlet characters of level `n` associated to an
+intermediate field `F` of `ℚ(ζₙ)/ℚ` equals the degree `[F : ℚ]`. -/
+theorem card_intermediateFieldEquivSubgroupChar (F : IntermediateField ℚ K) :
+    Nat.card (intermediateFieldEquivSubgroupChar n K R F) = Module.finrank ℚ F := by
+  unfold intermediateFieldEquivSubgroupChar
+  rw [OrderIso.trans_apply, OrderIso.trans_apply, OrderIso.dualDual_symm_apply,
+    IsGalois.intermediateFieldEquivSubgroup_apply, OrderIso.dual_apply, OrderDual.ofDual_toDual,
+    OrderDual.ofDual_toDual, card_subgroupGalEquivSubgroupChar, finrank_eq_fixingSubgroup_index,
+    ← Subgroup.index_eq_card]
+
 @[simp]
 theorem mem_intermediateFieldEquivSubgroupChar_iff (F : IntermediateField ℚ K)
     (χ : DirichletCharacter R n) :