Zulip Chat Archive

Stream: new members

Topic: quotients and equivalence classes


view this post on Zulip Calle Sönne (Dec 04 2020 at 16:21):

Hello. I would like to access the equivalence class of an element in a quotient (by an equivalence relation) as a subset of the "original" set. What is the best way to go about this? I found the \[[ \]] notation but it seems that this refers to the equivalence class as an element of the quotient. Should I just take the preimage under quotient.mk?

view this post on Zulip Kenny Lau (Dec 04 2020 at 16:22):

#xy

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 16:22):

I don't think we have equivalence classes! I might be wrong. I just usually define cl(x):={y | y R x}

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 16:22):

But I've only ever needed them when doing UG demo stuff like partitions = equiv relns

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:28):

So maybe to give some more context I am trying to prove that the quotient of a compact hausdorff space by its connected components is again hausdorff. To do this I want to apply the "normality" condition of my space to the connected components (which are the equivalence classes). So I need to access the equivalence classes somehow, but I am given elements in my quotient space so I am unsure how to proceed. So I know that I can just take a point in my class and then take the connected component of this, but then I dont know that its the equivalence class. So I want to access the equivalence class in such a way that lean knows its the equivalence class. Based on Kevins answer it seems that I should use quotient.mk \inv?

view this post on Zulip Reid Barton (Dec 04 2020 at 16:28):

I found docs#setoid.classes which is the set of all equivalence classes, and whose definition makes me think the official mathlib way is just something like what Kevin wrote

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 16:29):

I think I lied -- I think that 50% of the time I used to write x R y. However, when I realised that R need not be an equivalence relation I started thinking about "the elements of x" and started to use y R x consistently.

view this post on Zulip Reid Barton (Dec 04 2020 at 16:29):

Preimage under quotient.mk is probably quite easy to prove equal to that definition as well, so it shouldn't matter much

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:30):

Ah okay thanks then I will proceed like that

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:30):

The usual way to do this is with docs#quotient.exact and docs#quotient.sound

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 16:30):

It just occurred to me that RR could be \ni rather than \in

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:31):

Those are the two main functions I use whenever I deal with quotients to translate back an forth to the original relation

view this post on Zulip Reid Barton (Dec 04 2020 at 16:32):

Next you'll be saying we could write things like xyx \ge y

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:33):

Adam Topaz said:

Those are the two main functions I use whenever I deal with quotients to translate back an forth to the original relation

Oh okay, I did read those too but it did not occur to me how I should use them in my situation as I am directly given elements of the quotient, so as far as I know they are not of the form \[[ x \]]. Unless lean somehow still knows this behind the scenes?

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:33):

There's also docs#quotient.exists_rep

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:33):

That lets you choose representatives

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:34):

Adam Topaz said:

There's also docs#quotient.exists_rep

oh great. Thats much better, I was using quotient.out

view this post on Zulip Reid Barton (Dec 04 2020 at 16:34):

Or the induction principle says you can prove something for all elements of the quotient if you can prove it for everything of the form [[x]]

view this post on Zulip Reid Barton (Dec 04 2020 at 16:34):

https://leanprover-community.github.io/mathlib_docs/init/data/quot.html#quotient.induction_on

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:34):

In a tactic proof, you can use casesrcases or induction to get a representative.

view this post on Zulip Kenny Lau (Dec 04 2020 at 16:35):

I thought you need rcases for that

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:35):

You're right @Kenny Lau

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:35):

(I do think induction works as well though)

view this post on Zulip Reid Barton (Dec 04 2020 at 16:36):

right, which means you can use rintro \<x\> as well

view this post on Zulip Reid Barton (Dec 04 2020 at 16:37):

By the way, if you are working with quotient, are you using something like local attribute [instance] to impose the "same connected component" relation?

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:39):

Reid Barton said:

By the way, if you are working with quotient, are you using something like local attribute [instance] to impose the "same connected component" relation?

No, I just manually constructed the relation by saying x ~ y if x \in connected_component y and then proved that it was an equivalence relation

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:39):

I also showed that it was the same as saying that the connected components were equal

view this post on Zulip Kenny Lau (Dec 04 2020 at 16:40):

or you can just use quotient.xxxx'

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:40):

So you can either make the setoid a local instance, like Reid said, or you need to put ' next to all of these quotient.foo functions

view this post on Zulip Kenny Lau (Dec 04 2020 at 16:40):

I don't think you want a global instance on any compact hausdorff space

view this post on Zulip Reid Barton (Dec 04 2020 at 16:40):

But you also form the quotient space, right?

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:41):

and what is the advantage of doing this?

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:41):

Reid Barton said:

But you also form the quotient space, right?

yes

view this post on Zulip Kenny Lau (Dec 04 2020 at 16:41):

