Tensor products and linear maps

This file defines TensorProduct.map, the R-linear map from M ⊗ N to M₂ ⊗ N₂ defined by a pair of linear (or more generally semilinear) maps f : M → M₂ and g : N → N₂.

The notation f ⊗ₘ g is available for this map.

We also define one-sided versions lTensor and rTensor.

Tags

bilinear, tensor, tensor product

def TensorProduct.map {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The tensor product of a pair of linear maps between modules.

Equations

• TensorProduct.map f g = TensorProduct.lift ((TensorProduct.mk R₂ M₂ N₂).compl₂ g ∘ₛₗ f)

def RingTheory.LinearMap.«term_⊗ₘ_» : Lean.TrailingParserDescr

The tensor product of a pair of linear maps between modules.

Equations

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

@[simp]

theorem TensorProduct.map_tmul {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (m : M) (n : N) : (map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R₂] g n

theorem TensorProduct.map_comp_comm_eq {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map f g ∘ₛₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R₂ N₂ M₂) ∘ₛₗ map g f

Given semilinear maps f : M → P, g : N → Q, if we identify M ⊗ N with N ⊗ M and P ⊗ Q with Q ⊗ P, then this lemma states that f ⊗ g = g ⊗ f.

theorem TensorProduct.map_comm {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R N M) : (map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R₂ N₂ M₂) ((map g f) x)

theorem TensorProduct.range_map {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (map f g).range = Submodule.map₂ (mk R P Q) f.range g.range

theorem TensorProduct.range_map_eq_span_tmul {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (map f g).range = Submodule.span R {t : TensorProduct R P Q | ∃ (m : M) (n : N), f m ⊗ₜ[R] g n = t}

@[deprecated TensorProduct.range_map_eq_span_tmul (since := "2025-09-07")]

theorem TensorProduct.map_range_eq_span_tmul {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (map f g).range = Submodule.span R {t : TensorProduct R P Q | ∃ (m : M) (n : N), f m ⊗ₜ[R] g n = t}

Alias of TensorProduct.range_map_eq_span_tmul.

def TensorProduct.mapIncl {R : Type u_1} [CommSemiring R] {P : Type u_9} {Q : Type u_10} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] (p : Submodule R P) (q : Submodule R Q) : TensorProduct R ↥p ↥q →ₗ[R] TensorProduct R P Q

Given submodules p ⊆ P and q ⊆ Q, this is the natural map: p ⊗ q → P ⊗ Q.

Equations

• TensorProduct.mapIncl p q = TensorProduct.map p.subtype q.subtype

theorem TensorProduct.range_mapIncl {R : Type u_1} [CommSemiring R] {P : Type u_9} {Q : Type u_10} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] (p : Submodule R P) (q : Submodule R Q) : (mapIncl p q).range = Submodule.map₂ (mk R P Q) p q

theorem TensorProduct.map₂_eq_range_lift_comp_mapIncl {R : Type u_1} [CommSemiring R] {M : Type u_7} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] (f : P →ₗ[R] Q →ₗ[R] M) (p : Submodule R P) (q : Submodule R Q) : Submodule.map₂ f p q = (lift f ∘ₗ mapIncl p q).range

theorem TensorProduct.map_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) : map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) = map f₂ g₂ ∘ₛₗ map f₁ g₁

theorem TensorProduct.map_map {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R M N) : (map f₂ g₂) ((map f₁ g₁) x) = (map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁)) x

theorem TensorProduct.range_map_mono {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R M₂] [Module R M₃] [Module R N₂] [Module R N₃] {a : M →ₗ[R] M₂} {b : M₃ →ₗ[R] M₂} {c : N →ₗ[R] N₂} {d : N₃ →ₗ[R] N₂} (hab : a.range ≤ b.range) (hcd : c.range ≤ d.range) : (map a c).range ≤ (map b d).range

theorem TensorProduct.range_mapIncl_mono {R : Type u_1} [CommSemiring R] {P : Type u_9} {Q : Type u_10} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') : (mapIncl p q).range ≤ (mapIncl p' q').range

