Ensuring that a property holds for arbitrary group elements

Stream: new members

[Alex Griffin]

I have a collection of proofs (I previously posted about this) that show which elements of dihedral groups can and can't be central. Part of that shows that rotation elements of order at most 2 necessarily commute with all rotations and with all reflections. Now, I know that this means that these elements are central, because every element of the group is of this form. However, I realized that just having these proofs and saying that they imply centrality might be a bit of a handwave. Therefore, it would be beneficial to have a proof explicitly stating that these elements belong to the center, which would be done by providing a proof that, for any given x : dihedral_group n term, that these elements commute with x. The conceptual problem I'm having is how to extend a result of my form to one involving an arbitrary element. The group multiplication of dihedral_group n is defined in a way that is divided into a collection of cases, such as r i * r j, sr i * r j, etc. How can I get a result about whether two products of group elements are equal if the way they are computed is left up in the air?

For reference, here are the relevant pieces of code that show commutation for the individual cases:

import group_theory.specific_groups.dihedral
variables {n : ℕ}

/--
Rotations with order at most 2 commute with all rotations.
`i` is any `zmod n` term satisfying `2 * i = 0`.
-/
lemma r_mem_center_r {i : zmod n} (h : 2 * i = 0) (j : zmod n) : r i * r j = r j * r i :=
by simp [add_comm]

/--
Rotations with order at most 2 commute with all reflections.
`i` is any `zmod n` term satisfying `2 * i = 0`.
-/
lemma r_mem_center_sr {i : zmod n} (h : 2 * i = 0) (j : zmod n) : r i * sr j = sr j * r i :=
by simpa [sub_eq_add_neg, ← add_eq_zero_iff_neg_eq, ← two_mul]

[Kevin Buzzard]

Can you post a #mwe of a sorry which you'd like to see filled, rather than just asking a maths question?

[Eric Wieser]

I think you're looking for:

lemma r_mem_center {i : zmod n} (h : 2 * i = 0) (x : dihedral_group n) : r i * x = x * r i :=
begin
  cases x,
  -- now this is easy
end

[Alex Griffin]

Ah, did not realize that cases would work like that. That makes sense. Thank you very much, that did the trick.

[Eric Wieser]

Once you do that, I'd recommend you try to fit this into the mathlib structures

-- this stuff should be in mathlib but isn't
namespace subgroup

instance (G : Type*) [group G] (S : subgroup G) : mul_action S G :=
{ smul := λ a b, a * b,
  one_smul := λ a, one_mul _,
  mul_smul := λ a b, mul_assoc _ _ }

instance is_scalar_tower_right (G : Type*) [group G] (S : subgroup G) :
  is_scalar_tower S S G :=
⟨λ a b c, (mul_assoc _ _ _)⟩

end subgroup

I've left the sorries for you to solve for practice:

def dihedral_group.center : subgroup (dihedral_group n) :=
{ carrier := {x | ∃ i, 2 * i = 0 ∧ x = r i},
  one_mem' := sorry,
  mul_mem' := λ a b, sorry,
  inv_mem' := λ a, sorry }

instance : smul_comm_class (dihedral_group.center n) (dihedral_group n) (dihedral_group n) :=
{ smul_comm := λ a b c, show ↑a * (b * c) = b * (a * c), begin
    sorry
  end }

With these instances, you can now use lemmas like docs#smul_mul_assoc

[Kevin Buzzard]

Yes, I was going to get to that after I'd teased out a MWE :-) Actually making the definition of the centre is more useful than proving a theorem saying precisely which elements are in the centre

[Eric Wieser]

I think the mathlib definition of "center" is implicitly:

@[class]
abbreviation subgroup.is_center {G : Type*} [group G] (S : subgroup G) := smul_comm_class S G G

[Eric Wieser]

But I guess for that definition to make sense you need the other two instances I defined above that aren't in mathlib yet

[Eric Wieser]

PR'd more general version of those instances as #7665

[Eric Wieser]

Ok, everything in the "this stuff should be in mathlib but isn't" code block above is now in mathlib