Zulip Chat Archive

Stream: maths

Topic: discrete quotients and partitions


view this post on Zulip Patrick Massot (May 04 2021 at 18:51):

@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?

view this post on Zulip Adam Topaz (May 04 2021 at 18:57):

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

view this post on Zulip Patrick Massot (May 04 2021 at 18:59):

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

view this post on Zulip Adam Topaz (May 04 2021 at 19:16):

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.)

view this post on Zulip Patrick Massot (May 04 2021 at 19:17):

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

view this post on Zulip Patrick Massot (May 04 2021 at 19:19):

It is not imported by any other file in mathlib.

view this post on Zulip Adam Topaz (May 04 2021 at 19:20):

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 )

view this post on Zulip Patrick Massot (May 04 2021 at 19:26):

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

view this post on Zulip Adam Topaz (May 04 2021 at 19:30):

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.

view this post on Zulip Adam Topaz (May 04 2021 at 19:31):

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

view this post on Zulip Patrick Massot (May 04 2021 at 19:33):

Sure we need at least that.

view this post on Zulip Patrick Massot (May 04 2021 at 19:38):

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

view this post on Zulip Patrick Massot (May 04 2021 at 19:39):

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'.

view this post on Zulip Patrick Massot (May 04 2021 at 19:40):

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

view this post on Zulip Patrick Massot (May 04 2021 at 19:40):

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

view this post on Zulip Adam Topaz (May 04 2021 at 19:41):

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

view this post on Zulip Patrick Massot (May 04 2021 at 19:49):

Ah, I should handle that PR then.

view this post on Zulip Patrick Massot (May 04 2021 at 19:49):

I think the name le_rel is a bit obscure

view this post on Zulip Adam Topaz (May 04 2021 at 19:52):

le_rel is supposed to be le_relative_to

view this post on Zulip Adam Topaz (May 04 2021 at 19:52):

But the latter is mouthful

view this post on Zulip Patrick Massot (May 04 2021 at 19:53):

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

view this post on Zulip Adam Topaz (May 04 2021 at 19:55):

Maybe le_comap would be better?

view this post on Zulip Adam Topaz (May 04 2021 at 19:59):

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

view this post on Zulip Sebastien Gouezel (May 04 2021 at 20:00):

You mean lifts, right? :-)

view this post on Zulip Patrick Massot (May 04 2021 at 20:13):

Oh, but it's already waiting for bors

view this post on Zulip Adam Topaz (May 04 2021 at 20:15):

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

view this post on Zulip Patrick Massot (May 04 2021 at 20:16):

Actually the build was cancelled

view this post on Zulip Patrick Massot (May 04 2021 at 20:16):

so you could change that name

view this post on Zulip Patrick Massot (May 04 2021 at 20:17):

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

view this post on Zulip Bryan Gin-ge Chen (May 04 2021 at 20:17):

#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.)

view this post on Zulip Adam Topaz (May 04 2021 at 20:22):

Renamed.


Last updated: Jun 17 2021 at 17:28 UTC