Geometric connectedness of products of affine groups

The direct product of two affine groups over a field has coordinate Hopf algebra given by the tensor product of their coordinate algebras. This file applies the affine tensor-product connectedness theorem to show that geometric connectedness is preserved by this construction.

On the scheme side, the product is the fibre product of the two Hopf spectra over the spectrum of the ground field. Each projection has geometrically connected fibres by base change, and the other factor is connected. Structure morphisms to the spectrum of a field are universally open, so Mathlib's connectedness theorem for pullbacks applies. The standard affine pullback isomorphism then identifies the result with the spectrum of the tensor product.

Main declarations

• TauCeti.geometricallyConnectedCommHopfAlgProperty.tensorProduct: the tensor product of two geometrically connected commutative Hopf algebras is geometrically connected.
• TauCeti.geometricallyConnectedCommHopfAlgProperty.semidirectProduct: a semidirect product associated to an action of geometrically connected affine groups is geometrically connected.
• TauCeti.geometricallyConnectedCommHopfAlgProperty.productOfNormal: the multiplication image of a normal subgroup and another connected subgroup is geometrically connected when both factors are.

References

• J. S. Milne, Algebraic Groups (2017), Sections 1.c and 2.a.

This supplies the connectedness step in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. The binary product of two radical candidates is formed as the image of multiplication from a semidirect product whose underlying scheme is the direct product; the result below proves that source is geometrically connected.

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

The tensor product of two geometrically connected commutative Hopf algebras is geometrically connected. Contravariantly, direct products of geometrically connected affine groups over a field are geometrically connected.

The Hopf structure on the tensor product is irrelevant to connectedness, but packages the coordinate ring as the direct product in the same category used by the functor-of-points and unipotent-radical constructions.

theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.semidirectProduct {k : Type u} [Field k] (H K : CommHopfAlgCat k) (A : GrpObj.Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) (hH : geometricallyConnectedCommHopfAlgProperty k H) (hK : geometricallyConnectedCommHopfAlgProperty k K) : geometricallyConnectedCommHopfAlgProperty k A.coordinateHopfAlgebra

The semidirect product associated to an action of geometrically connected affine groups is geometrically connected.

The action changes the group law but not the underlying affine scheme: on coordinate algebras, the carrier remains the tensor product. This formulation is the one used when multiplication of two normal closed subgroups is made into a homomorphism by equipping their product with the conjugation semidirect-product structure.

theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.productOfNormal {k : Type u} [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) (hIc : geometricallyConnectedCommHopfAlgProperty k (CommHopfAlgCat.quotient H I)) (hJc : geometricallyConnectedCommHopfAlgProperty k (CommHopfAlgCat.quotient H J)) : geometricallyConnectedCommHopfAlgProperty k (CommHopfAlgCat.productOfNormal H I J hI)

The scheme-theoretic multiplication image of a normal geometrically connected closed affine subgroup and another geometrically connected closed affine subgroup is geometrically connected.