Conjugation by an element of a normal subgroup, seen through a commutative target

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.

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.

@[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.