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

• TensorProduct.liftAddHom f hf = (addConGen (TensorProduct.Eqv R M N)).lift (FreeAddMonoid.lift fun (mn : M × N) => (f mn.1) mn.2) ⋯

@[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

• TensorProduct.liftAux f' = TensorProduct.liftAddHom (LinearMap.toAddMonoidHom'.comp f'.toAddMonoidHom) ⋯

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

• TensorProduct.lift f' = { toFun := (↑(TensorProduct.liftAux f')).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[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

• TensorProduct.uncurry σ₁₂ M N P₂ = { toFun := TensorProduct.lift, map_add' := ⋯, map_smul' := ⋯ }

@[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

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

@[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

• TensorProduct.lcurry σ₁₂ M N P₂ = ↑(TensorProduct.lift.equiv σ₁₂ M N P₂).symm

@[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

• TensorProduct.curry f = (TensorProduct.lcurry σ₁₂ M N P₂) f

@[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

• TensorProduct.comm R M N = LinearEquiv.ofLinear (TensorProduct.lift (TensorProduct.mk R N M).flip) (TensorProduct.lift (TensorProduct.mk R M N).flip) ⋯ ⋯

@[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

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

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

@[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

• TensorProduct.mapOfCompatibleSMul' R A M N = { toAddHom := (TensorProduct.mapOfCompatibleSMul R A M N).toAddHom, map_smul' := ⋯ }

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

• TensorProduct.equivOfCompatibleSMul R A M N = { toLinearMap := TensorProduct.mapOfCompatibleSMul R A M N, invFun := ⇑(TensorProduct.mapOfCompatibleSMul A R M N), left_inv := ⋯, right_inv := ⋯ }

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

• TensorProduct.Neg.aux R = TensorProduct.lift (TensorProduct.mk R M N ∘ₗ (-LinearMap.id))

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

• TensorProduct.neg = { neg := ⇑(TensorProduct.Neg.aux R) }

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

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

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