Noetherian space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
- well_founded : well_founded gt
Type class for noetherian spaces. It is defined to be spaces whose open sets satisfies ACC.
theorem
topological_space.noetherian_space_iff_opens
(α : Type u_1)
[topological_space α] :
topological_space.noetherian_space α ↔ ∀ (s : topological_space.opens α), is_compact ↑s
@[protected, instance]
def
topological_space.noetherian_space.compact_space
(α : Type u_1)
[topological_space α]
[h : topological_space.noetherian_space α] :
@[protected]
theorem
topological_space.noetherian_space.is_compact
{α : Type u_1}
[topological_space α]
[topological_space.noetherian_space α]
(s : set α) :
@[protected]
theorem
topological_space.inducing.noetherian_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[topological_space.noetherian_space α]
{i : β → α}
(hi : inducing i) :
@[protected, instance]
def
topological_space.noetherian_space.set
{α : Type u_1}
[topological_space α]
[h : topological_space.noetherian_space α]
(s : set α) :
theorem
topological_space.noetherian_space_tfae
(α : Type u_1)
[topological_space α] :
[topological_space.noetherian_space α, well_founded (λ (s t : topological_space.closeds α), s < t), ∀ (s : set α), is_compact s, ∀ (s : topological_space.opens α), is_compact ↑s].tfae
@[protected, instance]
theorem
topological_space.noetherian_space_of_surjective
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[topological_space.noetherian_space α]
(f : α → β)
(hf : continuous f)
(hf' : function.surjective f) :
theorem
topological_space.noetherian_space_iff_of_homeomorph
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α ≃ₜ β) :
theorem
topological_space.noetherian_space.range
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
[topological_space.noetherian_space α]
(f : α → β)
(hf : continuous f) :
theorem
topological_space.noetherian_space_set_iff
{α : Type u_1}
[topological_space α]
(s : set α) :
topological_space.noetherian_space ↥s ↔ ∀ (t : set α), t ⊆ s → is_compact t
@[simp]
theorem
topological_space.noetherian_space.Union
{α : Type u_1}
[topological_space α]
{ι : Type u_2}
(f : ι → set α)
[finite ι]
[hf : ∀ (i : ι), topological_space.noetherian_space ↥(f i)] :
topological_space.noetherian_space (↥⋃ (i : ι), f i)
theorem
topological_space.noetherian_space.discrete
{α : Type u_1}
[topological_space α]
[topological_space.noetherian_space α]
[t2_space α] :
theorem
topological_space.noetherian_space.finite
{α : Type u_1}
[topological_space α]
[topological_space.noetherian_space α]
[t2_space α] :
finite α
Spaces that are both Noetherian and Hausdorff is finite.
@[protected, instance]
theorem
topological_space.noetherian_space.exists_finset_irreducible
{α : Type u_1}
[topological_space α]
[topological_space.noetherian_space α]
(s : topological_space.closeds α) :
theorem
topological_space.noetherian_space.finite_irreducible_components
{α : Type u_1}
[topological_space α]
[topological_space.noetherian_space α] :