Documentation

Mathlib.Topology.Compactness.CompactlyCoherentSpace

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 #

Main results #

References #

Compactly coherent spaces #

source
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.

Instances
    source
    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.

    source
    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.

    source
    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.

    source
    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.

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

    Every weakly locally compact space is a compactly coherent space.

    source
    @[deprecated CompactlyCoherentSpace.of_weaklyLocallyCompactSpace (since := "2025-05-30")]
    theorem Topology.IsCoherentWith.isCompact_of_weaklyLocallyCompact {X : Type u} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] :
    CompactlyCoherentSpace X

    Alias of CompactlyCoherentSpace.of_weaklyLocallyCompactSpace.

    Every weakly locally compact space is a compactly coherent space.

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

    Every sequential space is a compactly coherent space.

    source
    @[deprecated CompactlyCoherentSpace.of_sequentialSpace (since := "2025-05-30")]
    theorem Topology.IsCoherentWith.isCompact_of_seq {X : Type u} [TopologicalSpace X] [SequentialSpace X] :
    CompactlyCoherentSpace X

    Alias of CompactlyCoherentSpace.of_sequentialSpace.

    Every sequential space is a compactly coherent space.

    source
    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.

    source
    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.