Compactly generated topological spaces

This file defines compactly generated topological spaces A compactly generated space is a space X whose topology is coinduced by continuous maps from compact Hausdorff spaces to X. In such a space, a set s is closed (resp. open) if and only if for all compact Hausdorff space K and f : K → X continuous, f ⁻¹' s is closed (resp. open) in K.

We provide two definitions. UCompactlyGeneratedSpace.{u} X corresponds to the type class where the compact Hausdorff spaces are taken in an arbitrary universe u, and should therefore always be used with an explicit universe parameter. It is intended for categorical purposes.

CompactlyGeneratedSpace X corresponds to the case where compact Hausdorff spaces are taken in the same universe as X, and is intended for topological purposes.

We prov basic properties and instances, and prove that a SequentialSpace is compactly generated, as well as a Hausdorff WeaklyLocallyCompactSpace.

Main definitions

• UCompactlyGeneratedSpace.{u} X: the topology of X is coinduced by continuous maps coming from compact Hausdorff spaces in universe u.
• CompactlyGeneratedSpace X: the topology of X is coinduced by continuous maps coming from compact Hausdorff spaces in the same universe as X.

References

• https://en.wikipedia.org/wiki/Compactly_generated_space
• https://ncatlab.org/nlab/files/StricklandCGHWSpaces.pdf

Tags

compactly generated space

def TopologicalSpace.compactlyGenerated (X : Type w) [TopologicalSpace X] : TopologicalSpace X

The compactly generated topology on a topological space X. This is the finest topology which makes all maps from compact Hausdorff spaces to X, which are continuous for the original topology, continuous.

Note: this definition should be used with an explicit universe parameter u for the size of the compact Hausdorff spaces mapping to X.

Equations

• One or more equations did not get rendered due to their size.

theorem continuous_from_compactlyGenerated {X : Type w} {Y : Type x} [TopologicalSpace X] [t : TopologicalSpace Y] (f : X → Y) (h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) : Continuous f

class UCompactlyGeneratedSpace (X : Type v) [t : TopologicalSpace X] : Prop

A topological space X is compactly generated if its topology is finer than (and thus equal to) the compactly generated topology, i.e. it is coinduced by the continuous maps from compact Hausdorff spaces to X.

This version includes an explicit universe parameter u which should always be specified. It is intended for categorical purposes. See CompactlyGeneratedSpace for the version without this parameter, intended for topological purposes.

• le_compactlyGenerated : t ≤ TopologicalSpace.compactlyGenerated X

  The topology of X is finer than the compactly generated topology.

theorem UCompactlyGeneratedSpace.le_compactlyGenerated {X : Type v} [t : TopologicalSpace X] [self : UCompactlyGeneratedSpace X] : t ≤ TopologicalSpace.compactlyGenerated X

The topology of X is finer than the compactly generated topology.

theorem eq_compactlyGenerated {X : Type w} [t : TopologicalSpace X] [UCompactlyGeneratedSpace X] : t = TopologicalSpace.compactlyGenerated X

instance instUCompactlyGeneratedSpaceOfDiscreteTopology (X : Type v) [t : TopologicalSpace X] [DiscreteTopology X] : UCompactlyGeneratedSpace X

Equations

• ⋯ = ⋯

theorem uCompactlyGeneratedSpace_of_continuous_maps {X : Type w} [t : TopologicalSpace X] (h : ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y), (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f) : UCompactlyGeneratedSpace X

Let f : X → Y. Suppose that to prove that f is continuous, it suffices to show that for every compact Hausdorff space K and every continuous map g : K → X, f ∘ g is continuous. Then X is compactly generated.

theorem continuous_from_uCompactlyGeneratedSpace {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X] (f : X → Y) (h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) : Continuous f

If X is compactly generated, to prove that f : X → Y is continuous it is enough to show that for every compact Hausdorff space K and every continuous map g : K → X, f ∘ g is continuous.

