Zulip Chat Archive

Stream: Is there code for X?

Topic: iff.intro quotient.exact' quotient.sound'


view this post on Zulip Eric Wieser (Jan 19 2021 at 12:33):

Does this have a name? If not, what would be a good name for it?

view this post on Zulip Johan Commelin (Jan 19 2021 at 12:34):

I have no idea what the types of quotient.exact' and quotient.sound' are... so I don't know what this question is :wink:

view this post on Zulip Eric Wieser (Jan 19 2021 at 12:35):

I will update with the statement shortly...

view this post on Zulip Eric Wieser (Jan 19 2021 at 12:36):

lemma quotient.name_me {α : Type*} (x y : α) [s : setoid α] :
  quotient.mk x = quotient.mk y  x  y :=
quotient.exact, quotient.sound

lemma quotient.name_me' {α : Type*} (x y : α) (s : setoid α) :
  (quotient.mk' x : quotient s) = quotient.mk' y  setoid.r x y :=
quotient.exact', quotient.sound'

(xref: docs#quotient.exact, docs#quotient.exact', docs#quotient.sound, docs#quotient.sound')

view this post on Zulip Eric Wieser (Jan 19 2021 at 12:38):

Ah, it's docs#quotient.eq'

view this post on Zulip Kevin Buzzard (Jan 19 2021 at 12:53):

Your question reminds me that somewhere deep down in my job list is "write basic document on quotients explaining all the language used in mathlib"

view this post on Zulip Kevin Buzzard (Jan 19 2021 at 12:53):

For mathematicians it's particularly confusing, because we traditionally use lift to mean something else.

view this post on Zulip Eric Wieser (Jan 19 2021 at 12:58):

It probably doesn't help that the definitions and therefore documentation is split between core and mathlib


Last updated: May 16 2021 at 05:21 UTC