Zulip Chat Archive

Stream: Is there code for X?

Topic: fixed point free involutive automorphisms of groups are...

Johan Commelin (Mar 01 2024 at 10:02):

Consider the following lemma

import Mathlib.Data.Fintype.Card

lemma eq_inv_of_involutive_of_fixed_point_free {G : Type*} [Group G] [Finite G]
    (φ : G →* G) (hφ₁ : Function.Involutive φ) (hφ₂ : ∀ g, φ g = g → g = 1) : ⇑φ = (·⁻¹) := by
  let α : G → G := fun g ↦ φ g * g⁻¹
  suffices hα : α.Injective by
    ext g
    obtain ⟨x, rfl⟩ : ∃ x, α x = g := Finite.injective_iff_surjective.mp hα g
    simp [α, hφ₁ x]
  intro g₁ g₂ h
  suffices φ (g₁⁻¹ * g₂) = g₁⁻¹ * g₂ by
    simpa only [inv_mul_eq_one] using hφ₂ (g₁⁻¹ * g₂) this
  rw [← inv_mul_eq_one]
  simpa [α, mul_assoc] using congr_arg (φ g₂⁻¹ * · * g₂) h

Does this exist in mathlib?
If not:
(a) what should the name be?
(b) can we optimize the proof?

Kevin Buzzard (Mar 01 2024 at 10:19):

Oh I never knew that result!

Kevin Buzzard (Mar 01 2024 at 10:20):

What's a counterexample in the infinite case?

Johan Commelin (Mar 01 2024 at 10:21):

Free group on two generators with the obvious involution.

Johan Commelin (Mar 01 2024 at 10:21):

In the finite case, of course this implies that G is abelian.

Kevin Buzzard (Mar 01 2024 at 10:22):

...and has no elements of order 2

Johan Commelin (Mar 01 2024 at 10:22):

I guess we could call this the "odd order lemma" :rofl:

Riccardo Brasca (Mar 01 2024 at 10:23):

The proof is already quite short, isn't it? Or do you see a better math proof?

Johan Commelin (Mar 01 2024 at 10:24):

No, I don't. But I feel like this might have a 5-line proof instead of a 10-line proof.

Richard Copley (Mar 01 2024 at 12:06):

Here they split out a lemma (which is also hard to name).

theorem injective_commutator_of_fixed_point_free {G : Type*} [Group G] (φ : G →* G)
    (hφ₂ : ∀ g, φ g = g → g = 1) : Function.Injective fun g => φ g * g⁻¹ := by
  intro x y h
  rw [← mul_inv_eq_iff_eq_mul, mul_assoc, ← eq_inv_mul_iff_mul_eq, inv_inv, ← map_inv,
    ← map_mul] at h
  exact inv_mul_eq_one.mp <| hφ₂ _ h.symm

Richard Copley (Mar 01 2024 at 12:09):

And then

theorem eq_inv_of_involutive_of_fixed_point_free {G : Type*} [Group G] [Finite G]
    (φ : G →* G) (hφ₁ : Function.Involutive φ) (hφ₂ : ∀ g, φ g = g → g = 1) : ⇑φ = (·⁻¹) := by
  ext g
  obtain ⟨x, rfl⟩ := Finite.injective_iff_surjective.mp
    (injective_commutator_of_fixed_point_free φ hφ₂) g
  rw [map_mul, map_inv, mul_inv_rev, inv_inv, hφ₁]

Richard Copley (Mar 01 2024 at 13:04):

Johan Commelin said:

I guess we could call this the "odd order lemma" :rofl:

The "odd order" part can be stronger, as discussed here

Johan Commelin (Mar 01 2024 at 14:14):

@Richard Copley I guess that split makes sense. Do you know if there are more uses for the intermediate result?

Johan Commelin (Mar 01 2024 at 14:14):

Concerning the names... I'm not happy with "fixed point free" because 1 is a fixed point. But I don't know a better version.

Johan Commelin (Mar 01 2024 at 14:16):

Otoh, it seems that the groupprops wiki also uses that terminology, so maybe it isn't very evil.

Johan Commelin (Mar 01 2024 at 14:18):

Ooh, that wiki also lists another application of the intermediate result. That's good.

Richard Copley (Mar 01 2024 at 14:18):

Johan Commelin said:

Do you know if there are more uses for the intermediate result?

One other application is linked on its proof page, here.

Yeah, "phi is fixed-point free" or "phi is a fixed-point-free homomorphism" seem to be standard for group endomorphisms.

Johan Commelin (Mar 01 2024 at 14:20):

Do you understand why they call it the "commutator map"?

Richard Copley (Mar 01 2024 at 14:20):

No! I can't make that make sense.

Johan Commelin (Mar 01 2024 at 14:21):

It's conjugating $\sigma$ with left multiplication by $x$ , and evaluating the result at $1$ .

Johan Commelin (Mar 01 2024 at 14:21):

Not sure that is helpful...

Thomas Browning (Mar 01 2024 at 17:11):

There is a lot of theory of these fixed point free automorphisms (I think Gorenstein's book on finite groups might have a whole chapter about them, but I don't have a copy handy right now). But my memory is that the standard route to get the basic results is to first show injectivity/surjectively of g⁻¹ * φ g (or φ g * g⁻¹). From here, if φ ^ k = 1, then g * φ g * ... * φ^(k-1) g = 1 (or φ^(k-1) g * ... * φ g * g = 1). In particular, if φ ^ 2 = 1, then φ g = g⁻¹, so G is abelian. Another fun result is that a fixed point free automorphism will fix a unique Sylow p-subgroup for each prime p.

Kevin Buzzard (Mar 01 2024 at 17:13):

Are they studied in their own right or are they useful for e.g. classification of finite simple groups or whatever?

Johan Commelin (Mar 01 2024 at 17:13):

Certainly the latter. Maybe also the former :shrug:

Thomas Browning (Mar 01 2024 at 17:14):

Thompson's thesis proved that the existence of a fixed point free automorphism of prime order implies that the group is nilpotent.

Johan Commelin (Mar 01 2024 at 17:17):

@Thomas Browning So certainly it would make sense to define a predicate MonoidHom.FixedPointFree, if there are more than 5 lemmas about the concept.

Johan Commelin (Mar 01 2024 at 17:18):

Do you have a good name for $g \mapsto \phi g \cdot g^{-1}$ ?

Thomas Browning (Mar 01 2024 at 17:23):

No I don't, unfortunately. (And my preference would actually be g⁻¹ * φ g so that you get g * φ g * ... * φ^(k-1) g = 1)

Johan Commelin (Mar 01 2024 at 17:24):

Fine with me.

Johan Commelin (Mar 01 2024 at 17:24):

Do you think commutatorMap from groupprops is a sensible name? I still don't really understand that name.

Thomas Browning (Mar 01 2024 at 17:26):

It seems fine. I think the idea is that the usual commutator g⁻¹ * h⁻¹ * g * h is secretly g⁻¹ * φ g for φ being conjugation by h. So if your fixed point free automorphism is coming from a Frobenius semidirect product, then it actually is a commutator map.