Continuity of continuous map gluing

Stream: Is there code for X?

[Vincent Beffara]

I am defining the concatenation of continuous maps on intervals, like this:

import Mathlib

open Set Topology Metric unitInterval Filter ContinuousMap

namespace ContinuousMap

variable
  {α : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a b c : α}
  {E : Type*} [TopologicalSpace E]

def firstval (hab : a ≤ b) (f : C(Icc a b, E)) : E := f ⟨a, left_mem_Icc.2 hab⟩

def lastval (hab : a ≤ b) (f : C(Icc a b, E)) : E := f ⟨b, right_mem_Icc.2 hab⟩

noncomputable def concat (h : b ∈ Icc a c) (f : C(Icc a b, E)) (g : C(Icc b c, E)) :
    C(Icc a c, E) := by
  by_cases hb : f.lastval h.1 = g.firstval h.2
  · let h (t : α) : E := if t ≤ b then IccExtend h.1 f t else IccExtend h.2 g t
    suffices Continuous h from ⟨fun t => h t, by fun_prop⟩
    apply Continuous.if_le (by fun_prop) (by fun_prop) continuous_id continuous_const
    rintro x rfl ; simpa
  · exact .const _ (f ⟨a, left_mem_Icc.mpr h.1⟩) -- junk value

variable {f : C(Icc a b, E)} {g : C(Icc b c, E)}
variable {ι : Type} {p : Filter ι} {F : ι → C(Icc a b, E)} {G : ι → C(Icc b c, E)}

theorem cts (h : b ∈ Icc a c) (hfg : ∀ᶠ i in p, (F i).lastval h.1 = (G i).firstval h.2)
    (hf : Tendsto F p (𝓝 f)) (hg : Tendsto G p (𝓝 g)) :
    Tendsto (fun i => concat h (F i) (G i)) p (𝓝 (concat h f g)) := by
  sorry

end ContinuousMap

and I would like to show the continuity of the operation (cts above). Is there something like this in Mathlib already? All I found is docs#Path.continuous_trans which does something like it but without the compatibility condition which is ensured by the types...

[Anatole Dedecker]

This doesn’t sound like it would exist to me, but I think you could mimic the proof you linked to ? That is, uncurry the problem and then interpret it as continuity on some subtype of a product ? But it’s definitely a bit annoying

[Antoine Chambert-Loir]

If I understand your request correctly, this is mathematically a bit annoying too, because it uses the fact that intervals are locally compact (compactly generated would suffice).

[Antoine Chambert-Loir]

(Note that people will probably need it later for homotopies, and possibly higher stuff.)

[Vincent Beffara]

In the end the least annoying to use (in homotopies and such, as far as I was able to find out) is

variable
  {α : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] {a b c : α}
  {E : Type*} [TopologicalSpace E] {e e₀ : E}

noncomputable def concatCM (h : b ∈ Icc a c) :
    C({f : C(Icc a b, E) × C(Icc b c, E) // lastval h.1 f.1 = firstval h.2 f.2}, C(Icc a c, E)) := by

(with a pedestrian proof through IccExtend and unfolding the compact-open topology).

[Vincent Beffara]

#17621

[Vincent Beffara]

(Rereading the proof that I have, I do use local compactness. I'm not sure how necessary it is.) That was pure laziness, no local compactness is needed.