Decomposition of tensor product

In this file, we describe the properties of decomposition under tensor product. Suppose ℳ is a decomposition of an R-module M indexed by a type ι. Given an R-module N, the R-module M ⊗[R] N has a decomposition into pieces fun i ↦ (ℳ i) ⊗[R] N. Given a commutative R-algebra S, the S-module S ⊗[R] M has a decomposition fun i ↦ (ℳ i).baseChange S.

@[instance_reducible]

instance DirectSum.Decomposition.baseChange {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [Decomposition ℳ] [CommSemiring S] [Algebra R S] : Decomposition fun (i : ι) => Submodule.baseChange S (ℳ i)

Equations

• One or more equations did not get rendered due to their size.

theorem DirectSum.toBaseChange_injective {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [Decomposition ℳ] [CommSemiring S] [Algebra R S] (i : ι) : Function.Injective ⇑(Submodule.toBaseChange S (ℳ i))

theorem DirectSum.toBaseChange_bijective {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [Decomposition ℳ] [CommSemiring S] [Algebra R S] (i : ι) : Function.Bijective ⇑(Submodule.toBaseChange S (ℳ i))

def DirectSum.decomposeTensor {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] (i : ι) : Submodule R (TensorProduct R M N)

The submodule of a tensor product corresponding to a decomposition on the left.

Equations

• DirectSum.decomposeTensor ℳ N i = (LinearMap.rTensor N (ℳ i).subtype).range

theorem DirectSum.decomposeTensor_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] {i : ι} : decomposeTensor ℳ N i = (LinearMap.rTensor N (ℳ i).subtype).range

theorem DirectSum.subtype_rTensor_injective {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] [DecidableEq ι] [Decomposition ℳ] (i : ι) : Function.Injective ⇑(LinearMap.rTensor N (ℳ i).subtype)

noncomputable def DirectSum.decomposeTensorEquiv {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] [DecidableEq ι] [Decomposition ℳ] (i : ι) : TensorProduct R (↥(ℳ i)) N ≃ₗ[R] ↥(decomposeTensor ℳ N i)

The linear isomorphism to the submodule from the tensor product with a summand.

Equations

• DirectSum.decomposeTensorEquiv ℳ N i = LinearEquiv.ofInjective (LinearMap.rTensor N (ℳ i).subtype) ⋯

theorem DirectSum.decomposeTensorEquiv_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] [DecidableEq ι] [Decomposition ℳ] {i : ι} (x : TensorProduct R (↥(ℳ i)) N) : (decomposeTensorEquiv ℳ N i) x = ⟨(LinearMap.rTensor N (ℳ i).subtype) x, ⋯⟩

@[simp]

theorem DirectSum.val_decomposeTensorEquiv_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] [DecidableEq ι] [Decomposition ℳ] {i : ι} (x : TensorProduct R (↥(ℳ i)) N) : ↑((decomposeTensorEquiv ℳ N i) x) = (LinearMap.rTensor N (ℳ i).subtype) x

theorem DirectSum.decomposeTensorEquiv_of_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] [DecidableEq ι] [Decomposition ℳ] {i : ι} (x : TensorProduct R (↥(ℳ i)) N) : (congrLinearEquiv fun (i : ι) => decomposeTensorEquiv ℳ N i) ((of (fun (i : ι) => TensorProduct R (↥(ℳ i)) N) i) x) = (of (fun (i : ι) => ↥(decomposeTensor ℳ N i)) i) ((decomposeTensorEquiv ℳ N i) x)

theorem DirectSum.decomposeLinearEquiv_comp_subtype {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [Decomposition ℳ] {i : ι} : ↑(decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype = lof R ι (fun (i : ι) => ↥(ℳ i)) i

theorem DirectSum.coe_decomposeTensor_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) (N : Type u_5) [AddCommMonoid N] [Module R N] [DecidableEq ι] [Decomposition ℳ] (x : DirectSum ι fun (i : ι) => ↥(decomposeTensor ℳ N i)) : (DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) x = (LinearEquiv.rTensor N (decomposeLinearEquiv ℳ).symm) ((TensorProduct.directSumLeft R R (fun (i : ι) => ↥(ℳ i)) N).symm ((congrLinearEquiv (decomposeTensorEquiv ℳ N)).symm x))

@[reducible]

noncomputable def DirectSum.tensorDecomposition {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [Decomposition ℳ] (N : Type u_6) [AddCommGroup N] [Module R N] : Decomposition (decomposeTensor ℳ N)

The decomposition of a tensor product induced by a decomposition of the left module.

Equations

• One or more equations did not get rendered due to their size.

theorem DirectSum.IsInternal.baseChange {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [CommSemiring S] [Algebra R S] (hm : IsInternal ℳ) : IsInternal fun (i : ι) => Submodule.baseChange S (ℳ i)

theorem DirectSum.IsInternal.toBaseChange_bijective {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [CommSemiring S] [Algebra R S] (hm : IsInternal ℳ) (i : ι) : Function.Bijective ⇑(Submodule.toBaseChange S (ℳ i))

theorem DirectSum.IsInternal.toBaseChange_injective {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [CommSemiring R] [AddCommMonoid M] [Module R M] (ℳ : ι → Submodule R M) [DecidableEq ι] [CommSemiring S] [Algebra R S] (hm : IsInternal ℳ) (i : ι) : Function.Injective ⇑(Submodule.toBaseChange S (ℳ i))