From 55110dd53ae81a737489ebf1cc5a3f41f18135e0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 4 Aug 2023 11:31:53 +0000 Subject: [PATCH] tweak --- src/for_mathlib/algebra/algebra/opposite.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/for_mathlib/algebra/algebra/opposite.lean b/src/for_mathlib/algebra/algebra/opposite.lean index e9e98a884..53c3086ba 100644 --- a/src/for_mathlib/algebra/algebra/opposite.lean +++ b/src/for_mathlib/algebra/algebra/opposite.lean @@ -66,6 +66,8 @@ protected def unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B) := al end alg_hom +namespace alg_equiv + /-- An algebra iso `A ≃ₐ[R] B` can equivalently be viewed as an algebra iso `αᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/ @[simps] @@ -79,6 +81,12 @@ def alg_equiv.op : (A ≃ₐ[R] B) ≃ (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) := left_inv := λ f, alg_equiv.ext $ λ a, rfl, right_inv := λ f, alg_equiv.ext $ λ a, rfl } +/-- The 'unopposite' of an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. Inverse to `alg_equiv.op`. -/ +@[simp] +protected def unop : (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ (A ≃ₐ[R] B) := alg_equiv.op.symm + +end alg_equiv + /-- The double opposite is isomorphic as an algebra to the original type. -/ @[simps] def mul_opposite.op_op_alg_equiv : Aᵐᵒᵖᵐᵒᵖ ≃ₐ[R] A :=