theorem TensorProduct.lift_comp_map {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} {P₃ : Type u_18} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid P₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ P₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (i : M₂ →ₛₗ[σ₂₃] N₂ →ₛₗ[σ₂₃] P₃) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : lift i ∘ₛₗ map f g = lift ((i ∘ₛₗ f).compl₂ g)

@[simp]

theorem TensorProduct.map_id {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : map LinearMap.id LinearMap.id = LinearMap.id

@[simp]

theorem TensorProduct.map_one {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : map 1 1 = 1

theorem TensorProduct.map_mul {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N) : map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂

@[simp]

theorem TensorProduct.map_pow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) : map f g ^ n = map (f ^ n) (g ^ n)

theorem TensorProduct.map_add_left {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f₁ f₂ : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map (f₁ + f₂) g = map f₁ g + map f₂ g

theorem TensorProduct.map_add_right {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g₁ g₂ : N →ₛₗ[σ₁₂] N₂) : map f (g₁ + g₂) = map f g₁ + map f g₂

theorem TensorProduct.map_smul_left {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map (r • f) g = r • map f g

theorem TensorProduct.map_smul_right {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : map f (r • g) = r • map f g

def TensorProduct.mapBilinear {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] : (M →ₛₗ[σ₁₂] M₂) →ₗ[R₂] (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The tensor product of a pair of semilinear maps between modules, bilinear in both maps.

Equations

• TensorProduct.mapBilinear σ₁₂ M N M₂ N₂ = LinearMap.mk₂ R₂ TensorProduct.map ⋯ ⋯ ⋯ ⋯

def TensorProduct.lTensorHomToHomLTensor {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (P : Type u_9) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] : TensorProduct R₂ M₂ (P →ₛₗ[σ₁₂] N₂) →ₗ[R₂] P →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The canonical linear map from M₂ ⊗[R₂] (P →ₛₗ[σ₁₂] N₂) to P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂.

Equations

• TensorProduct.lTensorHomToHomLTensor σ₁₂ P M₂ N₂ = TensorProduct.lift (LinearMap.llcomp R₂ P N₂ (TensorProduct R₂ M₂ N₂) ∘ₗ TensorProduct.mk R₂ M₂ N₂)

def TensorProduct.rTensorHomToHomRTensor {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (P : Type u_9) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] : TensorProduct R₂ (P →ₛₗ[σ₁₂] M₂) N₂ →ₗ[R₂] P →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The canonical linear map from (P →ₛₗ[σ₁₂] M₂) ⊗[R₂] N₂ to P →ₛₗ[σ₁₂] M₂ ⊗[R₂] N₂.

Equations

• TensorProduct.rTensorHomToHomRTensor σ₁₂ P M₂ N₂ = TensorProduct.lift (LinearMap.llcomp R₂ P M₂ (TensorProduct R₂ M₂ N₂) ∘ₗ (TensorProduct.mk R₂ M₂ N₂).flip).flip

def TensorProduct.homTensorHomMap {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (M₂ : Type u_12) (N₂ : Type u_14) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] : TensorProduct R₂ (M →ₛₗ[σ₁₂] M₂) (N →ₛₗ[σ₁₂] N₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

The linear map from (M →ₛₗ[σ₁₂] M₂) ⊗ (N →ₛₗ[σ₁₂] N₂) to M ⊗ N →ₛₗ[σ₁₂] M₂ ⊗ N₂ sending f ⊗ₜ g to TensorProduct.map f g, the tensor product of the two maps.

Equations

• TensorProduct.homTensorHomMap σ₁₂ M N M₂ N₂ = TensorProduct.lift (TensorProduct.mapBilinear σ₁₂ M N M₂ N₂)

def TensorProduct.map₂ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] (f : M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃) (g : N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃) : TensorProduct R M N →ₛₗ[σ₁₃] TensorProduct R₂ M₂ N₂ →ₛₗ[σ₂₃] TensorProduct R₃ M₃ N₃

This is a binary version of TensorProduct.map: Given a bilinear map f : M ⟶ P ⟶ Q and a bilinear map g : N ⟶ S ⟶ T, if we think f and g as semilinear maps with two inputs, then map₂ f g is a bilinear map taking two inputs M ⊗ N → P ⊗ S → Q ⊗ S defined by map₂ f g (m ⊗ n) (p ⊗ s) = f m p ⊗ g n s.

Mathematically, TensorProduct.map₂ is defined as the composition M ⊗ N -map→ Hom(P, Q) ⊗ Hom(S, T) -homTensorHomMap→ Hom(P ⊗ S, Q ⊗ T).

Equations

• TensorProduct.map₂ f g = TensorProduct.homTensorHomMap σ₂₃ M₂ N₂ M₃ N₃ ∘ₛₗ TensorProduct.map f g

@[simp]

theorem TensorProduct.mapBilinear_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : ((mapBilinear σ₁₂ M N M₂ N₂) f) g = map f g

@[simp]

theorem TensorProduct.lTensorHomToHomLTensor_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {P : Type u_9} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] (m₂ : M₂) (f : P →ₛₗ[σ₁₂] N₂) (p : P) : ((lTensorHomToHomLTensor σ₁₂ P M₂ N₂) (m₂ ⊗ₜ[R₂] f)) p = m₂ ⊗ₜ[R₂] f p

@[simp]

theorem TensorProduct.rTensorHomToHomRTensor_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {P : Type u_9} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid P] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R₂ M₂] [Module R₂ N₂] [Module R P] (f : P →ₛₗ[σ₁₂] M₂) (n₂ : N₂) (p : P) : ((rTensorHomToHomRTensor σ₁₂ P M₂ N₂) (f ⊗ₜ[R₂] n₂)) p = f p ⊗ₜ[R₂] n₂

@[simp]

theorem TensorProduct.homTensorHomMap_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : (homTensorHomMap σ₁₂ M N M₂ N₂) (f ⊗ₜ[R₂] g) = map f g

@[simp]

theorem TensorProduct.map₂_apply_tmul {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] (f : M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃) (g : N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃) (m : M) (n : N) : (map₂ f g) (m ⊗ₜ[R] n) = map (f m) (g n)

@[simp]

theorem TensorProduct.map_zero_left {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (g : N →ₛₗ[σ₁₂] N₂) : map 0 g = 0

@[simp]

theorem TensorProduct.map_zero_right {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) : map f 0 = 0

def TensorProduct.congr {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : TensorProduct R M N ≃ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂

If M and P are semilinearly equivalent and N and Q are semilinearly equivalent then M ⊗ N and P ⊗ Q are semilinearly equivalent.

Equations

• TensorProduct.congr f g = LinearEquiv.ofLinear (TensorProduct.map ↑f ↑g) (TensorProduct.map ↑f.symm ↑g.symm) ⋯ ⋯

@[simp]

theorem TensorProduct.toLinearMap_congr {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : ↑(congr f g) = map ↑f ↑g

@[simp]

theorem TensorProduct.congr_tmul {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) (m : M) (n : N) : (congr f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R₂] g n

@[simp]

theorem TensorProduct.congr_symm_tmul {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) (p : M₂) (q : N₂) : (congr f g).symm (p ⊗ₜ[R₂] q) = f.symm p ⊗ₜ[R] g.symm q

theorem TensorProduct.congr_symm {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : (congr f g).symm = congr f.symm g.symm

@[simp]

theorem TensorProduct.congr_refl_refl {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : congr (LinearEquiv.refl R M) (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R M N)

theorem TensorProduct.congr_trans {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₃₁ : R₃ →+* R} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂) (g₁ : N ≃ₛₗ[σ₁₂] N₂) : congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂)

theorem TensorProduct.congr_congr {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] {σ₃₁ : R₃ →+* R} [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f₂ : M₂ ≃ₛₗ[σ₂₃] M₃) (g₂ : N₂ ≃ₛₗ[σ₂₃] N₃) (f₁ : M ≃ₛₗ[σ₁₂] M₂) (g₁ : N ≃ₛₗ[σ₁₂] N₂) (x : TensorProduct R M N) : (congr f₂ g₂) ((congr f₁ g₁) x) = (congr (f₁.trans f₂) (g₁.trans g₂)) x

theorem TensorProduct.congr_mul {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (f' : M ≃ₗ[R] M) (g' : N ≃ₗ[R] N) : congr (f * f') (g * g') = congr f g * congr f' g'

@[simp]

theorem TensorProduct.congr_pow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ) : congr f g ^ n = congr (f ^ n) (g ^ n)

@[simp]

theorem TensorProduct.congr_zpow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ) : congr f g ^ n = congr (f ^ n) (g ^ n)

theorem TensorProduct.map_bijective {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {f : M →ₗ[R] N} {g : P →ₗ[R] Q} (hf : Function.Bijective ⇑f) (hg : Function.Bijective ⇑g) : Function.Bijective ⇑(map f g)

instance TensorProduct.instSmall {R : Type u_22} {M : Type u_23} {N : Type u_24} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Small.{u, u_23} M] [Small.{u, u_24} N] : Small.{u, max u_24 u_23} (TensorProduct R M N)

def LinearMap.lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : TensorProduct R M N →ₗ[R] TensorProduct R M P

LinearMap.lTensor M f : M ⊗ N →ₗ M ⊗ P is the natural linear map induced by f : N →ₗ P.

Equations

• LinearMap.lTensor M f = TensorProduct.map LinearMap.id f

def LinearMap.rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : TensorProduct R N M →ₗ[R] TensorProduct R P M

LinearMap.rTensor M f : N ⊗ M →ₗ P ⊗ M is the natural linear map induced by f : N →ₗ P.

Equations

• LinearMap.rTensor M f = TensorProduct.map f LinearMap.id

theorem LinearMap.lTensor_def {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : lTensor M f = TensorProduct.map id f

theorem LinearMap.rTensor_def {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : rTensor M f = TensorProduct.map f id

@[simp]

theorem LinearMap.lTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) : (lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n

@[simp]

theorem LinearMap.rTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) : (rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m

@[simp]

theorem LinearMap.lTensor_comp_mk {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) : lTensor M f ∘ₗ (TensorProduct.mk R M N) m = (TensorProduct.mk R M P) m ∘ₗ f

@[simp]

theorem LinearMap.rTensor_comp_flip_mk {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) : rTensor M f ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f

theorem LinearMap.comm_comp_rTensor_comp_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) : ↑(TensorProduct.comm R P Q) ∘ₗ rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = lTensor Q g

theorem LinearMap.comm_comp_lTensor_comp_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N →ₗ[R] P) : ↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g ∘ₗ ↑(TensorProduct.comm R N Q) = rTensor Q g

theorem LinearMap.lTensor_inj_iff_rTensor_inj {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Injective ⇑(lTensor M f) ↔ Function.Injective ⇑(rTensor M f)

Given a linear map f : N → P, f ⊗ M is injective if and only if M ⊗ f is injective.

theorem LinearMap.lTensor_surj_iff_rTensor_surj {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Surjective ⇑(lTensor M f) ↔ Function.Surjective ⇑(rTensor M f)

Given a linear map f : N → P, f ⊗ M is surjective if and only if M ⊗ f is surjective.

theorem LinearMap.lTensor_bij_iff_rTensor_bij {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Bijective ⇑(lTensor M f) ↔ Function.Bijective ⇑(rTensor M f)

Given a linear map f : N → P, f ⊗ M is bijective if and only if M ⊗ f is bijective.

theorem LinearMap.smul_lTensor {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) {S : Type u_22} [CommSemiring S] [SMul R S] [Module S M] [IsScalarTower R S M] [SMulCommClass R S M] (s : S) (m : TensorProduct R M N) : s • (lTensor M f) m = (lTensor M f) (s • m)

def LinearMap.lTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (N →ₗ[R] P) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M P

lTensorHom M is the natural linear map that sends a linear map f : N →ₗ P to M ⊗ f.

See also Module.End.lTensorAlgHom.

Equations

• LinearMap.lTensorHom M = { toFun := LinearMap.lTensor M, map_add' := ⋯, map_smul' := ⋯ }

def LinearMap.rTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (N →ₗ[R] P) →ₗ[R] TensorProduct R N M →ₗ[R] TensorProduct R P M

rTensorHom M is the natural linear map that sends a linear map f : N →ₗ P to f ⊗ M.

See also Module.End.rTensorAlgHom.

Equations

• LinearMap.rTensorHom M = { toFun := fun (f : N →ₗ[R] P) => LinearMap.rTensor M f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.coe_lTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : ⇑(lTensorHom M) = lTensor M

@[simp]

theorem LinearMap.coe_rTensorHom {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : ⇑(rTensorHom M) = rTensor M

@[simp]

theorem LinearMap.lTensor_add {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : lTensor M (f + g) = lTensor M f + lTensor M g

@[simp]

theorem LinearMap.rTensor_add {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : rTensor M (f + g) = rTensor M f + rTensor M g

@[simp]

theorem LinearMap.lTensor_zero {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : lTensor M 0 = 0

@[simp]

theorem LinearMap.rTensor_zero {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : rTensor M 0 = 0

@[simp]

theorem LinearMap.lTensor_smul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) : lTensor M (r • f) = r • lTensor M f

@[simp]

theorem LinearMap.rTensor_smul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) : rTensor M (r • f) = r • rTensor M f

theorem LinearMap.lTensor_comp {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : lTensor M (g ∘ₗ f) = lTensor M g ∘ₗ lTensor M f

theorem LinearMap.lTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R M N) : (lTensor M (g ∘ₗ f)) x = (lTensor M g) ((lTensor M f) x)

theorem LinearMap.rTensor_comp {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : rTensor M (g ∘ₗ f) = rTensor M g ∘ₗ rTensor M f

theorem LinearMap.rTensor_comp_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R N M) : (rTensor M (g ∘ₗ f)) x = (rTensor M g) ((rTensor M f) x)

theorem LinearMap.lTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : Module.End R N) : lTensor M (f * g) = lTensor M f * lTensor M g

theorem LinearMap.rTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : Module.End R N) : rTensor M (f * g) = rTensor M f * rTensor M g

@[simp]

theorem LinearMap.lTensor_id {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : lTensor M id = id

theorem LinearMap.lTensor_id_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : (lTensor M id) x = x

@[simp]

theorem LinearMap.rTensor_id {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : rTensor M id = id

theorem LinearMap.rTensor_id_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R N M) : (rTensor M id) x = x

@[simp]

theorem LinearMap.lTensor_smul_action {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) : lTensor M (DistribSMul.toLinearMap R N r) = DistribSMul.toLinearMap R (TensorProduct R M N) r

@[simp]

theorem LinearMap.rTensor_smul_action {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) : rTensor M (DistribSMul.toLinearMap R N r) = DistribSMul.toLinearMap R (TensorProduct R N M) r

@[simp]

theorem LinearMap.lTensor_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : lTensor P g ∘ₗ rTensor N f = TensorProduct.map f g

@[simp]

theorem LinearMap.rTensor_comp_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : rTensor Q f ∘ₗ lTensor M g = TensorProduct.map f g

@[simp]

theorem LinearMap.map_comp_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) : TensorProduct.map f g ∘ₗ rTensor N f' = TensorProduct.map (f ∘ₗ f') g

@[simp]

theorem LinearMap.map_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) (x : TensorProduct R S N) : (TensorProduct.map f g) ((rTensor N f') x) = (TensorProduct.map (f ∘ₗ f') g) x

@[simp]

theorem LinearMap.map_comp_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) : TensorProduct.map f g ∘ₗ lTensor M g' = TensorProduct.map f (g ∘ₗ g')

@[simp]

theorem LinearMap.map_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) (x : TensorProduct R M S) : (TensorProduct.map f g) ((lTensor M g') x) = (TensorProduct.map f (g ∘ₗ g')) x

@[simp]

theorem LinearMap.rTensor_comp_map {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : rTensor Q f' ∘ₗ TensorProduct.map f g = TensorProduct.map (f' ∘ₗ f) g

@[simp]

theorem LinearMap.rTensor_map {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N) : (rTensor Q f') ((TensorProduct.map f g) x) = (TensorProduct.map (f' ∘ₗ f) g) x

@[simp]

theorem LinearMap.lTensor_comp_map {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : lTensor P g' ∘ₗ TensorProduct.map f g = TensorProduct.map f (g' ∘ₗ g)

@[simp]

theorem LinearMap.lTensor_map {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N) : (lTensor P g') ((TensorProduct.map f g) x) = (TensorProduct.map f (g' ∘ₗ g)) x

theorem LinearMap.lTensor_comp_comm {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] P) : lTensor N f ∘ₗ ↑(TensorProduct.comm R M N) = ↑(TensorProduct.comm R P N) ∘ₗ rTensor N f

theorem LinearMap.rTensor_comp_comm {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] P) : rTensor N f ∘ₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R N P) ∘ₗ lTensor N f

