Additional facts about modules over algebras. #
def
linear_map.restrict_scalars_linear_map
(k : Type u_1)
[comm_semiring k]
(A : Type u_2)
[semiring A]
[algebra k A]
(M : Type u_3)
[add_comm_monoid M]
[module k M]
[module A M]
[is_scalar_tower k A M]
(N : Type u_4)
[add_comm_monoid N]
[module k N]
[module A N]
[is_scalar_tower k A N] :
Restriction of scalars for linear maps between modules over a k
-algebra is itself k
-linear.
Equations
@[simp]
theorem
linear_map.restrict_scalars_linear_map_apply
(k : Type u_1)
[comm_semiring k]
(A : Type u_2)
[semiring A]
[algebra k A]
(M : Type u_3)
[add_comm_monoid M]
[module k M]
[module A M]
[is_scalar_tower k A M]
(N : Type u_4)
[add_comm_monoid N]
[module k N]
[module A N]
[is_scalar_tower k A N]
(fₗ : M →ₗ[A] N) :
⇑(linear_map.restrict_scalars_linear_map k A M N) fₗ = linear_map.restrict_scalars k fₗ