Compactly coherent spaces and the compact coherentification

In this file we will define compactly coherent spaces and the compact coherentification 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 while the compact coherentification is often called the k-ification.

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.
• CompactCoherentification: For a topological space X one can define another topology on X as follows: A is open iff for all compact sets 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.
• CompactCoherentification.isCompact_iff: The compact sets of a topological space and its compact coherentification agree.
• CompactCoherentification.instCompactlyCoherentSpace: The compact coherentification makes any space into a compactly coherent space.
• CompactCoherentification.homeo: The compact coherentification of a compactly coherent space X preserves the topology on X.
• CompactCoherentification.continuous_map_of_continuousOn: If a map f : X → Y is continuous on every compact subset of X then it is continuous when viewed as a map from CompactCoherentification X to CompactCoherentification Y.

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.

def CompactCoherentification (X : Type u_1) : Type u_1

A type synonym used for the compact coherentification of a topological space.

Equations

• CompactCoherentification X = X

def CompactCoherentification.«term𝐤_» : Lean.ParserDescr

A type synonym used for the compact coherentification of a topological space.

Equations

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

noncomputable def CompactCoherentification.mk (X : Type u_1) : X ≃ CompactCoherentification X

The map taking a space to its compact coherentification.

Equations

• CompactCoherentification.mk X = Equiv.refl X

noncomputable def CompactCoherentification.map {X : Type u_1} {Y : Type u_2} (f : X → Y) : CompactCoherentification X → CompactCoherentification Y

For a map f : X → Y of topological spaces, CompactCoherentification.map f is the corresponding map between the compact coherentifications of X and Y.

Equations

• CompactCoherentification.map f = ⇑(CompactCoherentification.mk Y) ∘ f ∘ ⇑(CompactCoherentification.mk X).symm

theorem CompactCoherentification.map_comp_mk {X : Type u_1} {Y : Type u_2} {f : X → Y} : CompactCoherentification.map f ∘ ⇑(CompactCoherentification.mk X) = ⇑(CompactCoherentification.mk Y) ∘ f

@[implicit_reducible]

noncomputable instance CompactCoherentification.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] : TopologicalSpace (CompactCoherentification X)

For a topological space X the compact coherentification is defined as: A is open iff for all compact sets B, the intersection A ∩ B is open in B.

Equations

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

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

A set A in the compact coherentification is open iff for all compact sets K, the intersection K ∩ A is open in K.

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

A set A is the compact coherentification is closed iff for all compact sets K, the intersection K ∩ A is closed in K.

theorem CompactCoherentification.continuous_dom_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : CompactCoherentification X → Y} : Continuous f ↔ ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K

theorem CompactCoherentification.continuous_mk_symm {X : Type u_1} [TopologicalSpace X] : Continuous ⇑(CompactCoherentification.mk X).symm

theorem CompactCoherentification.continuous_dom_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : Continuous (f ∘ ⇑(CompactCoherentification.mk X).symm)

theorem CompactCoherentification.isOpenMap_mk {X : Type u_1} [TopologicalSpace X] : IsOpenMap ⇑(CompactCoherentification.mk X)

theorem CompactCoherentification.continuousOn_isCompact_mk {X : Type u_1} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) : ContinuousOn (⇑(CompactCoherentification.mk X)) K

theorem CompactCoherentification.continuousOn_rng_of_isCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → CompactCoherentification Y} {K : Set X} (hK : IsCompact K) : ContinuousOn f K ↔ ContinuousOn (⇑(CompactCoherentification.mk Y).symm ∘ f) K

theorem CompactCoherentification.continuous_mk {X : Type u_1} [TopologicalSpace X] [CompactlyCoherentSpace X] : Continuous ⇑(CompactCoherentification.mk X)

theorem CompactCoherentification.continuous_rng_of_compactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → CompactCoherentification Y} [CompactSpace X] : Continuous f ↔ Continuous (⇑(CompactCoherentification.mk Y).symm ∘ f)

theorem CompactCoherentification.continuous_map_of_continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : ∀ (K : Set X), IsCompact K → ContinuousOn f K) : Continuous (CompactCoherentification.map f)

If a map f : X → Y is continuous on every compact subset of X then it is continuous when viewed as a map from CompactCoherentification X to CompactCoherentification Y.

theorem CompactCoherentification.continuous_map_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : Continuous (CompactCoherentification.map f)

theorem CompactCoherentification.continuous_mk_comp_iff_of_compactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] {f : X → Y} : Continuous (⇑(CompactCoherentification.mk Y) ∘ f) ↔ Continuous f

theorem CompactCoherentification.continuousOn_mk_comp_iff_of_Compact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {A : Set X} (hA : IsCompact A) {f : X → Y} : ContinuousOn (⇑(CompactCoherentification.mk Y) ∘ f) A ↔ ContinuousOn f A

theorem CompactCoherentification.isCompact_iff {X : Type u_1} [TopologicalSpace X] {K : Set (CompactCoherentification X)} : IsCompact K ↔ IsCompact (⇑(CompactCoherentification.mk X) ⁻¹' K)

The compact sets of a topological space and its compact coherentification agree.

theorem CompactCoherentification.isCompact_image_mk_iff {X : Type u_1} [TopologicalSpace X] {K : Set X} : IsCompact (⇑(CompactCoherentification.mk X) '' K) ↔ IsCompact K

The compact sets of a topological space and its compact coherentification agree.

instance CompactCoherentification.instCompactlyCoherentSpace {X : Type u_1} [TopologicalSpace X] : CompactlyCoherentSpace (CompactCoherentification X)

The compact coherentification makes any space into a compactly coherent space.

noncomputable def CompactCoherentification.homeo {X : Type u_1} [TopologicalSpace X] [CompactlyCoherentSpace X] : X ≃ₜ CompactCoherentification X

The compact coherentification preserves the topology of k-spaces.

Equations

• CompactCoherentification.homeo = { toEquiv := CompactCoherentification.mk X, continuous_toFun := ⋯, continuous_invFun := ⋯ }

instance CompactCoherentification.t2space {X : Type u_1} [TopologicalSpace X] [t : T2Space X] : T2Space (CompactCoherentification X)