English
An algebra equivalence can be transported to opposite sides via the op operation.
Русский
Алгебраическое эквивалентное отображение можно перенести на противоположную сторону через операцию op.
LaTeX
$$op : (A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ$$
Lean4
/-- An algebra iso `A ≃ₐ[R] B` can equivalently be viewed as an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`.
This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps!]
def op : (A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ
where
toFun f := { RingEquiv.op f.toRingEquiv with commutes' := fun r => MulOpposite.unop_injective <| f.commutes r }
invFun f := { RingEquiv.unop f.toRingEquiv with commutes' := fun r => MulOpposite.op_injective <| f.commutes r }
