# Documentation

Mathlib.Topology.NoetherianSpace

# 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.
theorem TopologicalSpace.noetherianSpace_iff (α : Type u_1) [] :
WellFounded fun x x_1 => x > x_1

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

Instances
theorem TopologicalSpace.noetherianSpace_iff_opens (α : Type u_1) [] :
∀ (s : ),
theorem TopologicalSpace.NoetherianSpace.isCompact {α : Type u_1} [] (s : Set α) :

In a Noetherian space, all sets are compact.

theorem Inducing.noetherianSpace {α : Type u_1} {β : Type u_2} [] [] {i : βα} (hi : ) :
theorem TopologicalSpace.noetherianSpace_TFAE (α : Type u_1) [] :
List.TFAE [, WellFounded fun s t => s < t, ∀ (s : Set α), , ∀ (s : ), ]
theorem TopologicalSpace.noetherianSpace_iff_isCompact {α : Type u_1} [] :
∀ (s : Set α),
theorem TopologicalSpace.noetherianSpace_of_surjective {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (hf : ) (hf' : ) :
theorem TopologicalSpace.noetherianSpace_iff_of_homeomorph {α : Type u_1} {β : Type u_2} [] [] (f : α ≃ₜ β) :
theorem TopologicalSpace.NoetherianSpace.range {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (hf : ) :
theorem TopologicalSpace.noetherianSpace_set_iff {α : Type u_1} [] (s : Set α) :
∀ (t : Set α), t s
@[simp]
theorem TopologicalSpace.NoetherianSpace.iUnion {α : Type u_1} [] {ι : Type u_3} (f : ιSet α) [] [hf : ∀ (i : ι), ] :
TopologicalSpace.NoetherianSpace ↑(⋃ (i : ι), f i)

Spaces that are both Noetherian and Hausdorff are finite.

theorem TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible {α : Type u_1} [] (s : ) :
S, (∀ (t : ), t S) s = sSup S

In a Noetherian space, every closed set is a finite union of irreducible closed sets.

theorem TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible {α : Type u_1} [] {s : Set α} (hs : ) :
S, (∀ (t : Set α), t S) (∀ (t : Set α), t S) s = ⋃₀ S

In a Noetherian space, every closed set is a finite union of irreducible closed sets.

theorem TopologicalSpace.NoetherianSpace.exists_finset_irreducible {α : Type u_1} [] (s : ) :
S, (∀ (k : { x // x S }), ) s = Finset.sup S id

In a Noetherian space, every closed set is a finite union of irreducible closed sets.