Geometric connectedness of affine products #
This file proves that the spectrum of a tensor product of commutative algebras over a field is geometrically connected when the spectra of both factors are geometrically connected. The tensor product spectrum is identified with the fibre product of the two spectra over the ground field.
Main declarations #
TauCeti.geometricallyConnected_tensorProduct: the tensor product of two commutative algebras with geometrically connected spectra is geometrically connected.
This is an affine-scheme prerequisite for the product constructions in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap.
theorem
TauCeti.geometricallyConnected_tensorProduct
{k : Type u}
[Field k]
(S T : Type u)
[CommRing S]
[CommRing T]
[Algebra k S]
[Algebra k T]
(hS : AlgebraicGeometry.GeometricallyConnected (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k S))))
(hT : AlgebraicGeometry.GeometricallyConnected (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k T))))
:
The spectrum of a tensor product of commutative algebras over a field is geometrically connected when the spectra of both factors are geometrically connected over that field.