Additional facts about modules over algebras. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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ₗ