English
If n is odd, there is a bijective correspondence between commuting pairs in DihedralGroup n and a direct sum of four copies of ZMod n (three copies plus a pair).
Русский
Если n нечетно, существует биекция между парами, которые commute в DihedralGroup n, и модульными компонентами ZMod n в составе трех копий плюс ZMod n × ZMod n.
LaTeX
$${(p,q) ∈ DihedralGroup(n) × DihedralGroup(n) : Commute(p,q)} ≃ ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n$$
Lean4
/-- 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. -/
@[simps]
def oddCommuteEquiv (hn : Odd n) :
{ p : DihedralGroup n × DihedralGroup n // Commute p.1 p.2 } ≃ ZMod n ⊕ ZMod n ⊕ ZMod n ⊕ ZMod n × ZMod n :=
let u := ZMod.unitOfCoprime 2 (Nat.prime_two.coprime_iff_not_dvd.mpr hn.not_two_dvd_nat)
have hu : ∀ a : ZMod n, a + a = 0 ↔ a = 0 := fun _ => ZMod.add_self_eq_zero_iff_eq_zero hn
{ toFun := fun
| ⟨⟨sr i, r _⟩, _⟩ => Sum.inl i
| ⟨⟨r _, sr j⟩, _⟩ => Sum.inr (Sum.inl j)
| ⟨⟨sr i, sr j⟩, _⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
| ⟨⟨r i, r j⟩, _⟩ => Sum.inr (Sum.inr (Sum.inr ⟨i, j⟩))
invFun := fun
| .inl i => ⟨⟨sr i, r 0⟩, congrArg sr ((add_zero i).trans (sub_zero i).symm)⟩
| .inr (.inl j) => ⟨⟨r 0, sr j⟩, congrArg sr ((sub_zero j).trans (add_zero j).symm)⟩
| .inr (.inr (.inl k)) => ⟨⟨sr (u⁻¹ * k), sr (u⁻¹ * k)⟩, rfl⟩
| .inr (.inr (.inr ⟨i, j⟩)) => ⟨⟨r i, r j⟩, congrArg r (add_comm i j)⟩
left_inv := fun
| ⟨⟨r _, r _⟩, _⟩ => rfl
| ⟨⟨r i, sr j⟩, h⟩ => by
simpa [-r_zero, sub_eq_add_neg, neg_eq_iff_add_eq_zero, hu, eq_comm (a := i) (b := 0)] using h.eq
| ⟨⟨sr i, r j⟩, h⟩ => by
simpa [-r_zero, sub_eq_add_neg, eq_neg_iff_add_eq_zero, hu, eq_comm (a := j) (b := 0)] using h.eq
| ⟨⟨sr i, sr j⟩, h⟩ => by
replace h := r.inj h
rw [← neg_sub, neg_eq_iff_add_eq_zero, hu, sub_eq_zero] at h
rw [Subtype.ext_iff, Prod.ext_iff, sr.injEq, sr.injEq, h, and_self, ← two_mul]
exact u.inv_mul_cancel_left j
right_inv := fun
| .inl _ => rfl
| .inr (.inl _) => rfl
| .inr (.inr (.inl k)) => congrArg (Sum.inr ∘ Sum.inr ∘ Sum.inl) <| two_mul (u⁻¹ * k) ▸ u.mul_inv_cancel_left k
| .inr (.inr (.inr ⟨_, _⟩)) => rfl }
