Almost-conjugate subgroups

Two subgroups H and K of a group G are almost conjugate (also called Gassmann equivalent, or locally conjugate) when they meet every conjugacy class of G in the same number of elements. Conjugate subgroups are almost conjugate, but the converse fails: there are finite groups with non-conjugate almost-conjugate subgroups. These are Gassmann's examples, and they are the group-theoretic input to the construction of non-isomorphic arithmetically equivalent number fields.

The notion is equivalently a statement about the coset spaces. For g : G the number of cosets of H fixed by g is related to the number of elements of H conjugate to g by the division-free identity

#(G ⧸ H)^g · |H| = |C_G(g)| · #(H ∩ [g])

(Subgroup.natCard_fixedBy_mul_natCard, in TauCeti.GroupTheory.QuotientGroup.Basic), where C_G(g) is the centralizer of g, written as the stabilizer of g for the conjugation action ConjAct G, and [g] is the conjugacy class of g. Both sides count the x : G with x⁻¹ g x ∈ H: on the left they are grouped by their coset x H, which g then fixes, and on the right by the conjugate x⁻¹ g x, whose fibre is a coset of the centralizer. Summing the defining counts over the conjugacy classes shows that almost-conjugate subgroups of a finite group have the same order, hence the same index. Dividing the fixed-coset identity by the common order then shows that H and K are almost conjugate exactly when every g : G fixes as many cosets of H as of K. Through the classification of permutation representations by fixed-point counts this says that H and K are almost conjugate exactly when the permutation representations on G ⧸ H and G ⧸ K are equivalent in characteristic zero; that consequence is TauCeti.almostConjugate_iff_nonempty_equiv_ofMulAction.

Main definitions

• Subgroup.AlmostConjugate H K: H and K meet every conjugacy class of G in the same number of elements. It is decidable for a finite group with decidable equality and decidable subgroup membership.

Main statements

• Subgroup.AlmostConjugate.refl, .symm, .trans: almost-conjugacy is an equivalence relation.
• Subgroup.AlmostConjugate.map and Subgroup.AlmostConjugate.comap: it is transported along group isomorphisms, by Subgroup.natCard_mem_carrier_map_and_mem_map. The matching statement for conjugacy itself is Subgroup.exists_map_conj_comap_eq_iff, in TauCeti.Algebra.Group.Subgroup.Conjugates.
• Subgroup.almostConjugate_conj_smul and Subgroup.almostConjugate_conj_smul_iff: conjugate subgroups are almost conjugate, and almost-conjugacy is invariant under simultaneous conjugation.
• Subgroup.natCard_eq_sum_natCard_mem_carrier: the order of a subgroup of a finite group is the sum over the conjugacy classes of the number of its elements in each.
• Subgroup.AlmostConjugate.natCard_eq and Subgroup.AlmostConjugate.index_eq: almost-conjugate subgroups of a finite group have the same order and the same index.
• Subgroup.almostConjugate_iff_forall_natCard_fixedBy_eq: almost-conjugacy is equality of the fixed-coset counts.
• Subgroup.almostConjugate_iff_forall_natCard_cycleType_eq: two subgroups of a finite symmetric group are almost conjugate exactly when they contain equally many permutations of each cycle type.

References

• F. Gassmann, Bemerkungen zur vorstehenden Arbeit von Hurwitz, Math. Z. 25 (1926), 665–675.
• R. Perlis, On the equation ζ_K(s) = ζ_K'(s), J. Number Theory 9 (1977), 342–360.

def Subgroup.AlmostConjugate {G : Type u_1} [Group G] (H K : Subgroup G) : Prop

Two subgroups H and K of G are almost conjugate when they meet every conjugacy class of G in the same number of elements.

