The dihedral groups: an enumeration, a recognition criterion, and the rotation subgroup

For n ≠ 0, DihedralGroup n is finite, but Fintype alone does not hand back a list of its elements, since Finset.toList is noncomputable. This file writes that list down, and evaluates DihedralGroup.exponent — which computes the exponent of DihedralGroup n as lcm n 2 — at the two orders the worked examples of the Burnside--Dixon--Schneider character-table algorithm are run on.

It then proves the recognition criterion: a group generated by two involutions, neither of them the identity, is a dihedral group, of order twice the order of their product. Every rank-two reflection group is presented to us in that shape, and this is what identifies it.

Finally it names the rotation subgroup. It is presented as the kernel of the reflection parity, so that it is normal of index 2; the defining dihedral relation is then recorded as TauCeti.conj_eq_inv_of_notMem_dihedralRotations, that conjugation by anything outside it inverts every rotation. Its cyclic coordinate is TauCeti.dihedralRotationsMulEquiv; the characters of the rotation subgroup that coordinate names are in TauCeti.GroupTheory.SpecificGroups.Dihedral.Character. The other subgroup the dihedral relation distinguishes, the two-element subgroup {1, sr i} generated by a single reflection, is described last: it is nontrivial, and proper except in DihedralGroup 1. The two subgroups are complementary at every degree, finite or not, which is the semidirect decomposition DihedralGroup n = C_n ⋊ C₂.

Main definitions

• TauCeti.dihedralElements: a computable enumeration of DihedralGroup n.
• TauCeti.dihedralHom: the homomorphism DihedralGroup n →* M attached to two involutions in a monoid whose product satisfies (s * t) ^ n = 1.
• TauCeti.dihedralGroupMulEquiv: that homomorphism as an isomorphism, when the two involutions generate G and neither is the identity.
• TauCeti.dihedralReflectionParity, TauCeti.dihedralRotations: the reflection parity and the rotation subgroup it cuts out, with TauCeti.dihedralRotationsMulEquiv its cyclic coordinate.

Main results

• TauCeti.mem_dihedralElements: that enumeration exhausts the group.
• TauCeti.exponent_dihedralGroup_three: DihedralGroup 3, of order 6, has exponent 6.
• TauCeti.exponent_dihedralGroup_four: DihedralGroup 4, of order 8, has exponent 4.
• TauCeti.range_dihedralHom: the image of the homomorphism is the subgroup generated by the two involutions.
• TauCeti.dihedralHom_injective: when the involutions are not the identity and their product has exact order n, the homomorphism is injective.
• TauCeti.dihedralHom_bijective and TauCeti.nonempty_dihedralGroup_mulEquiv: a group generated by two involutions other than the identity is the dihedral group of order twice the order of their product.
• TauCeti.index_dihedralRotations and TauCeti.card_dihedralRotations: the rotation subgroup has index 2 and order n.
• TauCeti.mem_zpowers_dihedralSr_iff: the subgroup generated by a reflection is the two-element subgroup {1, sr i}, with TauCeti.dihedralSr_ne_one and TauCeti.zpowers_dihedralSr_ne_top reading off that it is nontrivial, and proper except in DihedralGroup 1.
• TauCeti.isComplement'_dihedralRotations_zpowers_sr: the rotation subgroup and the subgroup generated by a reflection are complementary, at every degree, so DihedralGroup n = C_n ⋊ C₂.
• TauCeti.conj_eq_inv_of_notMem_dihedralRotations and TauCeti.conjNormal_eq_inv_of_notMem_dihedralRotations: conjugation by a reflection inverts every rotation, in the ambient group and inside the rotation subgroup.

def TauCeti.dihedralElements (n : ℕ) : List (DihedralGroup n)

The rotations r 0, …, r (n-1) of DihedralGroup n, each followed by the corresponding reflection. For n ≠ 0 this lists all 2 * n elements of the group, which is TauCeti.mem_dihedralElements. The body is exposed because a kernel computation over the group — such as the class data of TauCeti.dihedralClassData — has to reduce it.

