Some finiteness results of tensor product

This file contains some finiteness results of tensor product.

• TensorProduct.exists_multiset, TensorProduct.exists_finsupp_left, TensorProduct.exists_finsupp_right, TensorProduct.exists_finset: any element of M ⊗[R] N can be written as a finite sum of pure tensors. See also TensorProduct.span_tmul_eq_top.

• TensorProduct.exists_finite_submodule_left_of_finite, TensorProduct.exists_finite_submodule_right_of_finite, TensorProduct.exists_finite_submodule_of_finite: any finite subset of M ⊗[R] N is contained in M' ⊗[R] N, resp. M ⊗[R] N', resp. M' ⊗[R] N', for some finitely generated submodules M' and N' of M and N, respectively.

• TensorProduct.exists_finite_submodule_left_of_finite', TensorProduct.exists_finite_submodule_right_of_finite', TensorProduct.exists_finite_submodule_of_finite': variation of the above results where M and N are already submodules.

Tags

tensor product, finitely generated

theorem TensorProduct.exists_multiset {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : ∃ (S : Multiset (M × N)), x = (Multiset.map (fun (i : M × N) => i.1 ⊗ₜ[R] i.2) S).sum

For any element x of M ⊗[R] N, there exists a (finite) multiset { (m_i, n_i) } of M × N, such that x is equal to the sum of m_i ⊗ₜ[R] n_i.

theorem TensorProduct.exists_finsupp_left {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : ∃ (S : M →₀ N), x = S.sum fun (m : M) (n : N) => m ⊗ₜ[R] n

For any element x of M ⊗[R] N, there exists a finite subset { (m_i, n_i) } of M × N such that each m_i is distinct (we represent it as an element of M →₀ N), such that x is equal to the sum of m_i ⊗ₜ[R] n_i.

theorem TensorProduct.exists_finsupp_right {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : ∃ (S : N →₀ M), x = S.sum fun (n : N) (m : M) => m ⊗ₜ[R] n

For any element x of M ⊗[R] N, there exists a finite subset { (m_i, n_i) } of M × N such that each n_i is distinct (we represent it as an element of N →₀ M), such that x is equal to the sum of m_i ⊗ₜ[R] n_i.

theorem TensorProduct.exists_finset {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : ∃ (S : Finset (M × N)), x = S.sum fun (i : M × N) => i.1 ⊗ₜ[R] i.2

For any element x of M ⊗[R] N, there exists a finite subset { (m_i, n_i) } of M × N, such that x is equal to the sum of m_i ⊗ₜ[R] n_i.

theorem TensorProduct.exists_finite_submodule_of_finite {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (s : Set (TensorProduct R M N)) (hs : s.Finite) : ∃ (M' : Submodule R M) (N' : Submodule R N), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (TensorProduct.mapIncl M' N'))

For a finite subset s of M ⊗[R] N, there are finitely generated submodules M' and N' of M and N, respectively, such that s is contained in the image of M' ⊗[R] N' in M ⊗[R] N.

theorem TensorProduct.exists_finite_submodule_left_of_finite {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (s : Set (TensorProduct R M N)) (hs : s.Finite) : ∃ (M' : Submodule R M), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor N M'.subtype))

For a finite subset s of M ⊗[R] N, there exists a finitely generated submodule M' of M, such that s is contained in the image of M' ⊗[R] N in M ⊗[R] N.

theorem TensorProduct.exists_finite_submodule_right_of_finite {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (s : Set (TensorProduct R M N)) (hs : s.Finite) : ∃ (N' : Submodule R N), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))

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 TensorProduct.exists_finite_submodule_of_finite' {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ (M' : Submodule R M) (N' : Submodule R N) (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN)))

Variation of TensorProduct.exists_finite_submodule_of_finite where M and N are already submodules.

theorem TensorProduct.exists_finite_submodule_left_of_finite' {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ (M' : Submodule R M) (hM : M' ≤ M₁), Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.range (LinearMap.rTensor (↥N₁) (Submodule.inclusion hM)))

Variation of TensorProduct.exists_finite_submodule_left_of_finite where M and N are already submodules.

theorem TensorProduct.exists_finite_submodule_right_of_finite' {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ (N' : Submodule R N) (hN : N' ≤ N₁), Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor (↥M₁) (Submodule.inclusion hN)))

Variation of TensorProduct.exists_finite_submodule_right_of_finite where M and N are already submodules.