Additional facts about modules over algebras.

def LinearMap.restrictScalarsLinearMap (k : Type u_1) [CommSemiring k] (A : Type u_2) [Semiring A] [Algebra k A] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (N : Type u_4) [AddCommMonoid N] [Module k N] [Module A N] [IsScalarTower k A N] : (M →ₗ[A] N) →ₗ[k] M →ₗ[k] N

Restriction of scalars for linear maps between modules over a k-algebra is itself k-linear.

Equations

• LinearMap.restrictScalarsLinearMap k A M N = { toFun := ↑k, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.restrictScalarsLinearMap_apply (k : Type u_1) [CommSemiring k] (A : Type u_2) [Semiring A] [Algebra k A] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (N : Type u_4) [AddCommMonoid N] [Module k N] [Module A N] [IsScalarTower k A N] (fₗ : M →ₗ[A] N) : (LinearMap.restrictScalarsLinearMap k A M N) fₗ = ↑k fₗ