The semisimple-part endomorphism of a commutative affine group

Let H be the coordinate Hopf algebra of an affine group over a field k. A character of the group, that is, a group-like element c ∈ H, cannot distinguish a point from its semisimple part: c(g_s) = c(g). Indeed c is a homomorphism to a diagonalizable group, Jordan decomposition is natural, and every point of a diagonalizable group is semisimple.

Now let k be algebraically closed and let H be reduced, of finite type, and cocommutative, so that H represents a reduced commutative affine group G. In each finite-dimensional representation the semisimple parts of the points form a commuting family of semisimple operators. Every joint eigenspace of this family is stable under all points, hence a subcomodule, hence contains a weight vector; so each joint eigenvalue function is a character. Thus every matrix coefficient of g ↦ g_s is a linear combination of characters, and in particular is a regular function on G. Since H is reduced, its points separate its elements, and these regular functions assemble into a bialgebra endomorphism σ of H with g ∘ σ = g_s for every point g: the map g ↦ g_s is an endomorphism of the affine group G.

The endomorphism σ is idempotent and its image is the span of the group-like elements, the coordinate ring of the diagonalizable quotient of G. On points it fixes exactly the semisimple points and kills exactly the unipotent points. It is the input for realizing the semisimple and unipotent points as closed subgroups G_s and G_u with G ≅ G_s × G_u.

Reducedness is what makes points determine the endomorphism: in characteristic p, the only point of αₚ is the identity, so the identity and the trivial endomorphism of its coordinate ring both induce g ↦ g_s.

Main declarations

• TauCeti.HopfAlgebra.Point.semisimplePart_apply_of_isGroupLikeElem: characters take the same value on a point and on its semisimple part.
• TauCeti.HopfAlgebra.Point.iSup_iInf_eigenspace_semisimplePart_eq_top: in a finite-dimensional representation of a reduced commutative affine group, the semisimple parts of the points are simultaneously diagonalizable with characters as eigenvalues.
• TauCeti.HopfAlgebra.Point.exists_mem_groupLikeSetSpan_forall_apply_eq: every coordinate function evaluated at semisimple parts is a linear combination of characters.
• TauCeti.HopfAlgebra.Point.semisimplePartBialgHom: the semisimple-part endomorphism.
• TauCeti.HopfAlgebra.Point.mapDomain_semisimplePartBialgHom and TauCeti.HopfAlgebra.Point.eq_semisimplePartBialgHom_iff: its defining property on points and the resulting characterization.
• TauCeti.HopfAlgebra.Point.range_semisimplePartBialgHom and TauCeti.HopfAlgebra.Point.semisimplePartBialgHom_comp_self: it is an idempotent projection onto the span of the group-like elements.
• TauCeti.HopfAlgebra.Point.mapDomain_semisimplePartBialgHom_eq_self_iff and TauCeti.HopfAlgebra.Point.mapDomain_semisimplePartBialgHom_eq_one_iff: its fixed points are the semisimple points and its kernel consists of the unipotent points.

References

• A. Borel, Linear Algebraic Groups, §4.7.
• T. A. Springer, Linear Algebraic Groups, §§2.4 and 3.1.

theorem TauCeti.HopfAlgebra.Point.semisimplePart_apply_of_isGroupLikeElem (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) {c : H} (hc : IsGroupLikeElem k c) : (semisimplePart k H K g).ofConv c = g.ofConv c

Characters do not see unipotent parts. A group-like element of the coordinate Hopf algebra takes the same value on a point and on its semisimple part.

theorem TauCeti.HopfAlgebra.Point.basePointsRepresentation_semisimplePart_of_mem_weightSpace (k H : Type u) [Field k] [CommRing H] [HopfAlgebra k H] {M : Type u} [AddCommGroup M] [Module k M] [Comodule k H M] [PerfectField k] (g : WithConv (H →ₐ[k] k)) {c : GroupLike k H} {v : M} (hv : v ∈ c.weightSpace) : ((Comodule.basePointsRepresentation M) (semisimplePart k H k g)) v = g.ofConv ↑c • v

The semisimple part of a base-valued point acts on a vector of group-like weight c by the scalar g c.

