Connected components of Noetherian spaces

A Noetherian topological space has only finitely many connected components. Indeed, it has finitely many irreducible components, every irreducible set lies in one connected component, and the irreducible components cover the space. Consequently the quotient by connected components is a finite discrete space, and every connected component is open as well as closed.

Main declarations

• TauCeti.finite_connectedComponents_of_noetherianSpace: a Noetherian space has finitely many connected components.
• TauCeti.instLocallyConnectedSpaceOfNoetherianSpace: a Noetherian space is locally connected.

References

• The Stacks Project, Tag 0052, Noetherian topological spaces.

The finite-component conclusion is used for the identity-component and component-group milestone in Layer 3 of the ReductiveGroups roadmap. Applied to the spectrum of a finite-type coordinate algebra, it supplies the finiteness input for the construction of π₀.

theorem TauCeti.finite_connectedComponents_of_noetherianSpace {X : Type u} [TopologicalSpace X] [TopologicalSpace.NoetherianSpace X] : Finite (ConnectedComponents X)

A Noetherian space has finitely many connected components.

instance TauCeti.instLocallyConnectedSpaceOfNoetherianSpace {X : Type u} [TopologicalSpace X] [TopologicalSpace.NoetherianSpace X] : LocallyConnectedSpace X

A Noetherian space is locally connected. In particular, each connected component is clopen.