feat: expand API for StarAlgEquiv (leanprover-community#40517)

This PR adds API for `StarAlgEquiv`. It provides:

+ `StarAlgEquiv.toNonUnitalStarAlgHom`
+ `StarAlgEquiv.toStarAlgHom`
+ `StarAlgEquiv.arrowCongr'` (non-unital morphisms)
+ `StarAlgEquiv.arrowCongr` (unital morphisms)
+ `StarAlgEquiv.ofNonUnitalStarAlgHom` (non-unital morphisms)
+ `StarAlgEquiv.ofStarAlgHom` (unital morphisms); this was pre-existing, but used morphism classes instead of actual morphisms. This PR fixes that.

It also generalizes the type class hypothesis in `StarAlgEquiv.restrictScalars` so that it applies to non-unital algebras.

In addition, `StarAlgEquiv.refl` is protected and its type arguments made explicit.

Author: j-loreaux

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -723,17 +723,18 @@ theorem toRingEquiv_eq_coe (e : A ≃⋆ₐ[R] B) : e.toRingEquiv = e :=
 theorem ext {f g : A ≃⋆ₐ[R] B} (h : ∀ a, f a = g a) : f = g :=
   DFunLike.ext f g h
 
+variable (R A) in
 /-- The identity map is a star algebra isomorphism. -/
 @[refl]
-def refl : A ≃⋆ₐ[R] A :=
+protected def refl : A ≃⋆ₐ[R] A :=
   { StarRingEquiv.refl (A := A) with
     map_smul' := fun _ _ => rfl }
 
 instance : Inhabited (A ≃⋆ₐ[R] A) :=
-  ⟨refl⟩
+  ⟨.refl R A⟩
 
 @[simp]
-theorem coe_refl : ⇑(refl : A ≃⋆ₐ[R] A) = id :=
+theorem coe_refl : ⇑(StarAlgEquiv.refl R A) = id :=
   rfl
 
 /-- The inverse of a star algebra isomorphism is a star algebra isomorphism. -/
@@ -775,7 +776,7 @@ theorem symm_mk (e : A ≃⋆+* B) (h₁) : dsimp%
   rfl
 
 @[simp]
-theorem refl_symm : (StarAlgEquiv.refl : A ≃⋆ₐ[R] A).symm = StarAlgEquiv.refl :=
+theorem refl_symm : (StarAlgEquiv.refl R A).symm = .refl R A :=
   rfl
 
 @[simp]
@@ -845,7 +846,7 @@ theorem toAlgEquiv_injective : Function.Injective (toAlgEquiv (R := R) (A := A)
   fun _ _ h => ext <| AlgEquiv.congr_fun h
 
 @[simp]
-theorem toAlgEquiv_refl : (refl : A ≃⋆ₐ[R] A).toAlgEquiv = AlgEquiv.refl := rfl
+theorem toAlgEquiv_refl : (StarAlgEquiv.refl R A).toAlgEquiv = AlgEquiv.refl := rfl
 
 /-- Upgrade an algebra equivalence to a ⋆-algebra equivalence given that it preserves the
 `star` operation. -/
@@ -876,6 +877,190 @@ end AlgEquiv
 
 end Basic
 
+section NonUnitalArrowCongr
+
+variable {R A₁ A₂ A₃ A₁' A₂' A₃' : Type*} [Monoid R]
+  [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁]
+  [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂]
+  [NonUnitalNonAssocSemiring A₃] [DistribMulAction R A₃] [Star A₃]
+  [NonUnitalNonAssocSemiring A₁'] [DistribMulAction R A₁'] [Star A₁']
+  [NonUnitalNonAssocSemiring A₂'] [DistribMulAction R A₂'] [Star A₂']
+  [NonUnitalNonAssocSemiring A₃'] [DistribMulAction R A₃'] [Star A₃']
+  (e : A₁ ≃⋆ₐ[R] A₂)
+
+/-- Reintrepret a star algebra equivalence as a non-unital star algebra homomorphism. -/
+@[simps]
+def toNonUnitalStarAlgHom : A₁ →⋆ₙₐ[R] A₂ :=
+  { e with
+    toFun := e
+    map_zero' := map_zero e }
+
+@[simp]
+lemma toNonUnitalStarAlgHom_refl : (StarAlgEquiv.refl R A₁).toNonUnitalStarAlgHom = .id R A₁ :=
+  rfl
+
+@[simp]
+lemma toNonUnitalStarAlgHom_comp (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₂ : A₂ ≃⋆ₐ[R] A₃) :
+    e₂.toNonUnitalStarAlgHom.comp e₁.toNonUnitalStarAlgHom =
+      (e₁.trans e₂).toNonUnitalStarAlgHom := rfl
+
+/-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'` as star algebras, then the type
+of maps `A₁ →⋆ₙₐ[R] A₂` is equivalent to the type of maps `A₁' →⋆ₙₐ[R] A₂'`.
+
+For unital star algebra homomorphisms, see `StarAlgEquiv.arrowCongr`. -/
+@[simps apply]
+def arrowCongr' (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') :
+    (A₁ →⋆ₙₐ[R] A₂) ≃ (A₁' →⋆ₙₐ[R] A₂') where
+  toFun f := (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom
+  invFun f := (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom
+  left_inv f := by ext; simp
+  right_inv f := by ext; simp
+
+theorem arrowCongr'_comp (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂')
+    (e₃ : A₃ ≃⋆ₐ[R] A₃') (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₃) :
+    arrowCongr' e₁ e₃ (g.comp f) = (arrowCongr' e₂ e₃ g).comp (arrowCongr' e₁ e₂ f) := by
+  ext
+  simp
+
+@[simp]
+theorem arrowCongr'_refl : arrowCongr' (.refl _ _) (.refl _ _) = Equiv.refl (A₁ →⋆ₙₐ[R] A₂) :=
+  rfl
+
+@[simp]
+theorem arrowCongr'_trans (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₁' : A₁' ≃⋆ₐ[R] A₂')
+    (e₂ : A₂ ≃⋆ₐ[R] A₃) (e₂' : A₂' ≃⋆ₐ[R] A₃') :
+    arrowCongr' (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr' e₁ e₁').trans (arrowCongr' e₂ e₂') :=
+  rfl
+
+@[simp]
+theorem symm_arrowCongr' (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') :
+    (arrowCongr' e₁ e₂).symm = arrowCongr' e₁.symm e₂.symm :=
+  rfl
+
+/-- Construct a star algebra equivalence from a pair of non-unital star algebra homomorphisms. -/
+@[simps]
+def ofNonUnitalStarAlgHom (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁) (h₁ : g.comp f = .id R A₁)
+    (h₂ : f.comp g = .id R A₂) : A₁ ≃⋆ₐ[R] A₂ :=
+  { f with
+    toFun := f
+    invFun := g
+    left_inv x := congr($h₁ x)
+    right_inv x := congr($h₂ x) }
+
+@[simp]
+lemma toNonUnitalStarAlgHom_ofNonUnitalStarAlgHom (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
+    (h₁ : g.comp f = .id R A₁) (h₂ : f.comp g = .id R A₂) :
+    (ofNonUnitalStarAlgHom f g h₁ h₂).toNonUnitalStarAlgHom = f :=
+  rfl
+
+lemma symm_ofNonUnitalStarAlgHom (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
+    (h₁ : g.comp f = .id R A₁) (h₂ : f.comp g = .id R A₂) :
+    (ofNonUnitalStarAlgHom f g h₁ h₂).symm = ofNonUnitalStarAlgHom g f h₂ h₁ :=
+  rfl
+
+@[simp]
+lemma toNonUnitalStarAlgHom_symm_ofNonUnitalStarAlgHom (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
+    (h₁ : g.comp f = .id R A₁) (h₂ : f.comp g = .id R A₂) :
+    (ofNonUnitalStarAlgHom f g h₁ h₂).symm.toNonUnitalStarAlgHom = g :=
+  rfl
+
+end NonUnitalArrowCongr
+
+section Unital
+
+variable {R A₁ A₂ A₃ A₁' A₂' A₃' : Type*}
+  [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃]
+  [Semiring A₁'] [Semiring A₂'] [Semiring A₃']
+  [Algebra R A₁] [Algebra R A₂] [Algebra R A₃]
+  [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃']
+  [Star A₁] [Star A₂] [Star A₃]
+  [Star A₁'] [Star A₂'] [Star A₃']
+  (e : A₁ ≃⋆ₐ[R] A₂)
+
+/-- Reintrepret a star algebra equivalence as a star algebra homomorphism. -/
+@[simps]
+def toStarAlgHom : A₁ →⋆ₐ[R] A₂ :=
+  { e with
+    toFun := e
+    __ := e.toAlgEquiv.toAlgHom }
+
+@[simp]
+lemma toNonUnitalStarAlgHom_toStarAlgHom (e : A₁ ≃⋆ₐ[R] A₂) :
+    e.toStarAlgHom.toNonUnitalStarAlgHom = e.toNonUnitalStarAlgHom :=
+  rfl
+
+@[simp]
+lemma toStarAlgHom_refl : (StarAlgEquiv.refl R A₁).toStarAlgHom = .id R A₁ :=
+  rfl
+
+@[simp]
+lemma toStarAlgHom_comp (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₂ : A₂ ≃⋆ₐ[R] A₃) :
+    e₂.toStarAlgHom.comp e₁.toStarAlgHom = (e₁.trans e₂).toStarAlgHom := rfl
+
+/-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'` as star algebras, then the type
+of maps `A₁ →⋆ₐ[R] A₂` is equivalent to the type of maps `A₁' →⋆ₐ[R] A₂'`.
+
+For non-unital star algebra homomorphisms, see `StarAlgEquiv.arrowCongr'`. -/
+@[simps apply]
+def arrowCongr (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') : (A₁ →⋆ₐ[R] A₂) ≃ (A₁' →⋆ₐ[R] A₂') where
+  toFun f := (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom
+  invFun f := (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom
+  left_inv f := by ext; simp
+  right_inv f := by ext; simp
+
+theorem arrowCongr_comp (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂')
+    (e₃ : A₃ ≃⋆ₐ[R] A₃') (f : A₁ →⋆ₐ[R] A₂) (g : A₂ →⋆ₐ[R] A₃) :
+    arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f) := by
+  ext
+  simp
+
+@[simp]
+theorem arrowCongr_refl : arrowCongr (.refl _ _) (.refl _ _) = Equiv.refl (A₁ →⋆ₐ[R] A₂) :=
+  rfl
+
+@[simp]
+theorem arrowCongr_trans (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₁' : A₁' ≃⋆ₐ[R] A₂')
+    (e₂ : A₂ ≃⋆ₐ[R] A₃) (e₂' : A₂' ≃⋆ₐ[R] A₃') :
+    arrowCongr (e₁.trans e₂) (e₁'.trans e₂') = (arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂') :=
+  rfl
+
+@[simp]
+theorem symm_arrowCongr (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') :
+    (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm :=
+  rfl
+
+/-- Construct a star algebra equivalence from a pair of star algebra homomorphisms. -/
+@[simps]
+def ofStarAlgHom {R A B : Type*} [CommSemiring R]
+    [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B]
+    (f : A →⋆ₐ[R] B) (g : B →⋆ₐ[R] A) (h₁ : g.comp f = .id R A) (h₂ : f.comp g = .id R B) :
+    A ≃⋆ₐ[R] B :=
+  { f with
+    toFun := f
+    invFun := g
+    left_inv x := congr($h₁ x)
+    right_inv x := congr($h₂ x)
+    map_smul' := map_smul f }
+
+@[simp]
+lemma toStarAlgHom_ofStarAlgHom (f : A₁ →⋆ₐ[R] A₂) (g : A₂ →⋆ₐ[R] A₁)
+    (h₁ : g.comp f = .id R A₁) (h₂ : f.comp g = .id R A₂) :
+    (ofStarAlgHom f g h₁ h₂).toStarAlgHom = f :=
+  rfl
+
+lemma symm_ofStarAlgHom (f : A₁ →⋆ₐ[R] A₂) (g : A₂ →⋆ₐ[R] A₁)
+    (h₁ : g.comp f = .id R A₁) (h₂ : f.comp g = .id R A₂) :
+    (ofStarAlgHom f g h₁ h₂).symm = ofStarAlgHom g f h₂ h₁ :=
+  rfl
+
+@[simp]
+lemma toStarAlgHom_symm_ofStarAlgHom (f : A₁ →⋆ₐ[R] A₂) (g : A₂ →⋆ₐ[R] A₁)
+    (h₁ : g.comp f = .id R A₁) (h₂ : f.comp g = .id R A₂) :
+    (ofStarAlgHom f g h₁ h₂).symm.toStarAlgHom = g :=
+  rfl
+
+end Unital
+
 section Bijective
 
 variable {F G R A B : Type*} [Monoid R]
@@ -884,19 +1069,6 @@ variable [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B]
 variable [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B]
 variable [FunLike G B A] [NonUnitalAlgHomClass G R B A] [StarHomClass G B A]
 
-/-- If a (unital or non-unital) star algebra morphism has an inverse, it is an isomorphism of
-star algebras. -/
-@[simps]
-def ofStarAlgHom (f : F) (g : G) (h₁ : ∀ x, g (f x) = x) (h₂ : ∀ x, f (g x) = x) : A ≃⋆ₐ[R] B where
-  toFun := f
-  invFun := g
-  left_inv := h₁
-  right_inv := h₂
-  map_add' := map_add f
-  map_mul' := map_mul f
-  map_smul' := map_smul f
-  map_star' := map_star f
-
 /-- Promote a bijective star algebra homomorphism to a star algebra equivalence. -/
 noncomputable def ofBijective (f : F) (hf : Function.Bijective f) : A ≃⋆ₐ[R] B :=
   {
@@ -922,7 +1094,7 @@ variable {S R : Type*} [Mul R] [Add R] [Star R] [SMul S R]
 
 @[simps -isSimp one mul]
 instance aut : Group (R ≃⋆ₐ[S] R) where
-  one := refl
+  one := .refl _ _
   mul a b := b.trans a
   one_mul _ := rfl
   mul_one _ := rfl

Mathlib/Algebra/Star/Subalgebra.lean

@@ -869,6 +869,32 @@ end StarAlgHom
 
 section RestrictScalars
 
+section Equiv
+
+variable (R : Type*) {S A B : Type*} [CommSemiring R] [CommSemiring S]
+  [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [Module S A]
+  [Module S B] [Module R A] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B]
+  [Star A] [Star B]
+
+/-- Restrict the scalar ring of a star algebra equivalence. -/
+@[simps]
+def StarAlgEquiv.restrictScalars (f : A ≃⋆ₐ[S] B) : A ≃⋆ₐ[R] B :=
+  { (f : A →ₗ[S] B).restrictScalars R, f with
+    toFun := f }
+
+theorem StarAlgEquiv.restrictScalars_injective :
+    Function.Injective (StarAlgEquiv.restrictScalars R : (A ≃⋆ₐ[S] B) → A ≃⋆ₐ[R] B) :=
+  fun _ _ h => ext (DFunLike.congr_fun h ·)
+
+@[simp]
+theorem StarAlgEquiv.toNonUnitalStarAlgHom_restrictScalars (e : A ≃⋆ₐ[S] B) :
+    (e.restrictScalars R).toNonUnitalStarAlgHom = e.toNonUnitalStarAlgHom.restrictScalars R :=
+  rfl
+
+end Equiv
+
+section Unital
+
 variable (R : Type*) {S A B : Type*} [CommSemiring R]
   [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra S A] [Algebra S B]
   [Algebra R A] [Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B]
@@ -883,16 +909,12 @@ theorem StarAlgHom.restrictScalars_injective :
   fun f g h => StarAlgHom.ext fun x =>
     show f.restrictScalars R x = g.restrictScalars R x from DFunLike.congr_fun h x
 
-@[simps]
-def StarAlgEquiv.restrictScalars (f : A ≃⋆ₐ[S] B) : A ≃⋆ₐ[R] B :=
-  { (f : A →⋆ₐ[S] B).restrictScalars R, f with
-    toFun := f
-    map_smul' := map_smul ((f : A →⋆ₐ[S] B).restrictScalars R) }
+@[simp]
+theorem StarAlgEquiv.toStarAlgHom_restrictScalars (e : A ≃⋆ₐ[S] B) :
+    (e.restrictScalars R).toStarAlgHom = e.toStarAlgHom.restrictScalars R :=
+  rfl
 
-theorem StarAlgEquiv.restrictScalars_injective :
-    Function.Injective (StarAlgEquiv.restrictScalars R : (A ≃⋆ₐ[S] B) → A ≃⋆ₐ[R] B) :=
-  fun f g h => StarAlgEquiv.ext fun x =>
-    show f.restrictScalars R x = g.restrictScalars R x from DFunLike.congr_fun h x
+end Unital
 
 end RestrictScalars
 

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

@@ -894,7 +894,7 @@ lemma conjStarAlgEquiv_apply (e : H ≃ₗᵢ[𝕜] K) (x : H →L[𝕜] H) :
 @[simp] lemma symm_conjStarAlgEquiv (e : H ≃ₗᵢ[𝕜] K) :
     e.conjStarAlgEquiv.symm = e.symm.conjStarAlgEquiv := rfl
 
-@[simp] theorem conjStarAlgEquiv_refl : conjStarAlgEquiv (.refl 𝕜 H) = .refl := rfl
+@[simp] theorem conjStarAlgEquiv_refl : conjStarAlgEquiv (.refl 𝕜 H) = .refl _ _ := rfl
 
 theorem conjStarAlgEquiv_trans {G : Type*} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G]
     [CompleteSpace G] (e : H ≃ₗᵢ[𝕜] K) (f : K ≃ₗᵢ[𝕜] G) :