Scalar extension of images and powers of submodules

Extension of scalars commutes with taking images of submodules under linear maps, and preserves powers of submodules of an algebra. The latter applies, in particular, to the homogeneous pieces of tensor and exterior algebras, defined as powers of their generators.

@[simp]

theorem Submodule.baseChange_map {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (p : Submodule R M) : baseChange A (map f p) = map (LinearMap.baseChange A f) (baseChange A p)

Extension of scalars commutes with taking the image of a submodule under a linear map.

@[simp]

theorem LinearMap.baseChange_range {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) : Submodule.baseChange A f.range = (baseChange A f).range

Extension of scalars commutes with taking the range of a linear map.

@[simp]

theorem Submodule.baseChange_pow {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] (p : Submodule R B) (n : ℕ) : baseChange A (p ^ n) = baseChange A p ^ n

Extension of scalars preserves powers of submodules of an algebra.