quotient refactor

Stream: general

[Yury G. Kudryashov]

Recently, we discussed that we should move from using [setoid α] to {s : setoid α} or {r : α → α → Prop} [is_equiv r]. Another idea was to allow reusing the notation ⟦x⟧ for other functions. What do you think about this typeclass?

class has_quotient_map (α : out_param (Type*)) (β : Type*) :=
(mk : α → β)
(surjective_mk : function.surjective mk)

notation `⟦` x `⟧` := has_quotient_map.mk x

Note that α is an out_param, so Lean will find out the type of x from the type of ⟦x⟧ but not vice versa (which makes sense).

[Kevin Buzzard]

Will this fit well with the port to lean 4?

I've just spent a few days trying to teach quotients (anyone interested can check out the last four videos I uploaded to YouTube and my course repo) and this whole setoid class thing makes it quite complicated. Two examples which work really well are making Z mod 37 from Z and making Z from N x N. But the moment you try and do something like quotient groups (which depend on a parameter) then type class inference can't pick up the setoid because it depends on a parameter and you end up in this weird situation where sometimes the tactic state says your equivalence relation is R N (the definition you wrote which depends on the parameter N), sometimes it's setoid.r and sometimes it's ≈ (and writing helper lemmas involves @ everywhere). I was trying to make a worksheet for the students on quotient groups (something which they might definitely want to attempt as part of a project) and (for the first time in my course) I actually just gave up. It's such a mess. Any change which makes notation more likely to work in the situation where we can't have a setoid instance would get a big thumbs up from me

[Kevin Buzzard]

If you like you could regard quotient groups as some kind of test -- can you make them from first principles using simple tactic proofs and make the result comprehensible to someone who's read the relevant chapter of #tpil (because I couldn't)

[Gabriel Ebner]

Another idea was to allow reusing the notation ⟦x⟧ for other functions. What do you think about this typeclass?

First of all, note that Lean 4 no longer includes this global notation. We could remove it in Lean 3 core as well. Same goes for backporting the {s : Setoid α} change.

If we add a type class for ⟦⟧, it might be worth it to also use it for free_group.of and co.

[Yury G. Kudryashov]

Gabriel Ebner said:

If we add a type class for ⟦⟧, it might be worth it to also use it for free_group.of and co.

So, the surjectivity assumption should be in a separate typeclass. BTW, why ⟦⟧, not coe, for free_group.of?

[Eric Wieser]

That would create a diamond for a free group over nat

[Yury G. Kudryashov]

Indeed

[Yury G. Kudryashov]

Then we can't use "quotient" in the name. Any suggestions?

[Reid Barton]

has_mk? Not sure if serious

[Anatole Dedecker]

I was about to say has_canonical_mk but that’s not better x)

[Eric Wieser]

Would docs#free_algebra.ι and docs#tensor_algebra.ι etc be change to use that typeclass too? Or do we reserve ⟦⟧ for surjective maps? (edit: linkifier doesn't like those)

[Yury G. Kudryashov]

docs#free_group.of is definitely not surjective

[Adam Topaz]

Reid Barton said:

has_mk? Not sure if serious

I like this..

[Adam Topaz]

And I would also be very much in favor of using the mk notation for all examples of applying the unit of some adjunction in algebraic contexts (the free group, free algebra, tensor algebra are all examples)

[Reid Barton]

Conceptually it makes sense to group together all the examples mentioned so far (they are colimit/left adjoint-type constructions, that receive a map mk from the original data). :snail:

[Reid Barton]

And often ⟦⟧ will imitate the normal math notation, e.g. if you consider the free group on the elements of a group, then one writes $[g]$ for the generator of the free group to distinguish $[g][h]$ from $[gh]$.

[Yury G. Kudryashov]

I suggest the following migration path:

1. Drop ⟦⟧ notation in the core, replace it with something else (e.g., ⟬ ⟭). The new notation is to be removed once migration is done.
2. Add has_mk as described above. Build a theory around this notation in mathlib.
3. Gradually migrate from quotient.mk' to has_mk with new API. Possibly, replace some invisible coercions with visible has_mk.mk. E.g., I think that ⟦x⟧ looks better than an arrow for the quotient group but we can discuss this later.
4. Drop notation for quotient.mk.

[Gabriel Ebner]

replace it with something else (e.g., ⟬ ⟭).

Just mk should be enough. I don't think it's worth introducing a new notation for it. Lean 4 doesn't have it either.

[Yury G. Kudryashov]

We use it at least 500 times in mathlib.

[Gabriel Ebner]

But in mathlib we have has_mk, right?

[Yury G. Kudryashov]

We will but I want the first PR to be very simple.

[Yury G. Kudryashov]

Another option is to use a local notation for quotient.mk while we do the migration.