Conjugation of subgroups

A normal subgroup N of G carries the conjugation action MulAut.conjNormal of the whole of G. Conjugation by an element of N itself is inner, so a homomorphism ψ : N →* M to a commutative monoid cannot see it: conjugate elements of N have the same image in M.

Dually, conjugation cannot move a central element: a subgroup containing one has every conjugate containing it too.

For an action of G on a type, translation by g carries the orbits of a subgroup H onto the orbits of its conjugate g H g⁻¹.

Main statements

• MonoidHom.map_conjNormal_val: a homomorphism from a normal subgroup to a commutative monoid is unchanged by conjugation by an element of that subgroup.
• Subgroup.mem_conjAct_smul_of_mem_center: a central element of a subgroup lies in each of its conjugates.
• Subgroup.inclusion_conj_smul: the inclusion of a normal subgroup into a larger normal subgroup commutes with conjugation.
• TauCeti.MulAction.orbitRel_smul_smul_iff_of_conjAct_smul_eq: g • x and g • y lie in the same orbit of g H g⁻¹ exactly when x and y lie in the same orbit of H.

@[simp]

theorem MonoidHom.map_conjNormal_val {G : Type u_1} {M : Type u_2} [Group G] [CommMonoid M] {N : Subgroup G} [N.Normal] (ψ : ↥N →* M) (a x : ↥N) : ψ ((MulAut.conjNormal ↑a) x) = ψ x

Conjugation by an element of a normal subgroup does not move a homomorphism from that subgroup to a commutative monoid: conjugate elements have the same image in a commutative target.

theorem Subgroup.mem_conjAct_smul_of_mem_center {G : Type u_1} [Group G] {H : Subgroup G} {z : G} (hz : z ∈ center G) (c : G) (h : z ∈ H) : z ∈ ConjAct.toConjAct c • H

A central element of a subgroup lies in each of its conjugates, since conjugation fixes it.

theorem Subgroup.inclusion_conj_smul {G : Type u_1} [Group G] {H K : Subgroup G} [H.Normal] [K.Normal] (h : H ≤ K) (g : ConjAct G) (x : ↥H) : (inclusion h) (g • x) = g • (inclusion h) x

The inclusion of a normal subgroup H into a larger normal subgroup K commutes with the conjugation actions of ConjAct G on H and on K.

theorem TauCeti.MulAction.orbitRel_smul_smul_iff_of_conjAct_smul_eq {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H H' : Subgroup G} {g : G} (h : ConjAct.toConjAct g • H = H') (x y : X) : (MulAction.orbitRel (↥H') X) (g • x) (g • y) ↔ (MulAction.orbitRel (↥H) X) x y

Orbits of conjugate subgroups correspond under translation: if H' is the conjugate g H g⁻¹ of H, then g • x and g • y lie in the same H'-orbit exactly when x and y lie in the same H-orbit.