Noetherian space #
A Noetherian space is a topological space that satisfies any of the following equivalent conditions:
WellFounded ((· > ·) : TopologicalSpace.Opens α → TopologicalSpace.Opens α → Prop)
WellFounded ((· < ·) : TopologicalSpace.Closeds α → TopologicalSpace.Closeds α → Prop)
∀ s : Set α, IsCompact s
∀ s : TopologicalSpace.Opens α, IsCompact s
The first is chosen as the definition, and the equivalence is shown in
TopologicalSpace.noetherianSpace_TFAE
.
Many examples of noetherian spaces come from algebraic topology. For example, the underlying space of a noetherian scheme (e.g., the spectrum of a noetherian ring) is noetherian.
Main Results #
TopologicalSpace.NoetherianSpace.set
: Every subspace of a noetherian space is noetherian.TopologicalSpace.NoetherianSpace.isCompact
: Every set in a noetherian space is a compact set.TopologicalSpace.noetherianSpace_TFAE
: Describes the equivalent definitions of noetherian spaces.TopologicalSpace.NoetherianSpace.range
: The image of a noetherian space under a continuous map is noetherian.TopologicalSpace.NoetherianSpace.iUnion
: The finite union of noetherian spaces is noetherian.TopologicalSpace.NoetherianSpace.discrete
: A noetherian and Hausdorff space is discrete.TopologicalSpace.NoetherianSpace.exists_finset_irreducible
: Every closed subset of a noetherian space is a finite union of irreducible closed subsets.TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
: The number of irreducible components of a noetherian space is finite.
Type class for noetherian spaces. It is defined to be spaces whose open sets satisfies ACC.
- wellFounded_opens : WellFounded fun (x1 x2 : TopologicalSpace.Opens α) => x1 > x2
Instances
Equations
- ⋯ = ⋯
In a Noetherian space, all sets are compact.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Spaces that are both Noetherian and Hausdorff are finite.
Equations
- ⋯ = ⋯
In a Noetherian space, every closed set is a finite union of irreducible closed sets.
In a Noetherian space, every closed set is a finite union of irreducible closed sets.
In a Noetherian space, every closed set is a finite union of irreducible closed sets.