## Stream: Is there code for X?

### Topic: Quotient thing

#### Adam Topaz (Feb 01 2021 at 16:02):

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 (Feb 01 2021 at 16:07):

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

#### Eric Wieser (Feb 01 2021 at 16:08):

Your quotient_thing.setoid is docs#mul_action.orbit_rel

#### Eric Wieser (Feb 01 2021 at 16:09):

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 (Feb 01 2021 at 16:13):

Any suggestions on naming the quotient?

#### Eric Wieser (Feb 01 2021 at 16:19):

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 (Feb 01 2021 at 16:28):

mul_action.orbits?

Last updated: May 07 2021 at 22:14 UTC