Documentation

Mathlib.GroupTheory.SpecificGroups.Dihedral

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 : ℕ) :

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

Instances For

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 ⋯

@[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 = ⋯

instance DihedralGroup.instNontrivialDihedralGroup {n : ℕ} :

Nontrivial (DihedralGroup n)

Equations

⋯ = ⋯

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 := ⋯ } | Sum.inr (Sum.inl j) => { val := (DihedralGroup.r 0, DihedralGroup.sr j), property := ⋯ } | Sum.inr (Sum.inr (Sum.inl k)) => { val := (DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k), DihedralGroup.sr (↑(ZMod.unitOfCoprime 2 ⋯)⁻¹ * k)), property := ⋯ } | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (DihedralGroup.r i, DihedralGroup.r j), property := ⋯ }

@[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.

Instances For

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