Irreducibility in topological spaces

Main definitions

• IrreducibleSpace: a typeclass applying to topological spaces, stating that the space is not the union of a nontrivial pair of disjoint opens.
• IsIrreducible: for a nonempty set in a topological space, the property that the set is an irreducible space in the subspace topology.

On the definition of irreducible and connected sets/spaces

In informal mathematics, irreducible spaces are assumed to be nonempty. We formalise the predicate without that assumption as IsPreirreducible. In other words, the only difference is whether the empty space counts as irreducible. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.

def IsPreirreducible {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

A preirreducible set s is one where there is no non-trivial pair of disjoint opens on s.

Equations

• IsPreirreducible s = ∀ (u v : Set X), IsOpen u → IsOpen v → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))

def IsIrreducible {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

An irreducible set s is one that is nonempty and where there is no non-trivial pair of disjoint opens on s.

Equations

• IsIrreducible s = (Set.Nonempty s ∧ IsPreirreducible s)

theorem IsIrreducible.nonempty {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : IsIrreducible s) : Set.Nonempty s

theorem IsIrreducible.isPreirreducible {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : IsIrreducible s) : IsPreirreducible s

theorem isPreirreducible_empty {X : Type u_1} [TopologicalSpace X] : IsPreirreducible ∅

theorem Set.Subsingleton.isPreirreducible {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : Set.Subsingleton s) : IsPreirreducible s

theorem isPreirreducible_singleton {X : Type u_1} [TopologicalSpace X] {x : X} : IsPreirreducible {x}

theorem isIrreducible_singleton {X : Type u_1} [TopologicalSpace X] {x : X} : IsIrreducible {x}

theorem isPreirreducible_iff_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsPreirreducible (closure s) ↔ IsPreirreducible s

theorem isIrreducible_iff_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsIrreducible (closure s) ↔ IsIrreducible s

theorem IsPreirreducible.closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsPreirreducible s → IsPreirreducible (closure s)

Alias of the reverse direction of isPreirreducible_iff_closure.

theorem IsIrreducible.closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsIrreducible s → IsIrreducible (closure s)

Alias of the reverse direction of isIrreducible_iff_closure.

theorem exists_preirreducible {X : Type u_1} [TopologicalSpace X] (s : Set X) (H : IsPreirreducible s) : ∃ (t : Set X), IsPreirreducible t ∧ s ⊆ t ∧ ∀ (u : Set X), IsPreirreducible u → t ⊆ u → u = t

def irreducibleComponents (X : Type u_3) [TopologicalSpace X] : Set (Set X)

The set of irreducible components of a topological space.

Equations

• irreducibleComponents X = maximals (fun (x x_1 : Set X) => x ≤ x_1) {s : Set X | IsIrreducible s}

theorem isClosed_of_mem_irreducibleComponents {X : Type u_1} [TopologicalSpace X] (s : Set X) (H : s ∈ irreducibleComponents X) : IsClosed s

theorem irreducibleComponents_eq_maximals_closed (X : Type u_3) [TopologicalSpace X] : irreducibleComponents X = maximals (fun (x x_1 : Set X) => x ≤ x_1) {s : Set X | IsClosed s ∧ IsIrreducible s}

def irreducibleComponent {X : Type u_1} [TopologicalSpace X] (x : X) : Set X

A maximal irreducible set that contains a given point.

Equations

• irreducibleComponent x = Classical.choose (_ : ∃ (t : Set X), IsPreirreducible t ∧ {x} ⊆ t ∧ ∀ (u : Set X), IsPreirreducible u → t ⊆ u → u = t)

theorem irreducibleComponent_property {X : Type u_1} [TopologicalSpace X] (x : X) : IsPreirreducible (irreducibleComponent x) ∧ {x} ⊆ irreducibleComponent x ∧ ∀ (u : Set X), IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x

theorem mem_irreducibleComponent {X : Type u_1} [TopologicalSpace X] {x : X} : x ∈ irreducibleComponent x

theorem isIrreducible_irreducibleComponent {X : Type u_1} [TopologicalSpace X] {x : X} : IsIrreducible (irreducibleComponent x)

theorem eq_irreducibleComponent {X : Type u_1} [TopologicalSpace X] {s : Set X} {x : X} : IsPreirreducible s → irreducibleComponent x ⊆ s → s = irreducibleComponent x

theorem irreducibleComponent_mem_irreducibleComponents {X : Type u_1} [TopologicalSpace X] (x : X) : irreducibleComponent x ∈ irreducibleComponents X

theorem isClosed_irreducibleComponent {X : Type u_1} [TopologicalSpace X] {x : X} : IsClosed (irreducibleComponent x)

class PreirreducibleSpace (X : Type u_3) [TopologicalSpace X] : Prop

A preirreducible space is one where there is no non-trivial pair of disjoint opens.

• isPreirreducible_univ : IsPreirreducible Set.univ

  In a preirreducible space, Set.univ is a preirreducible set.

class IrreducibleSpace (X : Type u_3) [TopologicalSpace X] extends PreirreducibleSpace : Prop

An irreducible space is one that is nonempty and where there is no non-trivial pair of disjoint opens.

• isPreirreducible_univ : IsPreirreducible Set.univ
• toNonempty : Nonempty X

theorem IrreducibleSpace.isIrreducible_univ (X : Type u_3) [TopologicalSpace X] [IrreducibleSpace X] : IsIrreducible Set.univ

theorem irreducibleSpace_def (X : Type u_3) [TopologicalSpace X] : IrreducibleSpace X ↔ IsIrreducible ⊤

theorem nonempty_preirreducible_inter {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} [PreirreducibleSpace X] : IsOpen s → IsOpen t → Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s ∩ t)

