Geometric semisimple points of affine groups

This file packages the condition that every algebraic-closure-valued point of a commutative Hopf algebra is semisimple. It also uses the generic transport and product results to prove that this object property is invariant under isomorphisms and closed under tensor products.

Main declarations

• TauCeti.geometricallySemisimplePointsCommHopfAlgProperty: the object property asserting that every algebraic-closure-valued point is semisimple.
• TauCeti.geometricallySemisimplePointsCommHopfAlgProperty_of_surjective: closed subgroups of a group with semisimple geometric points again have semisimple geometric points.
• TauCeti.geometricallySemisimplePointsCommHopfAlgProperty.tensorProduct: geometric semisimplicity is closed under direct products of affine groups.

References

• T. A. Springer, Linear Algebraic Groups, §2.4.
• J. S. Milne, Algebraic Groups (2017), §12.c.

This supplies generic geometric semisimple-point infrastructure used by Layer 4 of the ReductiveGroups roadmap.

def TauCeti.geometricallySemisimplePointsCommHopfAlgProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (CommHopfAlgCat k)

The object property asserting that every algebraic-closure-valued point of a commutative Hopf algebra is a semisimple point.

Equations

• TauCeti.geometricallySemisimplePointsCommHopfAlgProperty k H = ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), TauCeti.HopfAlgebra.IsSemisimplePoint g

@[simp]

theorem TauCeti.geometricallySemisimplePointsCommHopfAlgProperty_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallySemisimplePointsCommHopfAlgProperty k H ↔ ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), HopfAlgebra.IsSemisimplePoint g

Membership in geometricallySemisimplePointsCommHopfAlgProperty means that every geometric point is semisimple.

instance TauCeti.instIsClosedUnderIsomorphismsCommHopfAlgCatGeometricallySemisimplePointsCommHopfAlgProperty (k : Type u) [Field k] : (geometricallySemisimplePointsCommHopfAlgProperty k).IsClosedUnderIsomorphisms

The geometric-point semisimplicity property is invariant under isomorphisms of commutative Hopf algebras.

theorem TauCeti.geometricallySemisimplePointsCommHopfAlgProperty_of_surjective (k : Type u) [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) (hH : geometricallySemisimplePointsCommHopfAlgProperty k H) : geometricallySemisimplePointsCommHopfAlgProperty k K

Geometric-point semisimplicity descends along a surjective morphism of coordinate Hopf algebras. Contravariantly, closed subgroups of a group with semisimple geometric points again have semisimple geometric points.

theorem TauCeti.geometricallySemisimplePointsCommHopfAlgProperty.tensorProduct (k : Type u) [Field k] (H K : CommHopfAlgCat k) (hH : geometricallySemisimplePointsCommHopfAlgProperty k H) (hK : geometricallySemisimplePointsCommHopfAlgProperty k K) : geometricallySemisimplePointsCommHopfAlgProperty k ↧(TensorProduct k ↑H ↑K)

The tensor product of two coordinate Hopf algebras with semisimple geometric points again has only semisimple geometric points. Contravariantly, geometric-point semisimplicity is closed under direct products of affine groups.

theorem TauCeti.geometricallySemisimplePointsCommHopfAlgProperty_iff_forall_unipotentPart_eq_one (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallySemisimplePointsCommHopfAlgProperty k H ↔ ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), HopfAlgebra.Point.unipotentPart k (↑H) (AlgebraicClosure k) g = 1

Every geometric point is semisimple exactly when the unipotent part of every geometric point is the identity.

theorem TauCeti.geometricallySemisimplePointsCommHopfAlgProperty_iff_forall_semisimplePart_eq_self (k : Type u) [Field k] (H : CommHopfAlgCat k) : geometricallySemisimplePointsCommHopfAlgProperty k H ↔ ∀ (g : WithConv (↑H →ₐ[k] AlgebraicClosure k)), HopfAlgebra.Point.semisimplePart k (↑H) (AlgebraicClosure k) g = g

Every geometric point is semisimple exactly when the semisimple part of every geometric point is the point itself.