The unipotent-part endomorphism of a commutative affine group

For a reduced commutative affine group of finite type over an algebraically closed field, Jordan decomposition is regular: both factors come from endomorphisms of the group scheme. This file constructs the unipotent projection as the convolution product of the inverse of the semisimple projection with the identity. Its action on base-valued points is g ↦ g_u.

The construction uses semisimplePartBialgHom, which already represents g ↦ g_s. The two endomorphisms are complementary idempotents. Their convolution product is the identity over every test algebra, including nonreduced algebras. These identities allow the semisimple and unipotent factors to be realized as closed subgroup schemes.

References

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

noncomputable def TauCeti.HopfAlgebra.Point.unipotentPartBialgHom (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 endomorphism representing the unipotent part of a reduced commutative affine group of finite type over an algebraically closed field.

theorem TauCeti.HopfAlgebra.Point.unipotentPartBialgHom_toAlgHom (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : ↑(unipotentPartBialgHom k H) = ((WithConv.toConv ↑(semisimplePartBialgHom k H))⁻¹ * WithConv.toConv (AlgHom.id k H)).ofConv

The unipotent projection is the convolution of the inverse semisimple projection and the identity.

theorem TauCeti.HopfAlgebra.Point.mapDomain_semisimplePartBialgHom_mul_mapDomain_unipotentPartBialgHom (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] {A : Type u_1} [CommSemiring A] [Algebra k A] (g : WithConv (H →ₐ[k] A)) : (semisimplePartBialgHom k H).mapDomain g * (unipotentPartBialgHom k H).mapDomain g = g

Over any test algebra, the two regular Jordan factors multiply to the original point.

theorem TauCeti.HopfAlgebra.Point.mapDomain_unipotentPartBialgHom (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)) : (unipotentPartBialgHom k H).mapDomain g = unipotentPart k H k g

The unipotent-part endomorphism represents g ↦ g_u on base-valued points.

@[simp]

theorem TauCeti.HopfAlgebra.Point.apply_unipotentPartBialgHom (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 ((unipotentPartBialgHom k H) f) = (unipotentPart k H k g).ofConv f

Evaluation of the regular unipotent projection at a base-valued point.

@[simp]

theorem TauCeti.HopfAlgebra.Point.toConv_comp_unipotentPartBialgHom (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 ↑(unipotentPartBialgHom k H)) = unipotentPart k H k g

Simp-normal form of the action of the unipotent projection on base-valued points.

theorem TauCeti.HopfAlgebra.Point.eq_unipotentPartBialgHom_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) : φ = unipotentPartBialgHom k H ↔ ∀ (g : WithConv (H →ₐ[k] k)), φ.mapDomain g = unipotentPart k H k g

The regular unipotent projection is uniquely determined by its base-valued points.

theorem TauCeti.HopfAlgebra.Point.mapDomain_unipotentPartBialgHom_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)) : (unipotentPartBialgHom k H).mapDomain g = g ↔ IsUnipotentPoint g

The unipotent projection fixes exactly the unipotent base-valued points.

theorem TauCeti.HopfAlgebra.Point.mapDomain_unipotentPartBialgHom_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)) : (unipotentPartBialgHom k H).mapDomain g = 1 ↔ IsSemisimplePoint g

The kernel of the unipotent projection on base-valued points consists exactly of the semisimple points.

@[simp]

theorem TauCeti.HopfAlgebra.Point.unipotentPartBialgHom_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] : (unipotentPartBialgHom k H).comp (unipotentPartBialgHom k H) = unipotentPartBialgHom k H

The regular unipotent projection is idempotent as a group-scheme endomorphism.

@[simp]

theorem TauCeti.HopfAlgebra.Point.unipotentPartBialgHom_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] : (unipotentPartBialgHom k H).comp (semisimplePartBialgHom k H) = (Bialgebra.unitBialgHom k H).comp (Bialgebra.counitBialgHom k H)

The semisimple projection after the unipotent projection is the trivial group-scheme endomorphism (composition reverses on coordinate algebras).

@[simp]

theorem TauCeti.HopfAlgebra.Point.semisimplePartBialgHom_comp_unipotentPartBialgHom (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 (unipotentPartBialgHom k H) = (Bialgebra.unitBialgHom k H).comp (Bialgebra.counitBialgHom k H)

The unipotent projection after the semisimple projection is the trivial group-scheme endomorphism (composition reverses on coordinate algebras).

theorem TauCeti.HopfAlgebra.Point.unipotentPartBialgHom_comp (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] {H' : Type u} [CommRing H'] [HopfAlgebra k H'] [Algebra.FiniteType k H'] [IsReduced H'] [Coalgebra.IsCocomm k H'] (φ : H →ₐc[k] H') : (unipotentPartBialgHom k H').comp φ = φ.comp (unipotentPartBialgHom k H)

The regular unipotent projection is natural in homomorphisms of reduced commutative affine groups. The equality is one of coordinate morphisms, so holds over every test algebra.