Documentation

Mathlib.Topology.Irreducible

Irreducibility in topological spaces #

Main definitions #

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) :

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

Equations
Instances For
    def IsIrreducible {X : Type u_1} [TopologicalSpace X] (s : Set X) :

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

    Equations
    Instances For
      theorem IsIrreducible.nonempty {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : IsIrreducible s) :
      s.Nonempty
      theorem Set.Subsingleton.isPreirreducible {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : s.Subsingleton) :

      Alias of the reverse direction of isPreirreducible_iff_closure.

      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 ut uu = t

      The set of irreducible components of a topological space.

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

        A maximal irreducible set that contains a given point.

        Equations
        Instances For

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

          Instances

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

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

            Instances
              theorem IrreducibleSpace.toNonempty {X : Type u_3} :
              ∀ {inst : TopologicalSpace X} [self : IrreducibleSpace X], Nonempty X
              theorem nonempty_preirreducible_inter {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} [PreirreducibleSpace X] :
              IsOpen sIsOpen ts.Nonemptyt.Nonempty(s t).Nonempty
              theorem IsOpen.dense {X : Type u_1} [TopologicalSpace X] {s : Set X} [PreirreducibleSpace X] (ho : IsOpen s) (hne : s.Nonempty) :

              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 : XY) (hf : ContinuousOn f s) :
              theorem IsIrreducible.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} (H : IsIrreducible s) (f : XY) (hf : ContinuousOn f s) :
              @[instance 100]

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

              Equations
              • =
              theorem isIrreducible_iff_sInter {X : Type u_1} [TopologicalSpace X] {s : Set X} :
              IsIrreducible s ∀ (U : Finset (Set X)), (∀ uU, IsOpen u)(∀ uU, (s u).Nonempty)(s ⋂₀ U).Nonempty

              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)), (∀ zt, IsClosed z)s ⋃₀ tzt, 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 : (S U).Nonempty) :
              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 : U.Nonempty) (hU' : IsOpen U) (h₁ : U S) (h₂ : S t) :

              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) :
              theorem IsPreirreducible.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {t : Set X} (ht : IsPreirreducible t) {f : YX} (hf : OpenEmbedding f) :