failing cases for continuity

Stream: mathlib4

[Tomas Skrivan]

I have few examples that I expect countinuity tactic to solve but it won't. However, I have no experience with Lean 3 continuity tactic and I might expect too much from it.

import Mathlib.Topology.Basic
import Mathlib.Topology.Constructions

variable {α β : Type}
variable {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]

example (f : X → α → Y) (hf : Continuous f)
  : Continuous (λ (x : X) => f x a) :=
by
  try continuity
  apply continuous_pi_iff.1
  apply hf

example (f : Y → α → β → X) (hf : Continuous f) (g : X → Y) (hg : Continuous g)
  : Continuous (λ (x : X) => f (g x) a b) :=
by try continuity
   apply continuous_pi_iff.1
   apply continuous_pi_iff.1
   try continuity -- still no?
   apply Continuous.comp' hf hg

example (f : Y → α → Z) (hf : Continuous f)
  : Continuous (λ (g : X → Y) (x : X) => f (g x) a) :=
by
  try continuity
  apply continuous_pi_iff.2
  intro x
  apply continuous_pi_iff.1
  apply Continuous.comp' hf
  continuity

How do I state that a function is jointly continuous in two arguments? Likely I have found aesop bug by following mahtlib style

example (f : X → X → Y)
  -- How to formulate joint continuity of arguments?
  (hf : ∀ {W} (g₁ g₂ : W → X), [TopologicalSpace W] → Continuous g₁ → Continuous g₂ → Continuous λ w => f (g₁ w) (g₂ w))
  : Continuous (λ x => f x x) :=
by
  -- continuity  -- causes this error
  /-
    application type mismatch
      hf
    argument has type
      Type
    but function has type
      ∀ {W : Type u_1} (g₁ g₂ : W → X) [inst : TopologicalSpace W],
        Continuous g₁ → Continuous g₂ → Continuous fun w => f (g₁ w) (g₂ w)
  -/
  apply hf id id; repeat continuity

There is no issue when the function f is not an argument to the example but separately stated function

opaque foo {X} (x y : X) : X := x

@[continuity]
axiom continuous_foo {W} [TopologicalSpace W] (f g : W → X) (hf : Continuous f) (hg : Continuous g)
  : Continuous λ x => foo (f x) (g x)

example
  : Continuous (λ x : X => foo x x) :=
by
  continuity

---

Are these known limitations? Is there a plan to fix it? I'm happy to help with it if someone points me in the right direction.

[Kevin Buzzard]

Being jointly continuous in two arguments is delicate! Mathematically if $X,Y,Z$ are topological spaces then we consider continuous functions $X\times Y\to Z$. However the usual process of currying turning this into X -> Y -> Z has a problem with continuity, because it's not possible in general to put a topological space structure on Y -> Z such that the continuous maps X \times Y -> Z are precisely the continuous maps X -> Y -> Z. I think that people usually work with the products in this case (indeed, they have to).

[Kevin Buzzard]

A related issue is that mathlib does put a topology on Y -> Z and this topology doesn't work at all (it can't see the topology on Y, it just regards Y as an index set and views the function space as a large product of copies of Z, so all information about the topology on Y is lost).

[Jireh Loreaux]

As Kevin is pointing out, this is why things like docs#continuous_mul are stated for the product α × α → α.

[Tomas Skrivan]

Yes, to reduce it to continuity in a single argument It would have to be states something like (hfy : ∀ x, Continuous (λ y => f x y)) (hfx : Continuous (λ x => λ y ==> f x y)) where (λ y ==> f x y) : ContinuousMap Y Z

[Kevin Buzzard]

If I'm understanding you correctly, then what I'm trying to say is that what you're suggesting is not possible (in the sense that it cannot be made equivalent to the statement about the map from the product being continuous).

[Tomas Skrivan]

So If I have an n-ary function I have to state a theorem similar to Continuous.mul/continuous_foo. It has to be fixed to the particular n-ary function.

[Tomas Skrivan]

Kevin Buzzard said:

If I'm understanding you correctly, then what I'm trying to say is that what you're suggesting is not possible (in the sense that it cannot be made equivalent to the statement about the map from the product being continuous).

Ahh you are right. I'm not too familiar with general topological spaces and in my head I was thinking about a different setting which forms cartesian closed category where you can (un)curry functions and you get such equivalence.

[Kevin Buzzard]

yeah, topological spaces are not a CCC and this is exactly the problem.

[Johan Commelin]

Solution: use condensed sets :wink:

[Tomas Skrivan]

I'm working with convenient vector spaces, probably will work with diffeological spaces in the future. If condensed sets can do similar stuff, I'm happy to work with them :)

[Tomas Skrivan]

But that still leaves me with the question, should I try to use/extend the continuity tactic/aesop or write my own tactic.

[Matthew Ballard]

Is it easy to make compactly generated topological spaces with existing tech?

[Adam Topaz]

Matthew Ballard said:

Is it easy to make compactly generated topological spaces with existing tech?

You could define them as spaces $X$ where a set $U$ is open if and only if $f^{-1}(U)$ is open for any continuous map $f : C \to X$ where $C$ is a comphaus. (to avoid unnecessary universe nonsense, we would make X and C live in the same universe)

[Adam Topaz]

that would make the relationship with condensed sets quite easy to prove, I think.

[Matthew Ballard]

Dumb question: are they the same as compactly generated in the preorder order sense?

[Adam Topaz]

I don't know what that term means for preorders... (or orders ;))

[Matthew Ballard]

I just did a cursory mathlib3 search for "compactly generated" and found orders and modules

[Matthew Ballard]

And I knew that modules wouldn't work :lol:

[Reid Barton]

I think it roughly means that the preorder is locally finitely presentable as a category, and it is not very related