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

Equations
    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โปยน.

      Equations
        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
          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
            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)