English
There is a canonical operation op on AlgHom to flip sides.
Русский
Существует каноническая операция op на AlgHom, переворачивающая стороны.
LaTeX
$$op : (A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ)$$
Lean4
/-- An algebra hom `A →ₐ[R] B` can equivalently be viewed as an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`.
This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps!]
protected def op : (A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ)
where
toFun f := { RingHom.op f.toRingHom with commutes' := fun r => unop_injective <| f.commutes r }
invFun f := { RingHom.unop f.toRingHom with commutes' := fun r => op_injective <| f.commutes r }
