Connectedness of prime spectrum

In this file we show some results on connectedness of the prime spectrum of a ring.

@[reducible, inline]

abbrev idempotents (R : Type u_2) [Mul R] : Set R

The set of idempotent elements of a multiplicative structure.

Equations

• idempotents R = {e : R | IsIdempotentElem e}

theorem subset_idempotents {R : Type u_1} [CommRing R] : {0, 1} ⊆ idempotents R

theorem PrimeSpectrum.preconnectedSpace_of_forall_isIdempotentElem {R : Type u_1} [CommRing R] (H : ∀ (e : R), IsIdempotentElem e → e = 0 ∨ e = 1) : PreconnectedSpace (PrimeSpectrum R)

If every idempotent is trivial, then Spec R is connected.

theorem PrimeSpectrum.basicOpen_eq_top_iff {R : Type u_1} [CommRing R] (f : R) : basicOpen f = ⊤ ↔ IsUnit f

theorem PrimeSpectrum.preconnectedSpace_iff_idempotents_subset {R : Type u_1} [CommRing R] : PreconnectedSpace (PrimeSpectrum R) ↔ idempotents R ⊆ {0, 1}

theorem PrimeSpectrum.connectedSpace_iff_idempotents_subset {R : Type u_1} [CommRing R] [Nontrivial R] : ConnectedSpace (PrimeSpectrum R) ↔ idempotents R ⊆ {0, 1}

theorem PrimeSpectrum.connectedSpace_iff_of_ringEquiv {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : ConnectedSpace (PrimeSpectrum R) ↔ ConnectedSpace (PrimeSpectrum S)

theorem PrimeSpectrum.preconnectedSpace_of_forall_connectedSpace_of_isSeparable {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (H : ∀ (K : Type v) [inst : Field K] [inst_1 : Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K], PreconnectedSpace (PrimeSpectrum (TensorProduct k K R))) (Ω : Type v) [Field Ω] [Algebra k Ω] [Algebra.IsSeparable k Ω] : PreconnectedSpace (PrimeSpectrum (TensorProduct k Ω R))

theorem PrimeSpectrum.connectedSpace_tensorProduct_of_isSepClosed {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] [IsSepClosed k] {S : Type u_2} [CommRing S] [Algebra k S] (hR : ConnectedSpace (PrimeSpectrum R)) (hS : ConnectedSpace (PrimeSpectrum S)) : ConnectedSpace (PrimeSpectrum (TensorProduct k R S))

Stacks Tag 037R

theorem PrimeSpectrum.connectedSpace_iff_of_isPurelyInseparable (k : Type u_2) (R : Type u_3) [CommRing R] [Field k] [Algebra k R] (K : Type u_4) [Field K] [Algebra k K] (L : Type u_5) [Field L] [Algebra k L] [Algebra K L] [IsScalarTower k K L] [IsPurelyInseparable K L] : ConnectedSpace (PrimeSpectrum (TensorProduct k K R)) ↔ ConnectedSpace (PrimeSpectrum (TensorProduct k L R))

theorem PrimeSpectrum.connectedSpace_iff_of_isAlgClosure_of_isSepClosure (k : Type u_2) (R : Type u_3) [CommRing R] [Field k] [Algebra k R] (K : Type u_4) [Field K] [Algebra k K] [IsSepClosure k K] (L : Type u_5) [Field L] [Algebra k L] [IsAlgClosure k L] : ConnectedSpace (PrimeSpectrum (TensorProduct k K R)) ↔ ConnectedSpace (PrimeSpectrum (TensorProduct k L R))

theorem PrimeSpectrum.connectedSpace_iff_of_isAlgClosure_of_isSepClosed (k : Type u_2) (R : Type u_3) [CommRing R] [Field k] [Algebra k R] [IsSepClosed k] (L : Type u_4) [Field L] [Algebra k L] [IsAlgClosure k L] : ConnectedSpace (PrimeSpectrum R) ↔ ConnectedSpace (PrimeSpectrum (TensorProduct k L R))

theorem PrimeSpectrum.connectedSpace_of_faithfullyFlat {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] [Module.FaithfullyFlat R S] [ConnectedSpace (PrimeSpectrum S)] : ConnectedSpace (PrimeSpectrum R)

theorem PrimeSpectrum.connectedSpace_of_isScalarTower {k : Type u} {R : Type u_1} [Field k] [CommRing R] [Algebra k R] (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra k K] [Algebra k L] [Algebra K L] [IsScalarTower k K L] [ConnectedSpace (PrimeSpectrum (TensorProduct k L R))] : ConnectedSpace (PrimeSpectrum (TensorProduct k K R))