SeparableSpace (C(X, Y))

Stream: maths

[Yury G. Kudryashov]

What are the right assumptions for a SeparableSpace C(X, Y) (or SecondCountableTopology C(X, Y)) instance?

[Yury G. Kudryashov]

Should I add one for [RCLike Y] and a compact R1 space X, based on Stone-Weierstrass? Or there is a more general version?

[Yury G. Kudryashov]

I think I can prove SecondCountableTopology with much weaker assumption, will try to formalize tonight when I arrive home.

[Yaël Dillies]

For SeparableSpace, I think you can replace compactness of X by local compactness (so that it works for X = Real)

[Yaël Dillies]

For SeparableSpace, I think you can replace compactness of X by local compactness (so that it works for X = Real)

[Yury G. Kudryashov]

Do you have a reference with a proof? Probably, I can prove it myself, but I can end up with a less general result this way.

[Yaël Dillies]

Sorry, local compactness clearly isn't enough (because you can have uncountably many connected components). But sigma-compactness should work, with the proof being that any open set in C(X, Y) somehow comes from an open set in C(Xₙ, Y) for some n, where Xₙ is a compact exhaustion of X. Don't have a formal proof yet, though, just a hunch.

[Yury G. Kudryashov]

I formalized the following theorem:

theorem compactOpen_eq_generateFrom {S : Set (Set X)} {T : Set (Set Y)}
    (hS₁ : ∀ K ∈ S, IsCompact K) (hT : IsTopologicalBasis T)
    (hS₂ : ∀ K V : Set X, IsCompact K → IsOpen V → K ⊆ V →
      ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ ∀ L ∈ s, L ⊆ V) :
    compactOpen = .generateFrom (.image2 (fun K t ↦
      {f : C(X, Y) | MapsTo f K (⋃₀ t)}) S {t : Set (Set Y) | t.Finite ∧ t ⊆ T}) := by

[Yury G. Kudryashov]

So, the goal is to construct a countably family of compact sets with hS₂ property above.

[Yury G. Kudryashov]

Here is a better version:

theorem compactOpen_eq_generateFrom₂ {S : Set (Set X)} {T : Set (Set Y)}
    (hS₁ : ∀ K ∈ S, IsCompact K) (hT : IsTopologicalBasis T)
    (hS₂ : ∀ V, IsOpen V → ∀ x ∈ V, ∃ K ∈ S, K ∈ 𝓝 x ∧ K ⊆ V) :
    compactOpen = .generateFrom (.image2 (fun K t ↦
      {f : C(X, Y) | MapsTo f K (⋃₀ t)}) S {t : Set (Set Y) | t.Finite ∧ t ⊆ T}) := by

[Yury G. Kudryashov]

(this hS₂ implies the previous one, but it's more readable)

[Yury G. Kudryashov]

I think that I can prove it assuming [LocallyCompactSpace X] [R1Space X] [SecondCountableTopology X]. Is R1Space X necessary here?

[Yury G. Kudryashov]

Also, can SecondCountableTopology be replaced with SigmaCompactSpace?

[Yury G. Kudryashov]

I don't have examples that I care about where these differences matter, but if it's easy to generalize, then I would do it. Otherwise, I'll PR my version tomorrow.

[Yury G. Kudryashov]

See #17706

[Yury G. Kudryashov]

Unless someone has a better proof, I suggest that we merge it with these assumptions, then generalize later if someone will need it.

[Yury G. Kudryashov]

Also, can some assumptions in instSeparableSpace be weakened?

[Yury G. Kudryashov]

@Steven Clontz Do you know a reference with right assumptions for theorems like these?

[Steven Clontz]

I've worked with Cp theory (C(X,R) with point-open topology) but haven't worked with compact-open in my research (just as toy examples in grad school). First thought was to look in "Recent Progress in General Topology", but no dice, all Cp theory. Sorry - I'll keep thinking about whether I might have something else on the shelf that could help here.

[Yury G. Kudryashov]

I can prove SecondCountable C(X, Y) with the following assumptions:

theorem secondCountableTopology [SecondCountableTopology Y]
    (hX : ∃ S : Set (Set X), S.Countable ∧ (∀ K ∈ S, IsCompact K) ∧
      ∀ f : C(X, Y), ∀ V, IsOpen V → ∀ x ∈ f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo f K V) :

Is hX true assuming that X is second countable and weakly locally compact while Y is second countable and R1?

[Yury G. Kudryashov]

Current version of the PR assumes that X is second countable and locally compact.

[Steven Clontz]

Well https://topology.pi-base.org/spaces?q=second+countable+%2B+Weakly+locally+compact+%2B+%7ELocally+compact comes up empty, so I would first consider whether there's any low-hanging fruit at https://topology.pi-base.org/spaces?q=second+countable+%2B+Weakly+locally+compact+%2B+%3FLocally+compact

[Steven Clontz]

I believe https://topology.pi-base.org/spaces/S000185 is a second countable compact (and therefore weakly locally compact) space that's not locally compact, so considering C(S185, R) might be instructive.

[Steven Clontz]

I pinged a colleague who said that X needs hemicompactness for C(X,R) to be first-countable, but your assumptions of second-countable and weakly locally compact are sufficient there: https://topology.pi-base.org/spaces?q=%7Ehemicompact%2Bsecond+countable%2BWeakly+locally+compact

[Yury G. Kudryashov]

Since we don't have hemicompactness yet, I'm going to leave this theorem with current assumptions.

[Steven Clontz]

Another possible trailhead: https://webhome.auburn.edu/~gruengf/papers/fans6.pdf points to https://www.sciencedirect.com/science/article/pii/016686418690009X, but again everything assumes $Y=\mathbb R$ or $Y=[0,1]$ within my usual radius of the literature.

[Yury G. Kudryashov]

I think that I've spent enough time on generalizing this. Whoever will need it for a non-locally compact space can write a better proof.