English
Conjugation in additive groups defines a homomorphism from G to AddAut G by g ↦ (h ↦ g + h - g).
Русский
Конъюгация в аддитивных группах задает гомоморфизм из G в AddAut G: g ↦ (h ↦ g + h - g).
LaTeX
$$$[AddGroup G] : G \to+ AddAut G$ with toFun g = (h \mapsto g + h - g)$$$
Lean4
/-- Additive group conjugation, `AddAut.conj g h = g + h - g`, as an additive monoid
homomorphism mapping addition in `G` into multiplication in the automorphism group `AddAut G`
(written additively in order to define the map). -/
def conj [AddGroup G] : G →+ Additive (AddAut G)
where
toFun
g :=
@Additive.ofMul (AddAut G)
{ toFun := fun h => g + h + -g
invFun := fun h => -g + h + g
left_inv := fun _ => by simp only [add_assoc, neg_add_cancel_left, neg_add_cancel, add_zero]
right_inv := fun _ => by simp only [add_assoc, add_neg_cancel_left, add_neg_cancel, add_zero]
map_add' := by simp only [add_assoc, neg_add_cancel_left, forall_const] }
map_add' g₁
g₂ := by
apply Additive.toMul.injective; ext h
change g₁ + g₂ + h + -(g₁ + g₂) = g₁ + (g₂ + h + -g₂) + -g₁
simp only [add_assoc, neg_add_rev]
map_zero' := by
apply Additive.toMul.injective; ext
simp only [zero_add, neg_zero, add_zero, toMul_ofMul, toMul_zero, one_apply]
rfl
