Zulip Chat Archive

Stream: Is there code for X?

Topic: Quotient thing


view this post on Zulip 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)

view this post on Zulip Eric Wieser (Feb 01 2021 at 16:07):

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

view this post on Zulip Eric Wieser (Feb 01 2021 at 16:08):

Your quotient_thing.setoid is docs#mul_action.orbit_rel

view this post on Zulip 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

view this post on Zulip Adam Topaz (Feb 01 2021 at 16:13):

Any suggestions on naming the quotient?

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Feb 01 2021 at 16:28):

mul_action.orbits?


Last updated: May 07 2021 at 22:14 UTC