feat(GroupTheory/FixedPointFree): New file (#11091)

This PR adds a new file containing the definition of fixed-point-free automorphisms and some basic properties.

Mathlib.lean

@@ -2335,6 +2335,7 @@ import Mathlib.GroupTheory.EckmannHilton
 import Mathlib.GroupTheory.Exponent
 import Mathlib.GroupTheory.FiniteAbelian
 import Mathlib.GroupTheory.Finiteness
+import Mathlib.GroupTheory.FixedPointFree
 import Mathlib.GroupTheory.FreeAbelianGroup
 import Mathlib.GroupTheory.FreeAbelianGroupFinsupp
 import Mathlib.GroupTheory.FreeGroup.Basic

Mathlib/Data/List/BigOperators/Basic.lean

@@ -447,6 +447,14 @@ theorem prod_drop_succ :
 #align list.prod_drop_succ List.prod_drop_succ
 #align list.sum_drop_succ List.sum_drop_succ
 
+/-- Cancellation of a telescoping product. -/
+@[to_additive "Cancellation of a telescoping sum."]
+theorem prod_range_div' (n : ℕ) (f : ℕ → G) :
+    ((range n).map fun k ↦ f k / f (k + 1)).prod = f 0 / f n := by
+  induction' n with n h
+  · exact (div_self' (f 0)).symm
+  · rw [range_succ, map_append, map_singleton, prod_append, prod_singleton, h, div_mul_div_cancel']
+
 end Group
 
 section CommGroup
@@ -461,6 +469,13 @@ theorem prod_inv : ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).prod
 #align list.prod_inv List.prod_inv
 #align list.sum_neg List.sum_neg
 
+/-- Cancellation of a telescoping product. -/
+@[to_additive "Cancellation of a telescoping sum."]
+theorem prod_range_div (n : ℕ) (f : ℕ → G) :
+    ((range n).map fun k ↦ f (k + 1) / f k).prod = f n / f 0 := by
+  have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div
+  rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']
+
 /-- Alternative version of `List.prod_set` when the list is over a group -/
 @[to_additive "Alternative version of `List.sum_set` when the list is over a group"]
 theorem prod_set' (L : List G) (n : ℕ) (a : G) :

Mathlib/GroupTheory/FixedPointFree.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2024 Thomas Browning. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning
+-/
+import Mathlib.GroupTheory.Perm.Cycle.Type
+import Mathlib.Algebra.GroupPower.IterateHom
+import Mathlib.GroupTheory.OrderOfElement
+
+/-!
+# Fixed-point-free automorphisms
+
+This file defines fixed-point-free automorphisms and proves some basic properties.
+
+An automorphism `φ` of a group `G` is fixed-point-free if `1 : G` is the only fixed point of `φ`.
+-/
+
+namespace MonoidHom
+
+variable {G : Type*}
+
+section Definitions
+
+variable (φ : G → G)
+
+/-- A function `φ : G → G` is fixed-point-free if `1 : G` is the only fixed point of `φ`. -/
+def FixedPointFree [One G] := ∀ g, φ g = g → g = 1
+
+/-- The commutator map `g ↦ g / φ g`. If `φ g = h * g * h⁻¹`, then `g / φ g` is exactly the
+  commutator `[g, h] = g * h * g⁻¹ * h⁻¹`. -/
+def commutatorMap [Div G] (g : G) := g / φ g
+
+@[simp] theorem commutatorMap_apply [Div G] (g : G) : commutatorMap φ g = g / φ g := rfl
+
+end Definitions
+
+namespace FixedPointFree
+
+-- todo: refactor Mathlib/Algebra/GroupPower/IterateHom to generalize φ to MonoidHomClass
+variable [Group G] {φ : G →* G} (hφ : FixedPointFree φ)
+
+theorem commutatorMap_injective : Function.Injective (commutatorMap φ) := by
+  refine' fun x y h ↦ inv_mul_eq_one.mp <| hφ _ _
+  rwa [map_mul, map_inv, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← eq_div_iff_mul_eq', ← division_def]
+
+variable [Finite G]
+
+theorem commutatorMap_surjective : Function.Surjective (commutatorMap φ) :=
+  Finite.surjective_of_injective hφ.commutatorMap_injective
+
+theorem prod_pow_eq_one {n : ℕ} (hn : φ^[n] = _root_.id) (g : G) :
+    ((List.range n).map (fun k ↦ φ^[k] g)).prod = 1 := by
+  obtain ⟨g, rfl⟩ := commutatorMap_surjective hφ g
+  simp only [commutatorMap_apply, iterate_map_div, ← Function.iterate_succ_apply]
+  rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']
+
+theorem coe_eq_inv_of_sq_eq_one (h2 : φ^[2] = _root_.id) : ⇑φ = (·⁻¹) := by
+  ext g
+  have key : 1 * g * φ g = 1 := hφ.prod_pow_eq_one h2 g
+  rwa [one_mul, ← inv_eq_iff_mul_eq_one, eq_comm] at key
+
+section Involutive
+
+variable (h2 : Function.Involutive φ)
+
+theorem coe_eq_inv_of_involutive : ⇑φ = (·⁻¹) :=
+  coe_eq_inv_of_sq_eq_one hφ  (funext h2)
+
+theorem commute_all_of_involutive (g h : G) : Commute g h := by
+  have key := map_mul φ g h
+  rwa [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_eq_inv, mul_inv_rev, inv_inv, inv_inv] at key
+
+/-- If a finite group admits a fixed-point-free involution, then it is commutative. -/
+def commGroupOfInvolutive : CommGroup G := .mk (hφ.commute_all_of_involutive h2)
+
+theorem orderOf_ne_two_of_involutive (g : G) : orderOf g ≠ 2 := by
+  intro hg
+  have key : φ g = g := by
+    rw [hφ.coe_eq_inv_of_involutive h2, inv_eq_iff_mul_eq_one, ← sq, ← hg, pow_orderOf_eq_one]
+  rw [hφ g key, orderOf_one] at hg
+  contradiction
+
+theorem odd_card_of_involutive : Odd (Nat.card G) := by
+  have := Fintype.ofFinite G
+  by_contra h
+  rw [← Nat.even_iff_not_odd, even_iff_two_dvd, Nat.card_eq_fintype_card] at h
+  obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card 2 h
+  exact hφ.orderOf_ne_two_of_involutive h2 g hg
+
+theorem odd_orderOf_of_involutive (g : G) : Odd (orderOf g) :=
+  Odd.of_dvd_nat (hφ.odd_card_of_involutive h2) (orderOf_dvd_natCard g)
+
+end Involutive
+
+end FixedPointFree
+
+end MonoidHom