## Stream: new members

### Topic: quotients and equivalence classes

#### 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?

#xy

#### 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}

#### Kevin Buzzard (Dec 04 2020 at 16:22):

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

#### 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?

#### 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

#### 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.

#### 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

#### Calle Sönne (Dec 04 2020 at 16:30):

Ah okay thanks then I will proceed like that

#### Adam Topaz (Dec 04 2020 at 16:30):

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

#### Kevin Buzzard (Dec 04 2020 at 16:30):

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

#### 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

#### Reid Barton (Dec 04 2020 at 16:32):

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

#### Calle Sönne (Dec 04 2020 at 16:33):

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?

#### Adam Topaz (Dec 04 2020 at 16:33):

There's also docs#quotient.exists_rep

#### Adam Topaz (Dec 04 2020 at 16:33):

That lets you choose representatives

#### Calle Sönne (Dec 04 2020 at 16:34):

There's also docs#quotient.exists_rep

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

#### 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]]

#### Reid Barton (Dec 04 2020 at 16:34):

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

#### Adam Topaz (Dec 04 2020 at 16:34):

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

#### Kenny Lau (Dec 04 2020 at 16:35):

I thought you need rcases for that

#### Adam Topaz (Dec 04 2020 at 16:35):

You're right @Kenny Lau

#### Adam Topaz (Dec 04 2020 at 16:35):

(I do think induction works as well though)

#### Reid Barton (Dec 04 2020 at 16:36):

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

#### 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?

#### 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

#### 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

#### Kenny Lau (Dec 04 2020 at 16:40):

or you can just use quotient.xxxx'

#### 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

#### Kenny Lau (Dec 04 2020 at 16:40):

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

#### Reid Barton (Dec 04 2020 at 16:40):

But you also form the quotient space, right?

#### Calle Sönne (Dec 04 2020 at 16:41):

and what is the advantage of doing this?

#### Calle Sönne (Dec 04 2020 at 16:41):

Reid Barton said:

But you also form the quotient space, right?

yes

#### Kenny Lau (Dec 04 2020 at 16:41):

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

#### 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

#### 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

#### Reid Barton (Dec 04 2020 at 16:42):

So using a local instance should work okay in this case

#### 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.

#### Calle Sönne (Dec 04 2020 at 16:43):

Oh okay so I defined instance procompletion_setoid

#### Calle Sönne (Dec 04 2020 at 16:44):

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

#### 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

below it

Ah okay

#### 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

#### Calle Sönne (Dec 04 2020 at 16:45):

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

#### Reid Barton (Dec 04 2020 at 16:45):

and this works out pretty well

#### 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)

#### 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:

#### Reid Barton (Dec 04 2020 at 16:49):

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

#### 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)

#### 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)

#### Calle Sönne (Dec 04 2020 at 16:52):

Thanks! I will try this

#### Reid Barton (Dec 04 2020 at 16:52):

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

#### Reid Barton (Dec 04 2020 at 16:52):

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

#### Adam Topaz (Dec 04 2020 at 16:53):

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

#### 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

#### 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

#### Calle Sönne (Dec 04 2020 at 17:11):

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:)

#### 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?

#### Calle Sönne (Dec 04 2020 at 17:47):

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

#### 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.

#### Adam Topaz (Dec 04 2020 at 17:53):

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

#### Adam Topaz (Dec 04 2020 at 17:58):

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

#### 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