# 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

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.

## Instances For

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.

## Instances

The topology of `X`

is finer than the compactly generated topology.

## Equations

- ⋯ = ⋯

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.

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.

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.

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.

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.

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.

If the topology of `X`

is coinduced by a continuous function whose domain is
compactly generated, then so is `X`

.

The quotient of a compactly generated space is compactly generated.

## Equations

- ⋯ = ⋯

The sum of two compactly generated spaces is compactly generated.

## Equations

- ⋯ = ⋯

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

## Equations

- ⋯ = ⋯

A sequential space is compactly generated.

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

## Equations

- ⋯ = ⋯

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

## Instances For

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.

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.

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.

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.

In a compactly generated space `X`

, a set `s`

is closed when `s ∩ K`

is
closed for every compact set `K`

.

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.

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.

In a compactly generated space `X`

, a set `s`

is open when `s ∩ K`

is
closed for every open set `K`

.

If the topology of `X`

is coinduced by a continuous function whose domain is
compactly generated, then so is `X`

.

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

## Equations

- ⋯ = ⋯

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.

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.

A Hausdorff and weakly locally compact space is compactly generated.

## Equations

- ⋯ = ⋯