Some lemmas about tensor_product #
theorem
TensorProduct.ext_iff'
{R : Type u_1}
{M : Type u_3}
{N : Type u_2}
{P : Type u_4}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
{g : TensorProduct R M N →ₗ[R] P}
{h : TensorProduct R M N →ₗ[R] P}
:
theorem
TensorProduct.ext'_iff
{R : Type u_1}
{M : Type u_4}
{N : Type u_3}
{P : Type u_5}
{Q : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
{g : TensorProduct R (TensorProduct R M N) Q →ₗ[R] P}
{h : TensorProduct R (TensorProduct R M N) Q →ₗ[R] P}
:
@[simp]
theorem
TensorProduct.map_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_4}
{P : Type u_3}
{Q : Type u_5}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
(x : M)
(y : N)
:
@[simp]
theorem
TensorProduct.comm_commutes
{R : Type u_1}
{M : Type u_3}
{N : Type u_2}
{P : Type u_4}
{Q : Type u_5}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
{g : TensorProduct R M N →ₗ[R] P}
{h : TensorProduct R M N →ₗ[R] Q}
:
↑(TensorProduct.comm R P Q) ∘ₗ TensorProduct.map g h = TensorProduct.map h g ∘ₗ ↑(TensorProduct.comm R (TensorProduct R M N) (TensorProduct R M N))
theorem
TensorProduct.comm_commutes'
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
{g : M →ₗ[R] M}
{h : M →ₗ[R] R}
:
↑(TensorProduct.comm R M R) ∘ₗ TensorProduct.map g h = TensorProduct.map h g ∘ₗ ↑(TensorProduct.comm R M M)
theorem
TensorProduct.assoc_comp_map
{R : Type u_1}
[CommSemiring R]
{M : Type u_2}
{N : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid M₂]
[AddCommMonoid N₂]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R M₂]
[Module R N₂]
[Module R P]
[Module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
(s : M₂ →ₗ[R] N₂)
:
↑(TensorProduct.assoc R P Q N₂) ∘ₗ TensorProduct.map (TensorProduct.map f t) s = TensorProduct.map f (TensorProduct.map t s) ∘ₗ ↑(TensorProduct.assoc R M N M₂)
theorem
TensorProduct.ext_threefold'
{R : Type u_1}
[CommSemiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
{g : TensorProduct R M (TensorProduct R N P) →ₗ[R] Q}
{h : TensorProduct R M (TensorProduct R N P) →ₗ[R] Q}
(H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] y ⊗ₜ[R] z) = h (x ⊗ₜ[R] y ⊗ₜ[R] z))
:
g = h
theorem
TensorProduct.assoc_symm_comp_map
{R : Type u_1}
[CommSemiring R]
{M : Type u_2}
{N : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
{P : Type u_6}
{Q : Type u_7}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid M₂]
[AddCommMonoid N₂]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R M₂]
[Module R N₂]
[Module R P]
[Module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
(s : M₂ →ₗ[R] N₂)
:
↑(TensorProduct.assoc R P Q N₂).symm ∘ₗ TensorProduct.map f (TensorProduct.map t s) = TensorProduct.map (TensorProduct.map f t) s ∘ₗ ↑(TensorProduct.assoc R M N M₂).symm
theorem
TensorProduct.comm_map
{R : Type u_1}
[CommSemiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
:
↑(TensorProduct.comm R P Q) ∘ₗ TensorProduct.map f t = TensorProduct.map t f ∘ₗ ↑(TensorProduct.comm R M N)
theorem
TensorProduct.comm_symm_map
{R : Type u_1}
[CommSemiring R]
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[AddCommMonoid Q]
[Module R M]
[Module R N]
[Module R P]
[Module R Q]
(f : M →ₗ[R] P)
(t : N →ₗ[R] Q)
:
↑(TensorProduct.comm R P Q).symm ∘ₗ TensorProduct.map t f = TensorProduct.map f t ∘ₗ ↑(TensorProduct.comm R M N).symm
theorem
TensorProduct.map_sum
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[Module R M₁]
[Module R M₂]
[Module R N₁]
[Module R N₂]
(x : M₁ →ₗ[R] M₂)
{α : Type u_6}
(s : Finset α)
(n : α → N₁ →ₗ[R] N₂)
:
TensorProduct.map x (∑ a ∈ s, n a) = ∑ a ∈ s, TensorProduct.map x (n a)
theorem
TensorProduct.sum_map
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[Module R M₁]
[Module R M₂]
[Module R N₁]
[Module R N₂]
{α : Type u_6}
(s : Finset α)
(n : α → N₁ →ₗ[R] N₂)
(x : M₁ →ₗ[R] M₂)
:
TensorProduct.map (∑ a ∈ s, n a) x = ∑ a ∈ s, TensorProduct.map (n a) x
theorem
TensorProduct.map_smul
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[Module R M₁]
[Module R M₂]
[Module R N₁]
[Module R N₂]
(x : M₁ →ₗ[R] M₂)
(y : N₁ →ₗ[R] N₂)
(a : R)
:
TensorProduct.map x (a • y) = a • TensorProduct.map x y
theorem
TensorProduct.smul_map
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[Module R M₁]
[Module R M₂]
[Module R N₁]
[Module R N₂]
(x : M₁ →ₗ[R] M₂)
(y : N₁ →ₗ[R] N₂)
(a : R)
:
TensorProduct.map (a • x) y = a • TensorProduct.map x y
theorem
TensorProduct.add_map
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[Module R M₁]
[Module R M₂]
[Module R N₁]
[Module R N₂]
(x : M₁ →ₗ[R] M₂)
(y : M₁ →ₗ[R] M₂)
(z : N₁ →ₗ[R] N₂)
:
TensorProduct.map (x + y) z = TensorProduct.map x z + TensorProduct.map y z
theorem
TensorProduct.map_zero
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{N₁ : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid N₁]
[AddCommMonoid M₂]
[AddCommMonoid N₂]
[Module R M₁]
[Module R N₁]
[Module R M₂]
[Module R N₂]
(x : M₁ →ₗ[R] N₁)
:
TensorProduct.map x 0 = 0
theorem
TensorProduct.zero_map
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{N₁ : Type u_3}
{M₂ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid N₁]
[AddCommMonoid M₂]
[AddCommMonoid N₂]
[Module R M₁]
[Module R N₁]
[Module R M₂]
[Module R N₂]
(x : M₁ →ₗ[R] N₁)
:
TensorProduct.map 0 x = 0
theorem
TensorProduct.zero_tmul_zero
{R : Type u_1}
[CommSemiring R]
{M : Type u_2}
{N : Type u_3}
[AddCommGroup M]
[AddCommGroup N]
[Module R M]
[Module R N]
:
theorem
TensorProduct.map_mul'_commute_iff
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[NonUnitalNonAssocSemiring M]
[NonUnitalNonAssocSemiring N]
[Module R M]
[Module R N]
[SMulCommClass R M M]
[SMulCommClass R N N]
[IsScalarTower R M M]
[IsScalarTower R N N]
{f : M →ₗ[R] N}
:
LinearMap.mul' R N ∘ₗ TensorProduct.map f f = f ∘ₗ LinearMap.mul' R M ↔ ∀ (x y : M), f (x * y) = f x * f y
theorem
Algebra.TensorProduct.map_toLinearMap
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{P : Type u_4}
{Q : Type u_5}
[CommSemiring R]
[Semiring M]
[Semiring N]
[Semiring P]
[Semiring Q]
[Algebra R M]
[Algebra R N]
[Algebra R P]
[Algebra R Q]
(f : M →ₐ[R] N)
(g : P →ₐ[R] Q)
:
(Algebra.TensorProduct.map f g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
theorem
AlgHom.commute_map_mul'
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[Semiring M]
[Semiring N]
[Algebra R M]
[Algebra R N]
(f : M →ₐ[R] N)
:
LinearMap.mul' R N ∘ₗ (Algebra.TensorProduct.map f f).toLinearMap = f.toLinearMap ∘ₗ LinearMap.mul' R M
theorem
AlgHom.commute_map_mul'_apply
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommSemiring R]
[Semiring M]
[Semiring N]
[Algebra R M]
[Algebra R N]
(f : M →ₐ[R] N)
(x : TensorProduct R M M)
:
(LinearMap.mul' R N) ((Algebra.TensorProduct.map f f) x) = f ((LinearMap.mul' R M) x)
theorem
TensorProduct.map_add
{R : Type u_1}
[CommSemiring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{N₁ : Type u_4}
{N₂ : Type u_5}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid N₁]
[AddCommMonoid N₂]
[Module R M₁]
[Module R M₂]
[Module R N₁]
[Module R N₂]
(x : M₁ →ₗ[R] M₂)
(y : M₁ →ₗ[R] M₂)
(z : N₁ →ₗ[R] N₂)
:
TensorProduct.map z (x + y) = TensorProduct.map z x + TensorProduct.map z y
theorem
TensorProduct.of_basis_eq_span
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[CommSemiring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
(x : TensorProduct 𝕜 E F)
{ι₁ : Type u_4}
{ι₂ : Type u_5}
[Fintype ι₁]
[Fintype ι₂]
(b₁ : Basis ι₁ 𝕜 E)
(b₂ : Basis ι₂ 𝕜 F)
: