Isomorphism classes

Stream: new members

[Adrián Doña Mateo]

I've been messing around with category_theory.isomorphism_classes but I'm not entirely sure how to use it. For instance, I think the type of isomorphism classes of Groups should be isomorphism_classes.obj (Cat.of Group). If I have (G : Type*) [group G] and I want to write its isomorphism class I would write ⟦Group.of G⟧, but for some reason this cannot find the right instance of setoid. This is what I have:

import category_theory.isomorphism_classes
import algebra.category.Group

open category_theory

variables (G : Type*) [group G]

-- This works
#check (@quotient.mk _ (is_isomorphic_setoid _) (Group.of G) : isomorphism_classes.obj (Cat.of Group))

-- But this doesn't
#check (⟦Group.of G⟧ : isomorphism_classes.obj (Cat.of Group))

[Bhavik Mehta]

This is probably because is_isomorphic_setoid isn't an instance, so @quotient.mk with naming the setoid is alright, but in the second case typeclass inference can't find it. There are two way to fix this - you could mark it as an instance in your file by writing local attribute [instance] is_isomorphic_setoid, or you could use quotient.mk' (Group.of G) instead of quotient.mk (Group.of G)

[Kevin Buzzard]

This trick about using primed quotient stuff to infer equivalences using unification rather than type class inference is something which you just pick up along the way, the documentation for this trick is pretty well-hidden.

[Bhavik Mehta]

There is this note though: https://leanprover-community.github.io/mathlib_docs/notes.html#implicit%20instance%20arguments

[Kevin Buzzard]

Yes but the "copy the entire quotient API putting primes in front of it" is slightly different I guess.

[Adam Topaz]

It's also incomplete: docs#quotient.lift'

[Adam Topaz]

docs#quotient.lift_on' is there

[Bhavik Mehta]

Adam Topaz said:

It's also incomplete: docs#quotient.lift'

Yeah this has caught me out quite a few times

[Bhavik Mehta]

By the way, an example of the local attribute approach is in https://github.com/leanprover-community/mathlib/blob/c25dad98caa98a707252412e59e309a1548215be/src/category_theory/skeletal.lean#L44, I'm sure there are others though

[Adrián Doña Mateo]

Okay, I finally understand what all those primes in the quotient definitions were doing. Thanks! Is there any downside to the local instance method if I plan to import this file somwhere else?