Zulip Chat Archive

Stream: new members

Topic: quotient, quotienting?


view this post on Zulip Huỳnh Trần Khanh (Feb 11 2021 at 05:35):

What does 'quotient' mean in Lean and its close relative, Coq?

view this post on Zulip Huỳnh Trần Khanh (Feb 11 2021 at 06:58):

oh, it's unusual for a question to take this long to receive an answer. guess i need to be more patient

view this post on Zulip Johan Commelin (Feb 11 2021 at 07:04):

It's like quotients in maths. Did you search #tpil for "quotient"?

view this post on Zulip Huỳnh Trần Khanh (Feb 11 2021 at 07:04):

oh I did a Google search lol and got no results, thanks for the reminder

view this post on Zulip Kevin Buzzard (Feb 11 2021 at 08:44):

Just like subsets are ways to make smaller objects Y from a big object X, quotients are another way -- a kind of duel way. A subset of X is an object Y and an injection from Y to X. A quotient of X is an object Y and a surjection from X to Y. For example the even integers are a subset of the integers, but the integers modulo 10 are naturally a quotient of the integers. You can think of them as a subset but this isn't such a cool way of doing it because 7 and 8 are integers mod 10 and their sum in the integers mod 10 is 5, but their sum in the integers is 15, which means that the injection doesn't preserve addition but the surjection (sending every integer to it's reduction modulo 10) does (as 15 gets mapped to 5).

view this post on Zulip Kevin Buzzard (Feb 11 2021 at 08:46):

In this mathlib file https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean I make the integers mod 37 as a quotient of the integers.

view this post on Zulip Kevin Buzzard (Feb 11 2021 at 08:50):

You make subsets of a type by putting a predicate on the type. The corresponding subset is the terms where the predicate is true. You make quotients of a type by putting a relation on the type. The corresponding quotient is the type you get if you regard terms which are related as actually being equal. For example you can put a relation on the naturals saying that a and b are related if they end in the same digit. The corresponding quotient would be the integers modulo 10, and the surjection from the integers sends two integers to the same residue class iff they end in the same digit.

view this post on Zulip Chris B (Feb 11 2021 at 09:06):

Logical verification also has a section on quotients with examples/exercises. https://github.com/blanchette/logical_verification_2020

view this post on Zulip Andrew Ashworth (Feb 11 2021 at 21:41):

Huỳnh Trần Khanh said:

oh I did a Google search lol and got no results, thanks for the reminder

I was curious and this: https://www.hedonisticlearning.com/posts/quotient-types-for-programmers.html was the second result when I searched for quotient + related words (don't remember)


Last updated: May 11 2021 at 12:15 UTC