I mean the quotient is just a finite discrete space isn't it

view this post on Zulip Reid Barton (Dec 04 2020 at 16:42):

What Kenny said--the design of quotients is a little odd because setoid being a type class means you should have only one instance of it per type

view this post on Zulip Reid Barton (Dec 04 2020 at 16:42):

but there's also no reason you wouldn't have other instances on some types that just happen to also be compact Hausdorff spaces or whatever

view this post on Zulip Reid Barton (Dec 04 2020 at 16:42):

So using a local instance should work okay in this case

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 16:43):

Kenny Lau said:

I mean the quotient is just a finite discrete space isn't it

I think that it can be profinite, e.g. Z_p is totally disconnected so the equivalence relation is just trivial here.

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:43):

Oh okay so I defined instance procompletion_setoid

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:44):

and now I should add local attribute [instance] above or something?

view this post on Zulip Reid Barton (Dec 04 2020 at 16:44):

I think there's a way to do it in a single declaration, but usually people just write def and then local attribute [instance] procompletion_setoid

view this post on Zulip Reid Barton (Dec 04 2020 at 16:44):

below it

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:45):

Ah okay

view this post on Zulip Reid Barton (Dec 04 2020 at 16:45):

and then, when you want to use the instance somewhere else, you also write the same local attribute [instance] there

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:45):

Oh so now I have made it into a "global" instance?

view this post on Zulip Reid Barton (Dec 04 2020 at 16:45):

and this works out pretty well

view this post on Zulip Reid Barton (Dec 04 2020 at 16:45):

Yes... and most likely a global instance for basically every topological space (with whatever conditions you imposed)

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:47):

So this was why I had to write Profinite.procompletion_setoid everywhere :grinning_face_with_smiling_eyes:

view this post on Zulip Reid Barton (Dec 04 2020 at 16:49):

oh yeah, it's weird that quotient itself takes the setoid explicitly

view this post on Zulip Reid Barton (Dec 04 2020 at 16:50):

You could organize it something like this:
define the setoid, make it a local instance and then define
def connected_components_quotient (X : Type*) [topological_space X] := quotient connected_components_setoid
(in general, this definition makes sense for general spaces X)

view this post on Zulip Reid Barton (Dec 04 2020 at 16:51):

then write an instance saying that connected_components_quotient X is Hausdorff if X is--at this point you no longer need the setoid instance in the statement (but you probably still need it for the proof)

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:52):

Thanks! I will try this

view this post on Zulip Reid Barton (Dec 04 2020 at 16:52):

actually I guess it's Hausdorff even if X isn't

view this post on Zulip Reid Barton (Dec 04 2020 at 16:52):

is that right? I guess the proof will answer that question :upside_down:

view this post on Zulip Adam Topaz (Dec 04 2020 at 16:53):

No (I think) that's not right. Can't think of an example though...

view this post on Zulip Calle Sönne (Dec 04 2020 at 16:53):

Reid Barton said:

is that right? I guess the proof will answer that question :upside_down:

Oh I thuoght that the proof would use that compact Hausdorff spaces are normal? And that connected components are closed

view this post on Zulip Reid Barton (Dec 04 2020 at 16:56):

Oh I see, I had something wrong in my head

view this post on Zulip Adam Topaz (Dec 04 2020 at 17:10):

@Calle Sönne It would be nice to prove the universal property mentioned here:
https://stacks.math.columbia.edu/tag/08ZL

view this post on Zulip Calle Sönne (Dec 04 2020 at 17:11):

Adam Topaz said:

Calle Sönne It would be nice to prove the universal property mentioned here:
https://stacks.math.columbia.edu/tag/08ZL

Oh yes, I will try doing that. (after I prove the hausdorff thing :grinning:)

view this post on Zulip Calle Sönne (Dec 04 2020 at 17:45):

Reid Barton said:

I found docs#setoid.classes which is the set of all equivalence classes, and whose definition makes me think the official mathlib way is just something like what Kevin wrote

So if people generally dont use the setoid.classes stuff, then what results do you use to show equivalence classes are disjoint?

view this post on Zulip Calle Sönne (Dec 04 2020 at 17:47):

Oh so maybe you use the quot.foo stuff for that

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 17:48):

You'll probably find that any question about equivalence classes can be reformulated as a question about quotients somehow.

view this post on Zulip Adam Topaz (Dec 04 2020 at 17:53):

If [[a]] = [[b]] then R a b is precisely docs#quotient.exact

view this post on Zulip Adam Topaz (Dec 04 2020 at 17:58):

Or if you want the converse that's docs#quotient.sound

view this post on Zulip Eric Wieser (Dec 05 2020 at 14:57):

I guess disjointness would be shown via an instance of nontrivial (quotient mysetoid)?


Last updated: May 08 2021 at 18:17 UTC