English
Let f be a system of linear maps G_i → G_j along i ≤ j, and let M be a module. Then the canonical map from the direct limit of G to the direct limit of G ⊗ M commutes with taking tmul by m ∈ M: applying fromDirectLimit to the element coming from i with g ∈ G_i and m ∈ M yields the element obtained by tensoring g with m after mapping g through f.
Русский
Пусть имеется система линейных отображений G_i → G_j, если i ≤ j, и модуль M. Тогда каноническое отображение из прямого предела G в прямой предел G ⊗ M согласуется с операцией тензорного произведения на m ∈ M: применение fromDirectLimit к элементу, полученному из i и g ∈ G_i, и m ∈ M, даёт элемент, соответствующий g под действием f, тензорно умноженный на m.
LaTeX
$$$\mathrm{fromDirectLimit}(f,M)\bigl(\mathrm{of}\ i\ (g) \otimes m\bigr) = \mathrm{of}\ f\; i\ g \otimes m$$$
Lean4
@[simp]
theorem fromDirectLimit_of_tmul {i : ι} (g : G i) (m : M) :
fromDirectLimit f M (of _ _ _ _ i (g ⊗ₜ m)) = (of _ _ _ f i g) ⊗ₜ m :=
lift_of (G := (G · ⊗[R] M)) _ _ (g ⊗ₜ m)
