The compact-open topology: discreteness, and pairing maps into a product

A continuous map f from a compact space to a discrete space has finite image, and each of its fibres is closed, hence compact. Prescribing the value of a map on each of those finitely many fibres is therefore a finite intersection of compact-open subbasic sets, so it is an open condition, and it pins the map down to f itself. Consequently C(X, Y) is discrete.

Compactness of X is used and not merely convenient: for X = ℕ discrete and Y = Bool the compact subsets of X are the finite ones, so the compact-open topology on C(ℕ, Bool) is the product topology, which is not discrete.

The file also records when pairing two maps into a product, (f, g) ↦ (x ↦ (f x, g x)), is continuous for the compact-open topologies. Mathlib's ContinuousMap.continuous_prodMk_const is the case where the first map is constant. The case where the second map is constant follows by swapping the factors, and the general case holds for every regular source: a compact set on which (f, g) lands in an open set U is covered by finitely many compact pieces on each of which (f, g) lands in a box inside U, and the pieces exist because every point has a closed neighbourhood inside any given open one. Regularity is used and not merely convenient: for the one-point compactification of ℚ as source and the Sierpiński space as both targets, the maps (f, g) with f ⁻¹' {⊤} ∪ g ⁻¹' {⊤} = univ do not form an open set. Topological groups are regular, so these are the continuity statements behind the pointwise operations on the iterated function spaces C(G, C(G, …)) of the coinduced resolution of a topological representation.

instance ContinuousMap.discreteTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [DiscreteTopology Y] : DiscreteTopology C(X, Y)

The compact-open topology on the continuous maps from a compact space to a discrete space is discrete.

theorem ContinuousMap.continuous_prodMk_const_right {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] : Continuous fun (p : C(X, Y) × Z) => p.1.prodMk (const X p.2)

Pairing a map with a constant in the right component of a product is continuous, the mirror image of Mathlib's ContinuousMap.continuous_prodMk_const, whose constant is the left component.

theorem ContinuousMap.continuous_prodMk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] [RegularSpace X] : Continuous fun (p : C(X, Y) × C(X, Z)) => p.1.prodMk p.2

Pairing two maps into a product is continuous for a regular source, in particular for a topological group.