feat: transfer star-related instances across equivalences

Author: j-loreaux

Mathlib/Algebra/Star/Basic.lean

@@ -93,7 +93,7 @@ theorem star_inj [InvolutiveStar R] {x y : R} : star x = star y ↔ x = y :=
   star_injective.eq_iff
 
 /-- `star` as an equivalence when it is involutive. -/
-protected def Equiv.star [InvolutiveStar R] : Equiv.Perm R :=
+protected def Equiv.Perm.star [InvolutiveStar R] : Equiv.Perm R :=
   star_involutive.toPerm _
 
 theorem eq_star_of_eq_star [InvolutiveStar R] {r s : R} (h : r = star s) : s = star r := by
@@ -522,6 +522,41 @@ theorem isRegular_star_iff [Mul R] [StarMul R] {x : R} :
 
 end Regular
 
+namespace Function.Injective
+
+variable {S : Type v} (f : R → S)
+
+/-- Given a type endowed with `star`, that `star` is involutive if it admits an injective map that
+preserves `star` to a type with whose `star` is involutive. See note [reducible non-instances]. -/
+protected abbrev involutiveStar [Star R] [InvolutiveStar S] (hf : Injective f)
+    (star : ∀ x, f (star x) = star (f x)) : InvolutiveStar R where
+  star_involutive r := hf <| by rw [star, star, star_star]
+
+/-- A type endowed with `star` and `*` is a star magma if it admits an injective map that
+preserves `star` and `*` to star magma.  See note [reducible non-instances]. -/
+protected abbrev starMul [Star R] [Mul R] [Mul S] [StarMul S] (hf : Injective f)
+    (star : ∀ x, f (star x) = star (f x)) (mul : ∀ x y, f (x * y) = f x * f y) :
+    StarMul R where
+  toInvolutiveStar := hf.involutiveStar _ star
+  star_mul x y := hf <| by rw [star, mul, star_mul, mul, star, star]
+
+/-- A additive monoid endowed with `star` is an additive star monoid if it admits an injective map
+that preserves `star` and `+` to an additive star monoid.  See note [reducible non-instances]. -/
+protected abbrev starAddMonoid [Star R] [AddMonoid R] [AddMonoid S] [StarAddMonoid S]
+    (hf : Injective f) (star : ∀ x, f (star x) = star (f x)) (add : ∀ x y, f (x + y) = f x + f y) :
+    StarAddMonoid R where
+  toInvolutiveStar := hf.involutiveStar f star
+  star_add x y := hf <| by rw [star, add, star_add, add, star, star]
+
+/-- A non-unital non-associative ring endowed with `star` is a star ring if it admits an injective
+map that preserves `star`, `*` and `+` to a star ring. See note [reducible non-instances]. -/
+protected abbrev starRing [Star R] [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S]
+    [StarRing S] (star : ∀ x, f (star x) = star (f x)) (add : ∀ x y, f (x + y) = f x + f y)
+    (mul : ∀ x y, f (x * y) = f x * f y) (hf : Injective f) :
+    StarRing R :=
+  { hf.starMul f star mul, hf.starAddMonoid f star add with }
+
+end Function.Injective
 
 namespace MulOpposite
 

Mathlib/Algebra/Star/TransferInstance.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Algebra.Star.Basic
+public import Mathlib.Algebra.Ring.TransferInstance
+
+/-! # Transfer algebraic structures across `Equiv`s
+
+This continues the pattern set in `Mathlib/Algebra/Group/TransferInstance.lean`.
+-/
+
+variable {R S : Type*}
+
+@[expose] public section
+
+namespace Equiv
+
+variable (e : R ≃ S)
+
+/-- Transfer `Star` across an `Equiv` -/
+protected abbrev star [Star S] : Star R where
+  star r := e.symm (star (e r))
+
+/-- Transfer `InvolutiveStar` across an `Equiv` -/
+protected abbrev InvolutiveStar [InvolutiveStar S] : InvolutiveStar R :=
+  let _ := e.star
+  e.injective.involutiveStar _ fun _ ↦ e.apply_symm_apply _
+
+/-- Transfer `StarMul` across an `Equiv` -/
+protected abbrev starMul [Mul S] [StarMul S] :
+    letI := e.mul
+    StarMul R := by
+  let := e.star
+  let := e.mul
+  apply e.injective.starMul <;> (intros; exact e.apply_symm_apply _)
+
+/-- Transfer `StarAddMonoid` across an `Equiv` -/
+protected abbrev starAddMonoid [AddMonoid S] [StarAddMonoid S] :
+    letI := e.addMonoid
+    StarAddMonoid R := by
+  let := e.star
+  let := e.addMonoid
+  apply e.injective.starAddMonoid <;> (intros; exact e.apply_symm_apply _)
+
+/-- Transfer `StarRing` across an `Equiv` -/
+protected abbrev starRing [NonUnitalNonAssocSemiring S] [StarRing S] :
+    letI := e.nonUnitalNonAssocSemiring
+    StarRing R := by
+  let := e.star
+  let := e.nonUnitalNonAssocSemiring
+  apply e.injective.starRing <;> (intros; exact e.apply_symm_apply _)
+
+end Equiv