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

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

Equations

• instDecidableEqDihedralGroup = decEqDihedralGroup✝

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

Equations

• DihedralGroup.instInhabitedDihedralGroup = { default := DihedralGroup.one }

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

The group structure on DihedralGroup n.

Equations

• DihedralGroup.instGroupDihedralGroup = Group.mk (_ : ∀ (a : DihedralGroup n), a⁻¹ * a = 1)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• DihedralGroup.instFintypeDihedralGroup = Fintype.ofEquiv (ZMod n ⊕ ZMod n) DihedralGroup.fintypeHelper

instance DihedralGroup.instInfiniteDihedralGroupOfNatNatInstOfNatNat : Infinite (DihedralGroup 0)

Equations

• DihedralGroup.instInfiniteDihedralGroupOfNatNatInstOfNatNat = (_ : Infinite (DihedralGroup 0))

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

Equations

• (_ : Nontrivial (DihedralGroup 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

@[simp]

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

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

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

@[simp]

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

If 0 < n, then sr i has order 2.

@[simp]

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

If 0 < n, then r 1 has order n.

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

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

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

@[simp]

theorem DihedralGroup.OddCommuteEquiv_symm_apply {n : ℕ} (hn : Odd n) : ∀ (x : ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n), (DihedralGroup.OddCommuteEquiv hn).symm x = match x with | Sum.inl i => { val := (DihedralGroup.sr i, DihedralGroup.r 0), property := (_ : DihedralGroup.sr (i + 0) = DihedralGroup.sr (i - 0)) } | Sum.inr (Sum.inl j) => { val := (DihedralGroup.r 0, DihedralGroup.sr j), property := (_ : DihedralGroup.sr (j - 0) = DihedralGroup.sr (j + 0)) } | Sum.inr (Sum.inr (Sum.inl k)) => { val := (DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k)), property := (_ : (DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k)).1 * (DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k)).2 = (DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k)).1 * (DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 (_ : Nat.Coprime 2 n))⁻¹ * k)).2) } | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (DihedralGroup.r i, DihedralGroup.r j), property := (_ : DihedralGroup.r (i + j) = DihedralGroup.r (j + i)) }

@[simp]

theorem DihedralGroup.OddCommuteEquiv_apply {n : ℕ} (hn : Odd n) : ∀ (x : { p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 }), (DihedralGroup.OddCommuteEquiv hn) x = match x with | { val := (DihedralGroup.sr i, DihedralGroup.r a), property := property } => Sum.inl i | { val := (DihedralGroup.r a, DihedralGroup.sr j), property := property } => Sum.inr (Sum.inl j) | { val := (DihedralGroup.sr i, DihedralGroup.sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j))) | { val := (DihedralGroup.r i, DihedralGroup.r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j)))

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.

Equations

• One or more equations did not get rendered due to their size.

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