theorem LinearMap.lTensor_comm {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] P) (x : TensorProduct R M N) : (lTensor N f) ((TensorProduct.comm R M N) x) = (TensorProduct.comm R P N) ((rTensor N f) x)

theorem LinearMap.rTensor_comm {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] P) (x : TensorProduct R N M) : (rTensor N f) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R N P) ((lTensor N f) x)

@[simp]

theorem LinearMap.rTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (n : ℕ) : rTensor N f ^ n = rTensor N (f ^ n)

@[simp]

theorem LinearMap.lTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] N) (n : ℕ) : lTensor M f ^ n = lTensor M (f ^ n)

def LinearEquiv.lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : TensorProduct R M N ≃ₗ[R] TensorProduct R M P

LinearEquiv.lTensor M f : M ⊗ N ≃ₗ M ⊗ P is the natural linear equivalence induced by f : N ≃ₗ P.

Equations

• LinearEquiv.lTensor M f = TensorProduct.congr (LinearEquiv.refl R M) f

def LinearEquiv.rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : TensorProduct R N M ≃ₗ[R] TensorProduct R P M

LinearEquiv.rTensor M f : N₁ ⊗ M ≃ₗ N₂ ⊗ M is the natural linear equivalence induced by f : N₁ ≃ₗ N₂.

