what does doset even mean

Stream: mathlib4

[Kevin Buzzard]

I recently discovered that mathlib has docs#Doset.doset . Can anyone guess what it means without clicking? I propose we rename it to what mathematicians call it. Or is this standard terminology? I'd never heard of it.

It means "Double coset". Can we rename to DoubleCoset?
```

[Edward van de Meent]

even reading the spoiler i couldn't figure it out, i had to go to the docs and expand the equation... i agree we should call it what mathematicians call it (unless of course there is a clearer way to express the concept)

[Damiano Testa]

I agree that it should be called what the spoiler says: without context (and maybe even with context!), I would have never guessed its meaning.

[Eric Wieser]

Maybe this should be a new threshold for whether mathlib should have something; introduce it with a silly name, and if no one complains within 3 years then maybe mathlib didn't need it after all!

[Kevin Buzzard]

I need it for FLT, and that was how I discovered it!

[Damiano Testa]

And given that Chris authored the file, I imagine that they wanted it for similar reasons!

[Kevin Buzzard]

Yes, we're both thinking about Hecke operators right now.

[Eric Wieser]

(I was kidding, I don't think mathlib should be pruned of things that no one currently wants)

[Johan Commelin]

I confess that I know what a Doset.doset is, without looking at the spoiler...

[Johan Commelin]

But I reviewed the PR that introduced it... so maybe you should take this data point with a grain of salt

[Ben Eltschig]

Eric Wieser said:

Maybe this should be a new threshold for whether mathlib should have something; introduce it with a silly name, and if no one complains within 3 years then maybe mathlib didn't need it after all!

I know you were kidding, but I'd still like to mention that they find use in the construction of universal orbifold coverings too, so I will need them if/when I get to formalising that. I don't think I would have easily found them under that name though, if I hadn't seen this post...

[Kevin Buzzard]

Mathlib has dosets. If you don't know what they are, then feel free to guess before reading on.

Dosets are a mathlibism. Doset isn't a word, it's not searchable, it's not guessable, it's confusing. We have them in one file in mathlib so it's easy to change Dosets to DoubleCosets, which is what they are, and is what the literature calls them. I want to add stuff to this file and do stuff with topological double cosets but I cannot get used to the mathlibism name; I think we should stick to the literature. We could have a vote on it but given that it was trivial to do the search-and-replace PR because they're only in one file right now, I made #27004 . Yes Doset is shorter than DoubleCoset. But why does this matter? If shortness matters and readability doesn't, I propose just changing it to D because that's just as incomprehensible.

[Eric Wieser]

(merged with the previous thread)

[Kevin Buzzard]

I'd forgotten my previous rant on the matter; at least this time I did something.

[Kevin Buzzard]

On top of that, I've just noticed that the module docstring talks about a non-existing rel which is called setoid in the code, although all lemmas about it still refer to rel. Should we just change setoid to rel (it's in the Doset namespace)

[Aaron Liu]

Quotient needs a redesign

[Eric Wieser]

Yeah, I would say leave the rel alone for that reason

[Eric Wieser]

The rel is vestigial from when the preferred spelling was someSetoid.rel x y, whereas now we write someSetoid.r x y which via a CoeFun (not FunLike) is someSetoid x y