Module

ConnectedDomainStalks.lean

Nyll.SchemeTheory.LocalGeometry.ConnectedDomainStalks

1 declaration indexed from sourceView source ↗

Module documentation

Connected schemes with domain stalks

On a locally Noetherian scheme with domain stalks, irreducible components are open and closed. Connectedness therefore forces one component to be the whole scheme, and reducedness follows directly from the stalks.

Imports2

Nyll.SchemeTheory.Divisors.EtaleIrreducibleComponents
Mathlib.Topology.Connected.Clopen

Imported by5

theorem

isIntegral_of_connected_of_isDomain_stalk

L27 ↗

AlgebraicGeometry.isIntegral_of_connected_of_isDomain_stalk

Documentation

A connected locally Noetherian scheme whose stalks are domains is integral.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open TopologicalSpace
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem isIntegral_of_connected_of_isDomain_stalk
    (X : Scheme.{u}) [IsLocallyNoetherian X] [ConnectedSpace X]
    (hdom : ∀ x : X, IsDomain (X.presheaf.stalk x)) : IsIntegral X

Module documentation

Connected schemes with domain stalks

Declarations

isIntegral_of_connected_of_isDomain_stalk