Documentation

Mathlib.Topology.Compactification.OnePoint

The OnePoint Compactification #

We construct the OnePoint compactification (the one-point compactification) of an arbitrary topological space X and prove some properties inherited from X.

Main definitions #

Main results #

Tags #

one-point compactification, compactness

Definition and basic properties #

In this section we define OnePoint X to be the disjoint union of X and , implemented as Option X. Then we restate some lemmas about Option X for OnePoint X.

def OnePoint (X : Type u_2) :
Type u_2

The OnePoint extension of an arbitrary topological space X

Equations
Instances For
    instance instReprOnePoint {X : Type u_1} [Repr X] :

    The repr uses the notation from the OnePoint locale.

    Equations
    • One or more equations did not get rendered due to their size.
    @[match_pattern]
    def OnePoint.infty {X : Type u_1} :

    The point at infinity

    Equations
    • OnePoint.infty = none
    Instances For

      The point at infinity

      Equations
      Instances For
        @[match_pattern]
        def OnePoint.some {X : Type u_1} :
        XOnePoint X

        Coercion from X to OnePoint X.

        Equations
        • OnePoint.some = some
        Instances For
          instance OnePoint.instCoeTC {X : Type u_1} :
          Equations
          • OnePoint.instCoeTC = { coe := OnePoint.some }
          Equations
          • OnePoint.instInhabited = { default := OnePoint.infty }
          instance OnePoint.instFintype {X : Type u_1} [Fintype X] :
          Equations
          instance OnePoint.infinite {X : Type u_1} [Infinite X] :
          Equations
          • =
          theorem OnePoint.coe_injective {X : Type u_1} :
          Function.Injective OnePoint.some
          theorem OnePoint.coe_eq_coe {X : Type u_1} {x : X} {y : X} :
          x = y x = y
          @[simp]
          theorem OnePoint.coe_ne_infty {X : Type u_1} (x : X) :
          x OnePoint.infty
          @[simp]
          theorem OnePoint.infty_ne_coe {X : Type u_1} (x : X) :
          OnePoint.infty x
          def OnePoint.rec {X : Type u_1} {C : OnePoint XSort u_2} (h₁ : C OnePoint.infty) (h₂ : (x : X) → C x) (z : OnePoint X) :
          C z

          Recursor for OnePoint using the preferred forms and ↑x.

          Equations
          Instances For
            theorem OnePoint.isCompl_range_coe_infty {X : Type u_1} :
            IsCompl (Set.range OnePoint.some) {OnePoint.infty}
            theorem OnePoint.range_coe_union_infty {X : Type u_1} :
            Set.range OnePoint.some {OnePoint.infty} = Set.univ
            @[simp]
            theorem OnePoint.insert_infty_range_coe {X : Type u_1} :
            insert OnePoint.infty (Set.range OnePoint.some) = Set.univ
            @[simp]
            theorem OnePoint.range_coe_inter_infty {X : Type u_1} :
            Set.range OnePoint.some {OnePoint.infty} =
            @[simp]
            theorem OnePoint.compl_range_coe {X : Type u_1} :
            (Set.range OnePoint.some) = {OnePoint.infty}
            theorem OnePoint.compl_infty {X : Type u_1} :
            {OnePoint.infty} = Set.range OnePoint.some
            theorem OnePoint.compl_image_coe {X : Type u_1} (s : Set X) :
            (OnePoint.some '' s) = OnePoint.some '' s {OnePoint.infty}
            theorem OnePoint.ne_infty_iff_exists {X : Type u_1} {x : OnePoint X} :
            x OnePoint.infty ∃ (y : X), y = x
            instance OnePoint.canLift {X : Type u_1} :
            CanLift (OnePoint X) X OnePoint.some fun (x : OnePoint X) => x OnePoint.infty
            Equations
            • =
            theorem OnePoint.not_mem_range_coe_iff {X : Type u_1} {x : OnePoint X} :
            xSet.range OnePoint.some x = OnePoint.infty
            theorem OnePoint.infty_not_mem_range_coe {X : Type u_1} :
            OnePoint.inftySet.range OnePoint.some
            theorem OnePoint.infty_not_mem_image_coe {X : Type u_1} {s : Set X} :
            OnePoint.inftyOnePoint.some '' s
            @[simp]
            theorem OnePoint.coe_preimage_infty {X : Type u_1} :
            OnePoint.some ⁻¹' {OnePoint.infty} =

            Topological space structure on OnePoint X #

            We define a topological space structure on OnePoint X so that s is open if and only if

            Then we reformulate this definition in a few different ways, and prove that (↑) : X → OnePoint X is an open embedding. If X is not a compact space, then we also prove that (↑) has dense range, so it is a dense embedding.

            Equations
            • One or more equations did not get rendered due to their size.
            theorem OnePoint.isOpen_def {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} :
            IsOpen s (OnePoint.infty sIsCompact (OnePoint.some ⁻¹' s)) IsOpen (OnePoint.some ⁻¹' s)
            theorem OnePoint.isOpen_iff_of_mem' {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty s) :
            IsOpen s IsCompact (OnePoint.some ⁻¹' s) IsOpen (OnePoint.some ⁻¹' s)
            theorem OnePoint.isOpen_iff_of_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty s) :
            IsOpen s IsClosed (OnePoint.some ⁻¹' s) IsCompact (OnePoint.some ⁻¹' s)
            theorem OnePoint.isOpen_iff_of_not_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.inftys) :
            IsOpen s IsOpen (OnePoint.some ⁻¹' s)
            theorem OnePoint.isClosed_iff_of_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty s) :
            IsClosed s IsClosed (OnePoint.some ⁻¹' s)
            theorem OnePoint.isClosed_iff_of_not_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.inftys) :
            IsClosed s IsClosed (OnePoint.some ⁻¹' s) IsCompact (OnePoint.some ⁻¹' s)
            @[simp]
            theorem OnePoint.isOpen_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} :
            IsOpen (OnePoint.some '' s) IsOpen s
            @[simp]
            theorem OnePoint.isClosed_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} :
            IsClosed (OnePoint.some '' s) IsClosed s IsCompact s

            An open set in OnePoint X constructed from a closed compact set in X

            Equations
            Instances For
              theorem OnePoint.infty_mem_opensOfCompl {X : Type u_1} [TopologicalSpace X] {s : Set X} (h₁ : IsClosed s) (h₂ : IsCompact s) :
              OnePoint.infty OnePoint.opensOfCompl s h₁ h₂
              theorem OnePoint.continuous_coe {X : Type u_1} [TopologicalSpace X] :
              Continuous OnePoint.some
              theorem OnePoint.isOpenMap_coe {X : Type u_1} [TopologicalSpace X] :
              IsOpenMap OnePoint.some
              theorem OnePoint.isClosed_infty {X : Type u_1} [TopologicalSpace X] :
              IsClosed {OnePoint.infty}
              theorem OnePoint.nhds_coe_eq {X : Type u_1} [TopologicalSpace X] (x : X) :
              nhds x = Filter.map OnePoint.some (nhds x)
              theorem OnePoint.nhdsWithin_coe_image {X : Type u_1} [TopologicalSpace X] (s : Set X) (x : X) :
              nhdsWithin (x) (OnePoint.some '' s) = Filter.map OnePoint.some (nhdsWithin x s)
              theorem OnePoint.nhdsWithin_coe {X : Type u_1} [TopologicalSpace X] (s : Set (OnePoint X)) (x : X) :
              nhdsWithin (x) s = Filter.map OnePoint.some (nhdsWithin x (OnePoint.some ⁻¹' s))
              theorem OnePoint.comap_coe_nhds {X : Type u_1} [TopologicalSpace X] (x : X) :
              Filter.comap OnePoint.some (nhds x) = nhds x
              instance OnePoint.nhdsWithin_compl_coe_neBot {X : Type u_1} [TopologicalSpace X] (x : X) [h : (nhdsWithin x {x}).NeBot] :
              (nhdsWithin x {x}).NeBot

              If x is not an isolated point of X, then x : OnePoint X is not an isolated point of OnePoint X.

              Equations
              • =
              theorem OnePoint.nhdsWithin_compl_infty_eq {X : Type u_1} [TopologicalSpace X] :
              nhdsWithin OnePoint.infty {OnePoint.infty} = Filter.map OnePoint.some (Filter.coclosedCompact X)
              instance OnePoint.nhdsWithin_compl_infty_neBot {X : Type u_1} [TopologicalSpace X] [NoncompactSpace X] :
              (nhdsWithin OnePoint.infty {OnePoint.infty}).NeBot

              If X is a non-compact space, then is not an isolated point of OnePoint X.

              Equations
              • =
              @[instance 900]
              instance OnePoint.nhdsWithin_compl_neBot {X : Type u_1} [TopologicalSpace X] [∀ (x : X), (nhdsWithin x {x}).NeBot] [NoncompactSpace X] (x : OnePoint X) :
              (nhdsWithin x {x}).NeBot
              Equations
              • =
              theorem OnePoint.nhds_infty_eq {X : Type u_1} [TopologicalSpace X] :
              nhds OnePoint.infty = Filter.map OnePoint.some (Filter.coclosedCompact X) pure OnePoint.infty
              theorem OnePoint.hasBasis_nhds_infty {X : Type u_1} [TopologicalSpace X] :
              (nhds OnePoint.infty).HasBasis (fun (s : Set X) => IsClosed s IsCompact s) fun (s : Set X) => OnePoint.some '' s {OnePoint.infty}
              @[simp]
              theorem OnePoint.comap_coe_nhds_infty {X : Type u_1} [TopologicalSpace X] :
              Filter.comap OnePoint.some (nhds OnePoint.infty) = Filter.coclosedCompact X
              theorem OnePoint.le_nhds_infty {X : Type u_1} [TopologicalSpace X] {f : Filter (OnePoint X)} :
              f nhds OnePoint.infty ∀ (s : Set X), IsClosed sIsCompact sOnePoint.some '' s {OnePoint.infty} f
              theorem OnePoint.ultrafilter_le_nhds_infty {X : Type u_1} [TopologicalSpace X] {f : Ultrafilter (OnePoint X)} :
              f nhds OnePoint.infty ∀ (s : Set X), IsClosed sIsCompact sOnePoint.some '' sf
              theorem OnePoint.tendsto_nhds_infty' {X : Type u_1} [TopologicalSpace X] {α : Type u_2} {f : OnePoint Xα} {l : Filter α} :
              Filter.Tendsto f (nhds OnePoint.infty) l Filter.Tendsto f (pure OnePoint.infty) l Filter.Tendsto (f OnePoint.some) (Filter.coclosedCompact X) l
              theorem OnePoint.tendsto_nhds_infty {X : Type u_1} [TopologicalSpace X] {α : Type u_2} {f : OnePoint Xα} {l : Filter α} :
              Filter.Tendsto f (nhds OnePoint.infty) l sl, f OnePoint.infty s ∃ (t : Set X), IsClosed t IsCompact t Set.MapsTo (f OnePoint.some) t s
              theorem OnePoint.continuousAt_infty' {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : OnePoint XY} :
              ContinuousAt f OnePoint.infty Filter.Tendsto (f OnePoint.some) (Filter.coclosedCompact X) (nhds (f OnePoint.infty))
              theorem OnePoint.continuousAt_infty {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : OnePoint XY} :
              ContinuousAt f OnePoint.infty snhds (f OnePoint.infty), ∃ (t : Set X), IsClosed t IsCompact t Set.MapsTo (f OnePoint.some) t s
              theorem OnePoint.continuousAt_coe {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : OnePoint XY} {x : X} :
              ContinuousAt f x ContinuousAt (f OnePoint.some) x

              If X is not a compact space, then the natural embedding X → OnePoint X has dense range.

              @[simp]
              theorem OnePoint.specializes_coe {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
              x y x y
              @[simp]
              theorem OnePoint.inseparable_coe {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
              theorem OnePoint.not_specializes_infty_coe {X : Type u_1} [TopologicalSpace X] {x : X} :
              ¬OnePoint.infty x
              theorem OnePoint.not_inseparable_infty_coe {X : Type u_1} [TopologicalSpace X] {x : X} :
              ¬Inseparable OnePoint.infty x
              theorem OnePoint.not_inseparable_coe_infty {X : Type u_1} [TopologicalSpace X] {x : X} :
              ¬Inseparable (x) OnePoint.infty
              theorem OnePoint.inseparable_iff {X : Type u_1} [TopologicalSpace X] {x : OnePoint X} {y : OnePoint X} :
              Inseparable x y x = OnePoint.infty y = OnePoint.infty ∃ (x' : X), x = x' ∃ (y' : X), y = y' Inseparable x' y'

              Compactness and separation properties #

              In this section we prove that OnePoint X is a compact space; it is a T₀ (resp., T₁) space if the original space satisfies the same separation axiom. If the original space is a locally compact Hausdorff space, then OnePoint X is a normal (hence, T₃ and Hausdorff) space.

              Finally, if the original space X is not compact and is a preconnected space, then OnePoint X is a connected space.

              For any topological space X, its one point compactification is a compact space.

              Equations
              • =

              The one point compactification of a T0Space space is a T0Space.

              Equations
              • =

              The one point compactification of a T1Space space is a T1Space.

              Equations
              • =

              The one point compactification of a locally compact R₁ space is a normal topological space.

              Equations
              • =

              If X is not a compact space, then OnePoint X is a connected space.

              Equations
              • =

              If X is an infinite type with discrete topology (e.g., ), then the identity map from CofiniteTopology (OnePoint X) to OnePoint X is not continuous.

              theorem Continuous.homeoOfEquivCompactToT2.t1_counterexample :
              ∃ (α : Type) (β : Type) (x : TopologicalSpace α) (x_1 : TopologicalSpace β), CompactSpace α T1Space β ∃ (f : α β), Continuous f ¬Continuous f.symm

              A concrete counterexample shows that Continuous.homeoOfEquivCompactToT2 cannot be generalized from T2Space to T1Space.

              Let α = OnePoint be the one-point compactification of , and let β be the same space OnePoint with the cofinite topology. Then α is compact, β is T1, and the identity map id : α → β is a continuous equivalence that is not a homeomorphism.