Topology of space of compactly supported functions

Stream: Is there code for X?

[Antoine Chambert-Loir]

Let $X$ and $Y$ be topological spaces, with a zero in $Y$.
The set $\mathscr C_c(X;Y)$ of continuous compactly supported functions $f\colon X\to Y$ has a natural topology, for which a map $T\colon\mathscr C_c(X;Y)\to Z$ is continuous if and only if, for every compact subset $K$ of $X$, the restriction $T_K\colon \mathscr C_K(X;Y)\to Z$ is continuous, where $\mathscr C_K(X;Y)$ is the set of continuous functions from $X$ to $Y$ whose support is contained in $K$.

Does Mathlib know about that?

[Johan Commelin]

Just to be clear, you are endowing $\mathscr C_K(X; Y)$ with the compact open topology, right? That part has been formalized in mathlib. But I'm not aware of a topology on compactly supported functions in mathlib.
@Yury G. Kudryashov will know

[Antoine Chambert-Loir]

I'm not sure I can endow $\mathscr C_K(X;Y)$ with the compact open topology, because that requires $Y$ to be a uniform space.
In fact, I intended to take simply the product topology, but they probably coincide when $Y$ is a uniform space.

[Antoine Chambert-Loir]

Here is something I could come up with (with a sorry to prove that the topology is the correct one)

import Mathlib.Topology.Defs.Induced
import Mathlib.Topology.Constructions
import Mathlib.Topology.Support

