polish implies second countable instance

Stream: maths

[Felix Weilacher]

Recently I tried adding the following instance to topology/metric_space/polish.lean:

instance second_countable_of_polish [topological_space α] [h : polish_space α] :
  second_countable_topology α := h.second_countable

This caused quite a few errors of the form maximum class-instance resolution depth has been reached in quite a few files. I tried adding a low priority to this instance. This fixed some of the errors but not all of them.

How should I address this? Actually, I don't understand why the polish_space class isn't defined with extends second_countable_topology in the first place. I'm aware that you can use upgrade_polish_space to introduce an instance of second_countable_topology yourself, but this seems like it defeats the purpose of type-class inference.

[Eric Wieser]

The docs at docs#polish_space.second_countable say

A Polish space is a topological space with second countable topology, that can be endowed with a metric for which it is complete. We register an instance from complete second countable metric space to polish space, and not the other way around as this is the most common use case.

[Eric Wieser]

Perhaps the missing explanation is "loops are not supported in Lean 3 TC search"

[Felix Weilacher]

I see, thanks for the explanation.

[Felix Weilacher]

Still, is there any way to give lean the ability to automatically find a second_countable_topology instance given a polish_space one without breaking things? It just feels very weird to be missing this.

[Eric Wieser]

Only if we remove the instance going in the other direction, docs#polish_space_of_complete_second_countable

[Eric Wieser]

My impression without any familiarity here is that the current choice is rather strange, and removing that instance in favor of the other one would likely make sense

[Eric Wieser]

@Sebastien Gouezel will certainly have more informed opinions here

[Eric Rodriguez]

For your purpose, for now you can try remove the instance in the file you're working on with local attribute [-instance] ... and add the other direction (maybe stuff will break)

[Sebastien Gouezel]

The typical situation is that you will have theorems on polish spaces that you will want to apply to second countable metric spaces (say, finite dimensional real normed vector spaces), so for the sake of appying the theory of polish spaces the current instance choice is the right one. On the other hand, I agree it is suboptimal for building the theory. But in fact what one does a lot is start from a polish space and then endow it with a complete metric space structure compatible with the topology -- and there is a command for this: at the beginning of the proof, do letI := upgrade_polish_space α, and then you will have a metric, and it will be known to be complete and second countable.

[Sebastien Gouezel]

Here I should mention that this issue will disappear with Lean 4, which allows loops in TC search, so we will have instances in both directions.

[Felix Weilacher]

Aha. Probably I will leave this alone in Lean 3 mathlib, then.

[Kevin Buzzard]

(deleted)

[Filippo A. E. Nuccio]

Kevin, was this an answer to my question about DVR's in the other stream?

[Felix Weilacher]

OK, Now that lean 4 is here I'd like to add this instance: I currently have a working draft pr where the definition of PolishSpace looks like:

class PolishSpace (α : Type*) [h : TopologicalSpace α] : Prop where
  secondCountableTopology : SecondCountableTopology α
  complete : ∃ m : MetricSpace α, m.toUniformSpace.toTopologicalSpace = h ∧
    @CompleteSpace α m.toUniformSpace
#align polish_space PolishSpace

instance secondCountable_of_polish [TopologicalSpace α] [h : PolishSpace α] :
    SecondCountableTopology α :=
  h.secondCountableTopology

My question for the experts: would it be better to replace this with

class PolishSpace (α : Type*) [h : TopologicalSpace α] extends SecondCountableTopology α : Prop where
  complete : ∃ m : MetricSpace α, m.toUniformSpace.toTopologicalSpace = h ∧
    @CompleteSpace α m.toUniformSpace
#align polish_space PolishSpace

and update later things accordingly?