Conjugate subgroups

This file characterizes membership in the orbit of a subgroup under conjugation and transports that orbit across a group isomorphism. A conjugate of H ≤ G is the image of H under MulAut.conj g for some g : G. The number of conjugates is the normalizer index. Consequently, a conjugation-invariant sum over subgroups can be grouped by their conjugacy classes with that multiplicity.

Main definitions

• MulEquiv.conjugateSubgroupsEquiv: a group isomorphism identifies the conjugates of corresponding subgroups.

Main results

• TauCeti.mem_orbit_conjAct_iff: orbit membership is subgroup conjugation.
• Subgroup.index_normalizer_eq_ncard_orbit: the number of conjugates is the index of the normalizer.
• Subgroup.ncard_orbit_mul_relIndex_normalizer: multiplying the number of conjugates by [N_G(H) : H] gives [G : H].
• TauCeti.sum_subgroups_eq_sum_conjugacy: group a conjugation-invariant sum by subgroup conjugacy classes.

@[simp]

theorem TauCeti.mem_orbit_conjAct_iff {G : Type u_1} [Group G] {H H' : Subgroup G} : H' ∈ MulAction.orbit (ConjAct G) H ↔ ∃ (g : G), Subgroup.map (↑(MulAut.conj g)) H = H'

Membership in the conjugacy orbit of H means being obtained from H by conjugation.

theorem Subgroup.index_normalizer_eq_ncard_orbit {G : Type u_1} [Group G] (H : Subgroup G) : (normalizer ↑H).index = (MulAction.orbit (ConjAct G) H).ncard

The number of conjugates of a subgroup is the index of its normalizer.

theorem Subgroup.ncard_orbit_mul_relIndex_normalizer {G : Type u_1} [Group G] (H : Subgroup G) : (MulAction.orbit (ConjAct G) H).ncard * H.relIndex (normalizer ↑H) = H.index

The number of conjugates of H times [N_G(H) : H] is [G : H].

theorem TauCeti.sum_subgroups_eq_sum_conjugacy {G : Type u_1} {M : Type u_2} [Group G] [Fintype G] [AddCommMonoid M] (f : Subgroup G → M) (hf : ∀ (g : G) (H : Subgroup G), f (Subgroup.map (↑(MulAut.conj g)) H) = f H) : ∑ H : Subgroup G, f H = ∑ ω : MulAction.orbitRel.Quotient (ConjAct G) (Subgroup G), (Subgroup.normalizer ↑(Quotient.out ω)).index • f (Quotient.out ω)

A conjugation-invariant sum over subgroups can be grouped by conjugacy classes, weighted by the normalizer index of each representative.

def MulEquiv.conjugateSubgroupsEquiv {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) : ↑(MulAction.orbit (ConjAct G) H) ≃ ↑(MulAction.orbit (ConjAct G') (Subgroup.map (↑e) H))

A group isomorphism identifies the sets of conjugates of corresponding subgroups.

Equations

• e.conjugateSubgroupsEquiv H = e.mapSubgroup.subtypeEquiv ⋯

@[simp]

theorem MulEquiv.conjugateSubgroupsEquiv_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (J : ↑(MulAction.orbit (ConjAct G) H)) : ↑((e.conjugateSubgroupsEquiv H) J) = Subgroup.map ↑e ↑J

On conjugate subgroups the equivalence maps each subgroup along the given isomorphism.

@[simp]

theorem MulEquiv.conjugateSubgroupsEquiv_symm_apply {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') (H : Subgroup G) (J : ↑(MulAction.orbit (ConjAct G') (Subgroup.map (↑e) H))) : ↑((e.conjugateSubgroupsEquiv H).symm J) = Subgroup.map ↑e.symm ↑J

The inverse equivalence maps a conjugate subgroup along the inverse isomorphism.