exists_finite_submodule_left_of_setFinite'

English

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

Русский

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

LaTeX

$$$\exists M', hM',\ hM' ≤ M_1, s ⊆ range (M' .subtype. rTensor N_1)$$$

Lean4

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

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