feat(algebra/star): star_linear_equiv (#9426)

Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Author: eric-wieser

src/algebra/ring/comp_typeclasses.lean

@@ -5,6 +5,7 @@ Authors: Frédéric Dupuis, Heather Macbeth
 -/
 
 import algebra.ring.basic
+import data.equiv.ring
 
 /-!
 # Propositional typeclasses on several ring homs
@@ -90,6 +91,31 @@ instance triples₂ {σ₂₁ : R₂ →+* R₁} [ring_hom_inv_pair σ₁₂ σ
   ring_hom_comp_triple σ₂₁ σ₁₂ (ring_hom.id R₂) :=
 ⟨by simp only [comp_eq₂]⟩
 
+/--
+Construct a `ring_hom_inv_pair` from both directions of a ring equiv.
+
+This is not an instance, as for equivalences that are involutions, a better instance
+would be `ring_hom_inv_pair e e`. Indeed, this declaration is not currently used in mathlib.
+
+See note [reducible non-instances].
+-/
+@[reducible]
+lemma of_ring_equiv (e : R₁ ≃+* R₂) :
+  ring_hom_inv_pair (↑e : R₁ →+* R₂) ↑e.symm :=
+⟨e.symm_to_ring_hom_comp_to_ring_hom, e.symm.symm_to_ring_hom_comp_to_ring_hom⟩
+
+/--
+Swap the direction of a `ring_hom_inv_pair`. This is not an instance as it would loop, and better
+instances are often available and may often be preferrable to using this one. Indeed, this
+declaration is not currently used in mathlib.
+
+See note [reducible non-instances].
+-/
+@[reducible]
+lemma symm (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁) [ring_hom_inv_pair σ₁₂ σ₂₁] :
+  ring_hom_inv_pair σ₂₁ σ₁₂ :=
+⟨ring_hom_inv_pair.comp_eq₂, ring_hom_inv_pair.comp_eq⟩
+
 end ring_hom_inv_pair
 
 namespace ring_hom_comp_triple

src/algebra/star/basic.lean

@@ -4,14 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import tactic.apply_fun
-import algebra.order.ring
-import algebra.opposites
-import algebra.big_operators.basic
-import algebra.group_power.lemmas
 import algebra.field_power
 import data.equiv.ring_aut
-import data.equiv.mul_add_aut
 import group_theory.group_action.units
+import algebra.ring.comp_typeclasses
 
 /-!
 # Star monoids, rings, and modules
@@ -288,6 +284,17 @@ attribute [simp] star_smul
 instance star_monoid.to_star_module [comm_monoid R] [star_monoid R] : star_module R R :=
 ⟨star_mul'⟩
 
+namespace ring_hom_inv_pair
+
+/-- Instance needed to define star-linear maps over a commutative star ring
+(ex: conjugate-linear maps when R = ℂ).  -/
+instance [comm_semiring R] [star_ring R] :
+  ring_hom_inv_pair ((star_ring_aut : ring_aut R) : R →+* R)
+    ((star_ring_aut : ring_aut R) : R →+* R) :=
+⟨ring_hom.ext star_star, ring_hom.ext star_star⟩
+
+end ring_hom_inv_pair
+
 /-! ### Instances -/
 
 namespace units

src/algebra/star/module.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser, Frédéric Dupuis
+-/
+import algebra.star.basic
+import data.equiv.module
+
+/-!
+# The star operation, bundled as a star-linear equiv
+
+We define `star_linear_equiv`, which is the star operation bundled as a star-linear map.
+It is defined on a star algebra `A` over the base ring `R`.
+
+## TODO
+
+- Define `star_linear_equiv` for noncommutative `R`. We only the commutative case for now since,
+  in the noncommutative case, the ring hom needs to reverse the order of multiplication. This
+  requires a ring hom of type `R →+* Rᵒᵖ`, which is very undesirable in the commutative case.
+  One way out would be to define a new typeclass `is_op R S` and have an instance `is_op R R`
+  for commutative `R`.
+- Also note that such a definition involving `Rᵒᵖ` or `is_op R S` would require adding
+  the appropriate `ring_hom_inv_pair` instances to be able to define the semilinear
+  equivalence.
+-/
+
+/-- If `A` is a module over a commutative `R` with compatible actions,
+then `star` is a semilinear equivalence. -/
+def star_linear_equiv {R : Type*} {A : Type*}
+  [comm_ring R] [star_ring R] [semiring A] [star_ring A] [module R A] [star_module R A]  :
+    A ≃ₛₗ[((star_ring_aut : ring_aut R) : R →+* R)] A :=
+{ to_fun := star,
+  map_smul' := star_smul,
+  .. star_add_equiv }