Find the center of dihedral group.

Stream: new members

[Tristan]

It's easy to know that The center of the dihedral group $D_n$ is : if n is odd, then $Z(D_n)$ = \{e\} ; otherwise, $Z(D_n)$ = \{e, $r^{n/2}$\} .

open DihedralGroup

theorem center_of_dihedralGroup (n : ℕ) :
  IsSubgroup.center (DihedralGroup n) =
    if Even n then {1, r (Int.div2 n)} else {1} := by

However, I am puzzled about how to iterate over the elements of the dihedral group, specifically the elements of the forms $r$ and $sr$, to prove such an expression below.

1 goal
case pos.h.mpr.inr
n : ℕ
h : Even n
x g : DihedralGroup n
hx : x = r ↑(↑n).div2
⊢ g * x = x * g

I have a group element $g$ that I want to iterate over all elements of the dihedral group $D_n$, but I'm not sure how to do this.

[Yakov Pechersky]

Here's a start. I hope you see how I am able to iterate over all elements of the group using rintro. Your theorem isn't exactly true:

import Mathlib

@[to_additive (attr := simp)]
lemma isMulCentral_subsingleton {G : Type*} [Mul G] [Subsingleton G] (x : G) :
    IsMulCentral x := by
  constructor <;> intros <;> exact Subsingleton.elim _ _

@[simp]
lemma Set.center_subsingleton {G : Type*} [Mul G] [Subsingleton G] :
    Set.center G = univ := by
  ext; simp [Set.mem_center_iff]

open DihedralGroup

lemma isMulCentral_r_of_even (n : ℕ) :
    IsMulCentral (r n : DihedralGroup (2 * n)) := by
  constructor <;> repeat' (rintro ⟨⟩)
  rotate_left
  · simp [sub_eq_iff_eq_add, add_assoc, ← Nat.cast_add, ← two_mul n]
  all_goals simp; ring

lemma isMulCentral_sr_of_two (k : ZMod 2) : IsMulCentral (sr k) := by
  have hp : (2 : ZMod 2) = 0 := rfl
  constructor <;> repeat' (rintro (⟨⟩|⟨⟩))
  all_goals try (simp; ring1)
  · simp [eq_sub_iff_add_eq, add_assoc, ← two_mul, hp]
  · simp only [sr_mul_sr, r.injEq, eq_sub_iff_add_eq] -- annoying trivial rearrangement goal
    rw [sub_eq_add_neg, add_right_comm, ← two_mul,  ← sub_eq_add_neg, sub_eq_iff_eq_add,
      ← two_mul, hp]
    simp

lemma isMulCentral_sr_iff {n : ℕ} {k : ZMod n} :
    IsMulCentral (sr k) ↔ n = 1 ∨ n = 2 := by
  constructor
  · contrapose!
    intro hn h
    have key : (2 : ZMod n) ≠ 0 := by
      contrapose! hn
      -- annoying CharP goals
      rcases n with (_|_|_|_)
      · simp at hn
      · simp
      · simp
      · rw [← (ZMod.val_injective _).eq_iff, ZMod.val_two_eq_two_mod] at hn
        simp [Nat.mod_eq_of_lt] at hn
    apply key
    simpa [eq_neg_iff_add_eq_zero, ← two_mul] using h.comm (sr (k + 1))
  · rintro (rfl|rfl)
    · constructor <;> repeat' (rintro (⟨⟩|⟨⟩)) <;> repeat' (rintro (⟨⟩|⟨⟩)) <;>
      all_goals try (simp [← mul_assoc]; exact Subsingleton.elim _ _)
      all_goals (simp; exact Subsingleton.elim _ _)
    · exact isMulCentral_sr_of_two k


-- this is your theorem
theorem center_of_dihedralGroup_even (n : ℕ) :
    (Set.center (DihedralGroup (2 * n))) = {1, r n} := by
  rcases eq_or_ne n 1 with rfl|hn
  · ext (⟨k⟩|⟨k⟩)
    · fin_cases k
      · simp
      · simpa [Set.mem_center_iff] using isMulCentral_r_of_even 1
    · sorry -- false, since sr 0 is in the center, and it isn't 1 or r n
  refine (le_antisymm ?_ ?_).symm
  · intro g
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff]
    rintro (rfl|rfl)
    · simp
    · simp only [Set.mem_center_iff, isMulCentral_r_of_even n]
  rintro (⟨k⟩|⟨k⟩) <;>
    simp only [Set.mem_center_iff, Set.mem_insert_iff, Set.mem_singleton_iff, reduceCtorEq,
      or_false, r.injEq]
  · sorry
  · sorry

[Aaron Liu]

Since DihedralGroup 2 is isomorphic to the klein-four group, its center is the whole group.
Since DihedralGroup 1 is cyclic, its center is also the whole group.
The center of DihedralGroup 0 is trivial, and does not include sr 0.

You should be able to prove the theorem assuming 3 ≤ n.

[Tristan]

Thank you very much! With your guidance, I was able to complete the subsequent proof. However, I’m quite curious—how did you come up with the final simp only statement:
simp only [Set.mem_center_iff, Set.mem_insert_iff, Set.mem_singleton_iff, reduceCtorEq, or_false, r.injEq]
I tried using simp?, but it didn't simplify to this level. I truly admire your expertise in writing Lean code!