def ContinuousMapWithSupport {X : Type*} [TopologicalSpace X] (S : Set X)
  (Y : Type*) [TopologicalSpace Y] [Zero Y] :=
  { f : X → Y // Continuous f ∧ tsupport f ≤ S }

notation:9000 "C[" X ", " Y " | " S "]"=> ContinuousMapWithSupport (X := X) S Y

def TopologicalSpace.continuousMapWithSupport
    {X : Type*} [TopologicalSpace X] (S : Set X)
    (Y : Type*) [TopologicalSpace Y] [Zero Y] :
  TopologicalSpace (C[X, Y | S])  := by
  refine TopologicalSpace.induced (fun f => f.val) (inferInstance)

def ContinuousMapWithCompactSupport
    (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] [Zero Y] :=
    { f : X → Y // Continuous f ∧ HasCompactSupport f }

notation:9000 "Cc[" X ", " Y "]"=> ContinuousMapWithCompactSupport X Y

def toContinuousMapWithCompactSupport
    {X : Type*} [TopologicalSpace X]
    {K : Set X} (hK : IsCompact K) {Y : Type*} [TopologicalSpace Y] [Zero Y]
    (f : C[X, Y | K]) : Cc[X, Y] :=
  ⟨f.val, f.prop.1, IsCompact.of_isClosed_subset hK (isClosed_tsupport _) f.prop.2 ⟩

instance (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] [Zero Y]
    (S : Set X) :
    TopologicalSpace (C[X, Y | S]) :=
  TopologicalSpace.continuousMapWithSupport S Y

instance TopologicalSpace.continuousMapWithCompactSupport
    (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] [Zero Y] :
    TopologicalSpace (Cc[X, Y]) :=
  TopologicalSpace.coinduced
    (fun (⟨K, f⟩ : Σ (K : {S : Set X // IsCompact S}), C[X,Y | K.val])
    ↦ (toContinuousMapWithCompactSupport K.prop f  : Cc[X, Y]))
    instTopologicalSpaceSigma


example
    (X Y Z : Type*) [TopologicalSpace X] [TopologicalSpace Y] [Zero Y]
    [TopologicalSpace Z] (T : Cc[X, Y] → Z) :
    Continuous T ↔ ∀ (K : Set X) (hK : IsCompact K),
      Continuous (T ∘ (toContinuousMapWithCompactSupport hK)) := sorry

[Jireh Loreaux]

I have a feeling @Moritz Doll might have been working with such a topology, but maybe not.

[Anatole Dedecker]

Antoine Chambert-Loir said:

I'm not sure I can endow $\mathscr C_K(X;Y)$ with the compact open topology, because that requires $Y$ to be a uniform space.

No there is no suh requirement, the compact open topology can be defined for topological codomain. This is a bit of a miracle because the key property is that it coincides with the topology of compact convergence when the codomain is uniform, but Mathlib knows about it.

In fact, I intended to take simply the product topology, but they probably coincide when $Y$ is a uniform space.

I'm pretty sure these do not coincide unless you ask for some equicontinuity.

[Anatole Dedecker]

Indeed we do not have this (unless I missed something recently), but I have been thinking about it for the purpose of distribution theory (the vanilla one, I don't need you need anything like this for the tempered case) where you also need to take into account some differentiablility. You can have a look at https://github.com/leanprover-community/mathlib4/compare/master...AD_test_functions (warning: very out of date) to see my first experiments with this kind of thing.
EDIT: It's important to note that for test functions you only require the universal property for linear map to a LCTVS, which also makes things slightly more annoying.

[Anatole Dedecker]

In any case, I think I already said that somewhere, but for me the most annoying part of all this is the boilerplate associated to a new type. If someone just takes care of it I'll happily define the topology and prove the universal property !

[Antoine Chambert-Loir]

In the above code, the topology on $\mathscr C_K(X;Y)$ is the product topology, which is not the good one. This point corrected, it remains to have a convenient way to define the inductive limit topology, which can be defined via docs#Topology.coinduced, because that function requires a single type. So one has to write the correct Sigma type.

[Antoine Chambert-Loir]

I couldn't find the compact open topology, just the topology of compact convergence, which needs a uniform structure on the target.

[Anatole Dedecker]

Ah, right, I didn’t look at the code snippet :man_facepalming:
The right way to define the inductive limit topology is to take the supremum of the coinduced topologies. From there the universal property will follow quite easily from the library (I’m not at my computer right now, but I can tinker with it later)

[Anatole Dedecker]

docs#ContinuousMap is endowed by default with the compact open topology, which is docs#ContinuousMap.compactOpen

[Antoine Chambert-Loir]

Thanks, @Anatole Dedecker , this works as you said :

import Mathlib.Topology.Defs.Induced
import Mathlib.Topology.Constructions
import Mathlib.Topology.Support
import Mathlib.Topology.CompactOpen
import Mathlib.Topology.Sets.Compacts

open TopologicalSpace ContinuousMap

variable (X : Type*) [TopologicalSpace X] (S : Set X) (K : Compacts X)
  (Y : Type*) [TopologicalSpace Y] [Zero Y]

variable {X}
def ContinuousMapWithSupport := { f : C(X, Y) // tsupport f ≤ S }

notation:9000 "C(" X ", " Y " | " S ")" => ContinuousMapWithSupport (X := X) S Y

def TopologicalSpace.continuousMapWithSupport :
    TopologicalSpace (C(X, Y | S))  := induced Subtype.val compactOpen

variable (X)
def ContinuousMapWithCompactSupport := { f : C(X, Y) // HasCompactSupport f }

notation:9000 "Cₖ(" X ", " Y ")"=> ContinuousMapWithCompactSupport X Y

variable {X}
def toContinuousMapWithCompactSupport (f : C(X, Y | K)) : Cₖ(X, Y) :=
  ⟨f.val,
   IsCompact.of_isClosed_subset K.isCompact (isClosed_tsupport _) f.prop⟩

variable {Y}
def TopologicalSpace.continuousMapWithCompactSupport :
    TopologicalSpace (Cₖ(X, Y)) :=
  iSup (fun K ↦ coinduced (toContinuousMapWithCompactSupport K _) (continuousMapWithSupport _ _))

local instance : TopologicalSpace Cₖ(X, Y) := continuousMapWithCompactSupport

local instance (S : Set X) : TopologicalSpace C(X, Y | S) := continuousMapWithSupport S Y

example
    (Z : Type*) [TopologicalSpace Z] (T : Cₖ(X, Y) → Z) :
    Continuous T ↔ ∀ (K : Compacts X),
      Continuous (T ∘ (toContinuousMapWithCompactSupport K Y)) := by
  constructor
  · intro hT K
    apply Continuous.comp hT
    apply continuous_iSup_rng (i := K)
    rw [continuous_iff_coinduced_le]
    exact le_rfl
  · intro hT
    rw [continuous_iSup_dom]
    intro K
    simp only [continuous_iff_coinduced_le, coinduced_compose]
    rw [← continuous_iff_coinduced_le]
    exact hT K

[Anatole Dedecker]

For your last proof you can just do:

example
    (Z : Type*) [TopologicalSpace Z] (T : Cₖ(X, Y) → Z) :
    Continuous T ↔ ∀ (K : Compacts X),
      Continuous (T ∘ (toContinuousMapWithCompactSupport K Y)) := by
  simp_rw [continuous_iSup_dom, continuous_coinduced_dom]