Base change of a monoid algebra

For a commutative semiring R, an R-algebra S and a monoid G, the base change R[G] ⊗[R] S of the monoid algebra is the monoid algebra S[G]: x ⊗ s is sent to s • x', where x' is x with its coefficients pushed forward to S. Mathlib's MonoidAlgebra.scalarTensorEquiv is this isomorphism, with the two tensor factors in the other order, for a commutative monoid and coefficient semiring; the version here requires neither G nor S to be commutative, so it applies to the group algebra of a nonabelian finite group.

The application is semisimplicity. When k is a field in which the order of a finite group G is nonzero, Maschke's theorem makes k[G] semisimple, hence so is the base change R[G] ⊗[R] k of the group algebra over any commutative ring R mapping to k. The rationalisation ℤ_p[G] ⊗[ℤ_p] ℚ_p of an integral group ring is the case this is used for.

Main definitions

• MonoidAlgebra.tensorAlgEquiv: the R-algebra isomorphism R[G] ⊗[R] S ≃ₐ[R] S[G].

Main results

• MonoidAlgebra.isSemisimpleRing_tensor: R[G] ⊗[R] k is a semisimple ring when k is a field in which the order of the finite group G is nonzero.

noncomputable def MonoidAlgebra.tensorAlgEquiv (R : Type u_1) [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (G : Type u_3) [Monoid G] : TensorProduct R (MonoidAlgebra R G) S ≃ₐ[R] MonoidAlgebra S G

Base change of a monoid algebra. For an R-algebra S, the base change R[G] ⊗[R] S of the monoid algebra of an arbitrary monoid G is the monoid algebra S[G], by x ⊗ s ↦ s • x' where x' has the coefficients of x pushed forward to S.

@[simp]

theorem MonoidAlgebra.tensorAlgEquiv_tmul (R : Type u_1) [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (G : Type u_3) [Monoid G] (x : MonoidAlgebra R G) (s : S) : (tensorAlgEquiv R S G) (x ⊗ₜ[R] s) = s • (mapAlgHom G (Algebra.ofId R S)) x

@[simp]

theorem MonoidAlgebra.tensorAlgEquiv_symm_single (R : Type u_1) [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (G : Type u_3) [Monoid G] (m : G) (s : S) : (tensorAlgEquiv R S G).symm (single m s) = single m 1 ⊗ₜ[R] s

instance MonoidAlgebra.isSemisimpleRing_tensor (R : Type u_1) [CommRing R] (k : Type u_2) [Field k] [Algebra R k] (G : Type u_3) [Group G] [Finite G] [NeZero ↑(Nat.card G)] : IsSemisimpleRing (TensorProduct R (MonoidAlgebra R G) k)

Maschke's theorem after base change. If k is a field in which the order of the finite group G is nonzero, then the base change R[G] ⊗[R] k of the group algebra over any commutative ring R mapping to k is a semisimple ring, being isomorphic to k[G].