English
There is a canonical linear equivalence between DirectLimit G f ⊗ M and DirectLimit (G ⊗ M) (f ▷ M).
Русский
Существует каноническое линейное эквивалентное отображение между DirectLimit G f ⊗ M и DirectLimit (G ⊗ M) (f ▷ M).
LaTeX
$$$\text{directLimitLeft}:\ DirectLimit G f \otimes_R M \simeq_\ell DirectLimit (G \otimes_R M) (f \triangleright M)$$$
Lean4
/-- For any element `x` of `M ⊗[R] N`, there exists a (finite) multiset `{ (m_i, n_i) }`
of `M × N`, such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`. -/
theorem exists_multiset (x : M ⊗[R] N) : ∃ S : Multiset (M × N), x = (S.map fun i ↦ i.1 ⊗ₜ[R] i.2).sum := by
induction x with
| zero => exact ⟨0, by simp⟩
| tmul x y => exact ⟨{(x, y)}, by simp⟩
| add x y hx hy =>
obtain ⟨Sx, hx⟩ := hx
obtain ⟨Sy, hy⟩ := hy
exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩
