Compactly coherent spaces and the k-ification

In this file we will define compactly coherent spaces and prove basic properties about them. This is a weaker version of CompactlyGeneratedSpace. These notions agree on Hausdorff spaces. They are both referred to as compactly generated spaces in the literature.

Main definitions

• CompactlyCoherentSpace: A compactly coherent space is a topological space in which a set A is open iff for every compact set B, the intersection A ∩ B is open in B.

Main results

• CompactlyCoherentSpace.of_weaklyLocallyCompactSpace: every weakly locally compact space is a compactly coherent space.
• CompactlyCoherentSpace.of_sequentialSpace: every sequential space is a compactly coherent space.

References

• [J. Munkres, Topology][Munkres2000]
• https://en.wikipedia.org/wiki/Compactly_generated_space

Compactly coherent spaces

class CompactlyCoherentSpace (X : Type u_1) [TopologicalSpace X] : Prop

A space is a compactly coherent space if the topology is generated by the compact sets.

• isCoherentWith : Topology.IsCoherentWith {K : Set X | IsCompact K}

  A space is a compactly coherent space if the topology is generated by the compact sets.

theorem CompactlyCoherentSpace.isOpen_iff {X : Type u} [TopologicalSpace X] [CompactlyCoherentSpace X] {A : Set X} : IsOpen A ↔ ∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' A)

A set A in a compactly coherent space is open iff for every compact set K, the intersection K ∩ A is open in K.

theorem CompactlyCoherentSpace.isClosed_iff {X : Type u} [TopologicalSpace X] [CompactlyCoherentSpace X] (A : Set X) : IsClosed A ↔ ∀ (K : Set X), IsCompact K → IsClosed (Subtype.val ⁻¹' A)

A set A in a compactly coherent space is closed iff for every compact set K, the intersection K ∩ A is closed in K.

theorem CompactlyCoherentSpace.of_isOpen {X : Type u} [TopologicalSpace X] (h : ∀ (A : Set X), (∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' A)) → IsOpen A) : CompactlyCoherentSpace X

If every set A is open if for every compact K the intersection K ∩ A is open in K, then the space is a compactly coherent space.

theorem CompactlyCoherentSpace.of_isClosed {X : Type u} [TopologicalSpace X] (h : ∀ (A : Set X), (∀ (K : Set X), IsCompact K → IsClosed (Subtype.val ⁻¹' A)) → IsClosed A) : CompactlyCoherentSpace X

If every set A is closed if for every compact K the intersection K ∩ A is closed in K, then the space is a compactly coherent space.

instance CompactlyCoherentSpace.of_weaklyLocallyCompactSpace {X : Type u} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] : CompactlyCoherentSpace X

Every weakly locally compact space is a compactly coherent space.

instance CompactlyCoherentSpace.of_sequentialSpace {X : Type u} [TopologicalSpace X] [SequentialSpace X] : CompactlyCoherentSpace X

Every sequential space is a compactly coherent space.

theorem CompactlyCoherentSpace.isOpen_iff_forall_compactSpace {X : Type u} [TopologicalSpace X] [CompactlyCoherentSpace X] (s : Set X) : IsOpen s ↔ ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)

In a compactly coherent space X, a set s is open iff f ⁻¹' s is open for every continuous map from a compact space.

theorem CompactlyCoherentSpace.of_isOpen_forall_compactSpace {X : Type u} [TopologicalSpace X] (h : ∀ (s : Set X), (∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) → IsOpen s) : CompactlyCoherentSpace X

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