English
If for every finitely generated submodule M' of M, M' ≤ M and M'.FG, we have M' LinearDisjoint N, then M LinearDisjoint N.
Русский
Если для каждого конечноблочного подмодуля M' подмодуля M выполняется линейная несовместность с N, то M и N несостоятельны.
LaTeX
$$∀ M' ≤ M, M'.FG → M'.LinearDisjoint N → M.LinearDisjoint N$$
Lean4
/-- If for any finitely generated submodules `M'` of `M`, `M'` and `N` are linearly disjoint,
then `M` and `N` themselves are linearly disjoint. -/
theorem of_linearDisjoint_fg_left (H : ∀ M' : Submodule R S, M' ≤ M → M'.FG → M'.LinearDisjoint N) :
M.LinearDisjoint N :=
(linearDisjoint_iff _ _).2 fun x y hxy ↦
by
obtain ⟨M', hM, hFG, h⟩ := TensorProduct.exists_finite_submodule_left_of_setFinite' { x, y } (Set.toFinite _)
rw [Module.Finite.iff_fg] at hFG
obtain ⟨x', hx'⟩ := h (show x ∈ { x, y } by simp)
obtain ⟨y', hy'⟩ := h (show y ∈ { x, y } by simp)
rw [← hx', ← hy']; congr
exact (H M' hM hFG).injective (by simp [← mulMap_comp_rTensor _ hM, hx', hy', hxy])
