exists_fg_le_subset_range_rTensor_subtype

English

For any x in N ⊗M, there exists a finitely generated submodule J ≤ N and y ∈ J ⊗M such that x = rTensor M J.subtype y.

Русский

Для любого x в N ⊗ M найдется FG-подмодуль J ⊆ N и элемент y ∈ J ⊗ M с равенством x = rTensor M J.subtype y.

LaTeX

$$$\exists J \ (J.FG) (y) \in J ⊗R M \text{ with } x = rTensor M J.subtype y.$$$

Lean4

theorem exists_fg_le_subset_range_rTensor_subtype (s : Set (N ⊗[R] M)) (hs : s.Finite) :
    ∃ (J : Submodule R N) (_ : J.FG), s ⊆ LinearMap.range (rTensor M J.subtype) :=
  by
  choose J fg y eq using exists_fg_le_eq_rTensor_subtype (R := R) (M := M) (N := N)
  rw [← Set.finite_coe_iff] at hs
  refine
    ⟨⨆ x : s, J x, fg_iSup _ fun _ ↦ fg _, fun x hx ↦
      ⟨rTensor M (inclusion <| le_iSup _ ⟨x, hx⟩) (y x), .trans ?_ (eq x).symm⟩⟩
  rw [← comp_apply, ← rTensor_comp]; rfl

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