theorem uCompactlyGeneratedSpace_of_isClosed {X : Type w} [tX : TopologicalSpace X] (h : ∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)) → IsClosed s) : UCompactlyGeneratedSpace X

A topological space X is compactly generated if a set s is closed when f ⁻¹' s is closed for every continuous map f : K → X, where K is compact Hausdorff.

theorem uCompactlyGeneratedSpace_of_isOpen {X : Type w} [tX : TopologicalSpace X] (h : ∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) → IsOpen s) : UCompactlyGeneratedSpace X

A topological space X is compactly generated if a set s is open when f ⁻¹' s is open for every continuous map f : K → X, where K is compact Hausdorff.

theorem UCompactlyGeneratedSpace.isClosed {X : Type w} [tX : TopologicalSpace X] [UCompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)) : IsClosed s

In a compactly generated space X, a set s is closed when f ⁻¹' s is closed for every continuous map f : K → X, where K is compact Hausdorff.

theorem UCompactlyGeneratedSpace.isOpen {X : Type w} [tX : TopologicalSpace X] [UCompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) : IsOpen s

In a compactly generated space X, a set s is open when f ⁻¹' s is open for every continuous map f : K → X, where K is compact Hausdorff.

theorem uCompactlyGeneratedSpace_of_coinduced {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X] {f : X → Y} (hf : Continuous f) (ht : tY = TopologicalSpace.coinduced f tX) : UCompactlyGeneratedSpace Y

If the topology of X is coinduced by a continuous function whose domain is compactly generated, then so is X.

instance instUCompactlyGeneratedSpaceQuotient {X : Type w} [tX : TopologicalSpace X] {S : Setoid X} [UCompactlyGeneratedSpace X] : UCompactlyGeneratedSpace (Quotient S)

The quotient of a compactly generated space is compactly generated.

Equations

• ⋯ = ⋯

instance instUCompactlyGeneratedSpaceSum {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X] [UCompactlyGeneratedSpace Y] : UCompactlyGeneratedSpace (X ⊕ Y)

The sum of two compactly generated spaces is compactly generated.

Equations

• ⋯ = ⋯

instance instUCompactlyGeneratedSpaceSigma {ι : Type v} {X : ι → Type w} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), UCompactlyGeneratedSpace (X i)] : UCompactlyGeneratedSpace ((i : ι) × X i)

The sigma type associated to a family of compactly generated spaces is compactly generated.

Equations

• ⋯ = ⋯

@[instance 100]

instance instUCompactlyGeneratedSpaceOfSequentialSpace {X : Type w} [tX : TopologicalSpace X] [SequentialSpace X] : UCompactlyGeneratedSpace X

A sequential space is compactly generated.

The proof is taken from https://ncatlab.org/nlab/files/StricklandCGHWSpaces.pdf, Proposition 1.6.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CompactlyGeneratedSpace (X : Type u) [TopologicalSpace X] : Prop

A topological space X is compactly generated if its topology is finer than (and thus equal to) the compactly generated topology, i.e. it is coinduced by the continuous maps from compact Hausdorff spaces to X.

In this version, intended for topological purposes, the compact spaces are taken in the same universe as X. See UCompactlyGeneratedSpace for a version with an explicit universe parameter, intended for categorical purposes.

Equations

• CompactlyGeneratedSpace X = UCompactlyGeneratedSpace X

theorem continuous_from_compactlyGeneratedSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [CompactlyGeneratedSpace X] (f : X → Y) (h : ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (g : K → X), Continuous g → Continuous (f ∘ g)) : Continuous f

If X is compactly generated, to prove that f : X → Y is continuous it is enough to show that for every compact Hausdorff space K and every continuous map g : K → X, f ∘ g is continuous.

theorem compactlyGeneratedSpace_of_continuous_maps {X : Type u} [TopologicalSpace X] (h : ∀ {Y : Type u} [inst : TopologicalSpace Y] (f : X → Y), (∀ (K : Type u) [inst_1 : TopologicalSpace K] [inst_2 : CompactSpace K] [inst_3 : T2Space K] (g : K → X), Continuous g → Continuous (f ∘ g)) → Continuous f) : CompactlyGeneratedSpace X

