English
For M,N ⊆ Aᵐᵒᵖ, comap along the inverse op-equivalence distributes: comap op.symm (M*N) = comap op.symm N * comap op.symm M.
Русский
Для M,N ⊆ Aᵐᵒᵖ, comap по обратному отображению распадается: comap op.symm (M*N) = comap op.symm N * comap op.symm M.
LaTeX
$$$\\mathrm{comap}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) (M \\cdot N) = \\mathrm{comap}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) N \\cdot \\mathrm{comap}\\;\\bigl(\\mathrm{op\\,symm}\\bigr) M$$$
Lean4
theorem comap_op_mul (M N : Submodule R Aᵐᵒᵖ) :
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M :=
by simp_rw [comap_equiv_eq_map_symm, map_unop_mul]
