English
If s is a finite subset of I ⊗M for a submodule I of N, there exists J ≤ N with J FG and s ⊆ range(rTensor M (J.inclusion (hle))) for some hle: J ≤ I.
Русский
Пусть s — конечная подмножество внутри I ⊗M, тогда существует J ≤ N, FG, и указанное включение, так что s лежит в диапазоне тензорного отображения.
LaTeX
$$$\exists J \ (J.FG) (hle : J \le I), s \subseteq \mathrm{range}\bigl( rTensor M (J.inclusion hle) \bigr).$$$
Lean4
/-- Every `x : I ⊗ M` is the image of some `y : J ⊗ M`, where `J ≤ I` is finitely generated,
under the tensor product of `J.inclusion ‹J ≤ I› : J → I` and the identity `M → M`. -/
theorem exists_fg_le_eq_rTensor_inclusion (x : I ⊗ M) :
∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : J ⊗ M), x = rTensor M (J.inclusion hle) y :=
by
obtain ⟨J, fg, y, rfl⟩ := exists_fg_le_eq_rTensor_subtype x
refine ⟨J.map I.subtype, fg.map _, I.map_subtype_le J, rTensor M (I.subtype.submoduleMap J) y, ?_⟩
rw [← LinearMap.rTensor_comp_apply]; rfl