Equations

• TauCeti.dihedralElements n = List.flatMap (fun (i : ℕ) => [DihedralGroup.r ↑i, DihedralGroup.sr ↑i]) (List.range n)

theorem TauCeti.mem_dihedralElements {n : ℕ} [NeZero n] (g : DihedralGroup n) : g ∈ dihedralElements n

The enumeration TauCeti.dihedralElements exhausts the dihedral group.

@[simp]

theorem TauCeti.exponent_dihedralGroup_three : Monoid.exponent (DihedralGroup 3) = 6

The dihedral group of order 6, the symmetric group on three letters, has exponent 6.

@[simp]

theorem TauCeti.exponent_dihedralGroup_four : Monoid.exponent (DihedralGroup 4) = 4

The dihedral group of order 8 has exponent 4.

Recognizing a dihedral group

A group generated by two involutions s and t, neither of them the identity, is dihedral: its rotation subgroup is generated by c = s * t, and its reflections are the elements s * c ^ k. Turning that into an isomorphism means indexing the powers of c by ZMod n, where n is the order of c; the index i is read as the integer ZMod.cast i, and TauCeti.dihedralHom is the resulting homomorphism. Taking that representative in ℤ rather than in ℕ costs nothing and covers the modulus n = 0, where ZMod 0 is ℤ and an element of order 0 is one of infinite order: the criterion then recognizes the infinite dihedral group.

Constructing the homomorphism itself only needs c ^ n = 1. Its image is the subgroup generated by the involutions even when the order of c is smaller than n; exact order is needed for injectivity. At n = 0 the power relation is automatic, so any pair of involutions defines a map out of the infinite dihedral group.

The work is in injectivity. On the rotations it is the definition of the order of c. On the reflections it is the observation that s * c ^ k = 1 puts s inside the abelian subgroup generated by c, so that s both inverts and centralizes c; then c is its own inverse, and the parity of k makes s or t the identity. Both hypotheses s ≠ 1 and t ≠ 1 are therefore needed: for s = 1 the group is generated by the single involution t while orderOf (s * t) = 2, so it is not the dihedral group of order 4.

def TauCeti.dihedralHom {M : Type u_1} [Monoid M] {n : ℕ} {s t : M} (hs : s * s = 1) (ht : t * t = 1) (hn : (s * t) ^ n = 1) : DihedralGroup n →* M

The homomorphism out of the dihedral group determined by two involutions in a monoid whose product satisfies (s * t) ^ n = 1. The involutions are units, so rotations can be evaluated at integer representatives even when n = 0. The formulas are TauCeti.dihedralHom_r_units and TauCeti.dihedralHom_sr_units; for division monoids they simplify to TauCeti.dihedralHom_r and TauCeti.dihedralHom_sr. At n = 0 the power relation is automatic, so the map exists for every pair of involutions, regardless of the order of their product.

Equations

• TauCeti.dihedralHom hs ht hn = (Units.coeHom M).comp (TauCeti.dihedralGroupHom✝ ⋯ ⋯ ⋯)

@[simp]

theorem TauCeti.dihedralHom_r_units {M : Type u_1} [Monoid M] {n : ℕ} {s t : M} (hs : s * s = 1) (ht : t * t = 1) (hn : (s * t) ^ n = 1) (i : ZMod n) : (dihedralHom hs ht hn) (DihedralGroup.r i) = ↑(({ val := s, inv := s, val_inv := hs, inv_val := hs } * { val := t, inv := t, val_inv := ht, inv_val := ht }) ^ i.cast)

A rotation maps to the corresponding integer power of the product of the two units.

@[simp]

theorem TauCeti.dihedralHom_sr_units {M : Type u_1} [Monoid M] {n : ℕ} {s t : M} (hs : s * s = 1) (ht : t * t = 1) (hn : (s * t) ^ n = 1) (i : ZMod n) : (dihedralHom hs ht hn) (DihedralGroup.sr i) = s * ↑(({ val := s, inv := s, val_inv := hs, inv_val := hs } * { val := t, inv := t, val_inv := ht, inv_val := ht }) ^ i.cast)

