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) [TopologicalSpace α] : TopologicalSpace.NoetherianSpace α ↔ WellFounded fun (x x_1 : TopologicalSpace.Opens α) => x > x_1

class TopologicalSpace.NoetherianSpace (α : Type u_1) [TopologicalSpace α] : Prop

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

• wellFounded_opens : WellFounded fun (x x_1 : TopologicalSpace.Opens α) => x > x_1

theorem TopologicalSpace.noetherianSpace_iff_opens (α : Type u_1) [TopologicalSpace α] : TopologicalSpace.NoetherianSpace α ↔ ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s

instance TopologicalSpace.NoetherianSpace.compactSpace (α : Type u_1) [TopologicalSpace α] [h : TopologicalSpace.NoetherianSpace α] : CompactSpace α

Equations

• (_ : CompactSpace α) = (_ : CompactSpace α)

theorem TopologicalSpace.NoetherianSpace.isCompact {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : Set α) : IsCompact s

In a Noetherian space, all sets are compact.

theorem Inducing.noetherianSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace.NoetherianSpace α] {i : β → α} (hi : Inducing i) : TopologicalSpace.NoetherianSpace β

instance TopologicalSpace.NoetherianSpace.set {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : Set α) : TopologicalSpace.NoetherianSpace ↑s

Stacks: Lemma 0052 (1)

Equations

• (_ : TopologicalSpace.NoetherianSpace ↑s) = (_ : TopologicalSpace.NoetherianSpace { x : α // x ∈ s })

theorem TopologicalSpace.noetherianSpace_TFAE (α : Type u_1) [TopologicalSpace α] : List.TFAE [TopologicalSpace.NoetherianSpace α, WellFounded fun (s t : TopologicalSpace.Closeds α) => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s]

theorem TopologicalSpace.noetherianSpace_iff_isCompact {α : Type u_1} [TopologicalSpace α] : TopologicalSpace.NoetherianSpace α ↔ ∀ (s : Set α), IsCompact s

theorem TopologicalSpace.NoetherianSpace.wellFounded_closeds {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] : WellFounded fun (s t : TopologicalSpace.Closeds α) => s < t

instance TopologicalSpace.instNoetherianSpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology {α : Type u_3} : TopologicalSpace.NoetherianSpace (CofiniteTopology α)

Equations

• (_ : TopologicalSpace.NoetherianSpace (CofiniteTopology α)) = (_ : TopologicalSpace.NoetherianSpace (CofiniteTopology α))

theorem TopologicalSpace.noetherianSpace_of_surjective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace.NoetherianSpace α] (f : α → β) (hf : Continuous f) (hf' : Function.Surjective f) : TopologicalSpace.NoetherianSpace β

theorem TopologicalSpace.noetherianSpace_iff_of_homeomorph {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) : TopologicalSpace.NoetherianSpace α ↔ TopologicalSpace.NoetherianSpace β

theorem TopologicalSpace.NoetherianSpace.range {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace.NoetherianSpace α] (f : α → β) (hf : Continuous f) : TopologicalSpace.NoetherianSpace ↑(Set.range f)

theorem TopologicalSpace.noetherianSpace_set_iff {α : Type u_1} [TopologicalSpace α] (s : Set α) : TopologicalSpace.NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t

@[simp]

theorem TopologicalSpace.noetherian_univ_iff {α : Type u_1} [TopologicalSpace α] : TopologicalSpace.NoetherianSpace ↑Set.univ ↔ TopologicalSpace.NoetherianSpace α

theorem TopologicalSpace.NoetherianSpace.iUnion {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} (f : ι → Set α) [Finite ι] [hf : ∀ (i : ι), TopologicalSpace.NoetherianSpace ↑(f i)] : TopologicalSpace.NoetherianSpace ↑(⋃ (i : ι), f i)

theorem TopologicalSpace.NoetherianSpace.discrete {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] [T2Space α] : DiscreteTopology α

theorem TopologicalSpace.NoetherianSpace.finite {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] [T2Space α] : Finite α

Spaces that are both Noetherian and Hausdorff are finite.

instance TopologicalSpace.Finite.to_noetherianSpace {α : Type u_1} [TopologicalSpace α] [Finite α] : TopologicalSpace.NoetherianSpace α

Equations

• (_ : TopologicalSpace.NoetherianSpace α) = (_ : TopologicalSpace.NoetherianSpace α)

theorem TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : TopologicalSpace.Closeds α) : ∃ (S : Set (TopologicalSpace.Closeds α)), Set.Finite S ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ 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} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] {s : Set α} (hs : IsClosed s) : ∃ (S : Set (Set α)), Set.Finite S ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ 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} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (s : TopologicalSpace.Closeds α) : ∃ (S : Finset (TopologicalSpace.Closeds α)), (∀ (k : { x : TopologicalSpace.Closeds α // x ∈ S }), IsIrreducible ↑↑k) ∧ s = Finset.sup S id

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

theorem TopologicalSpace.NoetherianSpace.finite_irreducibleComponents {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] : Set.Finite (irreducibleComponents α)

Stacks: Lemma 0052 (2)

theorem TopologicalSpace.NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (Z : Set α) (H : Z ∈ irreducibleComponents α) : ∃ (o : Set α), IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

Stacks: Lemma 0052 (3)