## Stream: maths

### Topic: discrete quotients and partitions

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

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

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

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

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

#### Patrick Massot (May 04 2021 at 19:19):

It is not imported by any other file in mathlib.

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

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

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

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

#### Patrick Massot (May 04 2021 at 19:33):

Sure we need at least that.

#### Patrick Massot (May 04 2021 at 19:38):

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

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

#### Patrick Massot (May 04 2021 at 19:40):

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

#### Patrick Massot (May 04 2021 at 19:40):

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

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

#### Patrick Massot (May 04 2021 at 19:49):

Ah, I should handle that PR then.

#### Patrick Massot (May 04 2021 at 19:49):

I think the name le_rel is a bit obscure

#### Adam Topaz (May 04 2021 at 19:52):

le_rel is supposed to be le_relative_to

#### Adam Topaz (May 04 2021 at 19:52):

But the latter is mouthful

#### Patrick Massot (May 04 2021 at 19:53):

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

#### Adam Topaz (May 04 2021 at 19:55):

Maybe le_comap would be better?

#### Adam Topaz (May 04 2021 at 19:59):

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

#### Sebastien Gouezel (May 04 2021 at 20:00):

You mean lifts, right? :-)

#### Patrick Massot (May 04 2021 at 20:13):

Oh, but it's already waiting for bors

#### Adam Topaz (May 04 2021 at 20:15):

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

#### Patrick Massot (May 04 2021 at 20:16):

Actually the build was cancelled

#### Patrick Massot (May 04 2021 at 20:16):

so you could change that name

#### Patrick Massot (May 04 2021 at 20:17):

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

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

#### Adam Topaz (May 04 2021 at 20:22):

Renamed.

Last updated: Jun 17 2021 at 17:28 UTC