Documentation

Mathlib.LinearAlgebra.TensorProduct.Basic

Universal property of the tensor product #

Given any bilinear map f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂, there is a unique semilinear map TensorProduct.lift f : TensorProduct R M N →ₛₗ[σ₁₂] P₂ whose composition with the canonical bilinear map TensorProduct.mk is the given bilinear map f. Uniqueness is shown in the theorem TensorProduct.lift.unique.

Tags #

bilinear, tensor, tensor product

def TensorProduct.liftAddHom {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] (f : M →+ N →+ P) (hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)) :

TensorProduct R M N →+ P

Lift an R-balanced map to the tensor product. A map f : M →+ N →+ P additive in both components is R-balanced, or middle linear with respect to R, if scalar multiplication in either argument is equivalent, f (r • m) n = f m (r • n). Note that strictly the first action should be a right-action by R, but for now R is commutative so it doesn't matter.

Equations

Instances For

@[simp]

theorem TensorProduct.liftAddHom_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] (f : M →+ N →+ P) (hf : ∀ (r : R) (m : M) (n : N), (f (r • m)) n = (f m) (r • n)) (m : M) (n : N) :

(liftAddHom f hf) (m ⊗ₜ[R] n) = (f m) n

def TensorProduct.liftAux {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) :

TensorProduct R M N →+ P₂

Auxiliary function to constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations

Instances For

theorem TensorProduct.liftAux_tmul {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) :

(liftAux f') (m ⊗ₜ[R] n) = (f' m) n

@[simp]

theorem TensorProduct.liftAux.smulₛₗ {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (r : R) (x : TensorProduct R M N) :

(liftAux f') (r • x) = σ₁₂ r • (liftAux f') x

theorem TensorProduct.liftAux.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] {f : M →ₗ[R] N →ₗ[R] P} (r : R) (x : TensorProduct R M N) :

(liftAux f) (r • x) = r • (liftAux f) x

def TensorProduct.lift {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) :

TensorProduct R M N →ₛₗ[σ₁₂] P₂

Constructing a linear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

This works for semilinear maps.

Equations

Instances For

@[simp]

theorem TensorProduct.lift.tmul {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (x : M) (y : N) :

(lift f') (x ⊗ₜ[R] y) = (f' x) y

@[simp]

theorem TensorProduct.lift.tmul' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} (x : M) (y : N) :

(lift f').toAddHom (x ⊗ₜ[R] y) = (f' x) y

theorem TensorProduct.ext' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) :

g = h

theorem TensorProduct.lift.unique {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} {g : TensorProduct R M N →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f' x) y) :

g = lift f'

theorem TensorProduct.lift_mk {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

lift (mk R M N) = LinearMap.id

theorem TensorProduct.lift_compr₂ₛₗ {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} {P₂ : Type u_17} {P₃ : Type u_18} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [AddCommMonoid P₃] [Module R M] [Module R N] [Module R₂ P₂] [Module R₃ P₃] {f' : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (h : P₂ →ₛₗ[σ₂₃] P₃) :

lift (f'.compr₂ₛₗ h) = h ∘ₛₗ lift f'

theorem TensorProduct.lift_compr₂ {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 →ₗ[R] P} (g : P →ₗ[R] Q) :

lift (f.compr₂ g) = g ∘ₗ lift f

theorem TensorProduct.lift_mk_compr₂ₛₗ {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (g : TensorProduct R M N →ₛₗ[σ₁₂] P₂) :

lift ((mk R M N).compr₂ₛₗ g) = g

theorem TensorProduct.lift_mk_compr₂ {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 : TensorProduct R M N →ₗ[R] P) :

lift ((mk R M N).compr₂ f) = f

theorem TensorProduct.ext {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂} (H : (mk R M N).compr₂ₛₗ g = (mk R M N).compr₂ₛₗ h) :

g = h

This used to be an @[ext] lemma, but it fails very slowly when the ext tactic tries to apply it in some cases, notably when one wants to show equality of two linear maps. The @[ext] attribute is now added locally where it is needed. Using this as the @[ext] lemma instead of TensorProduct.ext' allows ext to apply lemmas specific to M →ₗ _ and N →ₗ _.

See note [partially-applied ext lemmas].

theorem TensorProduct.ext_iff {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂} :

g = h ↔ (mk R M N).compr₂ₛₗ g = (mk R M N).compr₂ₛₗ h

def TensorProduct.uncurry {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] :

(M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) →ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] P₂

Linearly constructing a semilinear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations

Instances For

@[simp]

theorem TensorProduct.uncurry_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) :

((uncurry σ₁₂ M N P₂) f) (m ⊗ₜ[R] n) = (f m) n

def TensorProduct.lift.equiv {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] :

(M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) ≃ₗ[R₂] TensorProduct R M N →ₛₗ[σ₁₂] P₂

A linear equivalence constructing a semilinear map M ⊗ N → P given a bilinear map M → N → P with the property that its composition with the canonical bilinear map M → N → M ⊗ N is the given bilinear map M → N → P.

Equations

Instances For

@[simp]

theorem TensorProduct.lift.equiv_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) :

((equiv σ₁₂ M N P₂) f) (m ⊗ₜ[R] n) = (f m) n

@[simp]

theorem TensorProduct.lift.equiv_symm_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) :

(((equiv σ₁₂ M N P₂).symm f) m) n = f (m ⊗ₜ[R] n)

def TensorProduct.lcurry {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] (σ₁₂ : R →+* R₂) (M : Type u_7) (N : Type u_8) (P₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] :

(TensorProduct R M N →ₛₗ[σ₁₂] P₂) →ₗ[R₂] M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂

Given a semilinear map M ⊗ N → P, compose it with the canonical bilinear map M → N → M ⊗ N to form a bilinear map M → N → P.

Equations

Instances For

@[simp]

theorem TensorProduct.lcurry_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) :

(((lcurry σ₁₂ M N P₂) f) m) n = f (m ⊗ₜ[R] n)

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

M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂

Given a semilinear map M ⊗ N → P, compose it with the canonical bilinear map M → N → M ⊗ N to form a bilinear map M → N → P.

Equations

Instances For

@[simp]

theorem TensorProduct.curry_apply {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M) (n : N) :

((curry f) m) n = f (m ⊗ₜ[R] n)

theorem TensorProduct.curry_injective {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] :

Function.Injective curry

theorem TensorProduct.ext_threefold {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] {g h : TensorProduct R (TensorProduct R M N) P →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] y ⊗ₜ[R] z) = h (x ⊗ₜ[R] y ⊗ₜ[R] z)) :

