Local compactness from local data, and lifting compact sets along open maps

A space in which every point has a locally compact neighbourhood is locally compact (TauCeti.locallyCompactSpace_of_forall_exists_mem_nhds).

Along an open map out of a weakly locally compact space, every compact subset of the range lies in the image of a compact set (IsOpenMap.exists_isCompact_subset_image). This is how a compactness statement about a quotient, such as a group modulo a kernel, is pulled back to the group.

A continuous injection out of a weakly locally compact space into a Hausdorff space is a topological embedding on an open neighbourhood of any compact set (Continuous.exists_opens_isEmbedding_restrict).

theorem TauCeti.locallyCompactSpace_of_forall_exists_mem_nhds {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∃ U ∈ nhds x, LocallyCompactSpace ↑U) : LocallyCompactSpace X

A space in which every point has a locally compact neighbourhood is locally compact.

theorem IsOpenMap.exists_isCompact_subset_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] {f : X → Y} (hf : IsOpenMap f) {K : Set Y} (hK : IsCompact K) (hKf : K ⊆ Set.range f) : ∃ (L : Set X), IsCompact L ∧ K ⊆ f '' L

Along an open map out of a weakly locally compact space, every compact subset of the range is contained in the image of a compact set.

theorem Continuous.exists_opens_isEmbedding_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] [T2Space Y] {f : X → Y} (hf : Continuous f) (hinj : Function.Injective f) {K : Set X} (hK : IsCompact K) : ∃ (W : TopologicalSpace.Opens X), K ⊆ ↑W ∧ Topology.IsEmbedding fun (q : ↥W) => f ↑q

A continuous injection from a weakly locally compact space into a Hausdorff space restricts to a topological embedding on some open neighbourhood of any compact set.