theorem IsOpen.dense {X : Type u_1} [TopologicalSpace X] {s : Set X} [PreirreducibleSpace X] (ho : IsOpen s) (hne : Set.Nonempty s) : Dense s

In a (pre)irreducible space, a nonempty open set is dense.

theorem IsPreirreducible.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (H : IsPreirreducible s) (f : X → Y) (hf : ContinuousOn f s) : IsPreirreducible (f '' s)

theorem IsIrreducible.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (H : IsIrreducible s) (f : X → Y) (hf : ContinuousOn f s) : IsIrreducible (f '' s)

theorem Subtype.preirreducibleSpace {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : IsPreirreducible s) : PreirreducibleSpace ↑s

theorem Subtype.irreducibleSpace {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : IsIrreducible s) : IrreducibleSpace ↑s

instance instIrreducibleSpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology {X : Type u_3} [Infinite X] : IrreducibleSpace (CofiniteTopology X)

An infinite type with cofinite topology is an irreducible topological space.

Equations

• (_ : IrreducibleSpace (CofiniteTopology X)) = (_ : IrreducibleSpace (CofiniteTopology X))

theorem isIrreducible_iff_sInter {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsIrreducible s ↔ ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, Set.Nonempty (s ∩ u)) → Set.Nonempty (s ∩ ⋂₀ ↑U)

A set s is irreducible if and only if for every finite collection of open sets all of whose members intersect s, s also intersects the intersection of the entire collection (i.e., there is an element of s contained in every member of the collection).

theorem isPreirreducible_iff_closed_union_closed {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

A set is preirreducible if and only if for every cover by two closed sets, it is contained in one of the two covering sets.

theorem isIrreducible_iff_sUnion_closed {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z

A set is irreducible if and only if for every cover by a finite collection of closed sets, it is contained in one of the members of the collection.

theorem subset_closure_inter_of_isPreirreducible_of_isOpen {X : Type u_1} [TopologicalSpace X] {S : Set X} {U : Set X} (hS : IsPreirreducible S) (hU : IsOpen U) (h : Set.Nonempty (S ∩ U)) : S ⊆ closure (S ∩ U)

A nonempty open subset of a preirreducible subspace is dense in the subspace.

theorem IsPreirreducible.subset_irreducible {X : Type u_1} [TopologicalSpace X] {t : Set X} {S : Set X} {U : Set X} (ht : IsPreirreducible t) (hU : Set.Nonempty U) (hU' : IsOpen U) (h₁ : U ⊆ S) (h₂ : S ⊆ t) : IsIrreducible S

If ∅ ≠ U ⊆ S ⊆ t such that U is open and t is preirreducible, then S is irreducible.

theorem IsPreirreducible.open_subset {X : Type u_1} [TopologicalSpace X] {t : Set X} {U : Set X} (ht : IsPreirreducible t) (hU : IsOpen U) (hU' : U ⊆ t) : IsPreirreducible U

theorem IsPreirreducible.interior {X : Type u_1} [TopologicalSpace X] {t : Set X} (ht : IsPreirreducible t) : IsPreirreducible (interior t)

theorem IsPreirreducible.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {t : Set X} (ht : IsPreirreducible t) {f : Y → X} (hf : OpenEmbedding f) : IsPreirreducible (f ⁻¹' t)