directLimitLeft — Mathlib

English

There is a canonical linear equivalence between (lim G) ⊗ M and lim (G ⊗ M) with the appropriate system, establishing that tensoring commutes with direct limits on the left.

Русский

Существует каноническое линейное биективное отображение между (lim G) ⊗ M и lim (G ⊗ M) с нужной системой, показывающее, что тензорирование слева сохраняет прямые пределы.

LaTeX

$$$\text{directLimitLeft}:\ DirectLimit G f \otimes_R M \cong_\ell DirectLimit (\lambda x, G x \otimes_R M) (f \triangleright M)$$$

Lean4

/-- `limᵢ (Gᵢ ⊗ M)` and `(limᵢ Gᵢ) ⊗ M` are isomorphic as modules
-/
noncomputable def directLimitLeft : DirectLimit G f ⊗[R] M ≃ₗ[R] DirectLimit (G · ⊗[R] M) (f ▷ M) :=
  LinearEquiv.ofLinear (toDirectLimit f M) (fromDirectLimit f M) (by ext; simp) (by ext; simp)

Похожие утверждения