Conjugation in Hopf-algebra coordinates #
For a commutative Hopf algebra H over a commutative semiring R, this file constructs the
algebra morphism H →ₐ[R] H ⊗[R] H representing the left conjugation action
(g, x) ↦ g * x * g⁻¹. The first tensor factor is the conjugating variable and the second is
the acted-on variable.
The construction uses the convolution group of points: if i₁(h) = h ⊗ₜ 1 and
i₂(h) = 1 ⊗ₜ h are the two universal tensor-factor points, then the coordinate morphism
is the underlying algebra map of i₁ * i₂ * i₁⁻¹. Its characteristic theorem says that
post-composing with Algebra.TensorProduct.productMap g x gives the point g * x * g⁻¹.
The identity and associativity theorems record that this morphism is the coordinate form of a left group action. No bialgebra-morphism structure is asserted: joint conjugation is not generally a group homomorphism from the product.
Main declarations #
TauCeti.HopfAlgebra.conjugationAlgHom: the coordinate algebra morphism of left conjugation.TauCeti.HopfAlgebra.tensorProduct_map_comp_conjugationAlgHom: the coordinate conjugation morphism is natural in the Hopf algebra.TauCeti.HopfAlgebra.productMap_comp_conjugationAlgHom: evaluation at arbitrary algebra-valued points.TauCeti.HopfAlgebra.conjugationAlgHom_counit_left: the identity element acts trivially.TauCeti.HopfAlgebra.conjugationAlgHom_counit_right: conjugation fixes the identity element.TauCeti.HopfAlgebra.conjugationAlgHom_coassoc: the coordinate action-associativity law.
References #
The orientation follows J. S. Milne, Algebraic Groups (2017), §3.5 and §10.20, where
Ad(g)(x) = g x g⁻¹. The adjoint-coaction action structure is also described in
I. Heckenberger and H.-J. Schneider, Hopf Algebras and Root Systems, §3.7. This is the
conjugation/adjoint-morphism prerequisite in Layer 3, “Normality and quotients”, of
TauCetiRoadmap/ReductiveGroups/README.md.
The coordinate algebra morphism of the left conjugation action.
The first tensor factor is the conjugating variable and the second is the acted-on variable.
As a universal point, this is i₁ * i₂ * i₁⁻¹, so on algebra-valued points it represents
(g, x) ↦ g * x * g⁻¹.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coordinate morphism of left conjugation is the convolution product of the two universal tensor-factor points and the inverse of the first.
Evaluating the coordinate morphism of left conjugation at two algebra-valued points gives their group-theoretic conjugate.
Here g is the conjugating point and x is the acted-on point. The product map sends a pure
tensor h ⊗ₜ k to g(h) * x(k).
Evaluation against an arbitrary algebra map out of the tensor square. Every algebra map
φ : H ⊗[R] H →ₐ[R] A is the product map of its two restrictions, so composing it with the
conjugation morphism conjugates the second restriction by the first. This is the restriction form
of productMap_comp_conjugationAlgHom, which needs φ presented as a product map.
The coordinate morphism of conjugation is natural in the commutative Hopf algebra.
The identity point acts trivially by conjugation. This is the pointwise product-map form of the left-unit law for the coordinate action.
Conjugation fixes the identity point.
Under the canonical left-unit identification, applying the counit to the conjugating
coordinate makes conjugation the identity. This is the coordinate identity-action law
(ε ⊗ id) ∘ c♯ = id.
Under the canonical right-unit identification, applying the counit to the acted-on coordinate gives the identity point. This is the coordinate formula saying that conjugation fixes the group identity.
The coordinate morphism of left conjugation satisfies the action-associativity law.
The left side represents conjugation by the product of the first two universal points, while the right side represents successive conjugation by the second and then the first. The tensor associator identifies their common target.