Sequential space

Stream: maths

[Yury G. Kudryashov]

According to Wikipedia, docs#sequential_space is called a Fréchet–Urysohn space and docs#is_seq_closed_iff_is_closed is the definition of a sequential space. Is it correct? If yes, should we fix the definition?

[Floris van Doorn]

a sequential space is a topological space whose topology can be completely characterized by its convergent/divergent sequences.

Fréchet–Urysohn spaces are exactly those spaces for which knowledge of which sequences converge to which limits (and which sequences do not) suffices to completely determine the space's topology.

Hmm

[Yury G. Kudryashov]

Yes, these are two formalizations of the same idea.

[Floris van Doorn]

That's fair. The informal descriptions make it sound like the concepts are equivalent :-)

[Floris van Doorn]

But if these are the commonly accepted names, we should follow them.

[Yury G. Kudryashov]

I've just accidentally noticed this. I never used either of these names in a paper, so I would prefer to hear from a topologist before making a PR.

[Yury G. Kudryashov]

With the current definition, I can prove

import topology.sequences

local notation f ` ⟶ ` limit := tendsto f at_top (𝓝 limit)

variables {α β : Type*} [topological_space α] [topological_space β]

lemma nhds_basis_closeds (a : α) : (𝓝 a).has_basis (λ s : set α, a ∉ s ∧ is_closed s) compl :=
⟨λ t, (nhds_basis_opens a).mem_iff.trans $ compl_surjective.exists.trans $
  by simp only [is_open_compl_iff, mem_compl_iff]⟩

lemma tendsto_nhds_iff_seq_tendsto [sequential_space α] {f : α → β} {a : α} {b : β} :
  tendsto f (𝓝 a) (𝓝 b) ↔ ∀ u : ℕ → α, (u ⟶ a) → (f ∘ u ⟶ b) :=
begin
  refine ⟨λ hf u hu, hf.comp hu,
    λ h, ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 _⟩,
  rintro s ⟨hbs, hsc⟩,
  refine ⟨closure (f ⁻¹' s), ⟨mt _ hbs, is_closed_closure⟩, λ x, mt $ λ hx, subset_closure hx⟩,
  rw [← sequential_space.sequential_closure_eq_closure],
  rintro ⟨u, hus, hu⟩,
  exact hsc.mem_of_tendsto (h u hu) (eventually_of_forall hus)
end

[Yury G. Kudryashov]

Is it true with the Wikipedia definition?

[Reid Barton]

I never realized these are different and yes we should fix the definition

[Reid Barton]

Yury G. Kudryashov said:

Is it true with the Wikipedia definition?

Yes, this should be true for the Wikipedia notion of sequential space. The "global" version of this property is given under "Sequential continuity" on the "sequential space" page.

[Yury G. Kudryashov]

How do I prove the non-global version? We have the global version, see docs#continuous_iff_sequentially_continuous

[Reid Barton]

(Well but that is for mathlib's stronger notion of sequential space right?)

[Yury G. Kudryashov]

The proof only uses the weaker version.

[Reid Barton]

OK, I don't necessarily believe the pointwise version any more for sequential spaces

[Yury G. Kudryashov]

Do we need Fréchet-Urysohn spaces, or only sequential spaces?

[Reid Barton]

Personally, I have only seen sequential spaces (they form one "convenient category" for algebraic topology).

[Reid Barton]

I wonder what the space are for which your lemma holds (continuity at any point can be tested on sequences converging to that point)

[Yury G. Kudryashov]

I guess, exactly Fréchet-Urysohn. Suppose that this is true for any f : α → bool (with the discrete topology on bool). Take a set s : set α and a point a ∈ closure s. Then f : λ x, if x ∈ s then tt else ff does not tend to ff as x → a. Thus there exists u : nat → α that converges to a such that f ∘ u does not converge to ff. This means that infinitely many u k belong to s, so we can take this subsequence.

[Yury G. Kudryashov]

I'm going to make a PR later tonight.

[Reid Barton]

Nice!