obtain topology from Borel σ-algebra?

Stream: maths

[Floris van Doorn]

We have the type docs#MeasureTheory.AEEqFun α →ₘ[μ] β of functions that are (strongly) measurable and are quotiented by a.e.-equality w.r.t. a measure μ on α. We have the coercion docs#MeasureTheory.AEEqFun.cast that picks an arbitrary representative from an equivalence class.
Given a (strongly) measurable function f : α → β we of course cannot expect that (mk f).out is the same as f, and it will only be a.e.-equal. So for example, we have docs#MeasureTheory.AEEqFun.coeFn_one that only states that ⇑(1 : α →ₘ[μ] β) =ᵐ[μ] 1, but is not actually an equality of functions.

We could do better: we could modify AEEqFun.cast so that it picks out the constant functions on the nose, e.g.

def cast (f : α →ₘ[μ] β) : α → β :=
  if h : ∃ (g : α → β) (hg : AEStronglyMeasurable g μ),
    f = mk g hg ∧ g ∈ range (Function.const α) then
    Classical.choose h else
    -- existing definition

This is nice, because we can get a (non-definitional) equality of functions ⇑(1 : α →ₘ[μ] β) = 1, not just a.e.-equality.

Can we do better than this? I would like to do the same for any continuous function. The problem with this is that we are not assuming that α is a topological space, only a measurable space. I think that requiring a topological space on α is unacceptable.

Now one thing we could do is to check "if the σ-algebra is the Borel σ-algebra of a topological space, there exists a continuous representative g w.r.t. that topology, choose a continuous representative."
However, this doens't work, since many topologies give the same σ-algebra. E.g. on ℝ the coarsest topology that is finer than the usual topology but also makes {0} open should generate the same σ-algebra.

So here is my mathematical question: given a σ-algebra, is there a "nice" condition P on topologies, such that for the common cases (Banach spaces, or at the very least, ℝⁿ) there is at most one topology satisfying P that generates the usual σ-algebra on those spaces? (Or at least, the usual topology should be the finest such topology.)

[Floris van Doorn]

#12949 is the PR for the constant case. Unfortunately we need the condition [NeZero μ] to prove ⇑(1 : α →ₘ[μ] β) x = 1, so we also need the unconditional a.e.-equality.

[Sébastien Gouëzel]

The answer to your question (if I understand it correctly) is no: even on R, there are two arbitrarily nice topologies which are not the same but generate the Borel sigma algebra: take the usual topology, and the push-forward of this topology under a Borel-measurable non-continuous map.

[Floris van Doorn]

Oh, I think you are right... That is unfortunate.

[Yury G. Kudryashov]

Also, take the discrete topology on Bool and the measure dirac false. Then the quotient space knows nothing about the value at true and has no way to recover it.

[Yury G. Kudryashov]

So, even if the output is continuous, it is not guaranteed to be the original function.

[Floris van Doorn]

But that is not a problem, since I'm fine with it only working in common analysis cases (e.g. with a Haar measure).

But indeed, even for constant functions, I have to assume that the measure is not the zero measure.