The commutator morphism in Hopf-algebra coordinates

For a commutative Hopf algebra H over a commutative semiring R, this file constructs the algebra morphism

H ⟶ H ⊗[R] H

representing the group commutator (g, h) ↦ g * h * g⁻¹ * h⁻¹. If i₁ and i₂ are the two universal points with values in H ⊗[R] H, the morphism is the algebra map underlying the convolution point i₁ * i₂ * i₁⁻¹ * i₂⁻¹.

The commutator is not generally a group homomorphism from the product, so this construction is an algebra morphism rather than a bialgebra morphism. Its kernel nevertheless determines the smallest closed subgroup scheme containing the image, constructed in TauCeti.Algebra.AlgebraicGroup.Derived.Basic.

Main declarations

• TauCeti.HopfAlgebra.commutatorAlgHom: the coordinate algebra morphism of the commutator.
• TauCeti.HopfAlgebra.map_comp_commutatorAlgHom: commutators commute with a Hopf-algebra morphism.
• TauCeti.HopfAlgebra.productMap_comp_commutatorAlgHom: evaluation at two algebra-valued points.

References

• J. S. Milne, Algebraic Groups (2017), §6d.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 10.

This is the coordinate prerequisite for the derived group G_der in Layer 6 of the ReductiveGroups roadmap.

noncomputable def TauCeti.HopfAlgebra.commutatorAlgHom {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] : H →ₐ[R] TensorProduct R H H

The coordinate algebra morphism of the group commutator (g, h) ↦ g * h * g⁻¹ * h⁻¹.

The two tensor factors are the two commutator variables, in that order.

Equations

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

theorem TauCeti.HopfAlgebra.toConv_commutatorAlgHom {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] : WithConv.toConv commutatorAlgHom = WithConv.toConv ↑Bialgebra.TensorProduct.includeLeft * WithConv.toConv ↑Bialgebra.TensorProduct.includeRight * (WithConv.toConv ↑Bialgebra.TensorProduct.includeLeft)⁻¹ * (WithConv.toConv ↑Bialgebra.TensorProduct.includeRight)⁻¹

The commutator coordinate morphism is the convolution commutator of the two universal tensor-factor points.

theorem TauCeti.HopfAlgebra.map_comp_commutatorAlgHom {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] {K : Type w} [CommSemiring K] [HopfAlgebra R K] (f : H →ₐc[R] K) : (↑(Bialgebra.TensorProduct.map f f)).comp commutatorAlgHom = commutatorAlgHom.comp ↑f

The coordinate morphism of the commutator is natural under morphisms of commutative Hopf algebras. This is the coordinate form of f([g, h]) = [f(g), f(h)].

@[simp]

theorem TauCeti.HopfAlgebra.productMap_comp_commutatorAlgHom {R : Type u} {H : Type v} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] {A : Type w} [CommSemiring A] [Algebra R A] (g h : WithConv (H →ₐ[R] A)) : (Algebra.TensorProduct.productMap g.ofConv h.ofConv).comp commutatorAlgHom = ⁅g, h⁆.ofConv

Evaluating the commutator coordinate morphism at two algebra-valued points gives their group-theoretic commutator.