English
A variant of the previous statement with simp, giving the same conclusion under simp assumptions.
Русский
Вариант предыдущего утверждения с использованием simp.
LaTeX
$$M.LinearDisjoint N$$
Lean4
/-- If for any finitely generated submodules `N'` of `N`, `M` and `N'` are linearly disjoint,
then `M` and `N` themselves are linearly disjoint. -/
theorem of_linearDisjoint_fg_right (H : ∀ N' : Submodule R S, N' ≤ N → N'.FG → M.LinearDisjoint N') :
M.LinearDisjoint N :=
(linearDisjoint_iff _ _).2 fun x y hxy ↦
by
obtain ⟨N', hN, hFG, h⟩ := TensorProduct.exists_finite_submodule_right_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 N' hN hFG).injective (by simp [← mulMap_comp_lTensor _ hN, hx', hy', hxy])
