opposite multiplication for subgroups

Stream: Is there code for X?

[Alex Kontorovich]

Hello, the mul action of a subgroup is by default on the left and I'd like to define a right action. Is there an easy way to pass encodable to the opposite action? Thanks!

def subgroup.opposite {G : Type*} [group G] (H : subgroup G) : subgroup Gᵐᵒᵖ :=
{ carrier := mul_opposite.op '' (H : set G),
  one_mem' := by simp [H.one_mem],
  mul_mem' := begin
    rintros _ _ ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩,
    use b*a,
    simp [H.mul_mem hb ha],
  end,
  inv_mem' := begin
    rintros _ ⟨a, ha, rfl⟩,
    use a⁻¹,
    simp [H.inv_mem ha],
  end}

instance {G : Type*} [group G] (H : subgroup G) [encodable H] : encodable H.opposite :=
{ encode := sorry,
  decode := sorry,
  encodek := sorry }

[Adam Topaz]

import group_theory.subgroup.basic

def subgroup.opposite {G : Type*} [group G] (H : subgroup G) : subgroup Gᵐᵒᵖ :=
{ carrier := mul_opposite.op '' (H : set G),
  one_mem' := by simp [H.one_mem],
  mul_mem' := begin
    rintros _ _ ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩,
    use b*a,
    simp [H.mul_mem hb ha],
  end,
  inv_mem' := begin
    rintros _ ⟨a, ha, rfl⟩,
    use a⁻¹,
    simp [H.inv_mem ha],
  end}

def subgroup.opposite_equiv {G : Type*} [group G] (H : subgroup G) :
  H ≃ H.opposite :=
{ to_fun := λ h, ⟨mul_opposite.op h.1, h, h.2, rfl⟩,
  inv_fun := λ h, ⟨h.1.unop, by { obtain ⟨h1,h2,h3⟩ := h.2, rw ← h3, exact h2 }⟩,
  left_inv := by tidy,
  right_inv := by tidy }

instance {G : Type*} [group G] (H : subgroup G) [encodable H] : encodable H.opposite :=
encodable.of_equiv H H.opposite_equiv.symm

[Adam Topaz]

Encodable is a class that only cares about the underlying type, so the correct way to do this would be to build up the API around the underlying type of your subgroup.opposite.

[Adam Topaz]

On the other hand, concerning the underlying question of right multiplicative actions, @Eric Wieser is the canonical person to ask.

[Eric Wieser]

I'm surprised we don't have docs#subgroup.op or docs#subgroup.opposite

[Eric Wieser]

I would recommend defining it via the preimage instead

[Eric Wieser]

import group_theory.subgroup.basic

def subgroup.opposite {G : Type*} [group G] (H : subgroup G) : subgroup Gᵐᵒᵖ :=
{ carrier := mul_opposite.unop ⁻¹' (H : set G),
  one_mem' := H.one_mem,
  mul_mem' := λ a b ha hb, H.mul_mem hb ha,
  inv_mem' := λ a, H.inv_mem }

@[simps]
def subgroup.opposite_equiv {G : Type*} [group G] (H : subgroup G) :
  H ≃ H.opposite :=
mul_opposite.op_equiv.subtype_equiv $ λ _, iff.rfl