exists_finite_submodule_right_of_setFinite'

English

Variation with submodules fixed on the right, giving a right finite-submodule result.

Русский

Вариант справа с фиксированными подмодулями справа, дающий правый конечный результат.

LaTeX

$$$\exists N', hN,\ Module.Finite R N',\ s ⊆ range (TensorProduct.map (inclusion hM) (inclusion hN))$$$

Lean4

/-- Variation of `TensorProduct.exists_finite_submodule_right_of_setFinite` where `M` and `N` are
already submodules. -/
theorem exists_finite_submodule_right_of_setFinite' (s : Set (M₁ ⊗[R] N₁)) (hs : s.Finite) :
    ∃ (N' : Submodule R N) (hN : N' ≤ N₁), Module.Finite R N' ∧ s ⊆ LinearMap.range ((inclusion hN).lTensor M₁) :=
  by
  obtain ⟨_, N', _, hN, _, hfin, h⟩ := exists_finite_submodule_of_setFinite' s hs
  refine ⟨N', hN, hfin, ?_⟩
  rw [← LinearMap.lTensor_comp_rTensor] at h
  exact h.trans (LinearMap.range_comp_le_range _ _)

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