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 ฯ†.

source
๐Ÿ”น coverage
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 ฯ†.

Instances For
    source
    ๐Ÿ”ธ coverage
    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โปยน.

    Instances For
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem MonoidHom.commutatorMap_apply {G : Type u_2} (ฯ† : G โ†’ G) [Div G] (g : G) :
      commutatorMap ฯ† g = g / ฯ† g
      source
      ๐Ÿ“ coverage
      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 โ‡‘ฯ†)
      source
      ๐Ÿ“ coverage
      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 โ‡‘ฯ†)
      source
      ๐Ÿ“ coverage
      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
      source
      ๐Ÿ“ coverage
      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โปยน
      source
      ๐Ÿ“ coverage
      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โปยน
      source
      ๐Ÿ“ coverage
      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
      source
      ๐Ÿ”ธ coverage
      @[implicit_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.

      Instances For
        source
        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
        source
        ๐Ÿ“ coverage
        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)
        source
        ๐Ÿ“ coverage
        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)