Automorphism actions on group algebras

Let L be a k-algebra and let its group of k-algebra automorphisms act linearly on an abelian group M through a representation rho. The coordinate algebra L[Multiplicative M] of the diagonalizable group D(M) admits a simultaneous action on coefficients and exponents:

σ ⬝ (a X^m) = σ(a) X^(ρ(σ) m).

This file constructs that action by k-algebra automorphisms and records both its coefficient formula and its semilinearity over L, together with its compatibility with the counit, comultiplication, and antipode. The construction needs no Galois hypothesis. For a finite Galois extension L/k, it supplies the semilinear descent datum used to descend D(M); when M is a finite-rank free lattice, D(M) is a split torus.

Main declarations

• TauCeti.GaloisDescent.groupAlgebraAction: the automorphism action on the group algebra by k-algebra automorphisms.
• TauCeti.GaloisDescent.groupAlgebraAction_single: its value on a monomial.
• TauCeti.GaloisDescent.coeff_groupAlgebraAction: its coefficient formula.
• TauCeti.GaloisDescent.groupAlgebraAction_smul: semilinearity over the coefficient algebra.
• Representation.IntertwiningMap.groupAlgebraAction_mapDomainBialgHom: compatibility with equivariant exponent maps.
• TauCeti.GaloisDescent.groupAlgebraActionSemilinearEquiv: the semilinear action.
• TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv: its tensor-square action.
• TauCeti.GaloisDescent.counit_groupAlgebraAction: compatibility with the counit.
• TauCeti.GaloisDescent.comul_groupAlgebraAction: compatibility with comultiplication.
• TauCeti.GaloisDescent.antipode_groupAlgebraAction: compatibility with the antipode.

References

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

Taking invariants of this action and identifying their scalar extension with the original split coordinate Hopf algebra recovers the descended group.

noncomputable def TauCeti.GaloisDescent.groupAlgebraAction {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [Semiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) : (L ≃ₐ[k] L) →* MonoidAlgebra L (Multiplicative M) ≃ₐ[k] MonoidAlgebra L (Multiplicative M)

The simultaneous coefficient and exponent action, bundled as a homomorphism to the group of k-algebra automorphisms. For finite Galois L/k, this is a semilinear descent datum.

Equations

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

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraAction_single {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [Semiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (m : Multiplicative M) (a : L) : ((groupAlgebraAction rho) sigma) (MonoidAlgebra.single m a) = MonoidAlgebra.single (Multiplicative.ofAdd ((rho sigma) (Multiplicative.toAdd m))) (sigma a)

The bundled automorphism action sends a monomial by acting on its coefficient and exponent.

@[simp]

theorem TauCeti.GaloisDescent.coeff_groupAlgebraAction {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [Semiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x : MonoidAlgebra L (Multiplicative M)) (m : Multiplicative M) : (((groupAlgebraAction rho) sigma) x).coeff m = sigma (x.coeff (Multiplicative.ofAdd ((rho sigma⁻¹) (Multiplicative.toAdd m))))

The coefficient formula for the bundled automorphism action.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraAction_smul {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [Semiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (a : L) (x : MonoidAlgebra L (Multiplicative M)) : ((groupAlgebraAction rho) sigma) (a • x) = sigma a • ((groupAlgebraAction rho) sigma) x

The automorphism action is semilinear over L: scalars are twisted by the same automorphism.

noncomputable def TauCeti.GaloisDescent.groupAlgebraActionSemilinearEquiv {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [Semiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) : MonoidAlgebra L (Multiplicative M) ≃ₛₗ[↑sigma.toRingEquiv] MonoidAlgebra L (Multiplicative M)

The automorphism action packaged as a semilinear equivalence over its automorphism of L.

Consumers stating this type should use open scoped TauCeti.GaloisDescent to activate the inverse-pair instances associated to a ring equivalence.

Equations

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

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraActionSemilinearEquiv_apply {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [Semiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x : MonoidAlgebra L (Multiplicative M)) : (groupAlgebraActionSemilinearEquiv rho sigma) x = ((groupAlgebraAction rho) sigma) x

The underlying map of the semilinear equivalence is the bundled automorphism action.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraActionSemilinearEquiv_symm_apply {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [Semiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x : MonoidAlgebra L (Multiplicative M)) : (groupAlgebraActionSemilinearEquiv rho sigma).symm x = ((groupAlgebraAction rho) sigma⁻¹) x

The inverse semilinear equivalence is the action of the inverse automorphism.

@[simp]

theorem Representation.IntertwiningMap.groupAlgebraAction_mapDomainBialgHom {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] {N : Type u_4} [AddCommGroup N] {rho : Representation ℤ (L ≃ₐ[k] L) M} {tau : Representation ℤ (L ≃ₐ[k] L) N} (f : rho.IntertwiningMap tau) (sigma : L ≃ₐ[k] L) (x : MonoidAlgebra L (Multiplicative M)) : ((TauCeti.GaloisDescent.groupAlgebraAction tau) sigma) ((MonoidAlgebra.mapDomainBialgHom L (AddMonoidHom.toMultiplicative f.toAddMonoidHom)) x) = (MonoidAlgebra.mapDomainBialgHom L (AddMonoidHom.toMultiplicative f.toAddMonoidHom)) (((TauCeti.GaloisDescent.groupAlgebraAction rho) sigma) x)

The map of split group algebras induced by an equivariant exponent map commutes with the simultaneous Galois action on coefficients and exponents.

noncomputable def TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) : TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M)) ≃ₛₗ[↑sigma.toRingEquiv] TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M))

On the tensor square of the coordinate algebra, the automorphism acts on both tensor factors.

Equations

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

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv_tmul {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x y : MonoidAlgebra L (Multiplicative M)) : (groupAlgebraTensorActionSemilinearEquiv rho sigma) (x ⊗ₜ[L] y) = ((groupAlgebraAction rho) sigma) x ⊗ₜ[L] ((groupAlgebraAction rho) sigma) y

The semilinear tensor action evaluates on a pure tensor by acting on both factors.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv_smul {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (a : L) (t : TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M))) : (groupAlgebraTensorActionSemilinearEquiv rho sigma) (a • t) = sigma a • (groupAlgebraTensorActionSemilinearEquiv rho sigma) t

The tensor-square action is semilinear over the coefficient algebra.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv_map_one {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) : (groupAlgebraTensorActionSemilinearEquiv rho sigma) 1 = 1

The tensor-square action preserves the multiplicative identity.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv_map_mul {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x y : TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M))) : (groupAlgebraTensorActionSemilinearEquiv rho sigma) (x * y) = (groupAlgebraTensorActionSemilinearEquiv rho sigma) x * (groupAlgebraTensorActionSemilinearEquiv rho sigma) y

The tensor-square action preserves multiplication.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv_one {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (t : TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M))) : (groupAlgebraTensorActionSemilinearEquiv rho 1) t = t

