discrete quotients and partitions

Stream: maths

[Patrick Massot]

@Calle Sönne and @Adam Topaz, when writing discrete_quotient, did you make a conscious choice to ignore setoid.partition? If no, do you think it's too late to reconcile those files?

[Adam Topaz]

TBH I didn't know that setoid/partition.lean existed. What in particular would you like to see reconciled @Patrick Massot ?

[Patrick Massot]

Half of discrete_quotient.lean is proving trivial stuff on partitions, equivalence relations and quotient that have nothing to do with topology.

[Adam Topaz]

The whole point of the discrete_quotient type is to endow the quotient with the discrete topology and still retain continuity with respect to the quotient map. There are a couple of lemmas about the fibers of discrete_quotient.proj that can be generalized (or exist already for general quotients), but I don't see how half of this file can be done with arbitrary quotients. (I actually asked a few days ago on zulip whether we had such lemmas about the equivalence classes associated to a setoid, but no one responded.)

[Patrick Massot]

I also didn't know about that file until I started to work on continuing the discrete quotient file.

[Patrick Massot]

It is not imported by any other file in mathlib.

[Adam Topaz]

A reasonable generalization is to define the type of all quotients of a type, then discrete_quotient can be a subtype, but I don't know whether such a thing would be actually useful (over just using the quotient API )

[Patrick Massot]

Thinking in terms of quotients is of course almost always better. But this story of profinite sets proves this is not always the case.

[Adam Topaz]

Maybe also worth mentioning that the code I originally had in LTE (and which was a modification of Calle's code) was in terms of partitions whose terms are clopen, and it turned out to be very cumbersome to work with in practice. Some lemmas which are proved essentially by refl with quotients required several lines when using partitions.

[Adam Topaz]

Perhaps a reasonable compromise is to construct a term of discrete_quotient X from a clopen partition?

[Patrick Massot]

Sure we need at least that.

[Patrick Massot]

But using setoid and setoid.classes in the definition of discrete_quotient would be nice.

[Patrick Massot]

Especially since you ordered variables in a way that the discrete quotient of X associated to a locally constant f : X → Y is associated to the relation x ∼ x' if f x' = f x instead of f x = f x'.

[Patrick Massot]

This line should really be (clopen : ∀ x, is_clopen { y | rel y x})

[Patrick Massot]

Of course this is equivalent since the relation is symmetric, but not defeq.

[Adam Topaz]

Yes, I agree. I wish I had known about setoid.classes before... Anyway, I can refactor once #7454 is merged

[Patrick Massot]

Ah, I should handle that PR then.

[Patrick Massot]

I think the name le_rel is a bit obscure

[Adam Topaz]

le_rel is supposed to be le_relative_to

[Adam Topaz]

But the latter is mouthful

[Patrick Massot]

I see. What is confusing is there are rel that mean relation everywhere in the neighborhood

[Adam Topaz]

Maybe le_comap would be better?

[Adam Topaz]

Or desc since this condition says precisely that a continuous map descends to the quotients

[Sebastien Gouezel]

You mean lifts, right? :-)

[Patrick Massot]

Oh, but it's already waiting for bors

[Adam Topaz]

Is it too late to cancel bors? It made a commit already it seems

[Patrick Massot]

Actually the build was cancelled

[Patrick Massot]

so you could change that name

[Patrick Massot]

All this quotient and partition stuff is a deeper rabbit hole than what I expected...

[Bryan Gin-ge Chen]

#7454 is still in "Waiting to run" status here, so it should be safe to make changes without disrupting anything. (In fact, the current "Running" batch is likely to time out anyways, so canceling even that batch will be fairly harmless.)

[Adam Topaz]

Renamed.