Documentation

Mathlib.GroupTheory.FixedPointFree

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} (φ : GG) [One G] :

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

Equations
Instances For
    def MonoidHom.commutatorMap {G : Type u_1} (φ : GG) [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
    Instances For
      @[simp]
      theorem MonoidHom.commutatorMap_apply {G : Type u_1} (φ : GG) [Div G] (g : G) :
      theorem MonoidHom.FixedPointFree.prod_pow_eq_one {G : Type u_1} [Group G] {φ : G →* G} [Finite G] (hφ : MonoidHom.FixedPointFree φ) {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} [Finite G] (hφ : MonoidHom.FixedPointFree φ) (h2 : (⇑φ)^[2] = id) :
      φ = fun (x : G) => x⁻¹
      theorem MonoidHom.FixedPointFree.coe_eq_inv_of_involutive {G : Type u_1} [Group G] {φ : G →* G} [Finite G] (hφ : MonoidHom.FixedPointFree φ) (h2 : Function.Involutive φ) :
      φ = fun (x : G) => x⁻¹
      theorem MonoidHom.FixedPointFree.commute_all_of_involutive {G : Type u_1} [Group G] {φ : G →* G} [Finite G] (hφ : MonoidHom.FixedPointFree φ) (h2 : Function.Involutive φ) (g : G) (h : G) :

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

      Equations
      Instances For