Quotient thing

Stream: Is there code for X?

[Adam Topaz]

Do we have something like the following construction? If not, what should we call it?!

import algebra

variables (G : Type*) [group G] (X : Type*) [mul_action G X]

-- TODO: Rename this!
namespace quotient_thing

@[simps]
def setoid : setoid X := ⟨λ x y, ∃ g : G, g • x = y,
λ x, ⟨1, by simp⟩,
λ x y ⟨g,hg⟩, ⟨g⁻¹, by simp [← hg]⟩,
λ x y z ⟨g,hg⟩ ⟨h,hh⟩, ⟨h * g, by simp [mul_smul, hh, hg]⟩⟩

end quotient_thing

def quotient_thing := quotient (quotient_thing.setoid G X)

[Eric Wieser]

∃ g : G, g • x = y is y ∈ mul_action.orbit G x if that helps

[Eric Wieser]

Your quotient_thing.setoid is docs#mul_action.orbit_rel

[Eric Wieser]

And the quotient by it seems to be used here: https://github.com/leanprover-community/mathlib/blob/39ecd1abaabede897b2e5367efc2af8cdcadcc5b/src/group_theory/sylow.lean#L39

[Adam Topaz]

Any suggestions on naming the quotient?

[Eric Wieser]

None, I don't actually know this stuff, I just remembered finding it when moving stuff around to fix import cycles

[Bryan Gin-ge Chen]

mul_action.orbits?