English
Under the opposite equivalence, the image of a product of submodules reverses the factors: map_op_mul(M,N) = map_op_mul(N,M) up to the order swap.
Русский
Через линейное выпукление противоположности образ произведения подмодулов меняет порядок факторов:
LaTeX
$$$\\mathrm{map\\,op}\\,(M \\cdot N) = \\mathrm{map\\,op}\\,N \\cdot \\mathrm{map\\,op}\\,M$$$
Lean4
theorem map_op_mul :
map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M :=
by
apply le_antisymm
· simp_rw [map_le_iff_le_comap]
refine mul_le.2 fun m hm n hn => ?_
rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
change op n * op m ∈ _
exact mul_mem_mul hn hm
· refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
rw [Submodule.mem_map_equiv] at hm hn ⊢
exact mul_mem_mul hn hm
