English
For a general F with a suitable algebra-linear structure, a universal compatibility holds: mulMap (M.map f) (N.map f) composed with tensor-map equals f composed with mulMap M N.
Русский
Для общего F с подходящей структурой линейного отображения сохраняется универсальная совместимость: mulMap (M.map f) (N.map f) ∘_tensor_map = f ∘ mulMap M N.
LaTeX
$${\; mulMap (M.map f) (N.map f) \circ\! TensorProduct.map ((f : S →_R[M] T).submoduleMap M) ((f : S →_R[M] T).submoduleMap N) = f \circ mulMap M N }$$
Lean4
theorem mulMap_map_comp_eq {T : Type w} [Semiring T] [Algebra R T] {F : Type*} [FunLike F S T] [AlgHomClass F R S T]
(f : F) :
mulMap (M.map f) (N.map f) ∘ₗ TensorProduct.map ((f : S →ₗ[R] T).submoduleMap M) ((f : S →ₗ[R] T).submoduleMap N) =
f ∘ₗ mulMap M N :=
by
ext
simp only [TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_comp, TensorProduct.curry_apply,
LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, TensorProduct.map_tmul, mulMap_tmul,
LinearMap.coe_coe, map_mul]
rfl
