opEquiv — Mathlib

English

There is an order isomorphism between Subalgebra R A and Subalgebra R Aᵐᵒᵖ, given by op and unop.

Русский

Существует упорядоченное изоморфное отображение между Subalgebra R A и Subalgebra R A^{op}, задаваемое операциями op и unop.

LaTeX

$$$ \operatorname{opEquiv} : \mathrm{Subalgebra}(R,A) \simeq_{\mathrm{ord}} \mathrm{Subalgebra}(R, A^{\mathrm{op}}). $$$

Lean4

/-- A subalgebra `S` of `A / R` determines a subalgebra `S.op` of the opposite ring `Aᵐᵒᵖ / R`. -/
@[simps]
def opEquiv : Subalgebra R A ≃o Subalgebra R Aᵐᵒᵖ
    where
  toFun := Subalgebra.op
  invFun := Subalgebra.unop
  left_inv := unop_op
  right_inv := op_unop
  map_rel_iff' := op_le_op_iff

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