g = h

theorem TensorProduct.ext_threefold' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] {g h : TensorProduct R M (TensorProduct R N P) →ₛₗ[σ₁₂] P₂} (H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] (y ⊗ₜ[R] z)) = h (x ⊗ₜ[R] (y ⊗ₜ[R] z))) :

g = h

theorem TensorProduct.ext_fourfold {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] [Module R Q] {g h : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₛₗ[σ₁₂] P₂} (H : ∀ (w : M) (x : N) (y : P) (z : Q), g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)) :

g = h

theorem TensorProduct.ext_fourfold' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] [Module R Q] {φ ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₛₗ[σ₁₂] P₂} (H : ∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) = ψ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z))) :

φ = ψ

Two semilinear maps (M ⊗ N) ⊗ (P ⊗ Q) → P₂ which agree on all elements of the form (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) are equal.

theorem TensorProduct.ext_fourfold'' {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] [Module R P] [Module R Q] {φ ψ : TensorProduct R (TensorProduct R M (TensorProduct R N P)) Q →ₛₗ[σ₁₂] P₂} (H : ∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z) = ψ (w ⊗ₜ[R] (x ⊗ₜ[R] y) ⊗ₜ[R] z)) :

φ = ψ

Two semilinear maps M ⊗ (N ⊗ P) ⊗ Q → P₂ which agree on all elements of the form m ⊗ₜ (n ⊗ₜ p) ⊗ₜ q are equal.

