Missing facts about `locally_constant`

Stream: maths

[Heather Macbeth]

I just PR'd (#15667) our first fact about complex manifolds: a holomorphic function on a compact connected complex manifold is constant. (This was unlocked by @Yury G. Kudryashov's latest version of the maximum principle, #15364.)

I wanted to state also the corresponding result without connectedness,

/-- A holomorphic function on a compact complex manifold is locally constant. -/
lemma mdifferentiable.locally_const_of_compact_space [compact_space M]
  {f : M → F} (hf : mdifferentiable 𝓘(ℂ, E) 𝓘(ℂ, F) f) :
  is_locally_constant f :=
sorry

but we are missing some API about locally constant functions, connected components, locally connected spaces, etc. The result I need is that a function constant on clopen preconnected sets is locally constant. I guess you could break this into two pieces,

• a function constant on connected components is locally constant
• a connected component is clopen -- maybe this needs the hypothesis that the space is locally connected? That definition isn't in mathlib yet but is done in sphere eversion, and could be PR'd from there. And then I guess we also need that manifolds are locally connected.

I won't get to any of this any time soon, posting it here in case anyone else feels like exercising their point-set topology muscles!

[Heather Macbeth]

Also just recorded this in an issue: #15669

[Johan Commelin]

I just want to record that this seems to be disjoint from the work on locally constant functions that has been done in LTE.
@Ashvni Narayanan has written a proof that the completion of loc.const is ctu functions, and we have some random bits and pieces about the sup-norm.
So, if you end up needing anything in that direction, please ping so that we can prioritise PRing those parts.

[Anatole Dedecker]

I think you also need local connectedness for both your full goal and your first point. Otherwise the identity on rationals is a counter example to both, right ?

[Ashvni Narayanan]

Heather Macbeth said:

I just PR'd (#15667) our first fact about complex manifolds: a holomorphic function on a compact connected complex manifold is constant. (This was unlocked by Yury G. Kudryashov's latest version of the maximum principle, #15364.)

I wanted to state also the corresponding result without connectedness,

/-- A holomorphic function on a compact complex manifold is locally constant. -/
lemma mdifferentiable.locally_const_of_compact_space [compact_space M]
  {f : M → F} (hf : mdifferentiable 𝓘(ℂ, E) 𝓘(ℂ, F) f) :
  is_locally_constant f :=
sorry

but we are missing some API about locally constant functions, connected components, locally connected spaces, etc. The result I need is that a function constant on clopen preconnected sets is locally constant. I guess you could break this into two pieces,

• a function constant on connected components is locally constant
• a connected component is clopen -- maybe this needs the hypothesis that the space is locally connected? That definition isn't in mathlib yet but is done in sphere eversion, and could be PR'd from there. And then I guess we also need that manifolds are locally connected.

I won't get to any of this any time soon, posting it here in case anyone else feels like exercising their point-set topology muscles!

It has been a while since I have looked at this stuff but I do have some results in the p-adic branch that might have proved/ will help in proving these results.

[Johan Commelin]

I think the biggest problem with locally_constant in mathlib atm is that the metric_space instance isn't set up in the right generality.

[Johan Commelin]

We should do uniform_space separately, etc... but it's all done in one go. That'll need a bit of a refactor.

[Anatole Dedecker]

#15965

[Johan Commelin]

@Anatole Dedecker Looks like there's a spurious typo in the diff.

[Anatole Dedecker]

Oh right, it's me hitting Shift instead of Control again :face_palm:

[Anatole Dedecker]

Should be fixed now