Continuous extension from a closed subspace of a profinite space

Let X be a profinite space — compact, Hausdorff and totally disconnected — and let Y be a discrete space. This file proves that a continuous map into Y defined on a closed subspace s ⊆ X extends to a continuous map on all of X, as soon as one of s and Y is nonempty; equivalently, that restriction C(X, Y) → C(s, Y) is surjective for every closed s ⊆ X when Y is nonempty.

This is the zero-dimensional analogue of the Tietze extension theorem. Nothing can be averaged here, since Y is a bare discrete space; instead the map has only finitely many fibres, because a compact subset of a discrete space is finite, and those fibres are separated by a clopen partition of X. Mathlib's Profinite.exists_lift_of_finite_of_injective_of_surjective packages that separation as a lifting property — this is where total disconnectedness is used — and the work below is the passage from a lifting square to an extension.

Main results

• TauCeti.exists_continuous_eqOn_range_subset_image: for a nonempty closed s, a map continuous on s extends to a continuous map on X whose range is still contained in the image of s.
• TauCeti.exists_continuous_eqOn: an ambient function continuous on an arbitrary closed s agrees there with a continuous function on X, without a nonemptiness assumption.
• ContinuousMap.exists_restrict_eq_of_discrete and ContinuousMap.restrict_surjective_of_discrete: the bundled form, for a closed set.
• ContinuousMap.exists_extension_of_discrete: the bundled form, for a closed embedding.

Implementation notes

The statements come both for a bare function together with ContinuousOn and for bundled ContinuousMaps. The unbundled form is the one continuous cochains are written in, and the bundled form mirrors Mathlib's Tietze API; it lives in the root ContinuousMap namespace, so that dot notation on a C(s, Y) reaches it, and carries an _of_discrete suffix to distinguish it from Mathlib's TietzeExtension form of the same statement.

The bundled forms need a nonemptiness hypothesis. If s is empty and Y is empty while X is not, there is a continuous map on s and none on X, so one of s and Y has to be assumed nonempty. In the unbundled form, the ambient function f : X → Y already rules out this obstruction.

Total disconnectedness of X is not decoration either. On the compact Hausdorff space [0, 1] ⊆ ℝ no map into a discrete space separates the two points of the closed subspace {0, 1}, so a map taking two distinct values there has no continuous extension; this is spelled out as an example in TauCeti/Topology/LocallyConstant/Preconnected.lean, where the preconnectedness that drives it lives. Discreteness of Y is what makes the fibres clopen, and it is likewise essential.

theorem TauCeti.exists_continuous_eqOn_range_subset_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [DiscreteTopology Y] {s : Set X} {f : X → Y} (hs : IsClosed s) (hsne : s.Nonempty) (hf : ContinuousOn f s) : ∃ (g : X → Y), Continuous g ∧ Set.EqOn g f s ∧ Set.range g ⊆ f '' s

Continuous extension from a closed subspace of a profinite space. A map continuous on a nonempty closed subset s of a profinite space, with values in a discrete space, extends to a continuous map on the whole space, and the extension can be chosen to take no value that is not already taken on s.

That last clause is what lets a consumer keep the extension inside a subgroup, a submodule, or any other set the original values lie in.

theorem TauCeti.exists_continuous_eqOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [DiscreteTopology Y] {s : Set X} {f : X → Y} (hs : IsClosed s) (hf : ContinuousOn f s) : ∃ (g : X → Y), Continuous g ∧ Set.EqOn g f s

Continuous extension from a closed subspace of a profinite space, for an ambient function continuous on an arbitrary closed subset. No nonemptiness hypothesis is needed.

The bundled form

These live in the root ContinuousMap namespace, next to Mathlib's Tietze extension theorems and within reach of dot notation on a C(s, Y).

theorem ContinuousMap.exists_restrict_eq_of_discrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [DiscreteTopology Y] {s : Set X} [Nonempty Y] (hs : IsClosed s) (f : C(↑s, Y)) : ∃ (g : C(X, Y)), restrict s g = f

Continuous extension from a closed subspace of a profinite space, bundled: a continuous map on a closed subspace of a profinite space, with values in a nonempty discrete space, is the restriction of a continuous map on the whole space.

This is the zero-dimensional counterpart of Mathlib's ContinuousMap.exists_restrict_eq, whose TietzeExtension hypothesis on the target no discrete space with more than one point satisfies.

theorem ContinuousMap.restrict_surjective_of_discrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [DiscreteTopology Y] {s : Set X} [Nonempty Y] (hs : IsClosed s) : Function.Surjective fun (g : C(X, Y)) => restrict s g

Restriction of continuous maps to a closed subspace of a profinite space is surjective, when the target is discrete and nonempty.

theorem ContinuousMap.exists_extension_of_discrete {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [DiscreteTopology Y] [Nonempty Y] {Z : Type u_3} [TopologicalSpace Z] {e : Z → X} (he : Topology.IsClosedEmbedding e) (f : C(Z, Y)) : ∃ (g : C(X, Y)), g.comp { toFun := e, continuous_toFun := ⋯ } = f

Continuous extension along a closed embedding into a profinite space.

The statement and the deduction of this form from the closed-subset form follow Mathlib's ContinuousMap.exists_extension in Mathlib/Topology/TietzeExtension.lean.