Semisimple points of a Hopf algebra

Let H be a Hopf algebra over a commutative semiring k and let K be a field equipped with a k-algebra structure. A K-valued point g : WithConv (H →ₐ[k] K) acts on the scalar extension of every finitely generated H-comodule. This file calls g semisimple when every one of those linear automorphisms is semisimple. The WithConv wrapper supplies the convolution group structure from the antipode of H; all group operations in the closure API below refer to that convolution law.

For the commutative coordinate Hopf algebra of an affine group scheme, taking K to be an algebraic closure of k gives the representation-theoretic definition of a geometric semisimple element. Semisimple points contain the identity and are closed under inverses and integer powers. Products of commuting semisimple points are semisimple over a perfect field, and semisimplicity is invariant under conjugation.

Main declarations

• TauCeti.HopfAlgebra.IsSemisimplePoint: a point acts semisimply in every finitely generated comodule.
• TauCeti.HopfAlgebra.isSemisimplePoint_iff_forall_isSemisimple_endOfPoint: the equivalent formulation using the underlying comodule action endomorphisms.
• TauCeti.HopfAlgebra.IsSemisimplePoint.inv, .mul_of_commute, and .zpow: closure under inversion, commuting products, and integer powers.
• TauCeti.HopfAlgebra.IsSemisimplePoint.mapDomain: precomposition by a bialgebra morphism preserves semisimple points.
• TauCeti.HopfAlgebra.isSemisimplePoint_mapDomain_iff: invariance of point semisimplicity under bialgebra isomorphisms.
• TauCeti.HopfAlgebra.isSemisimplePoint_pointsMulEquiv_iff: over a perfect field, a point of a product affine group is semisimple if and only if both component points are semisimple.
• TauCeti.HopfAlgebra.isSemisimplePoint_conj_iff: invariance under conjugation.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §2.4.

This supplies the intrinsic semisimple-element predicate needed by Layer 4, "Jordan decomposition", of the ReductiveGroups roadmap. It uses the representation--comodule dictionary built in Layer 1.

def TauCeti.HopfAlgebra.IsSemisimplePoint {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : Prop

A point g : WithConv (H →ₐ[k] K) of a Hopf algebra is semisimple when it acts by a semisimple linear automorphism on the scalar extension of every finitely generated comodule. The point type carries the convolution group structure supplied by the antipode of H, and the closure properties below use this group law.

When H is the commutative coordinate Hopf algebra of an affine group over k and K is an algebraic closure, this is the standard representation-theoretic definition of a geometric semisimple element.

Equations

• TauCeti.HopfAlgebra.IsSemisimplePoint g = ∀ (M : TauCeti.FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((TauCeti.Comodule.pointsAction ↑M) g)).IsSemisimple

theorem TauCeti.HopfAlgebra.isSemisimplePoint_def {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : IsSemisimplePoint g ↔ ∀ (M : FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).IsSemisimple

A point is semisimple exactly when it acts semisimply on each finitely generated comodule.

theorem TauCeti.HopfAlgebra.IsSemisimplePoint.mapDomain {k : Type u} {K : Type x} [CommSemiring k] [Field K] [Algebra k K] {H₁ : Type v} {H₂ : Type w} [Semiring H₁] [Semiring H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] {g : WithConv (H₂ →ₐ[k] K)} (hg : IsSemisimplePoint g) (φ : H₁ →ₐc[k] H₂) : IsSemisimplePoint ((AlgHom.mapDomain φ) g)

Precomposition by a bialgebra morphism preserves semisimple points. For commutative coordinate Hopf algebras, this says that a homomorphism of affine groups sends semisimple points to semisimple points.

theorem TauCeti.HopfAlgebra.isSemisimplePoint_mapDomain_iff {k : Type u} {K : Type x} [CommSemiring k] [Field K] [Algebra k K] {H₁ : Type v} {H₂ : Type w} [Semiring H₁] [Semiring H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] (e : H₁ ≃ₐc[k] H₂) (g : WithConv (H₂ →ₐ[k] K)) : IsSemisimplePoint ((AlgHom.mapDomain ↑e) g) ↔ IsSemisimplePoint g

Semisimplicity of points is invariant under precomposition by a bialgebra isomorphism.

theorem TauCeti.HopfAlgebra.isSemisimplePoint_iff_forall_isSemisimple_endOfPoint {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : IsSemisimplePoint g ↔ ∀ (M : FGComoduleCat k H), Module.End.IsSemisimple (Comodule.endOfPoint (↑M) g.ofConv)

A point is semisimple exactly when each underlying point-action endomorphism is semisimple.

@[simp]

theorem TauCeti.HopfAlgebra.isSemisimplePoint_one {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] : IsSemisimplePoint 1

The identity point is semisimple.

theorem TauCeti.HopfAlgebra.IsSemisimplePoint.inv {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] {g : WithConv (H →ₐ[k] K)} (hg : IsSemisimplePoint g) : IsSemisimplePoint g⁻¹

The inverse of a semisimple point is semisimple.

@[simp]

theorem TauCeti.HopfAlgebra.isSemisimplePoint_inv_iff {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : IsSemisimplePoint g⁻¹ ↔ IsSemisimplePoint g

A point is semisimple if and only if its inverse is semisimple.

theorem TauCeti.HopfAlgebra.IsSemisimplePoint.pow {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] {g : WithConv (H →ₐ[k] K)} (hg : IsSemisimplePoint g) (n : ℕ) : IsSemisimplePoint (g ^ n)

Every natural power of a semisimple point is semisimple.

theorem TauCeti.HopfAlgebra.IsSemisimplePoint.zpow {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] {g : WithConv (H →ₐ[k] K)} (hg : IsSemisimplePoint g) (n : ℤ) : IsSemisimplePoint (g ^ n)

Every integer power of a semisimple point is semisimple.

@[simp]

theorem TauCeti.HopfAlgebra.isSemisimplePoint_conj_iff {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] (g h : WithConv (H →ₐ[k] K)) : IsSemisimplePoint (h * g * h⁻¹) ↔ IsSemisimplePoint g

Semisimplicity of points is invariant under conjugation.

theorem TauCeti.HopfAlgebra.IsSemisimplePoint.mul_of_commute {k : Type u} {H : Type v} {K : Type x} [CommSemiring k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hg : IsSemisimplePoint g) (hh : IsSemisimplePoint h) (hcomm : Commute g h) : IsSemisimplePoint (g * h)

The product of two commuting semisimple points is semisimple.

@[simp]

theorem TauCeti.HopfAlgebra.isSemisimplePoint_pointsMulEquiv_iff {k : Type u} {K : Type x} [CommSemiring k] [Field K] [Algebra k K] {H₁ H₂ : Type v} [CommSemiring H₁] [CommSemiring H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [PerfectField K] (g : WithConv (TensorProduct k H₁ H₂ →ₐ[k] K)) : IsSemisimplePoint g ↔ IsSemisimplePoint (AffineGroup.Product.pointsMulEquiv g).1 ∧ IsSemisimplePoint (AffineGroup.Product.pointsMulEquiv g).2

Over a perfect field, a point of a product affine group is semisimple exactly when both factor points are semisimple.