English
Tensoring a directed system on the right preserves directedness: the system P_i ⊗ N is directed with connecting maps given by rTensor N (Submodule.inclusion).
Русский
Тензорирование направленной системы справа сохраняет направленность: система P_i ⊗ N направлена, переходы — rTensor N (Submodule.inclusion).
LaTeX
$$$\\text{DirectedSystem}(P_i, f_i^j) \\Rightarrow \\text{DirectedSystem}(P_i ⊗_R N, rTensor N (f_i^j)).$$$
Lean4
/-- Given a directed system of `R`-modules, tensoring it on the right gives a directed system -/
theorem rTensor {ι : 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 ↦ (F i) ⊗[R] N) (fun _ _ h ↦ rTensor N (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, ← rTensor_comp]
apply DFunLike.congr_fun
ext p n
simp [D.map_map]
