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 φ
.
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
Instances For
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
Instances For
@[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 ⇑φ)
:
theorem
MonoidHom.FixedPointFree.commutatorMap_surjective
{G : Type u_1}
[Group G]
{φ : G →* G}
[Finite G]
(hφ : MonoidHom.FixedPointFree ⇑φ)
:
theorem
MonoidHom.FixedPointFree.coe_eq_inv_of_involutive
{G : Type u_1}
[Group G]
{φ : G →* G}
[Finite G]
(hφ : MonoidHom.FixedPointFree ⇑φ)
(h2 : Function.Involutive ⇑φ)
:
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)
:
Commute g h
def
MonoidHom.FixedPointFree.commGroupOfInvolutive
{G : Type u_1}
[Group G]
{φ : G →* G}
[Finite G]
(hφ : MonoidHom.FixedPointFree ⇑φ)
(h2 : Function.Involutive ⇑φ)
:
If a finite group admits a fixed-point-free involution, then it is commutative.
Equations
- hφ.commGroupOfInvolutive h2 = CommGroup.mk ⋯
Instances For
theorem
MonoidHom.FixedPointFree.orderOf_ne_two_of_involutive
{G : Type u_1}
[Group G]
{φ : G →* G}
[Finite G]
(hφ : MonoidHom.FixedPointFree ⇑φ)
(h2 : Function.Involutive ⇑φ)
(g : G)
:
theorem
MonoidHom.FixedPointFree.odd_card_of_involutive
{G : Type u_1}
[Group G]
{φ : G →* G}
[Finite G]
(hφ : MonoidHom.FixedPointFree ⇑φ)
(h2 : Function.Involutive ⇑φ)
:
theorem
MonoidHom.FixedPointFree.odd_orderOf_of_involutive
{G : Type u_1}
[Group G]
{φ : G →* G}
[Finite G]
(hφ : MonoidHom.FixedPointFree ⇑φ)
(h2 : Function.Involutive ⇑φ)
(g : G)
: