feat(data/equiv/mul_add_aut): adding conjugation in an additive group (…

…#6774)

assuming `[add_group G]` this defines `G ->+ additive (add_aut G)`



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/equiv/mul_add_aut.lean

@@ -71,8 +71,8 @@ mul_equiv.apply_symm_apply _ _
 def to_perm : mul_aut M →* equiv.perm M :=
 by refine_struct { to_fun := mul_equiv.to_equiv }; intros; refl
 
-/-- group conjugation as a group homomorphism into the automorphism group.
-  `conj g h = g * h * g⁻¹` -/
+/-- Group conjugation, `mul_aut.conj g h = g * h * g⁻¹`, as a monoid homomorphism
+mapping multiplication in `G` into multiplication in the automorphism group `mul_aut G`. -/
 def conj [group G] : G →* mul_aut G :=
 { to_fun := λ g,
   { to_fun := λ h, g * h * g⁻¹,
@@ -85,7 +85,7 @@ def conj [group G] : G →* mul_aut G :=
 
 @[simp] lemma conj_apply [group G] (g h : G) : conj g h = g * h * g⁻¹ := rfl
 @[simp] lemma conj_symm_apply [group G] (g h : G) : (conj g).symm h = g⁻¹ * h * g := rfl
-@[simp] lemma conj_inv_apply {G : Type*} [group G] (g h : G) : (conj g)⁻¹ h = g⁻¹ * h * g := rfl
+@[simp] lemma conj_inv_apply [group G] (g h : G) : (conj g)⁻¹ h = g⁻¹ * h * g := rfl
 
 end mul_aut
 
@@ -127,4 +127,21 @@ add_equiv.apply_symm_apply _ _
 def to_perm : add_aut A →* equiv.perm A :=
 by refine_struct { to_fun := add_equiv.to_equiv }; intros; refl
 
+/-- Additive group conjugation, `add_aut.conj g h = g + h - g`, as an additive monoid
+homomorphism mapping addition in `G` into multiplication in the automorphism group `add_aut G`
+(written additively in order to define the map). -/
+def conj [add_group G] : G →+ additive (add_aut G) :=
+{ to_fun := λ g, @additive.of_mul (add_aut G)
+  { to_fun := λ h, g + h - g,
+    inv_fun := λ h, -g + h + g,
+    left_inv := λ _, by simp [add_assoc],
+    right_inv := λ _, by simp [add_assoc],
+    map_add' := by simp [add_assoc, sub_eq_add_neg] },
+  map_add' := λ _ _, by apply additive.to_mul.injective; ext; simp [add_assoc, sub_eq_add_neg],
+  map_zero' := by ext; simpa }
+
+@[simp] lemma conj_apply [add_group G] (g h : G) : conj g h = g + h - g := rfl
+@[simp] lemma conj_symm_apply [add_group G] (g h : G) : (conj g).symm h = -g + h + g := rfl
+@[simp] lemma conj_inv_apply [add_group G] (g h : G) : (-(conj g)) h = -g + h + g := rfl
+
 end add_aut