Quotient map to orbit space of group action is open

Stream: Is there code for X?

[Michael Rothgang]

The docstring for docs#IsOpenQuotientMap mentions that "the quotient map from a topological space to its quotient by the action of a group" is an open quotient map. I cannot find that fact in mathlib, though (I only see docs#isQuotientMap_quotient_mk'). What am I missing?

[Michael Rothgang]

docs#quotient_preimage_image_eq_union_mul certainly helps with showing the remaining "the quotient projection is an open map".

[Kevin Buzzard]

Is it docs#MulAction.isOpenQuotientMap_quotientMk ?

[Kevin Buzzard]

(I had to get on top of this sort of thing when developing the theory of the module topology)

[Michael Rothgang]

Looks like it, thank you!

[Kevin Buzzard]

I am a bit confused why #loogle ⊢ IsOpenQuotientMap ?a doesn't find it.

[Michael Rothgang]

If I may ask a follow-up question, that's closer to what I really want: given a group action of G on X, what's the best way to spell "the projection map is a local homeomorphism"? (I want to choose an inverse, e.g. near a certain point. My action is properly discontinuous.) docs#IsLocalHomeomorphOn (or without On) require me to construct an OpenPartialHomeomorph first.

[Michael Rothgang]

(I also loogled, without success. Just searching for IsOpenQuotientMap finds it, as hit number 30.)

[Kevin Buzzard]

(Oh! #loogle in VS Code reports fewer results than loogle.lean-lang,org ?)