Dihedral Groups

We define the dihedral groups DihedralGroup n, with elements r i and sr i for i : ZMod n.

For n ≠ 0, DihedralGroup n represents the symmetry group of the regular n-gon. r i represents the rotations of the n-gon by 2πi/n, and sr i represents the reflections of the n-gon. DihedralGroup 0 corresponds to the infinite dihedral group.

inductive DihedralGroup (n : ℕ) : Type

For n ≠ 0, DihedralGroup n represents the symmetry group of the regular n-gon. r i represents the rotations of the n-gon by 2πi/n, and sr i represents the reflections of the n-gon. DihedralGroup 0 corresponds to the infinite dihedral group.

• r {n : ℕ} : ZMod n → DihedralGroup n
• sr {n : ℕ} : ZMod n → DihedralGroup n

@[implicit_reducible]

instance instDecidableEqDihedralGroup {n✝ : ℕ} : DecidableEq (DihedralGroup n✝)

def instDecidableEqDihedralGroup.decEq {n✝ : ℕ} (x✝ x✝¹ : DihedralGroup n✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance DihedralGroup.instInhabited {n : ℕ} : Inhabited (DihedralGroup n)

@[implicit_reducible]

instance DihedralGroup.instGroup {n : ℕ} : Group (DihedralGroup n)

The group structure on DihedralGroup n.

@[simp]

theorem DihedralGroup.r_mul_r {n : ℕ} (i j : ZMod n) : r i * r j = r (i + j)

@[simp]

theorem DihedralGroup.r_mul_sr {n : ℕ} (i j : ZMod n) : r i * sr j = sr (j - i)

@[simp]

theorem DihedralGroup.sr_mul_r {n : ℕ} (i j : ZMod n) : sr i * r j = sr (i + j)

@[simp]

theorem DihedralGroup.sr_mul_sr {n : ℕ} (i j : ZMod n) : sr i * sr j = r (j - i)

@[simp]

theorem DihedralGroup.inv_r {n : ℕ} (i : ZMod n) : (r i)⁻¹ = r (-i)

@[simp]

theorem DihedralGroup.inv_sr {n : ℕ} (i : ZMod n) : (sr i)⁻¹ = sr i

@[simp]

theorem DihedralGroup.r_zero {n : ℕ} : r 0 = 1

theorem DihedralGroup.one_def {n : ℕ} : 1 = r 0

@[simp]

theorem DihedralGroup.r_pow {n : ℕ} (i : ZMod n) (k : ℕ) : r i ^ k = r (i * ↑k)

@[simp]

theorem DihedralGroup.r_zpow {n : ℕ} (i : ZMod n) (k : ℤ) : r i ^ k = r (i * ↑k)

def DihedralGroup.equivSum {n : ℕ} : DihedralGroup n ≃ ZMod n ⊕ ZMod n

The equivalence between the dihedral group and the sum of ZMods.

@[simp]

theorem DihedralGroup.equivSum_symm_apply {n : ℕ} (x✝ : ZMod n ⊕ ZMod n) : equivSum.symm x✝ = match x✝ with | Sum.inl j => r j | Sum.inr j => sr j

@[simp]

theorem DihedralGroup.equivSum_apply {n : ℕ} (x✝ : DihedralGroup n) : equivSum x✝ = match x✝ with | r j => Sum.inl j | sr j => Sum.inr j

@[implicit_reducible]

instance DihedralGroup.instFintypeOfNeZeroNat {n : ℕ} [NeZero n] : Fintype (DihedralGroup n)

If 0 < n, then DihedralGroup n is a finite group.

instance DihedralGroup.instInfiniteOfNatNat : Infinite (DihedralGroup 0)

instance DihedralGroup.instNontrivial {n : ℕ} : Nontrivial (DihedralGroup n)

theorem DihedralGroup.card {n : ℕ} [NeZero n] : Fintype.card (DihedralGroup n) = 2 * n

If 0 < n, then DihedralGroup n has 2n elements.

theorem DihedralGroup.nat_card {n : ℕ} : Nat.card (DihedralGroup n) = 2 * n

theorem DihedralGroup.r_one_pow {n : ℕ} (k : ℕ) : r 1 ^ k = r ↑k

theorem DihedralGroup.r_one_zpow {n : ℕ} (k : ℤ) : r 1 ^ k = r ↑k

theorem DihedralGroup.r_one_pow_n {n : ℕ} : r 1 ^ n = 1

theorem DihedralGroup.sr_mul_self {n : ℕ} (i : ZMod n) : sr i * sr i = 1

@[simp]

theorem DihedralGroup.orderOf_sr {n : ℕ} (i : ZMod n) : orderOf (sr i) = 2

sr i has order 2.

@[simp]

theorem DihedralGroup.orderOf_r_one {n : ℕ} : orderOf (r 1) = n

r 1 has order n.

theorem DihedralGroup.orderOf_r {n : ℕ} [NeZero n] (i : ZMod n) : orderOf (r i) = n / n.gcd i.val

If 0 < n, then r i has order n / gcd n i.

theorem DihedralGroup.exponent {n : ℕ} : Monoid.exponent (DihedralGroup n) = lcm n 2

theorem DihedralGroup.not_commutative {n : ℕ} : n ≠ 1 → n ≠ 2 → ¬Std.Commutative fun (x y : DihedralGroup n) => x * y

theorem DihedralGroup.commutative_iff {n : ℕ} : (Std.Commutative fun (x y : DihedralGroup n) => x * y) ↔ n = 1 ∨ n = 2

theorem DihedralGroup.not_isCyclic {n : ℕ} (h1 : n ≠ 1) : ¬IsCyclic (DihedralGroup n)

theorem DihedralGroup.isCyclic_iff {n : ℕ} : IsCyclic (DihedralGroup n) ↔ n = 1

instance DihedralGroup.instIsKleinFourOfNatNat : IsKleinFour (DihedralGroup 2)

def DihedralGroup.oddCommuteEquiv {n : ℕ} (hn : Odd n) : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } ≃ ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n

If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs (represented as $n + n + n + n*n$) of commuting elements.

@[simp]

theorem DihedralGroup.oddCommuteEquiv_symm_apply {n : ℕ} (hn : Odd n) (x✝ : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n) : (oddCommuteEquiv hn).symm x✝ = match x✝ with | Sum.inl i => ⟨(sr i, r 0), ⋯⟩ | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩ | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)), ⋯⟩ | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩

@[simp]

theorem DihedralGroup.oddCommuteEquiv_apply {n : ℕ} (hn : Odd n) (x✝ : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }) : (oddCommuteEquiv hn) x✝ = match x✝ with | ⟨(sr i, r a), property⟩ => Sum.inl i | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j) | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j))) | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j)))

theorem DihedralGroup.card_commute_odd {n : ℕ} (hn : Odd n) : Nat.card { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } = n * (n + 3)

If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs of commuting elements.

theorem DihedralGroup.card_conjClasses_odd {n : ℕ} (hn : Odd n) : Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2

theorem DihedralGroup.center_eq_bot_of_odd_ne_one {n : ℕ} (hodd : Odd n) (hne1 : n ≠ 1) : Subgroup.center (DihedralGroup n) = ⊥