feat: MonoidHom.toAdditiveRight as a MulEquiv (#27047)

From Toric

Author: YaelDillies

Mathlib/Algebra/Group/TypeTags/Hom.lean

@@ -3,21 +3,19 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Algebra.Group.Equiv.Defs
+import Mathlib.Algebra.Group.Hom.Basic
 import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-!
 # Transport algebra morphisms between additive and multiplicative types.
 -/
 
-
-universe u v
-
-variable {α : Type u} {β : Type v}
-
 open Additive (ofMul toMul)
 open Multiplicative (ofAdd toAdd)
 
+variable {M N α β : Type*}
+
 /-- Reinterpret `α →+ β` as `Multiplicative α →* Multiplicative β`. -/
 @[simps]
 def AddMonoidHom.toMultiplicative [AddZeroClass α] [AddZeroClass β] :
@@ -37,6 +35,9 @@ def AddMonoidHom.toMultiplicative [AddZeroClass α] [AddZeroClass β] :
 lemma AddMonoidHom.coe_toMultiplicative [AddZeroClass α] [AddZeroClass β] (f : α →+ β) :
     ⇑(toMultiplicative f) = ofAdd ∘ f ∘ toAdd := rfl
 
+@[simp]
+lemma AddMonoidHom.toMultiplicative_id [AddZeroClass α] : (id α).toMultiplicative = .id _ := rfl
+
 /-- Reinterpret `α →* β` as `Additive α →+ Additive β`. -/
 @[simps]
 def MonoidHom.toAdditive [MulOneClass α] [MulOneClass β] :
@@ -53,9 +54,14 @@ def MonoidHom.toAdditive [MulOneClass α] [MulOneClass β] :
   }
 
 @[simp, norm_cast]
-lemma MonoidHom.coe_toMultiplicative [MulOneClass α] [MulOneClass β] (f : α →* β) :
+lemma MonoidHom.coe_toAdditive [MulOneClass α] [MulOneClass β] (f : α →* β) :
     ⇑(toAdditive f) = ofMul ∘ f ∘ toMul := rfl
 
+@[deprecated (since := "2025-11-07")]
+alias MonoidHom.coe_toMultiplicative := MonoidHom.coe_toAdditive
+
+@[simp] lemma MonoidHom.toAdditive_id [MulOneClass α] : (id α).toAdditive = .id _ := rfl
+
 /-- Reinterpret `Additive α →+ β` as `α →* Multiplicative β`. -/
 @[simps]
 def AddMonoidHom.toMultiplicativeRight [MulOneClass α] [AddZeroClass β] :
@@ -153,3 +159,36 @@ lemma proving equality in `α →* Multiplicative β` from equality in `Additive
 lemma Additive.addMonoidHom_ext [MulOneClass α] [AddZeroClass β]
     (f g : Additive α →+ β) (h : f.toMultiplicativeRight = g.toMultiplicativeRight) : f = g :=
   AddMonoidHom.toMultiplicativeRight.injective h
+
+section AddCommMonoid
+variable [AddMonoid M] [AddCommMonoid N]
+
+@[simp]
+lemma AddMonoidHom.toMultiplicative_add (f g : M →+ N) :
+    (f + g).toMultiplicative = f.toMultiplicative * g.toMultiplicative := rfl
+
+end AddCommMonoid
+
+/-- `AddMonoidHom.toMultiplicativeLeft` as an `AddEquiv`. -/
+def AddMonoidHom.toMultiplicativeLeftAddEquiv [AddMonoid M] [CommMonoid N] :
+    (M →+ Additive N) ≃+ Additive (Multiplicative M →* N) where
+  toEquiv := AddMonoidHom.toMultiplicativeLeft.trans Additive.ofMul
+  map_add' _ _ := rfl
+
+/-- `AddMonoidHom.toMultiplicativeRight` as an `AddEquiv`. -/
+def AddMonoidHom.toMultiplicativeRightAddEquiv [Monoid M] [AddCommMonoid N] :
+    (Additive M →+ N) ≃+ Additive (M →* Multiplicative N) where
+  toEquiv := AddMonoidHom.toMultiplicativeRight.trans Additive.ofMul
+  map_add' _ _ := rfl
+
+/-- `MonoidHom.toAdditiveLeft` as a `MulEquiv`. -/
+def MonoidHom.toAdditiveLeftMulEquiv [Monoid M] [AddCommMonoid N] :
+    (M →* Multiplicative N) ≃* Multiplicative (Additive M →+ N) where
+  toEquiv := MonoidHom.toAdditiveLeft.trans Multiplicative.ofAdd
+  map_mul' _ _ := rfl
+
+/-- `MonoidHom.toAdditiveRight` as a `MulEquiv`. -/
+def MonoidHom.toAdditiveRightMulEquiv [AddMonoid M] [CommMonoid N] :
+    (Multiplicative M →* N) ≃* Multiplicative (M →+ Additive N) where
+  toEquiv := MonoidHom.toAdditiveRight.trans Multiplicative.ofAdd
+  map_mul' _ _ := rfl