Closed Jordan factors of commutative affine groups

For a reduced commutative affine group of finite type over an algebraically closed field, the images of the regular Jordan projections are smooth closed subgroup schemes. Their base-field points are exactly the semisimple and unipotent points, respectively. The semisimple factor is diagonalizable, and is a torus when the ambient group is connected; the unipotent factor is geometrically unipotent. This is the commutative splitting used in the structure theory of solvable affine groups.

Over every commutative test algebra, the two closed factors are the fixed subgroups of the projections, and multiplication gives a unique factorization into these subgroups. The test-algebra universe is independent of the base-field and coordinate-algebra universe. For nonreduced test algebras, these are scheme-theoretic Jordan factors; no assertion of operator semisimplicity over such algebras is made.

The construction uses the regular projections semisimplePartBialgHom and unipotentPartBialgHom and the coordinate image factorization CommHopfAlgCat.image.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.HopfAlgebra.Point.semisimpleFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : CommHopfAlgCat k

The coordinate Hopf algebra of the closed semisimple factor, the image of the regular semisimple projection.

@[reducible, inline]

noncomputable abbrev TauCeti.HopfAlgebra.Point.unipotentFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : CommHopfAlgCat k

The coordinate Hopf algebra of the closed unipotent factor, the image of the regular unipotent projection.

instance TauCeti.HopfAlgebra.Point.instIsCocommSemisimpleFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : Coalgebra.IsCocomm k ↑(semisimpleFactor k H)

The closed semisimple factor is commutative.

instance TauCeti.HopfAlgebra.Point.instIsCocommUnipotentFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : Coalgebra.IsCocomm k ↑(unipotentFactor k H)

The closed unipotent factor is commutative.

instance TauCeti.HopfAlgebra.Point.instSmoothSemisimpleFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : Algebra.Smooth k ↑(semisimpleFactor k H)

The closed semisimple factor is smooth.

instance TauCeti.HopfAlgebra.Point.instSmoothUnipotentFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : Algebra.Smooth k ↑(unipotentFactor k H)

The closed unipotent factor is smooth.

@[simp]

theorem TauCeti.HopfAlgebra.Point.mem_quotientPointsSubgroup_ker_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] (A : CommAlgCat k) (g : WithConv (H →ₐ[k] ↑A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (semisimplePartBialgHom k H)) A ↔ (semisimplePartBialgHom k H).mapDomain g = g

The closed semisimple factor represents fixed points of the regular semisimple projection over every test algebra.

@[simp]

theorem TauCeti.HopfAlgebra.Point.mem_quotientPointsSubgroup_ker_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] (A : CommAlgCat k) (g : WithConv (H →ₐ[k] ↑A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (unipotentPartBialgHom k H)) A ↔ (unipotentPartBialgHom k H).mapDomain g = g

The closed unipotent factor represents fixed points of the regular unipotent projection over every test algebra.

@[simp]

theorem TauCeti.HopfAlgebra.Point.mem_quotientPointsSubgroup_ker_semisimplePartBialgHom_base_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)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (semisimplePartBialgHom k H)) ↧k ↔ IsSemisimplePoint g

The base-field points of the closed semisimple factor are exactly the semisimple points of the ambient group.

@[simp]

theorem TauCeti.HopfAlgebra.Point.mem_quotientPointsSubgroup_ker_unipotentPartBialgHom_base_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)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (unipotentPartBialgHom k H)) ↧k ↔ IsUnipotentPoint g

The base-field points of the closed unipotent factor are exactly the unipotent points of the ambient group.

theorem TauCeti.HopfAlgebra.Point.groupLikeSetSpan_semisimpleFactor_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] : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤

The closed semisimple factor is diagonalizable: its coordinate Hopf algebra is spanned by its group-like elements.

theorem TauCeti.HopfAlgebra.Point.smoothUnipotentCommHopfAlgProperty_unipotentFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] : smoothUnipotentCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.of k ↑(unipotentFactor k H))

The closed unipotent factor is a smooth unipotent affine group, with unipotence understood geometrically through all finite-dimensional representations.

theorem TauCeti.HopfAlgebra.Point.torusCommHopfAlgProperty_semisimpleFactor (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (hH : geometricallyConnectedCommHopfAlgProperty k ↧H) : torusCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.of k ↑(semisimpleFactor k H))

For a connected commutative affine group, its closed semisimple factor is a torus.

noncomputable def TauCeti.HopfAlgebra.Point.jordanFactorsMulEquiv (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (A : CommAlgCat k) : WithConv (H →ₐ[k] ↑A) ≃* ↥(CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (semisimplePartBialgHom k H)) A) × ↥(CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (unipotentPartBialgHom k H)) A)

Multiplication identifies ambient points with the product of the two closed Jordan factor subgroups over every commutative test algebra. The forward map applies the two regular Jordan projections; its inverse multiplies the included points.

@[simp]

theorem TauCeti.HopfAlgebra.Point.jordanFactorsMulEquiv_fst_coe (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (A : CommAlgCat k) (g : WithConv (H →ₐ[k] ↑A)) : ↑((jordanFactorsMulEquiv k H A) g).1 = (semisimplePartBialgHom k H).mapDomain g

The first factor is the regular semisimple projection.

@[simp]

theorem TauCeti.HopfAlgebra.Point.jordanFactorsMulEquiv_snd_coe (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (A : CommAlgCat k) (g : WithConv (H →ₐ[k] ↑A)) : ↑((jordanFactorsMulEquiv k H A) g).2 = (unipotentPartBialgHom k H).mapDomain g

The second factor is the regular unipotent projection.

@[simp]

theorem TauCeti.HopfAlgebra.Point.jordanFactorsMulEquiv_symm_apply (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (A : CommAlgCat k) (s : ↥(CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (semisimplePartBialgHom k H)) A)) (u : ↥(CommHopfAlgCat.quotientPointsSubgroup (↧H) (HopfIdeal.ker (unipotentPartBialgHom k H)) A)) : (jordanFactorsMulEquiv k H A).symm (s, u) = ↑s * ↑u

The inverse factorization map multiplies the two included points.

theorem TauCeti.HopfAlgebra.Point.jordanFactorsMulEquiv_mapValue (k H : Type u) [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [Coalgebra.IsCocomm k H] (A : CommAlgCat k) {B : CommAlgCat k} (φ : A ⟶ B) (g : WithConv (H →ₐ[k] ↑A)) : (jordanFactorsMulEquiv k H B) ((CommAlgCat.Hom.hom φ).mapValue g) = ((CommHopfAlgCat.mapQuotientPointsSubgroup (↧H) (HopfIdeal.ker (semisimplePartBialgHom k H)) φ) ((jordanFactorsMulEquiv k H A) g).1, (CommHopfAlgCat.mapQuotientPointsSubgroup (↧H) (HopfIdeal.ker (unipotentPartBialgHom k H)) φ) ((jordanFactorsMulEquiv k H A) g).2)

The closed-factor decomposition is natural under a change of test algebra.