Conjugation is bijection

Stream: Is there code for X?

[Alex Kontorovich]

I'm sure we have this but can't find it?

import Mathlib.GroupTheory.GroupAction.Basic

theorem Group.Bijective_conjugate {α : Type _} [Group α] (g : α) :
    Function.Bijective (fun h ↦ g * h * g⁻¹) := sorry

[Alex Kontorovich]

Should probably be a comp of right and left multiplication being bijective?

[Alex Kontorovich]

Anything simpler than this?

import Mathlib.GroupTheory.GroupAction.Basic

theorem Group.Bijective_conjugate {α : Type _} [Group α] (g : α) :
    Function.Bijective (fun h ↦ g * h * g⁻¹) := by
  convert (mulLeft_bijective g).comp (mulRight_bijective g⁻¹) using 1
  simp [Function.comp, mul_assoc]

[Eric Wieser]

import Mathlib.GroupTheory.GroupAction.ConjAct

theorem Group.Bijective_conjugate {α : Type _} [Group α] (g : α) :
    Function.Bijective (fun h ↦ g * h * g⁻¹) :=
  (MulAction.toPerm (ConjAct.toConjAct g)).bijective

[Eric Wieser]

Which is exploiting that the statement is the same as Function.Bijective (ConjAct.toConjAct g • ·) which in turn is just a standard result about group actions

[Eric Wieser]

In the spirit of your code, you just had the left and right in the wrong order:

import Mathlib.GroupTheory.GroupAction.Basic

theorem Group.Bijective_conjugate {α : Type _} [Group α] (g : α) :
    Function.Bijective (fun h ↦ g * h * g⁻¹) :=
  (mulRight_bijective g⁻¹).comp (mulLeft_bijective g)

[Alex Kontorovich]

Great, thanks; is it worth adding this to mathlib? (It was annoying that exact? didn't find it...) If so, what's the right name, perhaps Group.Conj_bijective is closer?

[Alex Kontorovich]

And what's better, to phrase it as a bijection, or permutation?

[Jireh Loreaux]

IMHO it seems overly specific to have this, since it's true for any group action, and we already have the code to do it generally. But others may disagree with me.

[Anatole Dedecker]

We have docs#MulAut.conj which should be all you need