English
For M,N in Aᵐᵒᵖ, applying the inverse op-linear map to M*N yields N*M after mapping: map (op.symm) (M*N) = map (op.symm) N * map (op.symm) M.
Русский
Для M,N в Aᵐᵒᵖ, применение инверсии оп-линейного отображения к произведению M*N дает N*M: map (op.symm) (M*N) = map (op.symm) N * map (op.symm) M.
LaTeX
$$$\\mathrm{map}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) (M \\cdot N) = \\mathrm{map}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) N \\cdot \\mathrm{map}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) M$$$
Lean4
theorem map_unop_mul (M N : Submodule R Aᵐᵒᵖ) :
map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M :=
have : Function.Injective (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) := LinearEquiv.injective _
map_injective_of_injective this <| by
rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe, LinearEquiv.symm_trans_self,
LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
