Geometric connectedness under base change

Geometric connectedness of a commutative Hopf algebra is preserved by and descends along extension of the base field. In particular, H is geometrically connected over k if and only if the scalar extension K ⊗[k] H is geometrically connected over any field extension K / k.

Preservation compares an arbitrary further extension L / K with the original geometric connectedness condition using the canonical algebra equivalence

L ⊗[K] (K ⊗[k] H) ≃ L ⊗[k] H.

For descent, a common overfield of K and an algebraically closed extension of k compares the two scalar extensions, after which connectedness descends along an injective map.

Main declarations

• TauCeti.geometricallyConnectedCommHopfAlgProperty.baseChange: geometric connectedness is preserved by extension of the base field.
• TauCeti.geometricallyConnectedCommHopfAlgProperty.of_baseChange: geometric connectedness descends from an extension of the base field.
• TauCeti.geometricallyConnectedCommHopfAlgProperty.baseChange_iff: geometric connectedness is equivalent before and after extension of the base field.

References

• J. S. Milne, Algebraic Groups (2017), §2.a.

This is base-change infrastructure for Layer 3, "Identity component and component group", of the ReductiveGroups roadmap: connectedness there is geometric and is therefore used after extending the ground field.

theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.baseChange (k K : Type u) [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) (hH : geometricallyConnectedCommHopfAlgProperty k H) : geometricallyConnectedCommHopfAlgProperty K (CommHopfAlgCat.baseChange H)

Geometric connectedness is preserved by extension of the base field.

For fields k → K, if the spectrum of H ⊗[k] L is connected for every field extension L / k, then the spectrum of (K ⊗[k] H) ⊗[K] L is connected for every field extension L / K. The two rings are identified by cancellation of successive scalar extensions.

theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.of_baseChange (k K : Type u) [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) (hH : geometricallyConnectedCommHopfAlgProperty K (CommHopfAlgCat.baseChange H)) : geometricallyConnectedCommHopfAlgProperty k H

Geometric connectedness descends from an extension of the base field.

If K ⊗[k] H is geometrically connected over a field extension K / k, then H is geometrically connected over k.

theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.baseChange_iff (k K : Type u) [Field k] [Field K] [Algebra k K] (H : CommHopfAlgCat k) : geometricallyConnectedCommHopfAlgProperty K (CommHopfAlgCat.baseChange H) ↔ geometricallyConnectedCommHopfAlgProperty k H

Geometric connectedness is equivalent before and after extension of the base field.