Let f : X → Y. Suppose that to prove that f is continuous, it suffices to show that for every compact Hausdorff space K and every continuous map g : K → X, f ∘ g is continuous. Then X is compactly generated.

theorem compactlyGeneratedSpace_of_isClosed {X : Type u} [TopologicalSpace X] (h : ∀ (s : Set X), (∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X), Continuous f → IsClosed (f ⁻¹' s)) → IsClosed s) : CompactlyGeneratedSpace X

A topological space X is compactly generated if a set s is closed when f ⁻¹' s is closed for every continuous map f : K → X, where K is compact Hausdorff.

theorem CompactlyGeneratedSpace.isClosed' {X : Type u} [TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X), Continuous f → IsClosed (f ⁻¹' s)) : IsClosed s

In a compactly generated space X, a set s is closed when f ⁻¹' s is closed for every continuous map f : K → X, where K is compact Hausdorff.

theorem CompactlyGeneratedSpace.isClosed {X : Type u} [TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)) : IsClosed s

In a compactly generated space X, a set s is closed when s ∩ K is closed for every compact set K.

theorem compactlyGeneratedSpace_of_isOpen {X : Type u} [TopologicalSpace X] (h : ∀ (s : Set X), (∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) → IsOpen s) : CompactlyGeneratedSpace X

A topological space X is compactly generated if a set s is open when f ⁻¹' s is open for every continuous map f : K → X, where K is compact Hausdorff.

theorem CompactlyGeneratedSpace.isOpen' {X : Type u} [TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) : IsOpen s

In a compactly generated space X, a set s is open when f ⁻¹' s is open for every continuous map f : K → X, where K is compact Hausdorff.

theorem CompactlyGeneratedSpace.isOpen {X : Type u} [TopologicalSpace X] [CompactlyGeneratedSpace X] {s : Set X} (hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen (s ∩ K)) : IsOpen s

In a compactly generated space X, a set s is open when s ∩ K is closed for every open set K.

theorem compactlyGeneratedSpace_of_coinduced {X : Type u} [tX : TopologicalSpace X] {Y : Type u} [tY : TopologicalSpace Y] [CompactlyGeneratedSpace X] {f : X → Y} (hf : Continuous f) (ht : tY = TopologicalSpace.coinduced f tX) : CompactlyGeneratedSpace Y

If the topology of X is coinduced by a continuous function whose domain is compactly generated, then so is X.

instance instCompactlyGeneratedSpaceSigma {ι : Type u} {X : ι → Type v} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), CompactlyGeneratedSpace (X i)] : CompactlyGeneratedSpace ((i : ι) × X i)

The sigma type associated to a family of compactly generated spaces is compactly generated.

Equations

• ⋯ = ⋯

theorem compactlyGeneratedSpace_of_isClosed_of_t2 {X : Type u} [TopologicalSpace X] [T2Space X] (h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s) : CompactlyGeneratedSpace X

Let s ⊆ X. Suppose that X is Hausdorff, and that to prove that s is closed, it suffices to show that for every compact set K ⊆ X, s ∩ K is closed. Then X is compactly generated.

theorem compactlyGeneratedSpace_of_isOpen_of_t2 {X : Type u} [TopologicalSpace X] [T2Space X] (h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' s)) → IsOpen s) : CompactlyGeneratedSpace X

Let s ⊆ X. Suppose that X is Hausdorff, and that to prove that s is open, it suffices to show that for every compact set K ⊆ X, s ∩ K is open in K. Then X is compactly generated.

@[instance 100]

instance instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpaceOfT2Space {X : Type u} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [T2Space X] : CompactlyGeneratedSpace X

A Hausdorff and weakly locally compact space and compactly generated.

Equations

• ⋯ = ⋯