English
The canonical maps from components to the direct limit are injective under the directed-system hypotheses.
Русский
Канонические вложения компонент в прямой предел инъективны при заданных условиях направленной системы.
LaTeX
$$$\\forall i,\\; (\\mathrm{of}\\;G\\;f'\\;i)\\;\\text{injective}.$$$
Lean4
theorem exists_rTensor_fg_inclusion_eq {N : Submodule R P} (hN : N.FG) {x y : N ⊗[R] M}
(eq : N.subtype.rTensor M x = N.subtype.rTensor M y) :
∃ N', N'.FG ∧ ∃ h : N ≤ N', (N.inclusion h).rTensor M x = (N.inclusion h).rTensor M y := by
classical
lift N to { N : Submodule R P // N.FG } using hN
apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
apply_fun directLimitLeft _ _ at eq
simp_rw [← LinearMap.rTensor_comp_apply, ←
(LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
exact ⟨_, N'.2, le, eq⟩
