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 φ.

def MonoidHom.FixedPointFree {G : Type u_1} (φ : G → G) [One G] : Prop

A function φ : G → G is fixed-point-free if 1 : G is the only fixed point of φ.

Equations

• MonoidHom.FixedPointFree φ = ∀ (g : G), φ g = g → g = 1

def MonoidHom.commutatorMap {G : Type u_1} (φ : G → G) [Div G] (g : G) : G

The commutator map g ↦ g / φ g. If φ g = h * g * h⁻¹, then g / φ g is exactly the commutator [g, h] = g * h * g⁻¹ * h⁻¹.

Equations

• MonoidHom.commutatorMap φ g = g / φ g

@[simp]

theorem MonoidHom.commutatorMap_apply {G : Type u_1} (φ : G → G) [Div G] (g : G) : MonoidHom.commutatorMap φ g = g / φ g

theorem MonoidHom.FixedPointFree.commutatorMap_injective {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) : Function.Injective (MonoidHom.commutatorMap ⇑φ)

theorem MonoidHom.FixedPointFree.commutatorMap_surjective {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] : Function.Surjective (MonoidHom.commutatorMap ⇑φ)

theorem MonoidHom.FixedPointFree.prod_pow_eq_one {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] {n : ℕ} (hn : (⇑φ)^[n] = id) (g : G) : (List.map (fun (k : ℕ) => (⇑φ)^[k] g) (List.range n)).prod = 1

theorem MonoidHom.FixedPointFree.coe_eq_inv_of_sq_eq_one {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] (h2 : (⇑φ)^[2] = id) : ⇑φ = fun (x : G) => x⁻¹

theorem MonoidHom.FixedPointFree.coe_eq_inv_of_involutive {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] (h2 : Function.Involutive ⇑φ) : ⇑φ = fun (x : G) => x⁻¹

theorem MonoidHom.FixedPointFree.commute_all_of_involutive {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] (h2 : Function.Involutive ⇑φ) (g : G) (h : G) : Commute g h

def MonoidHom.FixedPointFree.commGroupOfInvolutive {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] (h2 : Function.Involutive ⇑φ) : CommGroup G

If a finite group admits a fixed-point-free involution, then it is commutative.

Equations

• hφ.commGroupOfInvolutive h2 = CommGroup.mk ⋯

theorem MonoidHom.FixedPointFree.orderOf_ne_two_of_involutive {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] (h2 : Function.Involutive ⇑φ) (g : G) : orderOf g ≠ 2

theorem MonoidHom.FixedPointFree.odd_card_of_involutive {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] (h2 : Function.Involutive ⇑φ) : Odd (Nat.card G)

theorem MonoidHom.FixedPointFree.odd_orderOf_of_involutive {G : Type u_1} [Group G] {φ : G →* G} (hφ : MonoidHom.FixedPointFree ⇑φ) [Finite G] (h2 : Function.Involutive ⇑φ) (g : G) : Odd (orderOf g)