Connected prime spectra and idempotents

The prime spectrum of a nontrivial commutative ring is connected exactly when the ring has no idempotents other than zero and one. Mathlib identifies idempotents with clopen subsets of the prime spectrum; this file records the resulting connectedness criterion in the form used by coordinate rings of geometrically connected affine schemes.

Main declarations

• TauCeti.eq_zero_or_eq_one_of_isIdempotentElem: an idempotent is zero or one when Spec R is connected.
• TauCeti.connectedSpace_primeSpectrum_iff_idempotent_eq_zero_or_one: Spec R is connected if and only if every idempotent of R is zero or one.
• TauCeti.connectedSpace_primeSpectrum_of_injective: connectedness descends along an injective ring homomorphism.

theorem TauCeti.eq_zero_or_eq_one_of_isIdempotentElem {R : Type u_1} [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {e : R} (he : IsIdempotentElem e) : e = 0 ∨ e = 1

An idempotent in a commutative ring with connected prime spectrum is zero or one.

theorem TauCeti.connectedSpace_primeSpectrum_iff_idempotent_eq_zero_or_one {R : Type u_1} [CommRing R] [Nontrivial R] : ConnectedSpace (PrimeSpectrum R) ↔ ∀ (e : R), IsIdempotentElem e → e = 0 ∨ e = 1

The prime spectrum of a nontrivial commutative ring is connected exactly when its only idempotents are zero and one.

theorem TauCeti.connectedSpace_primeSpectrum_of_injective {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [ConnectedSpace (PrimeSpectrum S)] (f : R →+* S) (hf : Function.Injective ⇑f) : ConnectedSpace (PrimeSpectrum R)

Connectedness of prime spectra descends along injective ring homomorphisms.