A reflection maps to the first involution times the corresponding power of the unit product.

theorem TauCeti.dihedralHom_injective {M : Type u_1} [Monoid M] {n : ℕ} {s t : M} (hs : s * s = 1) (ht : t * t = 1) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hn : orderOf (s * t) = n) : Function.Injective ⇑(dihedralHom hs ht ⋯)

Two involutions other than the identity embed the dihedral group in a monoid. If neither of s and t is the identity, then TauCeti.dihedralHom is injective, where n is the order of s * t.

theorem TauCeti.dihedralHom_r {G : Type u_1} [DivisionMonoid G] {n : ℕ} {s t : G} (hs : s * s = 1) (ht : t * t = 1) (hn : (s * t) ^ n = 1) (i : ZMod n) : (dihedralHom hs ht hn) (DihedralGroup.r i) = (s * t) ^ i.cast

TauCeti.dihedralHom sends the rotation r i to the power (s * t) ^ i in a division monoid.

theorem TauCeti.dihedralHom_sr {G : Type u_1} [DivisionMonoid G] {n : ℕ} {s t : G} (hs : s * s = 1) (ht : t * t = 1) (hn : (s * t) ^ n = 1) (i : ZMod n) : (dihedralHom hs ht hn) (DihedralGroup.sr i) = s * (s * t) ^ i.cast

TauCeti.dihedralHom sends the reflection sr i to s * (s * t) ^ i in a division monoid.

theorem TauCeti.range_dihedralHom {G : Type u_1} [Group G] {n : ℕ} {s t : G} (hs : s * s = 1) (ht : t * t = 1) (hn : (s * t) ^ n = 1) : (dihedralHom hs ht hn).range = Subgroup.closure {s, t}

The image of TauCeti.dihedralHom is the subgroup generated by the two involutions.

theorem TauCeti.dihedralHom_bijective {G : Type u_1} [Group G] {n : ℕ} {s t : G} (hs : s * s = 1) (ht : t * t = 1) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hn : orderOf (s * t) = n) (hgen : Subgroup.closure {s, t} = ⊤) : Function.Bijective ⇑(dihedralHom hs ht ⋯)

A group generated by two involutions other than the identity is dihedral. If the involutions s and t generate G and neither is the identity, then TauCeti.dihedralHom identifies G with the dihedral group of order 2 * n, where n is the order of s * t.

noncomputable def TauCeti.dihedralGroupMulEquiv {G : Type u_1} [Group G] {n : ℕ} {s t : G} (hs : s * s = 1) (ht : t * t = 1) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hn : orderOf (s * t) = n) (hgen : Subgroup.closure {s, t} = ⊤) : DihedralGroup n ≃* G

A group generated by two involutions other than the identity is the dihedral group of order twice the order of their product. The isomorphism is TauCeti.dihedralHom: the rotation r i is the power (s * t) ^ i, and the reflection sr i is s * (s * t) ^ i.

It is what identifies the Weyl group of a rank-two root system in TauCeti.nonempty_dihedralGroup_mulEquiv_weylGroup.

Equations

• TauCeti.dihedralGroupMulEquiv hs ht hs1 ht1 hn hgen = MulEquiv.ofBijective (TauCeti.dihedralHom hs ht ⋯) ⋯

@[simp]

theorem TauCeti.dihedralGroupMulEquiv_apply {G : Type u_1} [Group G] {n : ℕ} {s t : G} (hs : s * s = 1) (ht : t * t = 1) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hn : orderOf (s * t) = n) (hgen : Subgroup.closure {s, t} = ⊤) (x : DihedralGroup n) : (dihedralGroupMulEquiv hs ht hs1 ht1 hn hgen) x = (dihedralHom hs ht ⋯) x

TauCeti.dihedralGroupMulEquiv is TauCeti.dihedralHom.