theorem TauCeti.HopfAlgebra.Point.iSup_iInf_eigenspace_semisimplePart_eq_top {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (M : Type u) [AddCommGroup M] [Module k M] [Comodule k H M] [FiniteDimensional k M] : ⨆ (c : GroupLike k H), ⨅ (g : WithConv (H →ₐ[k] k)), ((Comodule.basePointsRepresentation M) (semisimplePart k H k g)).eigenspace (g.ofConv ↑c) = ⊤

Semisimple parts are simultaneously diagonalizable by characters. In a finite-dimensional representation of a reduced commutative affine group of finite type over an algebraically closed field, the representation is spanned by the joint eigenspaces of the semisimple parts of the points, and on each of them the semisimple part of g acts by g c for a character c.

theorem TauCeti.HopfAlgebra.Point.exists_mem_groupLikeSetSpan_forall_apply_eq {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (f : H) : ∃ h ∈ Subcoalgebra.groupLikeSetSpan Set.univ, ∀ (g : WithConv (H →ₐ[k] k)), g.ofConv h = (semisimplePart k H k g).ofConv f

The semisimple part is a regular function of the point. For a reduced commutative affine group of finite type over an algebraically closed field, every coordinate function evaluated on semisimple parts, g ↦ f(g_s), is given by an element of the span of the characters.

noncomputable def TauCeti.HopfAlgebra.Point.semisimplePartBialgHom (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : H →ₐc[k] H

The semisimple-part endomorphism of a commutative affine group. For a reduced commutative affine group of finite type over an algebraically closed field, this is the bialgebra endomorphism of the coordinate Hopf algebra representing the group endomorphism g ↦ g_s; see mapDomain_semisimplePartBialgHom.

@[simp]

theorem TauCeti.HopfAlgebra.Point.apply_semisimplePartBialgHom {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (g : WithConv (H →ₐ[k] k)) (f : H) : g.ofConv ((semisimplePartBialgHom k H) f) = (semisimplePart k H k g).ofConv f

The semisimple-part endomorphism represents g ↦ g_s.

theorem TauCeti.HopfAlgebra.Point.mapDomain_semisimplePartBialgHom {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (g : WithConv (H →ₐ[k] k)) : (semisimplePartBialgHom k H).mapDomain g = semisimplePart k H k g

Precomposition with the semisimple-part endomorphism sends every point to its semisimple part.

@[simp]

theorem TauCeti.HopfAlgebra.Point.toConv_comp_semisimplePartBialgHom {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (g : WithConv (H →ₐ[k] k)) : WithConv.toConv (g.ofConv.comp ↑(semisimplePartBialgHom k H)) = semisimplePart k H k g

Simp-normal form of mapDomain_semisimplePartBialgHom, written after normalization by BialgHom.mapDomain_apply.

theorem TauCeti.HopfAlgebra.Point.eq_semisimplePartBialgHom_iff {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (φ : H →ₐc[k] H) : φ = semisimplePartBialgHom k H ↔ ∀ (g : WithConv (H →ₐ[k] k)), φ.mapDomain g = semisimplePart k H k g

The semisimple-part endomorphism is the unique bialgebra endomorphism representing g ↦ g_s.

theorem TauCeti.HopfAlgebra.Point.semisimplePartBialgHom_mem_groupLikeSetSpan {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (f : H) : (semisimplePartBialgHom k H) f ∈ Subcoalgebra.groupLikeSetSpan Set.univ

The semisimple-part endomorphism takes values in the span of the characters.

theorem TauCeti.HopfAlgebra.Point.semisimplePartBialgHom_apply_of_isGroupLikeElem {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] {c : H} (hc : IsGroupLikeElem k c) : (semisimplePartBialgHom k H) c = c

The semisimple-part endomorphism fixes every character.

theorem TauCeti.HopfAlgebra.Point.semisimplePartBialgHom_apply_of_mem_groupLikeSetSpan {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] {f : H} (hf : f ∈ Subcoalgebra.groupLikeSetSpan Set.univ) : (semisimplePartBialgHom k H) f = f

The semisimple-part endomorphism fixes the span of the characters.

theorem TauCeti.HopfAlgebra.Point.range_semisimplePartBialgHom {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : (↑(semisimplePartBialgHom k H)).range = (Subcoalgebra.groupLikeSetSpan Set.univ).toSubmodule

The semisimple-part endomorphism projects onto the characters. Its range is the span of the group-like elements, the coordinate ring of the diagonalizable quotient.

@[simp]

theorem TauCeti.HopfAlgebra.Point.semisimplePartBialgHom_comp_self {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : (semisimplePartBialgHom k H).comp (semisimplePartBialgHom k H) = semisimplePartBialgHom k H

The semisimple-part endomorphism is idempotent.

theorem TauCeti.HopfAlgebra.Point.mapDomain_semisimplePartBialgHom_eq_self_iff {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (g : WithConv (H →ₐ[k] k)) : (semisimplePartBialgHom k H).mapDomain g = g ↔ IsSemisimplePoint g

The points fixed by the semisimple-part endomorphism are exactly the semisimple points.

theorem TauCeti.HopfAlgebra.Point.mapDomain_semisimplePartBialgHom_eq_one_iff {k H : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (g : WithConv (H →ₐ[k] k)) : (semisimplePartBialgHom k H).mapDomain g = 1 ↔ IsUnipotentPoint g

The kernel of the semisimple-part endomorphism on points consists exactly of the unipotent points.