TopologicalSpace.noetherianSpace_iff_opens
theorem TopologicalSpace.noetherianSpace_iff_opens :
∀ (α : Type u_1) [inst : TopologicalSpace α],
TopologicalSpace.NoetherianSpace α ↔ ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s
The theorem `TopologicalSpace.noetherianSpace_iff_opens` establishes an equivalence between two conditions for a given type `α` with a `TopologicalSpace` structure. The first condition is that `α` is a Noetherian space, that means every nonempty set of open subsets of `α` has a minimal element. The second condition is that for every open subset `s` of `α`, the set `s` is compact. Here, a set being compact means that for any nontrivial filter `f` that contains the set, there exists an element in the set such that every set in the filter intersects with every neighborhood of that element.
More concisely: A topological space is Noetherian if and only if every open subset is compact.
|
TopologicalSpace.NoetherianSpace.finite
theorem TopologicalSpace.NoetherianSpace.finite :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.NoetherianSpace α] [inst : T2Space α],
Finite α
This theorem states that for any type 'α' that has a topological space structure, if 'α' is a Noetherian space and a Hausdorff space (also known as T2 space), then 'α' is finite. Here, a Noetherian space is a topological space that satisfies the descending chain condition for closed subsets, and a Hausdorff space is a topological space where any two distinct points have disjoint neighborhoods. The theorem thus captures a property of topological spaces that are both Noetherian and Hausdorff, stating that such spaces are always finite.
More concisely: A Noetherian and Hausdorff topological space is a finite space.
|
TopologicalSpace.NoetherianSpace.isCompact
theorem TopologicalSpace.NoetherianSpace.isCompact :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.NoetherianSpace α] (s : Set α),
IsCompact s
This theorem states that in a Noetherian topological space, all sets are compact. Formally, for any type `α` that has a topological space structure and is a Noetherian space, any set `s` of type `α` is compact. In other words, for any nontrivial filter `f` that contains `s`, there exists an element `x` in `s` such that every set of `f` intersects every neighborhood of `x`.
More concisely: In a Noetherian topological space, every set is compact.
|
TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible
theorem TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.NoetherianSpace α]
(s : TopologicalSpace.Closeds α), ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
The theorem states that in a Noetherian topological space, every closed set can be expressed as a finite union of irreducible closed sets. Here, a Noetherian topological space is one that satisfies the descending chain condition for closed sets, and an irreducible set is one that is nonempty and does not admit a non-trivial pair of disjoint open subsets. Specifically, for every closed set in the space, there exists a finite set of irreducible closed subsets such that every subset in the set is irreducible and the closed set is the supremum (least upper bound) of the set.
More concisely: In a Noetherian topological space, every closed set is the supremum of a finite number of irreducible closed sets.
|
TopologicalSpace.noetherianSpace_TFAE
theorem TopologicalSpace.noetherianSpace_TFAE :
∀ (α : Type u_1) [inst : TopologicalSpace α],
[TopologicalSpace.NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s,
∀ (s : TopologicalSpace.Opens α), IsCompact ↑s].TFAE
This theorem states that for any topological space `α`, the following propositions are equivalent:
1. `α` is a Noetherian space, which means it satisfies the descending chain condition, i.e., there is no infinite descending chain of open subsets.
2. The relation "s < t" is well-founded on the set of all subsets of `α`. Here, "s < t" indicates that `s` is strictly included in `t`.
3. Every subset of `α` is compact. A subset `s` is said to be compact if for every nontrivial filter `f` that contains `s`, there exists an element `x` in `s` such that every set of `f` meets every neighborhood of `x`.
4. Every open subset of `α` is compact. In other words, for every open subset `s` of `α`, if `f` is a nontrivial filter that contains `s`, then there is an element `x` in `s` where every set of `f` meets every neighborhood of `x`.
This theorem forms a link between the notions of Noetherian spaces, well-foundation of the strict inclusion relation, and compactness of all subsets and open subsets for any given topological space.
More concisely: A topological space is Noetherian if and only if the strict inclusion relation on its subsets is well-founded and every subset is compact.
|
TopologicalSpace.NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent
theorem TopologicalSpace.NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.NoetherianSpace α],
∀ Z ∈ irreducibleComponents α, ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z
This theorem, referenced as Lemma 0052 (3) in the Stacks Project, states that for any Noetherian topological space `α`, for any set `Z` that is an irreducible component of `α`, there exists an open set `o` such that `o` is nonempty and is a subset of `Z`. In other words, in a Noetherian topological space, every irreducible component contains a nonempty open set.
More concisely: In a Noetherian topological space, every irreducible component contains a nonempty open subset.
|
TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible
theorem TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.NoetherianSpace α] {s : Set α},
IsClosed s → ∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = S.sUnion
The theorem `TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible` states that in a Noetherian topological space, any closed set can be represented as a finite union of irreducible closed sets. Here, a Noetherian space is a type of topological space that has the property that every non-empty collection of closed subsets has a minimal element. An irreducible set is a non-empty set which doesn't permit a non-trivial pair of disjoint open subsets. The theorem guarantees the existence of a finite collection of such irreducible closed sets which, when taken their union, yield the original closed set.
More concisely: In a Noetherian topological space, every closed set can be written as a finite union of irreducible closed sets.
|
TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
theorem TopologicalSpace.NoetherianSpace.finite_irreducibleComponents :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.NoetherianSpace α],
(irreducibleComponents α).Finite
This theorem states that for any type `α` which is equipped with a `TopologicalSpace` structure and also given that this topological space is a `NoetherianSpace`, the set of irreducible components of this topological space is finite. Here, irreducible components of a topological space refer to the maximal irreducible subsets of the space. An irreducible set in a topological space is a non-empty subset that cannot be expressed as the union of two proper closed subsets. This theorem is referred to as Lemma 0052 (2) in the Stacks Project.
More concisely: In a Noetherian topological space, the number of irreducible components is finite.
|
TopologicalSpace.NoetherianSpace.exists_finset_irreducible
theorem TopologicalSpace.NoetherianSpace.exists_finset_irreducible :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.NoetherianSpace α]
(s : TopologicalSpace.Closeds α), ∃ S, (∀ (k : { x // x ∈ S }), IsIrreducible ↑↑k) ∧ s = S.sup id
This theorem states that in a Noetherian topological space, every closed set can be expressed as a finite union of irreducible closed sets. Here, a set is considered irreducible if it is nonempty and there are no non-trivial pair of disjoint open sets within it. In the context of the theorem, the Noetherian space is of any arbitrary type `α` and a closed set `s` in this topological space is considered. The theorem guarantees that there exists a finite set `S` such that every element `k` in `S` corresponds to an irreducible set, and the union of all such irreducible sets forms the original closed set `s`.
More concisely: In a Noetherian topological space, every closed set can be expressed as a finite union of irreducible closed sets.
|