theorem TauCeti.nonempty_dihedralGroup_mulEquiv {G : Type u_1} [Group G] {n : ℕ} {s t : G} (hs : s * s = 1) (ht : t * t = 1) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hn : orderOf (s * t) = n) (hgen : Subgroup.closure {s, t} = ⊤) : Nonempty (DihedralGroup n ≃* G)

A group generated by two involutions other than the identity is the dihedral group of order twice the order of their product, the existential form of TauCeti.dihedralGroupMulEquiv.

The rotation subgroup

The rotations form a subgroup of index 2, and the cleanest way to get it — together with its normality — is as the kernel of the reflection parity, the homomorphism onto ZMod 2 that records whether an element is a rotation or a reflection. The relation that makes the dihedral group dihedral, s r s⁻¹ = r⁻¹, is then the statement that conjugation by anything outside the rotation subgroup inverts every rotation.

def TauCeti.dihedralReflectionParity (n : ℕ) : DihedralGroup n →* Multiplicative (ZMod 2)

The reflection parity of a dihedral element: 0 on the rotations r i and 1 on the reflections sr i. Written multiplicatively so that it is a MonoidHom whose kernel is the rotation subgroup.

Equations

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

@[simp]

theorem TauCeti.dihedralReflectionParity_r {n : ℕ} (i : ZMod n) : (dihedralReflectionParity n) (DihedralGroup.r i) = 1

@[simp]

theorem TauCeti.dihedralReflectionParity_sr {n : ℕ} (i : ZMod n) : (dihedralReflectionParity n) (DihedralGroup.sr i) = Multiplicative.ofAdd 1

theorem TauCeti.dihedralReflectionParity_surjective (n : ℕ) : Function.Surjective ⇑(dihedralReflectionParity n)

The reflection parity is onto.

def TauCeti.dihedralRotations (n : ℕ) : Subgroup (DihedralGroup n)

The rotation subgroup of DihedralGroup n, the kernel of the reflection parity. It is normal of index 2, and TauCeti.dihedralRotationsMulEquiv identifies it with Multiplicative (ZMod n), so it is cyclic (TauCeti.isCyclic_dihedralRotations) and in particular commutative.

Equations

• TauCeti.dihedralRotations n = (TauCeti.dihedralReflectionParity n).ker

instance TauCeti.dihedralRotations_normal (n : ℕ) : (dihedralRotations n).Normal

@[simp]

theorem TauCeti.mem_dihedralRotations_iff {n : ℕ} {g : DihedralGroup n} : g ∈ dihedralRotations n ↔ ∃ (i : ZMod n), g = DihedralGroup.r i

Membership in the rotation subgroup is being a rotation.

theorem TauCeti.r_mem_dihedralRotations {n : ℕ} (i : ZMod n) : DihedralGroup.r i ∈ dihedralRotations n

A rotation lies in the rotation subgroup. Not a simp lemma: simp already closes this through TauCeti.mem_dihedralRotations_iff; it is kept as the membership proof to hand to the subtype constructor.

theorem TauCeti.sr_notMem_dihedralRotations {n : ℕ} (i : ZMod n) : DihedralGroup.sr i ∉ dihedralRotations n

A reflection does not lie in the rotation subgroup. Not a simp lemma, for the same reason as TauCeti.r_mem_dihedralRotations.

@[simp]

theorem TauCeti.index_dihedralRotations (n : ℕ) : (dihedralRotations n).index = 2

The rotation subgroup has index 2.

instance TauCeti.finiteIndex_dihedralRotations (n : ℕ) : (dihedralRotations n).FiniteIndex

The rotation subgroup has finite index, for every n -- including n = 0, where DihedralGroup n is infinite.

theorem TauCeti.card_dihedralRotations (n : ℕ) : Nat.card ↥(dihedralRotations n) = n

The rotation subgroup has n elements: it has index 2 in a group of order 2 * n. For n = 0 both sides are the junk value 0 that Nat.card takes on an infinite group.

Not a simp lemma: TauCeti.mem_dihedralRotations_iff rewrites the membership predicate inside the coercion, so the left-hand side here is not in simp-normal form.

