# 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.wellFounded_opens {α : Type u_1} [] [self : ] :
WellFounded fun (x x_1 : ) => x > x_1
theorem TopologicalSpace.noetherianSpace_iff_opens (α : Type u_1) [] :
∀ (s : ),
@[instance 100]
Equations
• =
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 : ) :
instance TopologicalSpace.NoetherianSpace.set {α : Type u_1} [] (s : Set α) :

Stacks: Lemma 0052 (1)

Equations
• =
theorem TopologicalSpace.noetherianSpace_TFAE (α : Type u_1) [] :
[, WellFounded fun (s t : ) => s < t, ∀ (s : Set α), , ∀ (s : ), ].TFAE
theorem TopologicalSpace.noetherianSpace_iff_isCompact {α : Type u_1} [] :
∀ (s : Set α),
Equations
• =
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 α) :
ts,
@[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.

@[instance 100]
Equations
• =
theorem TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible {α : Type u_1} [] (s : ) :
∃ (S : ), S.Finite (tS, ) 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 : Set (Set α)), S.Finite (tS, ) (tS, ) 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 = S.sup id

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