opComm — Mathlib

English

Swap the opposite on a morphism using a canonical equivalence.

Русский

Обменять противоположную сторону на морфизме с помощью канонического эквивалента.

LaTeX

$$opComm : (A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B)$$

Lean4

/-- 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

Похожие утверждения