Strict tensor product (wip)

noncomputable instance TensorProduct.assocHasCoe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] : CoeFun (TensorProduct R (TensorProduct R E F) G) fun (x : TensorProduct R (TensorProduct R E F) G) => TensorProduct R E (TensorProduct R F G)

Equations

• TensorProduct.assocHasCoe = { coe := fun (x : TensorProduct R (TensorProduct R E F) G) => (TensorProduct.assoc R E F G) x }

noncomputable instance TensorProduct.assocSymmHasCoe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] : CoeFun (TensorProduct R E (TensorProduct R F G)) fun (x : TensorProduct R E (TensorProduct R F G)) => TensorProduct R (TensorProduct R E F) G

Equations

• TensorProduct.assocSymmHasCoe = { coe := fun (x : TensorProduct R E (TensorProduct R F G)) => (TensorProduct.assoc R E F G).symm x }

@[simp]

theorem TensorProduct.assoc_tmul_coe {R : Type u_4} {E : Type u_1} {F : Type u_2} {G : Type u_3} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] (a : E) (b : F) (c : G) : (a ⊗ₜ[R] b) ⊗ₜ[R] c = (TensorProduct.assoc R E F G).symm (a ⊗ₜ[R] b ⊗ₜ[R] c)

theorem TensorProduct.assoc_coe_coe {R : Type u_1} {E : Type u_3} {F : Type u_2} {G : Type u_4} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] (a : TensorProduct R (TensorProduct R E F) G) : a = (TensorProduct.assoc R E F G).symm ((TensorProduct.assoc R E F G) a)

@[simp]

theorem TensorProduct.tmul_assoc_coe {R : Type u_4} {E : Type u_1} {F : Type u_2} {G : Type u_3} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] (a : E) (b : F) (c : G) : a ⊗ₜ[R] b ⊗ₜ[R] c = (TensorProduct.assoc R E F G) ((a ⊗ₜ[R] b) ⊗ₜ[R] c)

theorem TensorProduct.coe_coe_assoc {R : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_3} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] (a : TensorProduct R E (TensorProduct R F G)) : a = (TensorProduct.assoc R E F G) ((TensorProduct.assoc R E F G).symm a)

noncomputable instance TensorProduct.lidHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] : CoeFun (TensorProduct R R E) fun (x : TensorProduct R R E) => E

Equations

• TensorProduct.lidHasCoe = { coe := fun (x : TensorProduct R R E) => (TensorProduct.lid R E) x }

noncomputable instance TensorProduct.ridHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] : CoeFun (TensorProduct R E R) fun (x : TensorProduct R E R) => E

Equations

• TensorProduct.ridHasCoe = { coe := fun (x : TensorProduct R E R) => (TensorProduct.rid R E) x }

noncomputable instance TensorProduct.lidSymmHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] : Coe E (TensorProduct R R E)

Equations

• TensorProduct.lidSymmHasCoe = { coe := fun (x : E) => (TensorProduct.lid R E).symm x }

@[reducible]

noncomputable instance TensorProduct.ridSymmHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] : Coe E (TensorProduct R E R)

Equations

• TensorProduct.ridSymmHasCoe = { coe := fun (x : E) => (TensorProduct.rid R E).symm x }

theorem TensorProduct.lid_coe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] (x : E) (r : R) : r ⊗ₜ[R] x = r • (TensorProduct.lid R E).symm x

theorem TensorProduct.rid_coe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] (x : E) (r : R) : x ⊗ₜ[R] r = r • (TensorProduct.rid R E).symm x

theorem TensorProduct.lid_symm_coe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] (x : E) : (TensorProduct.lid R E).symm x = 1 ⊗ₜ[R] x

theorem TensorProduct.rid_symm_coe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] (x : E) : (TensorProduct.rid R E).symm x = x ⊗ₜ[R] 1

theorem TensorProduct.lid_coe' {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] (x : E) (r : R) : r ⊗ₜ[R] x = r • (TensorProduct.lid R E).symm x

theorem TensorProduct.rid_coe' {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] (x : E) (r : R) : x ⊗ₜ[R] r = r • (TensorProduct.rid R E).symm x

theorem TensorProduct.lid_coe_rid_coe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] (x : E) : (TensorProduct.lid R E).symm x = (TensorProduct.lid R E).symm ((TensorProduct.rid R E) ((TensorProduct.rid R E).symm x))

noncomputable instance funTensorProductAssocHasCoe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] {A : Type u_5} : CoeFun (TensorProduct R (TensorProduct R E F) G → A) fun (x : TensorProduct R (TensorProduct R E F) G → A) => TensorProduct R E (TensorProduct R F G) → A

Equations

• funTensorProductAssocHasCoe = { coe := fun (f : TensorProduct R (TensorProduct R E F) G → A) (x : TensorProduct R E (TensorProduct R F G)) => f ((TensorProduct.assoc R E F G).symm x) }

noncomputable instance LinearMap.tensorProductAssocHasCoe {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] {A : Type u_5} [AddCommMonoid A] [Module R A] : Coe (TensorProduct R (TensorProduct R E F) G →ₗ[R] A) (TensorProduct R E (TensorProduct R F G) →ₗ[R] A)

Equations