[Tristan]

Yakov Pechersky said:

Here's a start. I hope you see how I am able to iterate over all elements of the group using rintro. Your theorem isn't exactly true:

import Mathlib

@[to_additive (attr := simp)]
lemma isMulCentral_subsingleton {G : Type*} [Mul G] [Subsingleton G] (x : G) :
    IsMulCentral x := by
  constructor <;> intros <;> exact Subsingleton.elim _ _

@[simp]
lemma Set.center_subsingleton {G : Type*} [Mul G] [Subsingleton G] :
    Set.center G = univ := by
  ext; simp [Set.mem_center_iff]

open DihedralGroup

lemma isMulCentral_r_of_even (n : ℕ) :
    IsMulCentral (r n : DihedralGroup (2 * n)) := by
  constructor <;> repeat' (rintro ⟨⟩)
  rotate_left
  · simp [sub_eq_iff_eq_add, add_assoc, ← Nat.cast_add, ← two_mul n]
  all_goals simp; ring

lemma isMulCentral_sr_of_two (k : ZMod 2) : IsMulCentral (sr k) := by
  have hp : (2 : ZMod 2) = 0 := rfl
  constructor <;> repeat' (rintro (⟨⟩|⟨⟩))
  all_goals try (simp; ring1)
  · simp [eq_sub_iff_add_eq, add_assoc, ← two_mul, hp]
  · simp only [sr_mul_sr, r.injEq, eq_sub_iff_add_eq] -- annoying trivial rearrangement goal
    rw [sub_eq_add_neg, add_right_comm, ← two_mul,  ← sub_eq_add_neg, sub_eq_iff_eq_add,
      ← two_mul, hp]
    simp

lemma isMulCentral_sr_iff {n : ℕ} {k : ZMod n} :
    IsMulCentral (sr k) ↔ n = 1 ∨ n = 2 := by
  constructor
  · contrapose!
    intro hn h
    have key : (2 : ZMod n) ≠ 0 := by
      contrapose! hn
      -- annoying CharP goals
      rcases n with (_|_|_|_)
      · simp at hn
      · simp
      · simp
      · rw [← (ZMod.val_injective _).eq_iff, ZMod.val_two_eq_two_mod] at hn
        simp [Nat.mod_eq_of_lt] at hn
    apply key
    simpa [eq_neg_iff_add_eq_zero, ← two_mul] using h.comm (sr (k + 1))
  · rintro (rfl|rfl)
    · constructor <;> repeat' (rintro (⟨⟩|⟨⟩)) <;> repeat' (rintro (⟨⟩|⟨⟩)) <;>
      all_goals try (simp [← mul_assoc]; exact Subsingleton.elim _ _)
      all_goals (simp; exact Subsingleton.elim _ _)
    · exact isMulCentral_sr_of_two k


-- this is your theorem
theorem center_of_dihedralGroup_even (n : ℕ) :
    (Set.center (DihedralGroup (2 * n))) = {1, r n} := by
  rcases eq_or_ne n 1 with rfl|hn
  · ext (⟨k⟩|⟨k⟩)
    · fin_cases k
      · simp
      · simpa [Set.mem_center_iff] using isMulCentral_r_of_even 1
    · sorry -- false, since sr 0 is in the center, and it isn't 1 or r n
  refine (le_antisymm ?_ ?_).symm
  · intro g
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff]
    rintro (rfl|rfl)
    · simp
    · simp only [Set.mem_center_iff, isMulCentral_r_of_even n]
  rintro (⟨k⟩|⟨k⟩) <;>
    simp only [Set.mem_center_iff, Set.mem_insert_iff, Set.mem_singleton_iff, reduceCtorEq,
      or_false, r.injEq]
  · sorry
  · sorry

Thank you very much! With your guidance, I was able to complete the subsequent proof. However, I’m quite curious—how did you come up with the final simp only statement:
simp only [Set.mem_center_iff, Set.mem_insert_iff, Set.mem_singleton_iff, reduceCtorEq, or_false, r.injEq]
I tried using simp?, but it didn't simplify to this level. I truly admire your expertise in writing Lean code!

[Tristan]

Aaron Liu said:

Since DihedralGroup 2 is isomorphic to the klein-four group, its center is the whole group.
Since DihedralGroup 1 is cyclic, its center is also the whole group.
The center of DihedralGroup 0 is trivial, and does not include sr 0.

You should be able to prove the theorem assuming 3 ≤ n.

Thanks for your advice, that was my oversight.

[Yakov Pechersky]

Here is how I got the all-goal simp only: I did a simp? [Set.mem_center_iff] on both subgoals and then used the union:

  rintro (⟨k⟩|⟨k⟩)
  · simp? [Set.mem_center_iff] -- Try this: simp only [Set.mem_center_iff, Set.mem_insert_iff, Set.mem_singleton_iff, r.injEq]
  · simp? [Set.mem_center_iff] -- simp only [Set.mem_center_iff, Set.mem_insert_iff, Set.mem_singleton_iff, reduceCtorEq, or_false]