Is there a name for "closure is the union of `Specializes`"?

Stream: maths

[Yury G. Kudryashov]

Is there a name for one the following properties?

import Mathlib.Topology.Inseparable

variable {X : Type*} [TopologicalSpace X]

def myProp (s : Set X) : Prop :=
  ∀ x ∈ closure s, ∃ y ∈ s, x ⤳ y

def myProp' (s : Set X) : Prop :=
  ∀ x ∈ closure s, ∃ y ∈ s, Inseparable x y

E.g., compacts in R1Spaces and all closed sets in any topology satisfy these properties.
Also, if s is a set in a complete space and it has this property (they're equivalent in R0 spaces), then it is complete.
This can be used to show that some functional spaces like ContinuousMap, ContinuousLinearMap, ContinuousMultilinearMap are complete without separability of the codomain.

More precisely, if the interiors of s ∈ 𝔖 cover the whole space, then the set of continuous functions in X →ᵤ[𝔖] Y has myProp. This together with #10844 implies CompleteSpace for all the spaces above (assuming [WeaklyLocallyCompact X] for ContinuousMap and seminormable topology on the codomain for the rest).

[Johan Commelin]

It somehow feels almost opposite to being a sober space: $\exists y \in S, \forall x \in \bar S, y \leadsto x$ (holds for irreducible $S$).

[Yury G. Kudryashov]

It's possible that I got the direction of the arrow wrong (it's past 1am here) but I definitely need ∀ x in closure s, ∃ y ∈ s, _

[Yury G. Kudryashov]

I can say IsClosed (SeparationQuotient.mk '' s)

[Yury G. Kudryashov]