def TensorProduct.comm (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct R M N ≃ₗ[R] TensorProduct R N M

The tensor product of modules is commutative, up to linear equivalence.

Equations

Instances For

@[simp]

theorem TensorProduct.comm_tmul (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

(TensorProduct.comm R M N) (m ⊗ₜ[R] n) = n ⊗ₜ[R] m

@[simp]

theorem TensorProduct.comm_symm (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

(TensorProduct.comm R M N).symm = TensorProduct.comm R N M

theorem TensorProduct.comm_symm_tmul (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

(TensorProduct.comm R M N).symm (n ⊗ₜ[R] m) = m ⊗ₜ[R] n

theorem TensorProduct.lift_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) {P₂ : Type u_17} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P₂] [Module R M] [Module R N] [Module R₂ P₂] (f : M →ₛₗ[σ₁₂] N →ₛₗ[σ₁₂] P₂) :

lift f ∘ₛₗ ↑(TensorProduct.comm R N M) = lift f.flip

@[simp]

theorem TensorProduct.comm_trans_comm (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct.comm R N M ≪≫ₗ TensorProduct.comm R M N = LinearEquiv.refl R (TensorProduct R N M)

theorem TensorProduct.comm_comp_comm (R : Type u_1) [CommSemiring R] (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :

↑(TensorProduct.comm R N M) ∘ₗ ↑(TensorProduct.comm R M N) = LinearMap.id

@[simp]

theorem TensorProduct.comm_comp_comm_assoc (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 : P →ₗ[R] TensorProduct R M N) :

↑(TensorProduct.comm R N M) ∘ₗ ↑(TensorProduct.comm R M N) ∘ₗ f = f

@[simp]

theorem TensorProduct.comm_comm (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) :

(TensorProduct.comm R M N) ((TensorProduct.comm R N M) x) = x

def TensorProduct.mapOfCompatibleSMul (R : Type u_1) [CommSemiring R] (A : Type u_6) (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] :

TensorProduct A M N →ₗ[A] TensorProduct R M N

If M and N are both R- and A-modules and their actions on them commute, and if the A-action on M ⊗[R] N can switch between the two factors, then there is a canonical A-linear map from M ⊗[A] N to M ⊗[R] N.

Equations

Instances For

@[simp]

theorem TensorProduct.mapOfCompatibleSMul_tmul (R : Type u_1) [CommSemiring R] (A : Type u_6) (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] (m : M) (n : N) :

(mapOfCompatibleSMul R A M N) (m ⊗ₜ[A] n) = m ⊗ₜ[R] n

theorem TensorProduct.mapOfCompatibleSMul_surjective (R : Type u_1) [CommSemiring R] (A : Type u_6) (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] :

Function.Surjective ⇑(mapOfCompatibleSMul R A M N)

def TensorProduct.mapOfCompatibleSMul' (R : Type u_1) [CommSemiring R] (A : Type u_6) (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] :

TensorProduct A M N →ₗ[R] TensorProduct R M N

mapOfCompatibleSMul R A M N is also R-linear.

Equations

Instances For

def TensorProduct.equivOfCompatibleSMul (R : Type u_1) [CommSemiring R] (A : Type u_6) (M : Type u_7) (N : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [CompatibleSMul R A M N] [CompatibleSMul A R M N] :

TensorProduct A M N ≃ₗ[A] TensorProduct R M N

If the R- and A-actions on M and N satisfy CompatibleSMul both ways, then M ⊗[A] N is canonically isomorphic to M ⊗[R] N.

Equations

Instances For

def TensorProduct.Neg.aux (R : Type u_1) [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid N] [Module R M] [Module R N] :

TensorProduct R M N →ₗ[R] TensorProduct R M N

Auxiliary function to defining negation multiplication on tensor product.

Equations

Instances For

instance TensorProduct.neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid N] [Module R M] [Module R N] :

Neg (TensorProduct R M N)

Equations

theorem TensorProduct.neg_add_cancel {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) :

-x + x = 0

instance TensorProduct.addCommGroup {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid N] [Module R M] [Module R N] :

AddCommGroup (TensorProduct R M N)

Equations

theorem TensorProduct.neg_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) :

(-m) ⊗ₜ[R] n = -m ⊗ₜ[R] n

theorem TensorProduct.tmul_neg {R : Type u_1} [CommSemiring R] {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (m : M) (p : P) :

m ⊗ₜ[R] (-p) = -m ⊗ₜ[R] p

theorem TensorProduct.tmul_sub {R : Type u_1} [CommSemiring R] {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (m : M) (p₁ p₂ : P) :

m ⊗ₜ[R] (p₁ - p₂) = m ⊗ₜ[R] p₁ - m ⊗ₜ[R] p₂

theorem TensorProduct.sub_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid N] [Module R M] [Module R N] (m₁ m₂ : M) (n : N) :

(m₁ - m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n

instance TensorProduct.CompatibleSMul.int {R : Type u_1} [CommSemiring R] {M : Type u_2} {P : Type u_4} [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] :

CompatibleSMul R ℤ M P

While the tensor product will automatically inherit a ℤ-module structure from AddCommGroup.toIntModule, that structure won't be compatible with lemmas like tmul_smul unless we use a ℤ-Module instance provided by TensorProduct.left_module.

When R is a Ring we get the required TensorProduct.compatible_smul instance through IsScalarTower, but when it is only a Semiring we need to build it from scratch. The instance diamond in compatible_smul doesn't matter because it's in Prop.

instance TensorProduct.CompatibleSMul.unit {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommMonoid N] [Module R M] [Module R N] {S : Type u_7} [Monoid S] [DistribMulAction S M] [DistribMulAction S N] [CompatibleSMul R S M N] :

CompatibleSMul R Sˣ M N