migrate to `QuotLike` API

Stream: mathlib4

[Yuyang Zhao]

I would like to get more feedback on #16421 QuotLike API. This typeclass is primarily for use by type synonyms of Quot and docs#Quotient. Using QuotLike API for type synonyms of Quot and docs#Quotient will avoid defeq abuse caused by directly using Quot and docs#Quotient APIs.

This PR also adds some typeclasses to support different ways to find the quotient map that should be used, which resolves the problem mentioned in this porting note.

I expect most of the APIs in mathlib that use docs#Quotient to migrate to QuotLike to avoid defeq abuse and duplication issues. It has been tested in #16428, and works fine up to LinearAlgebra.Quotient.Basic.

[Adam Topaz]

Can you please give some examples of existing issues that this would solve?

[Adam Topaz]

To be honest, it’s not clear to me why we would want this change. The class docs#SetLike is useful because we frequently have bundled subobjects in the algebraic hierarchy. But that’s not the case for quotients.

[Violeta Hernández]

What sort of def-eq abuse? The def-eqs that exist for definitions such as Quotient.lift are very convenient ones, and are presumably the whole reason we treat Quot.sound as an axiom instead of just declaring the type of equivalence classes.

[Yuyang Zhao]

Maybe this isn't the best example. We recently cleared up some Quotient API usage in #18205, replacing them with the API duplicated for Cardinal. Similarly, we may have to duplicate a lot of the Quotient API for every type synonym of Quotient.

[Yuyang Zhao]

Using the QuotLike API doesn't break defeq. It just doesn't always produce Quotient in the proof, but instead the type you want. Then there's no need to copy the quotient API for various types.

[Violeta Hernández]

Well, in that case, the issue was that the preferred form of the quotient is #x rather than [[x]]. Something similar happens with docs#Ordinal.inductionOn, which uses type r rather than [[(a, r, wo)]].

[Violeta Hernández]

Is that the issue being solved?

[Yuyang Zhao]

Currently after almost every quotient type is defined, the first thing to do is to define a constructor that is a synonym for Quotient.mk, and the second thing might be to define a simp lemma to turn Quotient.mk into the custom constructor. I hope QuotLike will make us not have to do that.

[Yuyang Zhao]

In #16428 I made # another notation for mkQ, but I haven't tested it further.

[Violeta Hernández]

Oh, so the idea is every type can declare a QuotLike instance using whatever the preferred form of the constructor is? That seems very useful.

[Violeta Hernández]

Out of curiosity, what are other examples of quotient types which use a default constructor other than [[x]]?

[Violeta Hernández]

I guess there's also docs#Surreal.mk

[Violeta Hernández]

Though yeah, I'm not sure if this QuotLike API can help much in cases where the constructor takes in different arguments than the quotient, such as this one or in the ordinal case.

[Violeta Hernández]

Seems like you would need some tactic machinery instead

[Eric Wieser]

AUII, the proposal is to replace Quotient.mk : X -> Quotient someInternalSetoid with QuotLike.mk X -> TheActualTypeName, eliminating the custom mks entirely but also avoiding the abuse of defeq of the types

[Adam Topaz]

I think if we want to try something like this, then I would be inclined to try to mimic SetLike. We can identify Setoid X with the type of quotients of X, and define QuotientLike T X to say that T behaves like Setoid X. What the PR in this thread seems to miss is that in most situations of interest the quotient map is not just a plain function, but rather a morphism of some kind (a group hom, ring hom, continuous map, etc.), so one would still have to introduce an additional definition for the quotient map as a bundled morphism in most situations with the proposed approach. If we instead "bundle" quotients as I suggested here, and make a QuotientLike class, we could also introduce, for example, MonoidQuotientClass which would follow the analogy SubmonoidClass : SetLike :: MonoidQuotientClass : QuotientLike.

[Adam Topaz]

Namely something like this:

import Mathlib.Data.Setoid.Basic

instance {α : Sort u} : CoeSort (Setoid α) (Sort u) where
  coe s := Quotient s

class QuotientLike (S : Type u) (α : outParam <| Type v) where
  coe : S → Setoid α
  coe_injective : Function.Injective coe

instance : QuotientLike (Setoid α) α where
  coe s := s
  coe_injective _ _ h := h

instance [QuotientLike S α] : CoeTC S (Setoid α) where
  coe s := QuotientLike.coe s

instance [QuotientLike S α] : CoeSort S (Type _) where
  coe s := (s : Setoid α)

def QuotientLike.mk' [QuotientLike S α] (X : S) : α → X :=
  Quotient.mk _

[Adam Topaz]

I should clarify that I don't know whether this is a good idea, rather that it's analogous to SetLike which empirically seems to work quite well.

[Yuyang Zhao]

This sounds like an orthogonal proposal. It cannot be used for two specific types. Maybe QuotLike isn't the appropriate name. It may suggest that this typeclass is similar to FunLike and SetLike, but it is not.

[Edward van de Meent]

It may be called something like LawfulQuotient or QuotientType?

[Yuyang Zhao]

Also, QuotientLike typeclass in this proposal is not compatible with current API design. Both docs#QuotientGroup.mk' and docs#Ideal.Quotient.mk have an extra instance parameter.

[Aaron Liu]

Yuyang Zhao said:

Also, QuotientLike typeclass in this proposal is not compatible with current API design. Both docs#QuotientGroup.mk' and docs#Ideal.Quotient.mk have an extra instance parameter.

Why does this matter? You could attach an extra instance parameter to the relevant QuotientLike class.

[Yuyang Zhao]

def QuotientLike.mkMonoidHom [QuotientLike S α] [MonoidQuotientClass S α] (X : S) : α →* X := sorry

We want this function iiuc. Then what should S be for docs#QuotientGroup.mk' and docs#Ideal.Quotient.mk ?

[Aaron Liu]

This one doesn't make any sense to me, since the only choice for S is Type u but that's obviously not what you want to say.

[Yuyang Zhao]

In @Adam Topaz's example, α → X is actually α → Quotient (QuotientLike.coe X).

[Yuyang Zhao]

mkMonoidHom just replaces the function in mk' with MonoidHom.

[Aaron Liu]

Then I think @Adam Topaz is wrong, we should have α → S on the rhs and drop X.

[Aaron Liu]

Actually, I could make this work...

[Aaron Liu]

We would need to make some new types

structure QuotientGroup (G : Type*) [Group G] extends Setoid G where
  protected mul_left_sound' : ∀ (a b c : G), b ≈ c → a * b ≈ a * c

class QuotientGroup.Normal {G : Type*} [Group G] (q : QuotientGroup G) where
  protected mul_sound' : ∀ (a b c d : G), a ≈ c → b ≈ d → a * b ≈ c * d

[Kevin Buzzard]

docs#Con is close to this