# mathlibdocumentation

topology.noetherian_space

# Noetherian space #

A Noetherian space is a topological space that satisfies any of the following equivalent conditions:

• well_founded ((>) : opens α → opens α → Prop)
• well_founded ((<) : closeds α → closeds α → Prop)
• ∀ s : set α, is_compact s
• ∀ s : opens α, is_compact s

The first is chosen as the definition, and the equivalence is shown in topological_space.noetherian_space_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 #

• noetherian_space.set: Every subspace of a noetherian space is noetherian.
• noetherian_space.is_compact: Every subspace of a noetherian space is compact.
• noetherian_space_tfae: Describes the equivalent definitions of noetherian spaces.
• noetherian_space.range: The image of a noetherian space under a continuous map is noetherian.
• noetherian_space.Union: The finite union of noetherian spaces is noetherian.
• noetherian_space.discrete: A noetherian and hausdorff space is discrete.
• noetherian_space.exists_finset_irreducible : Every closed subset of a noetherian space is a finite union of irreducible closed subsets.
• noetherian_space.finite_irreducible_components: The number of irreducible components of a noetherian space is finite.
@[class]
structure topological_space.noetherian_space (α : Type u_1)  :
Prop
• well_founded :

Type class for noetherian spaces. It is defined to be spaces whose open sets satisfies ACC.

Instances of this typeclass
theorem topological_space.noetherian_space_iff (α : Type u_1)  :
@[protected, instance]
@[protected, instance]
def topological_space.noetherian_space.set {α : Type u_1} (s : set α) :
theorem topological_space.noetherian_space_tfae (α : Type u_1)  :
, well_founded (λ (s t : , s < t), ∀ (s : set α), , ∀ (s : , .tfae
theorem topological_space.noetherian_space.is_compact {α : Type u_1} (s : set α) :
theorem topological_space.noetherian_space_of_surjective {α : Type u_1} {β : Type u_2} (f : α → β) (hf : continuous f) (hf' : function.surjective f) :
theorem topological_space.noetherian_space_iff_of_homeomorph {α : Type u_1} {β : Type u_2} (f : α ≃ₜ β) :
theorem topological_space.noetherian_space.range {α : Type u_1} {β : Type u_2} (f : α → β) (hf : continuous f) :
theorem topological_space.noetherian_space_set_iff {α : Type u_1} (s : set α) :
∀ (t : set α), t s
@[simp]
theorem topological_space.noetherian_space.Union {α : Type u_1} {ι : Type u_2} (f : ι → set α) [finite ι] [hf : ∀ (i : ι), ] :
theorem topological_space.noetherian_space.finite {α : Type u_1} [t2_space α] :

Spaces that are both Noetherian and Hausdorff is finite.

@[protected, instance]
theorem topological_space.noetherian_space.exists_finset_irreducible {α : Type u_1}  :
∃ (S : , (∀ (k : S), s = S.sup id