opComm — Mathlib

English

There is a natural correspondence between algebra isomorphisms A ≃ B^op and A^op ≃ B, given by flipping the opposite side.

Русский

Существует естественная двухсторонняя связь между изоморфизмами алгебр A ≃ B^op и A^op ≃ B, полученная обменом стороны противоположности.

LaTeX

$$$ \\operatorname{opComm}: (A \\simeq_{R} B^{\\mathrm{op}}) \\simeq (A^{\\mathrm{op}} \\simeq_{R} B) $$$

Lean4

/-- Swap the `ᵐᵒᵖ` on an algebra isomorphism to the opposite side. -/
@[simps!]
def opComm : (A ≃ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ ≃ₐ[R] B) :=
  AlgEquiv.op.trans <| AlgEquiv.refl.equivCongr (opOp R B).symm

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