English
Under the unop map, power commuting holds: map (opLinearEquiv R).symm (M^n) = (map (opLinearEquiv R).symm M)^n.
Русский
При отображении обратно через унарный оператор сохраняется коммутирование степеней: map (opLinearEquiv R)^{-1}(M^n) = map (opLinearEquiv R)^{-1}(M)^n.
LaTeX
$$$\mathrm{map}(\mathrm{opLinearEquiv}_R).\mathrm{symm.toLinearMap}(\mathrm{M}^{n}) = (\mathrm{map}(\mathrm{opLinearEquiv}_R).\mathrm{symm.toLinearMap}(\mathrm{M}))^{n}$$$
Lean4
theorem map_unop_pow (n : ℕ) (M : 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) M ^ n :=
by rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]
