exists_finite_submodule_right_of_setFinite

English

Variant where N is a submodule and a finite submodule is found on the right, with a suitable range containment.

Русский

Вариант, где N является подмодулем, найден конечный правый подмодуль с подходящим вложением образа.

LaTeX

$$$\exists N', N' \le N,\ Module.Finite R N',\ s \subseteq \mathrm{range}( M \otimes (N'.subtype) )$$$

Lean4

/-- For a finite subset `s` of `M ⊗[R] N`, there exists a finitely generated
submodule `N'` of `N`, such that `s` is contained in the image
of `M ⊗[R] N'` in `M ⊗[R] N`. -/
theorem exists_finite_submodule_right_of_setFinite (s : Set (M ⊗[R] N)) (hs : s.Finite) :
    ∃ N' : Submodule R N, Module.Finite R N' ∧ s ⊆ LinearMap.range (N'.subtype.lTensor M) :=
  by
  obtain ⟨_, N', _, hfin, h⟩ := exists_finite_submodule_of_setFinite s hs
  refine ⟨N', hfin, ?_⟩
  rw [mapIncl, ← LinearMap.lTensor_comp_rTensor] at h
  exact h.trans (LinearMap.range_comp_le_range _ _)

Похожие утверждения