Tensor products of invariant group algebras

For a finite Galois extension L/k, the tensor square over k of the invariant group algebra is the invariant subalgebra of the tensor square over L of the split group algebra. The comparison sends x ⊗ y to the tensor of their inclusions. Its inverse converts the invariant-valued comultiplication into a comultiplication with values in the tensor square of the descended algebra.

There is no finite-generation assumption on the exponent group and no characteristic restriction. The proof uses the scalar-extension equivalence for the invariant group algebra and the compatibility of scalar extension with tensor products.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.23 and Appendix A.64.

noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsTensorEquiv {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) : TensorProduct k ↥(groupAlgebraInvariants rho) ↥(groupAlgebraInvariants rho) ≃ₐ[k] ↥(groupAlgebraTensorInvariants rho)

The tensor square of the descended group algebra is the invariant subalgebra of the split tensor square, for the diagonal semilinear Galois action.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsTensorEquiv_tmul {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (x y : ↥(groupAlgebraInvariants rho)) : ↑((groupAlgebraInvariantsTensorEquiv rho) (x ⊗ₜ[k] y)) = ↑x ⊗ₜ[L] ↑y

The tensor descent equivalence sends a pure tensor to the tensor of its inclusions.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraInvariantsTensorEquiv_symm_tmul {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (x y : ↥(groupAlgebraInvariants rho)) (h : ↑x ⊗ₜ[L] ↑y ∈ groupAlgebraTensorInvariants rho) : (groupAlgebraInvariantsTensorEquiv rho).symm ⟨↑x ⊗ₜ[L] ↑y, h⟩ = x ⊗ₜ[k] y

The inverse comparison recovers the tensor of invariant elements from their ambient tensor, independently of the proof of invariance.