theorem TauCeti.conj_eq_inv_of_notMem_dihedralRotations {n : ℕ} {s g : DihedralGroup n} (hs : s ∉ dihedralRotations n) (hg : g ∈ dihedralRotations n) : s * g * s⁻¹ = g⁻¹

Conjugation by a reflection inverts every rotation. This is the defining dihedral relation s r s⁻¹ = r⁻¹, stated for the subgroup rather than for a chosen generator; it is what makes the conjugate of a linear character of the rotation subgroup its inverse.

@[simp]

theorem TauCeti.conjNormal_eq_inv_of_notMem_dihedralRotations {n : ℕ} {s : DihedralGroup n} (hs : s ∉ dihedralRotations n) (x : ↥(dihedralRotations n)) : (MulAut.conjNormal s) x = x⁻¹

Conjugation by a reflection inverts every rotation, inside the rotation subgroup: this is TauCeti.conj_eq_inv_of_notMem_dihedralRotations read as an equality in dihedralRotations n, where the conjugation action of the ambient group on a normal subgroup lives.

def TauCeti.dihedralRotationsMulEquiv (n : ℕ) : ↥(dihedralRotations n) ≃* Multiplicative (ZMod n)

The rotation subgroup is ZMod n written multiplicatively: the rotation r i has coordinate i. This is the canonical coordinate on TauCeti.dihedralRotations, and it is what lets a character of the rotation subgroup be named by a single n-th root of unity.

Equations

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

@[simp]

theorem TauCeti.dihedralRotationsMulEquiv_r {n : ℕ} (i : ZMod n) : (dihedralRotationsMulEquiv n) ⟨DihedralGroup.r i, ⋯⟩ = Multiplicative.ofAdd i

@[simp]

theorem TauCeti.coe_dihedralRotationsMulEquiv_symm {n : ℕ} (i : Multiplicative (ZMod n)) : ↑((dihedralRotationsMulEquiv n).symm i) = DihedralGroup.r (Multiplicative.toAdd i)

instance TauCeti.isCyclic_dihedralRotations (n : ℕ) : IsCyclic ↥(dihedralRotations n)

The rotation subgroup is cyclic, Multiplicative (ZMod n) being so; in particular it is commutative.

The subgroup generated by a reflection

@[simp]

theorem TauCeti.dihedralSr_ne_one {n : ℕ} (i : ZMod n) : DihedralGroup.sr i ≠ 1

A reflection is not the identity.

@[simp]

theorem TauCeti.mem_zpowers_dihedralSr_iff {n : ℕ} {i : ZMod n} {g : DihedralGroup n} : g ∈ Subgroup.zpowers (DihedralGroup.sr i) ↔ g = 1 ∨ g = DihedralGroup.sr i

The subgroup generated by a reflection is {1, sr i}.

theorem TauCeti.zpowers_dihedralSr_ne_top {n : ℕ} (hn : n ≠ 1) (i : ZMod n) : Subgroup.zpowers (DihedralGroup.sr i) ≠ ⊤

The subgroup generated by a reflection is proper, except in DihedralGroup 1, the group of order two that a single reflection exhausts.

theorem TauCeti.eq_one_of_mem_dihedralRotations_of_mem_zpowers_sr {n : ℕ} {i : ZMod n} {g : DihedralGroup n} (hg : g ∈ dihedralRotations n) (hgs : g ∈ Subgroup.zpowers (DihedralGroup.sr i)) : g = 1

A rotation lying in the subgroup generated by a reflection is the identity: the two subgroups meet only there.

theorem TauCeti.isComplement'_dihedralRotations_zpowers_sr {n : ℕ} (i : ZMod n) : (dihedralRotations n).IsComplement' (Subgroup.zpowers (DihedralGroup.sr i))

The rotation subgroup and a reflection subgroup are complementary at every degree, so DihedralGroup n = C_n ⋊ C₂. This holds for every n, including n = 0, where it presents the infinite dihedral group as ℤ ⋊ C₂.