Conjugation on the group algebra of a normal subgroup

Let N be a normal subgroup of a group G. Conjugating by g : G is an automorphism of N (MulAut.conjNormal), so it permutes the basis of the group algebra k[N] and therefore induces an algebra automorphism of k[N]. This file packages that automorphism as a monoid homomorphism MonoidAlgebra.conjNormalAlgAut : G →* (k[N] ≃ₐ[k] k[N]), obtained by composing Mathlib's MonoidAlgebra.domCongrAut with MulAut.conjNormal.

Main definitions

• MonoidAlgebra.conjNormalAlgAut: conjugation by g : G as an algebra automorphism of k[N].

Main statements

• MonoidAlgebra.conjNormalAlgAut_single: conjugation acts on the group-algebra basis by conjugating the group element.

Conjugating by g and then by g⁻¹ is the identity; that cancellation is left to simp, which proves it from map_inv and AlgEquiv.symm_apply_apply.

noncomputable def MonoidAlgebra.conjNormalAlgAut (k : Type u_1) {G : Type u_2} [CommSemiring k] [Group G] (N : Subgroup G) [N.Normal] : G →* MonoidAlgebra k ↥N ≃ₐ[k] MonoidAlgebra k ↥N

Conjugation, read on the group algebra of a normal subgroup. Conjugating by g : G permutes N, hence permutes the basis of k[N], and the resulting algebra automorphism is what translation by a representation of G is semilinear over.

Equations

• MonoidAlgebra.conjNormalAlgAut k N = MonoidAlgebra.domCongrAut.comp MulAut.conjNormal

@[simp]

theorem MonoidAlgebra.conjNormalAlgAut_single {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {N : Subgroup G} [N.Normal] (g : G) (n : ↥N) (a : k) : ((conjNormalAlgAut k N) g) (single n a) = single ((MulAut.conjNormal g) n) a

Conjugation acts on the group-algebra basis by conjugating the group element.