English
There is an order isomorphism between Subring(R) and Subring(R^op) given by S ↦ S^{op} and its inverse S ↦ S^{unop}. This maps inclusions to inclusions preserving order.
Русский
Существует упорядоченное изоморождение между подкольцами кольца R и подкольцами противоположного кольца R^op, задаваемое S ↦ S^{op} и обратное S ↦ S^{unop}, сохраняющее порядок inclusion.
LaTeX
$$$\mathrm{op}: \mathrm{Subring}(R) \to \mathrm{Subring}(R^{op})\ \text{and its inverse}\ \mathrm{unop}: \mathrm{Subring}(R^{op}) \to \mathrm{Subring}(R)\ \text{form an order isomorphism}$$$
Lean4
/-- A subring `S` of `R` determines a subring `S.op` of the opposite ring `Rᵐᵒᵖ`. -/
@[simps]
def opEquiv : Subring R ≃o Subring Rᵐᵒᵖ where
toFun := Subring.op
invFun := Subring.unop
left_inv := unop_op
right_inv := op_unop
map_rel_iff' := op_le_op_iff