The tensor-square action of the identity automorphism is the identity.

@[simp]

theorem TauCeti.GaloisDescent.groupAlgebraTensorActionSemilinearEquiv_mul {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma tau : L ≃ₐ[k] L) (t : TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M))) : (groupAlgebraTensorActionSemilinearEquiv rho (sigma * tau)) t = (groupAlgebraTensorActionSemilinearEquiv rho sigma) ((groupAlgebraTensorActionSemilinearEquiv rho tau) t)

The tensor-square action of a product is the composite of the two actions.

@[simp]

theorem TauCeti.GaloisDescent.counit_groupAlgebraAction {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x : MonoidAlgebra L (Multiplicative M)) : CoalgebraStruct.counit (((groupAlgebraAction rho) sigma) x) = sigma (CoalgebraStruct.counit x)

The automorphism action commutes with the counit, with the scalar output acted on by the automorphism.

@[simp]

theorem TauCeti.GaloisDescent.antipode_groupAlgebraAction {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x : MonoidAlgebra L (Multiplicative M)) : (HopfAlgebraStruct.antipode L) (((groupAlgebraAction rho) sigma) x) = ((groupAlgebraAction rho) sigma) ((HopfAlgebraStruct.antipode L) x)

The automorphism action commutes with the antipode.

@[simp]

theorem TauCeti.GaloisDescent.comul_groupAlgebraAction {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring k] [AddCommGroup M] [CommSemiring L] [Algebra k L] (rho : Representation ℤ (L ≃ₐ[k] L) M) (sigma : L ≃ₐ[k] L) (x : MonoidAlgebra L (Multiplicative M)) : CoalgebraStruct.comul (((groupAlgebraAction rho) sigma) x) = (groupAlgebraTensorActionSemilinearEquiv rho sigma) (CoalgebraStruct.comul x)

The semilinear automorphism action commutes with comultiplication after acting on both tensor factors.