Documentation

GeometricallyP.Algebra.GeometricallyConnected

Geometrically connected algebras #

In this file we develop the theory of geometrically connected algebras over a field.

References #

source
class Algebra.GeometricallyConnected (k : Type u_2) (R : Type u_3) [Field k] [CommRing R] [Algebra k R] :
Prop

A k-algebra R is geometrically connected if Spec (AlgebraicClosure k ⊗[k] R) is connected. In this case, Spec (K ⊗[k] R) is connected for every field extension K of k (see Algebra.GeometricallyConnected.connectedSpace). Note: The stacks project definition is the latter condition, which is equivalent to the former by the above. The reason for choosing this definition is that it does not quantify over types.

Instances
    source
    theorem Algebra.geometricallyConnected_iff (k : Type u_2) (R : Type u_3) [Field k] [CommRing R] [Algebra k R] :
    GeometricallyConnected k R ↔ ConnectedSpace (PrimeSpectrum (TensorProduct k (AlgebraicClosure k) R))
    source
    theorem Algebra.GeometricallyConnected.iff_connectedSpace_separableClosure (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] :
    GeometricallyConnected k R ↔ ConnectedSpace (PrimeSpectrum (TensorProduct k (SeparableClosure k) R))
    source
    theorem Algebra.GeometricallyConnected.of_forall_connectedSpace_of_isSeparable (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] (H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K], ConnectedSpace (PrimeSpectrum (TensorProduct k K R))) :
    GeometricallyConnected k R

    If Spec (K ⊗[k] R) is connected for every finite separable extension K of k, then R is geometrically connected over k.

    source
    theorem Algebra.GeometricallyConnected.connectedSpace (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] [GeometricallyConnected k R] (K : Type u_3) [Field K] [Algebra k K] :
    ConnectedSpace (PrimeSpectrum (TensorProduct k K R))

    Stacks Tag 037S (part of the proof of (2) => (1))

    source
    theorem Algebra.GeometricallyConnected.of_connectedSpace_of_isSepClosed (k : Type u) (R : Type u_2) [CommRing R] [Field k] [Algebra k R] (Ω : Type u_3) [Field Ω] [Algebra k Ω] [IsSepClosed Ω] (H : ConnectedSpace (PrimeSpectrum (TensorProduct k Ω R))) :
    GeometricallyConnected k R

    If Ω is a separably closed extension of k such that Spec (Ω ⊗[k] R) is connected, R is geometrically connected over k.