Documentation

Mathlib.Topology.NoetherianSpace

Noetherian space #

A Noetherian space is a topological space that satisfies any of the following equivalent conditions:

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 #

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

Instances

    In a Noetherian space, all sets are compact.

    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)

    Spaces that are both Noetherian and Hausdorff are finite.

    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 α)), S.Finite (tS, IsClosed t) (tS, IsIrreducible t) s = ⋃₀ S

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

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