quotients and equivalence classes

Stream: new members

[Calle Sönne]

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?

[Kenny Lau]

#xy

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Calle Sönne]

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]

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]

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]

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]

Ah okay thanks then I will proceed like that

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Reid Barton]

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

[Calle Sönne]

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?

[Adam Topaz]

There's also docs#quotient.exists_rep

[Adam Topaz]

That lets you choose representatives

[Calle Sönne]

Adam Topaz said:

There's also docs#quotient.exists_rep

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

[Reid Barton]

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]

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

[Adam Topaz]

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

[Kenny Lau]

I thought you need rcases for that

[Adam Topaz]

You're right @Kenny Lau

[Adam Topaz]

(I do think induction works as well though)

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Kenny Lau]

or you can just use quotient.xxxx'

[Adam Topaz]

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]

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

[Reid Barton]

But you also form the quotient space, right?

[Calle Sönne]

and what is the advantage of doing this?

[Calle Sönne]

Reid Barton said:

But you also form the quotient space, right?

yes

[Kenny Lau]

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

[Reid Barton]

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]

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]

So using a local instance should work okay in this case

[Kevin Buzzard]

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]

Oh okay so I defined instance procompletion_setoid

[Calle Sönne]

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

[Reid Barton]

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

[Reid Barton]

below it

[Calle Sönne]

Ah okay

[Reid Barton]

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

[Calle Sönne]

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

[Reid Barton]

and this works out pretty well

[Reid Barton]

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

[Calle Sönne]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

Thanks! I will try this

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

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

[Calle Sönne]

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

[Reid Barton]

Oh I see, I had something wrong in my head

[Adam Topaz]

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

[Calle Sönne]

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

[Calle Sönne]

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]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Eric Wieser]

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