Reconstructing a group from its Galois module of characters

Let H be a commutative Hopf algebra over k which becomes spanned by group-like elements over a finite Galois extension L/k. Its coordinate algebra is recovered from the invariants of the group algebra on its characters over L, with the simultaneous Galois action on coefficients and characters. In particular this applies to tori split by L.

The comparison is canonical: after extension to L, it is inverse to evaluation of formal characters at their group-like values.

References

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

noncomputable def TauCeti.GaloisDescent.characterGroupAlgebraInvariantsEquiv (k : Type u_1) (L : Type u_2) (H : Type u_3) [Field k] [Field L] [Algebra k L] [CommRing H] [HopfAlgebra k H] (hspan : Submodule.span L (Set.range GroupLike.val) = ⊤) [IsGalois k L] [FiniteDimensional k L] : H ≃ₐc[k] ↥(groupAlgebraInvariants (Representation.ofMulDistribMulAction Gal(L/k) (GroupLike L (TensorProduct k L H))))

A commutative Hopf algebra split by a finite Galois extension is the invariant group algebra of its characters, with their natural Galois action. The comparison preserves both algebra and coalgebra structure, hence also the antipode.

Equations

• TauCeti.GaloisDescent.characterGroupAlgebraInvariantsEquiv k L H hspan = BialgEquiv.ofBijective (BialgHom.ofAlgHom (TauCeti.GaloisDescent.characterInvariantsAlgHom✝ k L H hspan) ⋯ ⋯) ⋯

@[simp]

theorem TauCeti.GaloisDescent.characterGroupAlgebraInvariantsEquiv_evaluation (k : Type u_1) (L : Type u_2) (H : Type u_3) [Field k] [Field L] [Algebra k L] [CommRing H] [HopfAlgebra k H] (hspan : Submodule.span L (Set.range GroupLike.val) = ⊤) [IsGalois k L] [FiniteDimensional k L] (a : H) : (GroupLike.evaluationBialgHom L (TensorProduct k L H)) ((MonoidAlgebra.domCongr L L (MulEquiv.multiplicativeAdditive (GroupLike L (TensorProduct k L H)))) ↑((characterGroupAlgebraInvariantsEquiv k L H hspan) a)) = 1 ⊗ₜ[k] a

Evaluation of the character expansion recovers the scalar extension of the original element. This characterizes the reconstruction without choosing a basis of characters.

@[simp]

theorem TauCeti.GaloisDescent.characterGroupAlgebraInvariantsEquiv_symm_evaluation (k : Type u_1) (L : Type u_2) (H : Type u_3) [Field k] [Field L] [Algebra k L] [CommRing H] [HopfAlgebra k H] (hspan : Submodule.span L (Set.range GroupLike.val) = ⊤) [IsGalois k L] [FiniteDimensional k L] (x : ↥(groupAlgebraInvariants (Representation.ofMulDistribMulAction Gal(L/k) (GroupLike L (TensorProduct k L H))))) : 1 ⊗ₜ[k] (characterGroupAlgebraInvariantsEquiv k L H hspan).symm x = (GroupLike.evaluationBialgHom L (TensorProduct k L H)) ((MonoidAlgebra.domCongr L L (MulEquiv.multiplicativeAdditive (GroupLike L (TensorProduct k L H)))) ↑x)

The inverse reconstruction evaluates an invariant formal character expansion in the original Hopf algebra. Its scalar extension is ordinary evaluation.