theorem Subgroup.almostConjugate_iff {G : Type u_1} [Group G] {H K : Subgroup G} : H.AlmostConjugate K ↔ ∀ (C : ConjClasses G), Nat.card { x : G // x ∈ C.carrier ∧ x ∈ H } = Nat.card { x : G // x ∈ C.carrier ∧ x ∈ K }

The defining property of almost-conjugacy.

theorem Subgroup.almostConjugate_iff_forall_natCard_isConj {G : Type u_1} [Group G] {H K : Subgroup G} : H.AlmostConjugate K ↔ ∀ (g : G), Nat.card { x : G // IsConj g x ∧ x ∈ H } = Nat.card { x : G // IsConj g x ∧ x ∈ K }

Almost-conjugacy read on conjugacy classes through their representatives: H and K are almost conjugate exactly when, for every g : G, they contain equally many conjugates of g.

@[instance_reducible]

instance Subgroup.instDecidableAlmostConjugateOfFintypeOfDecidableEqOfDecidablePredMem {G : Type u_1} [Group G] {H K : Subgroup G} [Fintype G] [DecidableEq G] [DecidablePred fun (x : G) => x ∈ H] [DecidablePred fun (x : G) => x ∈ K] : Decidable (H.AlmostConjugate K)

@[simp]

theorem Subgroup.AlmostConjugate.refl {G : Type u_1} [Group G] (H : Subgroup G) : H.AlmostConjugate H

Every subgroup is almost conjugate to itself.

theorem Subgroup.AlmostConjugate.rfl {G : Type u_1} [Group G] {H : Subgroup G} : H.AlmostConjugate H

Every subgroup is almost conjugate to itself; the implicit form of Subgroup.AlmostConjugate.refl.

theorem Subgroup.AlmostConjugate.symm {G : Type u_1} [Group G] {H K : Subgroup G} (h : H.AlmostConjugate K) : K.AlmostConjugate H

Almost-conjugacy is symmetric.

theorem Subgroup.AlmostConjugate.comm {G : Type u_1} [Group G] {H K : Subgroup G} : H.AlmostConjugate K ↔ K.AlmostConjugate H

Almost-conjugacy is symmetric, as an equivalence of propositions.

theorem Subgroup.AlmostConjugate.trans {G : Type u_1} [Group G] {H K L : Subgroup G} (h : H.AlmostConjugate K) (h' : K.AlmostConjugate L) : H.AlmostConjugate L

Almost-conjugacy is transitive.

theorem Subgroup.AlmostConjugate.equivalence {G : Type u_1} [Group G] : Equivalence AlmostConjugate

Almost-conjugacy is an equivalence relation on the subgroups of G.

Transport along isomorphisms and conjugation

theorem Subgroup.natCard_mem_carrier_map_and_mem_map {G : Type u_1} {Γ : Type u_2} [Group G] [Group Γ] (e : G ≃* Γ) (H : Subgroup G) (C : ConjClasses G) : Nat.card { y : Γ // y ∈ (ConjClasses.map (↑e) C).carrier ∧ y ∈ map (↑e) H } = Nat.card { x : G // x ∈ C.carrier ∧ x ∈ H }

A group isomorphism e identifies the elements of H in a conjugacy class C with the elements of e(H) in the conjugacy class e(C).

theorem Subgroup.AlmostConjugate.map {G : Type u_1} {Γ : Type u_2} [Group G] [Group Γ] {H K : Subgroup G} (h : H.AlmostConjugate K) (e : G ≃* Γ) : (Subgroup.map (↑e) H).AlmostConjugate (Subgroup.map (↑e) K)

Almost-conjugacy is transported along group isomorphisms.

theorem Subgroup.AlmostConjugate.comap {G : Type u_1} {Γ : Type u_2} [Group G] [Group Γ] {H K : Subgroup Γ} (h : H.AlmostConjugate K) (e : G ≃* Γ) : (Subgroup.comap (↑e) H).AlmostConjugate (Subgroup.comap (↑e) K)

Almost-conjugacy is pulled back along group isomorphisms.

@[simp]

theorem Subgroup.almostConjugate_conj_smul {G : Type u_1} [Group G] (g : G) (H : Subgroup G) : H.AlmostConjugate (MulAut.conj g • H)

Conjugate subgroups are almost conjugate. An inner automorphism maps every conjugacy class to itself, so it does not change the number of elements a subgroup has in it.

@[simp]

theorem Subgroup.almostConjugate_conj_smul_iff {G : Type u_1} [Group G] {H K : Subgroup G} (g : G) : (MulAut.conj g • H).AlmostConjugate (MulAut.conj g • K) ↔ H.AlmostConjugate K

Almost-conjugacy is invariant under simultaneous conjugation.

theorem Subgroup.natCard_eq_sum_natCard_mem_carrier {G : Type u_1} [Group G] [Finite G] [Fintype (ConjClasses G)] (H : Subgroup G) : Nat.card ↥H = ∑ C : ConjClasses G, Nat.card { x : G // x ∈ C.carrier ∧ x ∈ H }

The class equation of a subgroup. A subgroup H of a finite group G is the disjoint union of its intersections with the conjugacy classes of G, so its order is the sum of the numbers of elements of H in each conjugacy class.

theorem Subgroup.AlmostConjugate.natCard_eq {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] (h : H.AlmostConjugate K) : Nat.card ↥H = Nat.card ↥K

Almost-conjugate subgroups have the same order.

theorem Subgroup.AlmostConjugate.index_eq {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] (h : H.AlmostConjugate K) : H.index = K.index

Almost-conjugate subgroups have the same index.

theorem Subgroup.almostConjugate_iff_forall_natCard_fixedBy_eq {G : Type u_1} [Group G] {H K : Subgroup G} [Finite G] : H.AlmostConjugate K ↔ ∀ (g : G), Nat.card ↑(MulAction.fixedBy (G ⧸ H) g) = Nat.card ↑(MulAction.fixedBy (G ⧸ K) g)

Almost-conjugacy is equality of fixed-coset counts. Two subgroups H and K of a finite group G are almost conjugate exactly when every g : G fixes as many cosets of H as of K.

Subgroups of permutation groups

theorem Subgroup.almostConjugate_iff_forall_natCard_cycleType_eq {α : Type u_3} [Fintype α] [DecidableEq α] {H K : Subgroup (Equiv.Perm α)} : H.AlmostConjugate K ↔ ∀ (m : Multiset ℕ), Nat.card { σ : Equiv.Perm α // σ.cycleType = m ∧ σ ∈ H } = Nat.card { σ : Equiv.Perm α // σ.cycleType = m ∧ σ ∈ K }

Almost-conjugacy of permutation groups is equality of cycle-type counts. Two subgroups of Equiv.Perm α, for a finite type α, are almost conjugate exactly when they contain equally many permutations of each cycle type, because two permutations are conjugate exactly when they have the same cycle type (Equiv.Perm.isConj_iff_cycleType_eq).