• LinearMap.tensorProductAssocHasCoe = { coe := fun (f : TensorProduct R (TensorProduct R E F) G →ₗ[R] A) => f ∘ₗ ↑(TensorProduct.assoc R E F G).symm }

noncomputable instance funTensorProductAssocHasCoe' {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] {A : Type u_5} : Coe (TensorProduct R E (TensorProduct R F G) → A) (TensorProduct R (TensorProduct R E F) G → A)

Equations

• funTensorProductAssocHasCoe' = { coe := fun (f : TensorProduct R E (TensorProduct R F G) → A) (x : TensorProduct R (TensorProduct R E F) G) => f ((TensorProduct.assoc R E F G) x) }

noncomputable instance LinearMap.tensorProductAssocHasCoe' {R : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [CommSemiring R] [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [Module R E] [Module R F] [Module R G] {A : Type u_5} [AddCommMonoid A] [Module R A] : Coe (TensorProduct R E (TensorProduct R F G) →ₗ[R] A) (TensorProduct R (TensorProduct R E F) G →ₗ[R] A)

Equations

• LinearMap.tensorProductAssocHasCoe' = { coe := fun (f : TensorProduct R E (TensorProduct R F G) →ₗ[R] A) => f ∘ₗ ↑(TensorProduct.assoc R E F G) }

noncomputable instance funLidHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} : CoeFun (TensorProduct R R E → A) fun (x : TensorProduct R R E → A) => E → A

Equations

• funLidHasCoe = { coe := fun (f : TensorProduct R R E → A) (x : E) => f ((TensorProduct.lid R E).symm x) }

noncomputable instance LinearMap.tensorProductLidHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} [AddCommMonoid A] [Module R A] : Coe (TensorProduct R R E →ₗ[R] A) (E →ₗ[R] A)

Equations

• LinearMap.tensorProductLidHasCoe = { coe := fun (f : TensorProduct R R E →ₗ[R] A) => f ∘ₗ ↑(TensorProduct.lid R E).symm }

noncomputable instance funLidHasCoe' {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} : Coe (E → A) (TensorProduct R R E → A)

Equations

• funLidHasCoe' = { coe := fun (f : E → A) (x : TensorProduct R R E) => f ((TensorProduct.lid R E) x) }

noncomputable instance LinearMap.tensorProductLidHasCoe' {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} [AddCommMonoid A] [Module R A] : Coe (E →ₗ[R] A) (TensorProduct R R E →ₗ[R] A)

Equations

• LinearMap.tensorProductLidHasCoe' = { coe := fun (f : E →ₗ[R] A) => f ∘ₗ ↑(TensorProduct.lid R E) }

noncomputable instance funRidHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} : CoeFun (TensorProduct R E R → A) fun (x : TensorProduct R E R → A) => E → A

Equations

• funRidHasCoe = { coe := fun (f : TensorProduct R E R → A) (x : E) => f ((TensorProduct.rid R E).symm x) }

noncomputable instance LinearMap.tensorProductRidHasCoe {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} [AddCommMonoid A] [Module R A] : Coe (TensorProduct R E R →ₗ[R] A) (E →ₗ[R] A)

Equations

• LinearMap.tensorProductRidHasCoe = { coe := fun (f : TensorProduct R E R →ₗ[R] A) => f ∘ₗ ↑(TensorProduct.rid R E).symm }

noncomputable instance funRidHasCoe' {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} : Coe (E → A) (TensorProduct R E R → A)

Equations

• funRidHasCoe' = { coe := fun (f : E → A) (x : TensorProduct R E R) => f ((TensorProduct.rid R E) x) }

noncomputable instance LinearMap.tensorProductRidHasCoe' {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_3} [AddCommMonoid A] [Module R A] : Coe (E →ₗ[R] A) (TensorProduct R E R →ₗ[R] A)

Equations

• LinearMap.tensorProductRidHasCoe' = { coe := fun (f : E →ₗ[R] A) => f ∘ₗ ↑(TensorProduct.rid R E) }

theorem LinearMap.lid_coe {R : Type u_2} {E : Type u_3} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_1} [AddCommMonoid A] [Module R A] (f : E →ₗ[R] A) : f = (f ∘ₗ ↑(TensorProduct.lid R E)) ∘ₗ ↑(TensorProduct.lid R E).symm

theorem LinearMap.lid_symm_coe {R : Type u_2} {E : Type u_3} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_1} [AddCommMonoid A] [Module R A] (f : TensorProduct R R E →ₗ[R] A) : f = (f ∘ₗ ↑(TensorProduct.lid R E).symm) ∘ₗ ↑(TensorProduct.lid R E)

theorem LinearMap.rid_coe {R : Type u_2} {E : Type u_3} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_1} [AddCommMonoid A] [Module R A] (f : E →ₗ[R] A) : f = (f ∘ₗ ↑(TensorProduct.rid R E)) ∘ₗ ↑(TensorProduct.rid R E).symm

theorem LinearMap.rid_symm_coe {R : Type u_2} {E : Type u_3} [CommSemiring R] [AddCommGroup E] [Module R E] {A : Type u_1} [AddCommMonoid A] [Module R A] (f : TensorProduct R E R →ₗ[R] A) : f = (f ∘ₗ ↑(TensorProduct.rid R E).symm) ∘ₗ ↑(TensorProduct.rid R E)