Skip to content

Commit

Permalink
tweak
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Aug 4, 2023
1 parent 88af79f commit 55110dd
Showing 1 changed file with 8 additions and 0 deletions.
8 changes: 8 additions & 0 deletions src/for_mathlib/algebra/algebra/opposite.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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 :=
Expand Down

0 comments on commit 55110dd

Please sign in to comment.