English
There is a natural isomorphism (a direct limit) between the tensor product of a direct limit with M and the direct limit of tensoring each component with M, compatible with the system f.
Русский
Существует естественное изоморфизмное соответствие между прямым пределом G и модулем M и прямым пределом тензорного произведения, полученным по компонентам, совместимо с переходными отображениями системы f.
LaTeX
$$$\text{toDirectLimit}:\ DirectLimit G f \otimes_R M \to_\ell[R] DirectLimit (G \cdot \otimes_R M) (f \triangleright M)$$$
Lean4
/-- the map `(limᵢ Gᵢ) ⊗ M → limᵢ (Gᵢ ⊗ M)` from the bilinear map `limᵢ Gᵢ → M → limᵢ (Gᵢ ⊗ M)` given
by the family of maps `Gᵢ → M → limᵢ (Gᵢ ⊗ M)` where `gᵢ ↦ m ↦ [gᵢ ⊗ m]`
-/
noncomputable def toDirectLimit : DirectLimit G f ⊗[R] M →ₗ[R] DirectLimit (G · ⊗[R] M) (f ▷ M) :=
TensorProduct.lift <|
Module.DirectLimit.lift _ _ _ _
(fun i ↦ (TensorProduct.mk R _ _).compr₂ (of R ι _ (fun _i _j h ↦ (f _ _ h).rTensor M) i)) fun _ _ _ g ↦
DFunLike.ext _ _ (of_f (G := (G · ⊗[R] M)) (x := g ⊗ₜ ·))
