quotient vs orbits

Stream: maths

[Yury G. Kudryashov]

I want to formulate a lemma for the quotient by any group action, then apply it to the quotient group. What would you recommend? Redefine subgroup.quotient to be the orbits space of the left action? Introduce a predicate that relates the group action and the quotient space? Something else?

[Yury G. Kudryashov]

@Heather Macbeth @Alex Kontorovich This is about generalizing your haar_quotient file. IMHO we should have a definition of a Haar measure for an action and a theorem that says that the quotient of a Haar measure is a Haar measure (if 2 actions commute and we have a fundamental domain).

[Anatole Dedecker]

We do have the setoid, it’s docs#mul_action.orbit_rel, so you can just use docs#quotient on that, but there’s not much lemmas about it

[Yury G. Kudryashov]

The question is how to relate the quotient by this setoid and the quotient group.

[Yury G. Kudryashov]

Of course, I can prove equality of setoids and use it to construct a homeomorphism of the quotient spaces.

[Yury G. Kudryashov]

This is one of the possible ways, some other options are listed above.

[Anatole Dedecker]

Oh yeah sorry I missed this part :face_palm: