Theorems · Theorem · commutative algebra

Submodule.exists_fg_le_eq_rTensor_subtype

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R N M),
  ∃ J, ∃ (_ : J.FG), ∃ y, x = (LinearMap.rTensor M J.subtype) y

Every x : N ⊗ M is the image of some y : J ⊗ M, where J is a finitely generated submodule of N, under the tensor product of the inclusion J → N and the identity M → M.

Defined in

Mathlib.RingTheory.TensorProduct.Finite

Cited by

2 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule