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):
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):
Last updated: May 07 2021 at 22:14 UTC