feat(Algebra/Algebra/Opposite): A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ and (A ≃ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ ≃ₐ[R] B) (#6525)

This also adds the missing `AlgEquiv.equivCongr` as a more general version of `AlgEquiv.autCongr`.

Author: eric-wieser

Mathlib/Algebra/Algebra/Equiv.lean

@@ -83,13 +83,18 @@ end AlgEquivClass
 
 namespace AlgEquiv
 
-variable {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁}
+universe uR  uA₁ uA₂ uA₃ uA₁' uA₂' uA₃'
+variable {R : Type uR}
+variable {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃}
+variable {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'}
 
 section Semiring
 
 variable [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃]
+variable [Semiring A₁'] [Semiring A₂'] [Semiring A₃']
 
 variable [Algebra R A₁] [Algebra R A₂] [Algebra R A₃]
+variable [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃']
 
 variable (e : A₁ ≃ₐ[R] A₂)
 
@@ -438,9 +443,8 @@ theorem rightInverse_symm (e : A₁ ≃ₐ[R] A₂) : Function.RightInverse e.sy
 
 /-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'`, then the type of maps
 `A₁ →ₐ[R] A₂` is equivalent to the type of maps `A₁' →ₐ[R] A₂'`. -/
-def arrowCongr {A₁' A₂' : Type*} [Semiring A₁'] [Semiring A₂'] [Algebra R A₁'] [Algebra R A₂']
-    (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂')
-    where
+@[simps apply]
+def arrowCongr (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') : (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂') where
   toFun f := (e₂.toAlgHom.comp f).comp e₁.symm.toAlgHom
   invFun f := (e₂.symm.toAlgHom.comp f).comp e₁.toAlgHom
   left_inv f := by
@@ -451,8 +455,7 @@ def arrowCongr {A₁' A₂' : Type*} [Semiring A₁'] [Semiring A₂'] [Algebra
     simp only [← AlgHom.comp_assoc, comp_symm, AlgHom.id_comp, AlgHom.comp_id]
 #align alg_equiv.arrow_congr AlgEquiv.arrowCongr
 
-theorem arrowCongr_comp {A₁' A₂' A₃' : Type*} [Semiring A₁'] [Semiring A₂'] [Semiring A₃']
-    [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂')
+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
@@ -468,22 +471,52 @@ theorem arrowCongr_refl : arrowCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A
 #align alg_equiv.arrow_congr_refl AlgEquiv.arrowCongr_refl
 
 @[simp]
-theorem arrowCongr_trans {A₁' A₂' A₃' : Type*} [Semiring A₁'] [Semiring A₂'] [Semiring A₃']
-    [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂')
+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₂') := by
   ext
   rfl
 #align alg_equiv.arrow_congr_trans AlgEquiv.arrowCongr_trans
 
 @[simp]
-theorem arrowCongr_symm {A₁' A₂' : Type*} [Semiring A₁'] [Semiring A₂'] [Algebra R A₁']
-    [Algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :
+theorem arrowCongr_symm (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') :
     (arrowCongr e₁ e₂).symm = arrowCongr e₁.symm e₂.symm := by
   ext
   rfl
 #align alg_equiv.arrow_congr_symm AlgEquiv.arrowCongr_symm
 
+/-- If `A₁` is equivalent to `A₂` and `A₁'` is equivalent to `A₂'`, then the type of maps
+`A₁ ≃ₐ[R] A₁'` is equivalent to the type of maps `A₂ ≃ ₐ[R] A₂'`.
+
+This is the `AlgEquiv` version of `AlgEquiv.arrowCongr`. -/
+@[simps apply]
+def equivCongr (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') : (A₁ ≃ₐ[R] A₁') ≃ A₂ ≃ₐ[R] A₂' where
+  toFun ψ := e.symm.trans (ψ.trans e')
+  invFun ψ := e.trans (ψ.trans e'.symm)
+  left_inv ψ := by
+    ext
+    simp_rw [trans_apply, symm_apply_apply]
+  right_inv ψ := by
+    ext
+    simp_rw [trans_apply, apply_symm_apply]
+
+@[simp]
+theorem equivCongr_refl : equivCongr AlgEquiv.refl AlgEquiv.refl = Equiv.refl (A₁ ≃ₐ[R] A₁') := by
+  ext
+  rfl
+
+@[simp]
+theorem equivCongr_symm (e : A₁ ≃ₐ[R] A₂) (e' : A₁' ≃ₐ[R] A₂') :
+    (equivCongr e e').symm = equivCongr e.symm e'.symm :=
+  rfl
+
+@[simp]
+theorem equivCongr_trans (e₁₂ : A₁ ≃ₐ[R] A₂) (e₁₂' : A₁' ≃ₐ[R] A₂')
+    (e₂₃ : A₂ ≃ₐ[R] A₃) (e₂₃' : A₂' ≃ₐ[R] A₃') :
+    (equivCongr e₁₂ e₁₂').trans (equivCongr e₂₃ e₂₃') =
+      equivCongr (e₁₂.trans e₂₃) (e₁₂'.trans e₂₃') :=
+  rfl
+
 /-- If an algebra morphism has an inverse, it is an algebra isomorphism. -/
 def ofAlgHom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = AlgHom.id R A₂)
     (h₂ : g.comp f = AlgHom.id R A₁) : A₁ ≃ₐ[R] A₂ :=
@@ -527,20 +560,13 @@ theorem ofBijective_apply {f : A₁ →ₐ[R] A₂} {hf : Function.Bijective f}
 #align alg_equiv.of_bijective_apply AlgEquiv.ofBijective_apply
 
 /-- Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence. -/
--- Porting note: writing the `@[simps apply]`-generated lemma by hand
--- Maybe fixed by the changes in #2435?
+@[simps apply]
 def toLinearEquiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂ :=
   { e with
     toFun := e
     map_smul' := e.map_smul
     invFun := e.symm }
 #align alg_equiv.to_linear_equiv AlgEquiv.toLinearEquiv
-
--- Porting note: writing the `@[simps apply]`-generated lemma by hand
--- Maybe fixed by the changes in #2435?
-@[simp]
-theorem toLinearEquiv_apply : e.toLinearEquiv x = e x :=
-  rfl
 #align alg_equiv.to_linear_equiv_apply AlgEquiv.toLinearEquiv_apply
 
 @[simp]
@@ -675,17 +701,14 @@ theorem mul_apply (e₁ e₂ : A₁ ≃ₐ[R] A₁) (x : A₁) : (e₁ * e₂) x
   rfl
 #align alg_equiv.mul_apply AlgEquiv.mul_apply
 
-/-- An algebra isomorphism induces a group isomorphism between automorphism groups -/
+/-- An algebra isomorphism induces a group isomorphism between automorphism groups.
+
+This is a more bundled version of `AlgEquiv.equivCongr`. -/
 @[simps apply]
 def autCongr (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂ where
+  __ := equivCongr ϕ ϕ
   toFun ψ := ϕ.symm.trans (ψ.trans ϕ)
   invFun ψ := ϕ.trans (ψ.trans ϕ.symm)
-  left_inv ψ := by
-    ext
-    simp_rw [trans_apply, symm_apply_apply]
-  right_inv ψ := by
-    ext
-    simp_rw [trans_apply, apply_symm_apply]
   map_mul' ψ χ := by
     ext
     simp only [mul_apply, trans_apply, symm_apply_apply]

Mathlib/Algebra/Algebra/Opposite.lean

@@ -15,10 +15,13 @@ import Mathlib.Algebra.Ring.Opposite
 * `MulOpposite.instAlgebra`: the algebra on `Aᵐᵒᵖ`
 * `AlgHom.op`/`AlgHom.unop`: simultaneously convert the domain and codomain of a morphism to the
   opposite algebra.
+* `AlgHom.opComm`: swap which side of a morphism lies in the opposite algebra.
 * `AlgEquiv.op`/`AlgEquiv.unop`: simultaneously convert the source and target of an isomorphism to
   the opposite algebra.
+* `AlgEquiv.opOp`: any algebra is isomorphic to the opposite of its opposite.
 * `AlgEquiv.toOpposite`: in a commutative algebra, the opposite algebra is isomorphic to the
   original algebra.
+* `AlgEquiv.opComm`: swap which side of an isomorphism lies in the opposite algebra.
 -/
 
 
@@ -51,6 +54,19 @@ theorem algebraMap_apply (c : R) : algebraMap R Aᵐᵒᵖ c = op (algebraMap R
 
 end MulOpposite
 
+namespace AlgEquiv
+variable (R A)
+
+/-- An algebra is isomorphic to the opposite of its opposite. -/
+@[simps!]
+def opOp : A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ where
+  __ := RingEquiv.opOp A
+  commutes' _ := rfl
+
+@[simp] theorem toRingEquiv_opOp : (opOp R A : A ≃+* Aᵐᵒᵖᵐᵒᵖ) = RingEquiv.opOp A := rfl
+
+end AlgEquiv
+
 namespace AlgHom
 
 /--
@@ -109,6 +125,11 @@ abbrev unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B) := AlgHom.op
 theorem toRingHom_unop (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) : f.unop.toRingHom = RingHom.unop f.toRingHom :=
   rfl
 
+/-- Swap the `ᵐᵒᵖ` on an algebra hom to the opposite side. -/
+@[simps!]
+def opComm : (A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B) :=
+  AlgHom.op.trans <| AlgEquiv.refl.arrowCongr (AlgEquiv.opOp R B).symm
+
 end AlgHom
 
 namespace AlgEquiv
@@ -144,6 +165,11 @@ theorem toRingEquiv_unop (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :
     (AlgEquiv.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv :=
   rfl
 
+/-- Swap the `ᵐᵒᵖ` on an algebra isomorphism to the opposite side. -/
+@[simps!]
+def opComm : (A ≃ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ ≃ₐ[R] B) :=
+  AlgEquiv.op.trans <| AlgEquiv.refl.equivCongr (opOp R B).symm
+
 end AlgEquiv
 
 end Semiring

Mathlib/Algebra/Group/Opposite.lean

@@ -570,6 +570,13 @@ def MonoidHom.unop {M N} [MulOneClass M] [MulOneClass N] : (Mᵐᵒᵖ →* Nᵐ
 #align monoid_hom.unop MonoidHom.unop
 #align add_monoid_hom.unop AddMonoidHom.unop
 
+/-- A monoid is isomorphic to the opposite of its opposite. -/
+@[to_additive (attr := simps!)
+      "A additive monoid is isomorphic to the opposite of its opposite."]
+def MulEquiv.opOp (M : Type*) [Mul M] : M ≃* Mᵐᵒᵖᵐᵒᵖ where
+  __ := MulOpposite.opEquiv.trans MulOpposite.opEquiv
+  map_mul' _ _ := rfl
+
 /-- An additive homomorphism `M →+ N` can equivalently be viewed as an additive homomorphism
 `Mᵐᵒᵖ →+ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
 @[simps]

Mathlib/Algebra/Ring/Equiv.lean

@@ -402,6 +402,12 @@ protected def unop {α β} [Add α] [Mul α] [Add β] [Mul β] : αᵐᵒᵖ ≃
   RingEquiv.op.symm
 #align ring_equiv.unop RingEquiv.unop
 
+/-- A ring is isomorphic to the opposite of its opposite. -/
+@[simps!]
+def opOp (R : Type*) [Add R] [Mul R] : R ≃+* Rᵐᵒᵖᵐᵒᵖ where
+  __ := MulEquiv.opOp R
+  map_add' _ _ := rfl
+
 section NonUnitalCommSemiring
 
 variable (R) [NonUnitalCommSemiring R]