English
A variant of the finite-submodule result where M and N are themselves submodules, giving a finite left-submodule M' and N'.
Русский
Вариант результата о конечном подмодуле, где M и N являются подмодулями, дающий конечный левый подмодуль M' и N'.
LaTeX
$$$\exists M', N', M' \le M, N' \le N,\ Module.Finite R M',\ Module.Finite R N',\ s \subseteq \mathrm{range}( (inclusion\ M').rTensor N )$$$
Lean4
/-- For a finite subset `s` of `M ⊗[R] N`, there are finitely generated
submodules `M'` and `N'` of `M` and `N`, respectively, such that `s` is contained in the image
of `M' ⊗[R] N'` in `M ⊗[R] N`.
In particular, every element of a tensor product lies in the tensor product of some finite
submodules. -/
theorem exists_finite_submodule_of_setFinite (s : Set (M ⊗[R] N)) (hs : s.Finite) :
∃ (M' : Submodule R M) (N' : Submodule R N),
Module.Finite R M' ∧ Module.Finite R N' ∧ s ⊆ LinearMap.range (mapIncl M' N') :=
by
simp_rw [Module.Finite.iff_fg]
induction s, hs using Set.Finite.induction_on with
| empty => exact ⟨_, _, fg_bot, fg_bot, Set.empty_subset _⟩
| @insert a s _ _ ih =>
obtain ⟨M', N', hM', hN', h⟩ := ih
refine TensorProduct.induction_on a ?_ (fun x y ↦ ?_) fun x y hx hy ↦ ?_
· exact ⟨M', N', hM', hN', Set.insert_subset (zero_mem _) h⟩
· refine ⟨_, _, hM'.sup (fg_span_singleton x), hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩
· exact ⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩
· exact range_mapIncl_mono le_sup_left le_sup_left (h hz)
· obtain ⟨M₁', N₁', hM₁', hN₁', h₁⟩ := hx
obtain ⟨M₂', N₂', hM₂', hN₂', h₂⟩ := hy
refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩
· exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.mem_insert x s))
· exact range_mapIncl_mono le_sup_right le_sup_right (h₂ (Set.mem_insert y s))
· exact range_mapIncl_mono le_sup_left le_sup_left (h₁ (Set.subset_insert x s hz))
