English
Group conjugation defines a monoid homomorphism from G to MulAut G, given by g ↦ (h ↦ g h g^{-1}).
Русский
Обобщение конъюгации групп образует моноид-гомоморфизм G → MulAut G, задаваемый g ↦ (h ↦ g h g^{-1}).
LaTeX
$$$\text{def conj }[Group G] : G \to_* MulAut G$ with \; toFun\, g\, h = g h g^{-1}$$$
Lean4
/-- Group conjugation, `MulAut.conj g h = g * h * g⁻¹`, as a monoid homomorphism
mapping multiplication in `G` into multiplication in the automorphism group `MulAut G`.
See also the type `ConjAct G` for any group `G`, which has a `MulAction (ConjAct G) G` instance
where `conj G` acts on `G` by conjugation. -/
def conj [Group G] : G →* MulAut G
where
toFun
g :=
{ toFun := fun h => g * h * g⁻¹
invFun := fun h => g⁻¹ * h * g
left_inv := fun _ => by simp only [mul_assoc, inv_mul_cancel_left, inv_mul_cancel, mul_one]
right_inv := fun _ => by simp only [mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
map_mul' := by simp only [mul_assoc, inv_mul_cancel_left, forall_const] }
map_mul' g₁
g₂ := by
ext h
change g₁ * g₂ * h * (g₁ * g₂)⁻¹ = g₁ * (g₂ * h * g₂⁻¹) * g₁⁻¹
simp only [mul_assoc, mul_inv_rev]
map_one' := by ext; simp only [one_mul, inv_one, mul_one, one_apply]; rfl