But this adds an unnecessary type to the soup (though we'll need it for *linearMaps anyway to preserve *linear part).

[Yury G. Kudryashov]

I may need different arrows for "closure is a subset of any open that contains s" and "s is complete", too sleepy to be sure.

[Anatole Dedecker]

Yury, I'm not answering your original question, but about completeness of X →ᵤ[𝔖] Y you may want to have a look at mathlib#18017, which proves it the Bourbaki way. The main thing blocking me from making it into a proper PR is that it's waiting on a proper theory of ideals of sets, the main point being that X →ᵤ[𝔖] Y doesn't change when you replace 𝔖 by the generated ideal (I used to say bornology but it doesn't match our definition of bornology so I'm sticking to ideal). This allows to avoid assuming directedness of 𝔖 is basically all of the statements (as you noticed, these are essentially never really needed).
Next, the gadget introduced by Bourbaki is UniformSpace.LEWithClosedBasis, which allows deducing completeness from the completeness in product types. I quite like this approach from a moral point of view because it really separates the multiple parts of the proof (everything relies on this lemma) but I understand it may be easier to give an ad hoc proof. What do you think?

[Anatole Dedecker]

Yury G. Kudryashov said:

This together with #10844 implies CompleteSpace for all the spaces above (assuming [WeaklyLocallyCompact X] for ContinuousMap and seminormable topology on the codomain for the rest).

I don't understand why these extra assumptions are needed?

[Yury G. Kudryashov]

I think that we can give an ad hoc proof now, replace with a more integrated proof later.

[Anatole Dedecker]

Sure.

[Yury G. Kudryashov]

Note that my uniformity_eq lemmas can help with getting rid of DirectedOn assumptions too: instead of using HasBasis, you use eq_biInf.

[Yury G. Kudryashov]

About extra assumptions. To prove that C(X, Y) is complete you need to show that continuous functions are "closed mod inseparable" in X →ᵤ[{K | IsCompact K}] Y". If you have a limit point of the set of continuous function, then it's continuous on all compacts (because of the uniform convergence). I can't glue it into Continuous without weak local compactness.

[Anatole Dedecker]

Ah yes, I completely missed the point. Note that Bourbaki assumes "locally compact or metrizable", which suggests that we should be using compactly generated spaces, but that can wait.

[Yury G. Kudryashov]

What are compactly generated spaces? How do you proceed if the domain is metrizable, not locally compact?

[Anatole Dedecker]

The key property is that testing convergence reduces to testing it on compact subspaces (there are subtleties in the non Hausdorff case, maybe you want to test on maps from compact Hausdorff spaces, but let's put that aside for now). This is obviously true for locally compact spaces, and for metrizable spaces you just have to see that if $u_n \to l$ then $\{u_n | n\in\mathbb{N}\} \cup \{l\}$ is compact.

[Yury G. Kudryashov]

So, instead of "metrizable" you can say docs#SequentialSpace ?

[Anatole Dedecker]

Yes sure

[Anatole Dedecker]

(deleted)

[Yury G. Kudryashov]

About LEWithClosedBalls etc, in the file about Polish spaces @Sébastien Gouëzel proves the following lemma (I extracted it from a longer proof):

theorem CompleteSpace.iInf {ι : Sort*} {X : Type*} {u : ι → UniformSpace X}
    (hu : ∀ i, @CompleteSpace X (u i))
    (ht₀ : ∃ i₀, @T0Space X (u i₀).toTopologicalSpace ∧
      ∀ i, (u i).toTopologicalSpace ≤ (u i₀).toTopologicalSpace) :
    @CompleteSpace X (⨅ i, u i) := by
  refine @CompleteSpace.mk X ?_ fun {f} hf ↦ ?_
  rcases ht₀ with ⟨i₀, hsep₀, hi₀⟩
  have hf' : ∀ i, Cauchy (uniformSpace := u i) f := fun i ↦ hf.mono_uniformSpace (iInf_le _ _)
  choose x hfx using fun i ↦ @CompleteSpace.complete _ (u i) (hu i) f (hf' i)
  have hx : ∀ i, x i = x i₀ := fun i ↦ by
    let _ := u i₀
    have := hf.1
    exact tendsto_nhds_unique ((hfx i).trans <| nhds_mono (hi₀ i)) (hfx i₀)
  use x i₀
  rw [UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
  exact le_iInf fun i ↦ (hx i).symm ▸ hfx i

Does it follow from some general theory?

[Anatole Dedecker]

The wikipedia page actually does a good job at comparing possible definitions. The reason I wanted to be sure to pick "the right one" is that a lot of the theory about compact open topology can be done in this setup, but everyone treats only the T2 case so I want to see the proof to see which of the definition works in the non-T2 case.

[Anatole Dedecker]

Yury G. Kudryashov said:

About LEWithClosedBalls etc, in the file about Polish spaces Sébastien Gouëzel proves the following lemma (I extracted it from a longer proof):

theorem CompleteSpace.iInf {ι : Sort*} {X : Type*} {u : ι → UniformSpace X}
    (hu : ∀ i, @CompleteSpace X (u i))
    (ht₀ : ∃ i₀, @T0Space X (u i₀).toTopologicalSpace ∧
      ∀ i, (u i).toTopologicalSpace ≤ (u i₀).toTopologicalSpace) :
    @CompleteSpace X (⨅ i, u i) := by
  refine @CompleteSpace.mk X ?_ fun {f} hf ↦ ?_
  rcases ht₀ with ⟨i₀, hsep₀, hi₀⟩
  have hf' : ∀ i, Cauchy (uniformSpace := u i) f := fun i ↦ hf.mono_uniformSpace (iInf_le _ _)
  choose x hfx using fun i ↦ @CompleteSpace.complete _ (u i) (hu i) f (hf' i)
  have hx : ∀ i, x i = x i₀ := fun i ↦ by
    let _ := u i₀
    have := hf.1
    exact tendsto_nhds_unique ((hfx i).trans <| nhds_mono (hi₀ i)) (hfx i₀)
  use x i₀
  rw [UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
  exact le_iInf fun i ↦ (hx i).symm ▸ hfx i

Does it follow from some general theory?

I don't think this is related to LEWithClosedBasis, but I want to think about it.

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

What are compactly generated spaces? How do you proceed if the domain is metrizable, not locally compact?

Compactly generated spaces are topological spaces $X$ such that a function $f\colon X \to Y$ is continuous if and only if all its restrictions to compact subsets of $X$ are continuous. (There are subtleties whether compact should mean Hausdorff here.)

[Anatole Dedecker]

(And about wether you should take actual subspaces or maps from arbitrary compact spaces)

[Yury G. Kudryashov]

#10902 for now

[Yury G. Kudryashov]

Should we have a name for t ≤ ⨆ s ∈ 𝔖, .coinduced (Subtype.val : s → α) (.induced Subtype.val t)?

[Yury G. Kudryashov]

With some obvious lemmas like mono (enlarge the set), of_nhds (assuming that each point has a nhd in 𝔖), and of_seq (for sequential spaces).

[Anatole Dedecker]

Hmmm, so that compactly generated is just this for 𝔖 = compact subsets / T2 compact subsets ? There's still one of the three possible definition which isn't covered by this, but that sounds interesting. And I guess your hope is to generalize the proof of completeness for such a 𝔖? I'll think about it.

[Yury G. Kudryashov]

We have completeness of UniformOnFun for any 𝔖. If t ≤ ⨆ (s) (hs : IsCompact s), .coinduced (Subtype.val : s → α) (.induced Subtype.val t), then we can get completeness of ContinuousMap.

[Anatole Dedecker]

Yes, that's what I meant.

[Yury G. Kudryashov]

Is it true with some weaker assumption?

[Anatole Dedecker]

I believe this would work for any 𝔖 satisfying the condition you wrote above (as in, if you equip ContinuousMap with the corresponding topology) ? Because then it's easy to see that testing continuity is the same as testing continuity in any s ∈ 𝔖, and continuity is a closed condition in docs#UniformFun.

[Anatole Dedecker]

This should rather be stated as a condition for the map from ContinuousMap to UniformOnFun having closed range, and we leave the completeness part to when it's also a uniform inducing (to avoid dealing with nonstandard topologies).

[Yury G. Kudryashov]

If we equip ContinuousMap with the compact-open topology, is there a better assumption than t ≤ ⨆ (s) (hs : IsCompact s), .coinduced (Subtype.val : s → α) (.induced Subtype.val t)?

[Anatole Dedecker]

No, I don't think so

[Yury G. Kudryashov]

I want to prove completeness of ContinuousLinearMaps and ContinuousMultilinearMaps in the same way, reusing #10902 and #10844

[Anatole Dedecker]

Note that this is exactly compact generation (modulo the Hausdorff details)

[Yury G. Kudryashov]

Yes, I see. I don't know if assuming this for Hausdorff compact subsets is enough.

[Yury G. Kudryashov]

Proving completeness of E  →L[K] F without [T2Space F] will require a map outCLM : SeparationQuotient F →L[K] F and this will depend on #10644 to avoid choosing between docs#SeparationQuotient and docs#UniformSpace.SeparationQuotient.

[Yury G. Kudryashov]

BTW, for E →L[K] F, what's the right assumption on E? SequentialSpace? Something else?

[Anatole Dedecker]

Yury G. Kudryashov said:

Yes, I see. I don't know if assuming this for Hausdorff compact subsets is enough.

I think it's stronger to assume it for all Hausdorff compact subsets actually ? That's what Wikipedia says but I'm too tired to check why. So your lemma in #10902 is surely as general as it could be. My worry was rather what to choose as a definition of CompactGenerated, since we would like to pick a definition that is powerfull enough to do the whole theory of the compact-open topology.

[Yury G. Kudryashov]

What other properties depend on this definition?

[Anatole Dedecker]

Yury G. Kudryashov said:

BTW, for E →L[K] F, what's the right assumption on E? SequentialSpace? Something else?

I don't remember and I really need to sleep, but there are a lot of results about this in the section of Bourbaki, Topological Vector Spaces where they define the topology on E →L[K] F.

[Yury G. Kudryashov]

I don't have Bourbaki. Good night!

[Anatole Dedecker]

Yury G. Kudryashov said:

What other properties depend on this definition?

docs#Homeomorph.curry should work for compactly generated spaces IIUC

[Yury G. Kudryashov]

I can't prove docs#ContinuousMap.continuous_eval with these assumptions without assuming something about the codomain.