continuity of a function between generalized loop space

Stream: Is there code for X?

[Wenrong Zou]

I am constructing two type equivalent of Ω^M (Ω^N X) ≃ₜ Ω^(M⊕N) X, where Ω^M is GenLoop. I already define toFun, invFun and proved left_inv and right_inv. But I am stuck at prove toFun and invFun is continuous. I think the continuity should be proved easily (just followed by construction and maybe by fun_prop) or maybe I am wrong. I have tried for a while but failed. Could anyone give me some suggestion. Thanks in advance!

import Mathlib

open Cube

open scoped unitInterval Topology
open scoped Topology.Homotopy

variable {X : Type*} [TopologicalSpace X] (x : X) {M N : Type*}

/-- Homeomorphism `I^(M ⊕ N) ≃ₜ I^M × I^N`. -/
def sumHomeo (M N : Type*) : (I^(Sum M N)) ≃ₜ ((I^M) × (I^N)) where
  toFun y := (y ∘ Sum.inl, y ∘ Sum.inr)
  invFun y := fun s ↦ Sum.casesOn s y.1 y.2
  left_inv y := by
    ext s; cases s <;> rfl
  right_inv y := by
    ext s <;> rfl
  continuous_toFun := by
    fun_prop
  continuous_invFun := by
    refine continuous_pi ?_
    intro s
    cases s with
    | inl m =>
        simpa using (continuous_apply m).comp continuous_fst
    | inr n =>
        simpa using (continuous_apply n).comp continuous_snd

theorem boundary_sum_iff (M N : Type*) (y : I^(Sum M N)) :
    y ∈ Cube.boundary (Sum M N) ↔ (y ∘ Sum.inl : I^M) ∈ Cube.boundary M ∨
  (y ∘ Sum.inr : I^N) ∈ Cube.boundary N := by
  constructor
  · intro i
    obtain ⟨i, hi⟩ := i
    cases i with
    | inl m =>
        left
        refine ⟨m, ?_⟩
        simpa using hi
    | inr n =>
        right
        refine ⟨n, ?_⟩
        simpa using hi
  · rintro (hM | hN)
    · rcases hM with ⟨m, hm⟩
      exact ⟨Sum.inl m, by simpa using hm⟩
    · rcases hN with ⟨n, hn⟩
      exact ⟨Sum.inr n, by simpa using hn⟩

@[simps]
def currySum (q : ↑(Ω^ (M ⊕ N) X x)) : C(M → ↑I, (↑(Ω^ N X x))) where
  toFun a := ⟨(q.1.comp ⟨(sumHomeo M N).invFun, (sumHomeo M N).continuous_invFun⟩).curry.toFun a,
    fun _ hm => q.2 _ ((boundary_sum_iff _ _ _).mpr (Or.inr hm))⟩
  continuous_toFun := Continuous.subtype_mk (q.1.comp
    ⟨(sumHomeo M N).invFun, (sumHomeo M N).continuous_invFun⟩).curry.continuous_toFun _

/-- `Ω^M (Ω^N X) ≃ₜ Ω^(M ⊕ N) X`. -/
def iterHomeoSum :
    Ω^ M (Ω^ N X x) (GenLoop.const (N := N) (X := X) (x := x)) ≃ₜ Ω^ (Sum M N) X x where
  toFun p := by
    -- p is a map I^M → (I^N → X). We turn it into I^M × I^N → X, then I^(M ⊕ N) → X.
    refine ⟨(ContinuousMap.uncurry ⟨fun a => ⟨(p.1 a).1, ContinuousMap.continuous _⟩,
      Continuous.subtype_val (map_continuous p)⟩).comp ⟨(sumHomeo M N).toFun,
        (sumHomeo M N).continuous_toFun⟩, ?_⟩
    intro y hy
    rw [boundary_sum_iff] at hy
    rcases hy with hM | hN
    · -- Case: y restricted to M is in the boundary of I^M
      -- p maps boundary of M to the constant loop (const x)
      simp [sumHomeo, GenLoop.const, p.2 (y ∘ Sum.inl) hM]
    · -- Case: y restricted to N is in the boundary of I^N
      -- p(m) is always a loop, so it maps boundary of N to x
      simp [sumHomeo, (p.1 (y ∘ Sum.inl)).2 (y ∘ Sum.inr) hN]
  invFun q := by
    refine ⟨currySum x q, ?_⟩
    intro m hm
    ext n
    exact q.2 _ ((boundary_sum_iff _ _ _).mpr (Or.inl hm))
  left_inv p := by
    ext t : 1
    simp
    rfl
  right_inv p := by
    ext t
    simp [Function.uncurry]
    rfl
  continuous_toFun := by
    apply Continuous.subtype_mk
    refine Continuous.compCM ?_ continuous_const
    refine Continuous.comp' ContinuousMap.continuous_uncurry ?_
    /- I think this is just a coercion? But why fun_prop cannot solve this?
      Oh, it is underlying topology problem. -/
    sorry
  continuous_invFun := by
    apply Continuous.subtype_mk
    /- same as above-/
    sorry

[Junyan Xu]

exact (ContinuousMap.continuous_postcomp ⟨_, continuous_subtype_val⟩).comp continuous_subtype_val

works for the first sorry

[Wenrong Zou]

Thanks!

[Wenrong Zou]

I think the second one should follow the same spirit of this. or simply we just need to prove the function currySum x is continuous.

@[simps]
def currySum (q : ↑(Ω^ (M ⊕ N) X x)) : C(M → ↑I, (↑(Ω^ N X x))) where
  toFun a := ⟨(q.1.comp ⟨(sumHomeo M N).invFun, (sumHomeo M N).continuous_invFun⟩).curry.toFun a,
    fun _ hm => q.2 _ ((boundary_sum_iff _ _ _).mpr (Or.inr hm))⟩
  continuous_toFun := Continuous.subtype_mk (q.1.comp
    ⟨(sumHomeo M N).invFun, (sumHomeo M N).continuous_invFun⟩).curry.continuous_toFun _

lemma continuous_currySum (q : ↑(Ω^ (M ⊕ N) X x)) : Continuous (currySum x q) :=
  ContinuousMap.continuous (currySum x q)

lemma continuous_currySum_apply : Continuous (currySum x (M := M) (N := N)) := by
  sorry

[Junyan Xu]

This works:

lemma continuous_currySum_apply : Continuous (currySum x (M := M) (N := N)) := by
  apply ContinuousMap.continuous_of_continuous_uncurry
  apply Continuous.subtype_mk
  apply ContinuousMap.continuous_of_continuous_uncurry
  dsimp
  fun_prop

[Wenrong Zou]

Thanks! I used to think ContinuousMap.continuous_of_continuous_uncurry will not significantly reduce the difficulty of proving this. But it seems like this is the right thing to do. Thanks! :-)