English
Variation of both-left and right-submodule finite-submodule statements for maps between submodules.
Русский
Вариации левой и правой версий конечного подмодуля для отображений между подмодулями.
LaTeX
$$$\exists M', N', hM, hN,\ Module.Finite R M',\ Module.Finite R N',\ s \subseteq \mathrm{range}( TensorProduct.map (inclusion hM) (inclusion hN) )$$$
Lean4
/-- Variation of `TensorProduct.exists_finite_submodule_of_setFinite` where `M` and `N` are
already submodules. -/
theorem exists_finite_submodule_of_setFinite' (s : Set (M₁ ⊗[R] N₁)) (hs : s.Finite) :
∃ (M' : Submodule R M) (N' : Submodule R N) (hM : M' ≤ M₁) (hN : N' ≤ N₁),
Module.Finite R M' ∧ Module.Finite R N' ∧ s ⊆ LinearMap.range (TensorProduct.map (inclusion hM) (inclusion hN)) :=
by
obtain ⟨M', N', _, _, h⟩ := exists_finite_submodule_of_setFinite s hs
have hM := map_subtype_le M₁ M'
have hN := map_subtype_le N₁ N'
refine ⟨_, _, hM, hN, .map _ _, .map _ _, ?_⟩
rw [mapIncl, show M'.subtype = inclusion hM ∘ₗ M₁.subtype.submoduleMap M' by ext; simp,
show N'.subtype = inclusion hN ∘ₗ N₁.subtype.submoduleMap N' by ext; simp, map_comp] at h
exact h.trans (LinearMap.range_comp_le_range _ _)
