Topological separation classes

Stream: mathlib4

[Aaron Liu]

I found 6 pairs of classes (A, B) in mathlib that are related by (A X → T0Space X) ∧ (A X ↔ B (SeparationQuotient X)).
In order of increasing strength we have

• (R0Space, T1Space)
• (R1Space, T2Space)
• (RegularSpace, T3Space)
• (CompletelyRegularSpace, T35Space)
• (PerfectlyNormalSpace, T6Space)
• (TopologicalSpace.PseudoMetrizableSpace, TopologicalSpace.MetrizableSpace)

This causes some duplication, and I also remember @Yury G. Kudryashov saying something about typeclass loops in #mathlib4 > TC loops @ 💬.
Therefore I think we should consider removing the second class in each tuple, to reduce duplication and speed up typeclass inference. Does anyone else have a better idea?

[Eric Wieser]

By "related" do you mean "the Iff lemma exists" or "there is an instance in both directions"?

[Aaron Liu]

I mean that it is a true statement that doesn't necessarily have a proof yet in mathlib

[Johan Commelin]

I don't think people will be happy if you tell them that they should write R1Space (SeparationQuotient X) instead of T2Space X.

[Johan Commelin]

If we don't have instances in both directions, then there will not be TC loops, and so you also won't see a TC speedup.

[Johan Commelin]

I think it's fine to have both names, and the iff statements. We just shouldn't make instances in both directions.

[Edward van de Meent]

i imagine the most useful instances will be in the -> SeparationQuotient direction?

[Aaron Liu]

wait, what I wrote is wrong too general

[Aaron Liu]

fixed

[Aaron Liu]

Johan Commelin said:

I don't think people will be happy if you tell them that they should write R1Space (SeparationQuotient X) instead of T2Space X.

I was thinking more like [R1Space X] [T0Space X] instead of [T2Space X] (I don't think people will be too happy with this either)

[Aaron Liu]

I do remember seeing that to make a sober space you say [QuasiSober X] [T0Space X].

[Johan Commelin]

Since these are Prop-valued classes, I also think there is less of an issue. No risk of diamonds at all, and in general, defeq checks are trivial. So I think it's safe to have these TCs.

[Yaël Dillies]

Surely this is not fine, because T2Space X implies R1Space X in general (docs#T2Space.r1Space), so a typeclass search could go like

⊢ T2Space X
⊢ R1Space (SeparationQuotient X)
⊢ T2Space (SeparationQuotient X)
⊢ R1Space (SeparationQuotient (SeparationQuotient X))
⊢ T2Space (SeparationQuotient (SeparationQuotient X))
...

[Yury G. Kudryashov]

I added instances from T0Space X and R*Space X to T*Space X some time ago, because I was told that Lean 4 TC search can detect cycles.

[Yury G. Kudryashov]

If we drop T* classes, then we can write [R1Space X] [T0Space X] instead of [T2Space X]. No need to involve SeparationQuotient X at all. BTW, R1Space (SeparationQuotient X) is equivalent to R1Space X, not T2Space X.

[Aaron Liu]

Yury G. Kudryashov said:

BTW, R1Space (SeparationQuotient X) is equivalent to R1Space X, not T2Space X.

Sorry, I got them backwards, T2Space (SeparationQuotient X) is equivalent to R1Space X

[Jireh Loreaux]

I think that we need to make variable alias much more usable in Mathlib, especially as we move to more unbundling.

[Jireh Loreaux]

If we're able to simply write [T2Space X] and have it expand to [R1Space X] [T0Space X] behind the scenes (I think this is crucial to preserve readability of the source), then there would be no issue.

[Jireh Loreaux]

(Note: this would mean removing the current T2Space definition as it currently exists.)