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_2} (φ : 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_2} (φ : 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_2} (φ : G → G) [Div G] (g : G) : commutatorMap φ g = g / φ g

theorem MonoidHom.FixedPointFree.commutatorMap_injective {F : Type u_1} {G : Type u_2} [Group G] [FunLike F G G] [MonoidHomClass F G G] {φ : F} (hφ : FixedPointFree ⇑φ) : Function.Injective (commutatorMap ⇑φ)

theorem MonoidHom.FixedPointFree.commutatorMap_surjective {F : Type u_1} {G : Type u_2} [Group G] [FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G] (hφ : FixedPointFree ⇑φ) : Function.Surjective (commutatorMap ⇑φ)

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

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

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

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

@[instance_reducible]

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

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

Equations

• hφ.commGroupOfInvolutive h2 = { toGroup := inst✝³, mul_comm := ⋯ }

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

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

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