Irreducibility of connected schemes with domain stalks

This file supplies a prerequisite for the Standing hypotheses target of the Jacobian challenge roadmap (proving that a regular connected scheme is irreducible, as regular stalks are integral domains).

We prove that a locally noetherian connected scheme whose stalks have unique minimal primes is irreducible (irreducibleSpace_of_connected_of_unique_minimalPrime_stalk), from which we deduce that such a scheme is irreducible if its stalks are integral domains (irreducibleSpace_of_connected_of_isDomain_stalk).

The proof proceeds by showing that the irreducible components of such a scheme are pairwise disjoint and open (hence clopen), so connectedness forces a unique component.

Along the way we show that the minimal primes of the stalk at a point and the irreducible components containing that point are in bijection.

theorem TauCeti.AlgebraicGeometry.irreducibleSpace_of_connected_of_unique_minimalPrime_stalk (Z : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian Z] [ConnectedSpace ↥Z] (hStalks : (x : ↥Z) → Unique ↑(minimalPrimes ↑(Z.presheaf.stalk x))) : IrreducibleSpace ↥Z

A locally noetherian connected scheme whose stalks have unique minimal primes is irreducible.

theorem TauCeti.AlgebraicGeometry.irreducibleSpace_of_connected_of_isDomain_stalk (Z : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian Z] [ConnectedSpace ↥Z] (hStalks : ∀ (x : ↥Z), IsDomain ↑(Z.presheaf.stalk x)) : IrreducibleSpace ↥Z

A locally noetherian connected scheme whose stalks are integral domains is irreducible.