Irreducibility of connected schemes with domain stalks

We show that a locally noetherian connected scheme whose stalks are domains is irreducible; when its stalks are regular local rings, it is integral.

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). Since regular local rings are domains (TauCeti.IsRegularLocalRing.isDomain), a locally noetherian connected scheme whose stalks are regular local rings is integral (isIntegral_of_connected_of_isRegularLocalRing_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.

theorem TauCeti.AlgebraicGeometry.isIntegral_of_connected_of_isRegularLocalRing_stalk (Z : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian Z] [ConnectedSpace ↥Z] [∀ (x : ↥Z), IsRegularLocalRing ↑(Z.presheaf.stalk x)] : AlgebraicGeometry.IsIntegral Z

A locally noetherian connected scheme whose stalks are regular local rings is integral.