Generators of multiple tensor products #
Given a finite family of R-modules M i, if we have, for each i,
a family of generators of the module M i, then the tensor products
of these elements generate ⨂[R] i, M i.
In LinearAlgebra.PiTensorProduct.Finite, we deduce that if the modules M i
are finitely generated, then so is ⨂[R] i, M i.
noncomputable def
PiTensorProduct.equivPiTensorComplSingletonTensor
(R : Type u_1)
{ι : Type u_2}
[DecidableEq ι]
(M : ι → Type u_3)
[CommSemiring R]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
(i₀ : ι)
:
(PiTensorProduct R fun (i : ι) => M i) ≃ₗ[R] TensorProduct R (PiTensorProduct R fun (i : ↑{i₀}ᶜ) => M ↑i) (M i₀)
The linear equivalence between ⨂[R] i, M i and the tensor product of
the pi tensor product indexed by the complement of {i₀} and M i₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
PiTensorProduct.equivPiTensorComplSingletonTensor_tprod
(R : Type u_1)
{ι : Type u_2}
[DecidableEq ι]
(M : ι → Type u_3)
[CommSemiring R]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
(i₀ : ι)
(m : (i : ι) → M i)
:
(equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), m i) = ((tprod R) fun (j : ↑(Set.singleton i₀)ᶜ) => m ↑j) ⊗ₜ[R] m i₀
@[simp]
theorem
PiTensorProduct.equivPiTensorComplSingletonTensor_symm_tmul
(R : Type u_1)
{ι : Type u_2}
[DecidableEq ι]
(M : ι → Type u_3)
[CommSemiring R]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
(i₀ : ι)
(m : (i : ↑(Set.singleton i₀)ᶜ) → M ↑i)
(x : M i₀)
:
(equivPiTensorComplSingletonTensor R M i₀).symm (((tprod R) fun (j : ↑(Set.singleton i₀)ᶜ) => m j) ⊗ₜ[R] x) = ⨂ₜ[R] (i : ι), Function.subtypeNeLift i₀ m x i
theorem
PiTensorProduct.ext_of_span_eq_top
{R : Type u_1}
{ι : Type u_2}
[Finite ι]
{M : ι → Type u_3}
{N : Type u_4}
{γ : ι → Type u_5}
[CommSemiring R]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[AddCommMonoid N]
[Module R N]
{g : ⦃i : ι⦄ → γ i → M i}
(hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤)
{φ φ' : (PiTensorProduct R fun (i : ι) => M i) →ₗ[R] N}
(h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i)))
:
theorem
MultilinearMap.ext_of_span_eq_top
{R : Type u_1}
{ι : Type u_2}
[Finite ι]
{M : ι → Type u_3}
{N : Type u_4}
{γ : ι → Type u_5}
[CommSemiring R]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[AddCommMonoid N]
[Module R N]
{g : ⦃i : ι⦄ → γ i → M i}
(hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤)
{φ φ' : MultilinearMap R M N}
(h : ∀ (j : (i : ι) → γ i), (φ fun (i : ι) => g (j i)) = φ' fun (i : ι) => g (j i))
:
theorem
PiTensorProduct.submodule_span_eq_top
{R : Type u_1}
{ι : Type u_2}
[Finite ι]
{M : ι → Type u_3}
{γ : ι → Type u_5}
[CommRing R]
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
{g : ⦃i : ι⦄ → γ i → M i}
(hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤)
: