English
There exists a canonical ring isomorphism between Submodule R Aᵐᵒᵖ and the opposite of Submodule R A, given by transporting submodules along the linear equivalence A ≃ₗ[R] Aᵐᵒᵖ.
Русский
Существует каноническое кольцевое изоморфизм между Submodule R Aᵐᵒᵖ и противолежащим кольцом Submodule R A, получаемый перенесением подмодулей вдоль линейного эквивалента A ≃ₗ[R] Aᵐᵒᵖ.
LaTeX
$$$\mathrm{equivOpposite} : \mathrm{Submodule}(R, A^{\mathrm{op}}) \cong^+_* (\mathrm{Submodule}(R,A))^{\mathrm{op}}$$$
Lean4
/-- The ring of submodules of the opposite algebra is isomorphic to the opposite ring of
submodules. -/
@[simps apply symm_apply]
def equivOpposite : Submodule R Aᵐᵒᵖ ≃+* (Submodule R A)ᵐᵒᵖ
where
toFun p := op <| p.comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ)
invFun p := p.unop.comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A)
left_inv _ := SetLike.coe_injective <| rfl
right_inv _ := unop_injective <| SetLike.coe_injective rfl
map_add' p q := by simp [comap_equiv_eq_map_symm, ← op_add]
map_mul' _ _ := congr_arg op <| comap_op_mul _ _