Equations

• LinearEquiv.rTensor M f = TensorProduct.congr f (LinearEquiv.refl R M)

@[simp]

theorem LinearEquiv.coe_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(lTensor M f) = LinearMap.lTensor M ↑f

@[simp]

theorem LinearEquiv.coe_lTensor_symm {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(lTensor M f).symm = LinearMap.lTensor M ↑f.symm

@[simp]

theorem LinearEquiv.coe_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(rTensor M f) = LinearMap.rTensor M ↑f

@[simp]

theorem LinearEquiv.coe_rTensor_symm {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(rTensor M f).symm = LinearMap.rTensor M ↑f.symm

@[simp]

theorem LinearEquiv.lTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (n : N) : (lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n

@[simp]

theorem LinearEquiv.lTensor_symm_tmul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (p : P) : (lTensor M f).symm (m ⊗ₜ[R] p) = m ⊗ₜ[R] f.symm p

@[simp]

theorem LinearEquiv.rTensor_tmul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (n : N) : (rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m

@[simp]

theorem LinearEquiv.rTensor_symm_tmul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) (m : M) (p : P) : (rTensor M f).symm (p ⊗ₜ[R] m) = f.symm p ⊗ₜ[R] m

theorem LinearEquiv.comm_trans_rTensor_trans_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N ≃ₗ[R] P) : TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g

theorem LinearEquiv.comm_trans_lTensor_trans_comm_eq {R : Type u_1} [CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (g : N ≃ₗ[R] P) : TensorProduct.comm R N Q ≪≫ₗ lTensor Q g ≪≫ₗ TensorProduct.comm R Q P = rTensor Q g

theorem LinearEquiv.lTensor_trans {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) : lTensor M (f ≪≫ₗ g) = lTensor M f ≪≫ₗ lTensor M g

theorem LinearEquiv.lTensor_trans_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (x : TensorProduct R M N) : (lTensor M (f ≪≫ₗ g)) x = (lTensor M g) ((lTensor M f) x)

theorem LinearEquiv.rTensor_trans {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) : rTensor M (f ≪≫ₗ g) = rTensor M f ≪≫ₗ rTensor M g

theorem LinearEquiv.rTensor_trans_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (y : TensorProduct R N M) : (rTensor M (f ≪≫ₗ g)) y = (rTensor M g) ((rTensor M f) y)

theorem LinearEquiv.lTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : N ≃ₗ[R] N) : lTensor M (f * g) = lTensor M f * lTensor M g

theorem LinearEquiv.rTensor_mul {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : N ≃ₗ[R] N) : rTensor M (f * g) = rTensor M f * rTensor M g

@[simp]

theorem LinearEquiv.lTensor_refl {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : lTensor M (refl R N) = refl R (TensorProduct R M N)

theorem LinearEquiv.lTensor_refl_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : (lTensor M (refl R N)) x = x

@[simp]

theorem LinearEquiv.rTensor_refl {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : rTensor M (refl R N) = refl R (TensorProduct R N M)

theorem LinearEquiv.rTensor_refl_apply {R : Type u_1} [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (y : TensorProduct R N M) : (rTensor M (refl R N)) y = y

@[simp]

theorem LinearEquiv.rTensor_trans_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : rTensor N f ≪≫ₗ lTensor P g = TensorProduct.congr f g

@[simp]

theorem LinearEquiv.lTensor_trans_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : lTensor M g ≪≫ₗ rTensor Q f = TensorProduct.congr f g

@[simp]

theorem LinearEquiv.rTensor_trans_congr {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : S ≃ₗ[R] M) : rTensor N f' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g

@[simp]

theorem LinearEquiv.lTensor_trans_congr {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (g' : S ≃ₗ[R] N) : lTensor M g' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g)

@[simp]

theorem LinearEquiv.congr_trans_rTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f' : P ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : TensorProduct.congr f g ≪≫ₗ rTensor Q f' = TensorProduct.congr (f ≪≫ₗ f') g

@[simp]

theorem LinearEquiv.congr_trans_lTensor {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (g' : Q ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : TensorProduct.congr f g ≪≫ₗ lTensor P g' = TensorProduct.congr f (g ≪≫ₗ g')

@[simp]

theorem LinearEquiv.rTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (n : ℕ) : rTensor N f ^ n = rTensor N (f ^ n)

@[simp]

theorem LinearEquiv.rTensor_zpow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M ≃ₗ[R] M) (n : ℤ) : rTensor N f ^ n = rTensor N (f ^ n)

@[simp]

theorem LinearEquiv.lTensor_pow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N ≃ₗ[R] N) (n : ℕ) : lTensor M f ^ n = lTensor M (f ^ n)

@[simp]

theorem LinearEquiv.lTensor_zpow {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N ≃ₗ[R] N) (n : ℤ) : lTensor M f ^ n = lTensor M (f ^ n)

@[simp]

theorem LinearMap.lTensor_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommMonoid N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : lTensor M (f - g) = lTensor M f - lTensor M g

@[simp]

theorem LinearMap.rTensor_sub {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [AddCommMonoid N] [AddCommGroup P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (f g : N →ₗ[R] P) : rTensor Q (f - g) = rTensor Q f - rTensor Q g

@[simp]

theorem LinearMap.lTensor_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommMonoid N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : lTensor M (-f) = -lTensor M f

@[simp]

theorem LinearMap.rTensor_neg {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} {Q : Type u_5} [AddCommMonoid N] [AddCommGroup P] [AddCommMonoid Q] [Module R N] [Module R P] [Module R Q] (f : N →ₗ[R] P) : rTensor Q (-f) = -rTensor Q f

theorem Equiv.tensorProductComm_def (R : Type u_1) {A : Type u_2} {A' : Type u_3} {B : Type u_4} {B' : Type u_5} [CommSemiring R] [AddCommMonoid A'] [AddCommMonoid B'] [Module R A'] [Module R B'] (eA : A ≃ A') (eB : B ≃ B') : TensorProduct.comm R A B = TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm)