comap_unop_pow — Mathlib

English

For an AlgHom f, the map of submodules commutes with taking powers: map f (M^n) = (map f M)^n.

Русский

Для гомоморфизма f сохраняется возведение подмодулей в степень: map f (M^n) = (map f M)^n.

LaTeX

$$$\mathrm{map}(f^{\mathrm{toLinearMap}})(\mathrm{M}^{n}) = (\mathrm{map}(f^{\mathrm{toLinearMap}})\mathrm{M})^{n}$$$

Lean4

theorem comap_unop_pow (n : ℕ) :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M ^ n) =
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M ^ n :=
  (equivOpposite : Submodule R Aᵐᵒᵖ ≃+* _).symm.map_pow (op M) n

Похожие утверждения