coinduced neighborhoods

Stream: Is there code for X?

[Aaron Liu]

The neighborhoods for the induced topology are characterized by docs#nhds_induced. Is there a similar characterization of the neighborhoods of the coinduced topology?

[Ben Eltschig]

I don't think such a nice characterisation exists, unfortunately. docs#nhds_induced works nicely because the neighbourhood filter of x : X under the topology induced by f : X → Y only depends on the neighbourhood filter of a single point in Y, namely f x; but for a point y : Y, there are many points in X that map to it and all of their neighbourhood filters can affect the neighbourhood filter of x under the coinduced topology. So the nicest statement you could possibly hope for would be something like this:

import Mathlib

open Filter Topology

theorem nhds_coinduced {X Y : Type*} [T : TopologicalSpace X] (f : X → Y) (y : Y) :
    @nhds Y (T.coinduced f) y = ⨆ x ∈ f ⁻¹' {y}, map f (𝓝 x) := by
  ext s; simp only [Set.mem_preimage, Set.mem_singleton_iff, mem_iSup, mem_map]
  refine ⟨fun h x hx ↦ preimage_nhds_coinduced (hx ▸ h), fun h ↦ ?_⟩
  sorry

But if I'm not mistaken, even this is false: a set s : Set Y can have the property that f ⁻¹' s is a neighbourhood of each point in f ⁻¹' {y} without being a neighbourhood of y. For example, if for any set $Y$ with three distinct points $a,b,c$ you equip $Y\times\{0,1\}$ with the topology generated by $\{(a,0),(b,0)\}$ and $\{(a,1),(c,1)\}$, the topology coinduced on $Y$ by the projection $\pi:Y\times\{0,1\}\to Y$ is indiscrete, but every set containing $\{a,b,c\}$ has the property that its preimage is a neighbourhood of every point in the preimage of $a$.

[Aaron Liu]

Yeah this statement is definitely false, since I have a counterexample

[Aaron Liu]

Oh you have a counterexample too!