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.

@[reducible, inline]

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

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

Equations

• TopologicalSpace.NoetherianSpace α = WellFoundedGT (TopologicalSpace.Opens α)

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

@[instance 100]

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

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

In a Noetherian space, all sets are compact.

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

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

Stacks Tag 0052 ((1))

theorem TopologicalSpace.noetherianSpace_TFAE (α : Type u_1) [TopologicalSpace α] : [NoetherianSpace α, WellFoundedLT (Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s].TFAE

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

instance TopologicalSpace.instWellFoundedLTClosedsOfNoetherianSpace {α : Type u_1} [TopologicalSpace α] [NoetherianSpace α] : WellFoundedLT (Closeds α)

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

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

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

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

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

@[simp]

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

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

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

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

Spaces that are both Noetherian and Hausdorff are finite.

@[instance 100]

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

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

Stacks Tag 0052 ((2))

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

Stacks Tag 0052 ((3))