Documentation

Mathlib.LinearAlgebra.TensorProduct.Finiteness

Some finiteness results of tensor product #

This file contains some finiteness results of tensor product.

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 = iS, 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.