Documentation

TauCeti.Algebra.AlgebraicGroup.GroupAlgebra.Galois.Splitting

Splitting the descended group algebra #

For a finite Galois extension L/k and an integral representation on an abelian group M, scalar extension of the invariant coordinate Hopf algebra recovers L[M] as a bialgebra. The equivalence sends a ⊗ x to a • x. Thus it identifies the descended affine group after extension to its splitting field with the diagonalizable group of M.

The underlying algebra equivalence is groupAlgebraInvariantsBaseChangeEquiv. We prove that it respects the descended counit and comultiplication, using groupAlgebraInvariantsTensorEquiv to compare the tensor squares. Neither finite generation of M nor a restriction on the characteristic is needed.

References #

source
noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeBialgEquiv {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 L ↥(groupAlgebraInvariants rho) ≃ₐc[L] MonoidAlgebra L (Multiplicative M)

Extending the descended group algebra to its splitting field recovers the split group algebra as a bialgebra, with the standard scalar-extension Hopf structure on the source.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeBialgEquiv_toAlgEquiv {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) :
    (groupAlgebraInvariantsBaseChangeBialgEquiv rho).toAlgEquiv = groupAlgebraInvariantsBaseChangeEquiv rho

    Forgetting the coalgebra structure recovers the scalar-extension algebra equivalence.

    source
    @[simp]
    theorem TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeBialgEquiv_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) (a : L) (x : ↥(groupAlgebraInvariants rho)) :
    (groupAlgebraInvariantsBaseChangeBialgEquiv rho) (a ⊗ₜ[k] x) = a • ↑x

    On pure tensors the splitting isomorphism is scalar multiplication.

    source
    @[simp]
    theorem TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeBialgEquiv_symm_apply {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 : ↥(groupAlgebraInvariants rho)) :
    (groupAlgebraInvariantsBaseChangeBialgEquiv rho).symm ↑x = 1 ⊗ₜ[k] x

    An invariant split element corresponds to its tensor with one under the inverse splitting.

    source
    @[simp]
    theorem TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeBialgEquiv_smul {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) (sigma : Gal(L/k)) (x : TensorProduct k L ↥(groupAlgebraInvariants rho)) :
    (groupAlgebraInvariantsBaseChangeBialgEquiv rho) (sigma • x) = ((groupAlgebraAction rho) sigma) ((groupAlgebraInvariantsBaseChangeBialgEquiv rho) x)

    The splitting identifies the scalar-factor Galois action on the base change with the simultaneous coefficient and exponent action on the split group algebra.