English
The directed system obtained by lTensor (tensoring on the left) from FG-submodules of N yields a directed system of M ⊗_R F_i with connecting maps given by lTensor M (Submodule.inclusion).
Русский
Направленная система, полученная через lTensor (левая тензоризация), из FG-подмодулей N образует направленную систему M ⊗_R F_i с переходами lTensor M (Submodule.inclusion).
LaTeX
$$$\\text{DirectedSystem}(\\{ Q\\mid Q.FG \\}, M \\otimes_R Q, Q≤Q' \\mapsto \\text{lTensor}(M,\\;\\text{inclusion})).$$$
Lean4
/-- Given a directed system of `R`-modules, tensoring it on the left gives a directed system -/
theorem lTensor {ι : Type*} [Preorder ι] {F : ι → Type*} [∀ i, AddCommMonoid (F i)] [∀ i, Module R (F i)]
{f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j} (D : DirectedSystem F (fun _ _ h ↦ f h)) :
DirectedSystem (fun i ↦ M ⊗[R] (F i)) (fun _ _ h ↦ lTensor M (f h))
where
map_self i
t := by
rw [← id_apply (R := R) t]
apply DFunLike.congr_fun
ext m n
simp [D.map_self]
map_map {i j k} h h'
t := by
rw [← comp_apply, ← lTensor_comp]
apply DFunLike.congr_fun
ext p n
simp [D.map_map]
