theorem Algebra.TensorProduct.map_apply_map_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Semiring E] [Semiring F] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [Algebra R E] [Algebra R F] (f : A →ₐ[R] B) (g : C →ₐ[R] D) (z : B →ₐ[R] E) (w : D →ₐ[R] F) (x : TensorProduct R A C) : (map z w) ((map f g) x) = (map (z.comp f) (w.comp g)) x

theorem TensorProduct.map_apply_map_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [AddCommMonoid E] [AddCommMonoid F] [Module R A] [Module R B] [Module R C] [Module R D] [Module R E] [Module R F] (f : A →ₗ[R] B) (g : C →ₗ[R] D) (z : B →ₗ[R] E) (w : D →ₗ[R] F) (x : TensorProduct R A C) : (map z w) ((map f g) x) = (map (z ∘ₗ f) (w ∘ₗ g)) x

noncomputable def AlgEquiv.TensorProduct.map {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) : TensorProduct R A C ≃ₐ[R] TensorProduct R B D

Equations

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

@[simp]

theorem AlgEquiv.TensorProduct.map_tmul {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x : A) (y : C) : (map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y

noncomputable def LinearEquiv.TensorProduct.map {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A ≃ₗ[R] B) (g : C ≃ₗ[R] D) : TensorProduct R A C ≃ₗ[R] TensorProduct R B D

Equations

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

@[simp]

theorem LinearEquiv.TensorProduct.map_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A ≃ₗ[R] B) (g : C ≃ₗ[R] D) (x : TensorProduct R A C) : (map f g) x = (_root_.TensorProduct.map ↑f ↑g) x

@[simp]

theorem LinearEquiv.TensorProduct.map_symm_apply {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A ≃ₗ[R] B) (g : C ≃ₗ[R] D) (x : TensorProduct R B D) : (map f g).symm x = (_root_.TensorProduct.map ↑f.symm ↑g.symm) x

@[simp]

theorem AlgEquiv.TensorProduct.map_toLinearMap {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) : (map f g).toLinearMap = _root_.TensorProduct.map f.toLinearMap g.toLinearMap

theorem AlgEquiv.TensorProduct.map_map_toLinearMap {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} {E : Type u_6} {F : Type u_7} [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Semiring E] [Semiring F] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] [Algebra R E] [Algebra R F] (h : B ≃ₐ[R] E) (i : D ≃ₐ[R] F) (f : A ≃ₐ[R] B) (g : C ≃ₐ[R] D) (x : TensorProduct R A C) : (map h i) ((map f g) x) = (map (f.trans h) (g.trans i)) x

theorem AlgEquiv.TensorProduct.map_symm {R : Type u_1} [CommSemiring R] {B : Type u_2} {D : Type u_3} {E : Type u_4} {F : Type u_5} [Semiring B] [Semiring D] [Semiring E] [Semiring F] [Algebra R B] [Algebra R D] [Algebra R E] [Algebra R F] (h : B ≃ₐ[R] E) (i : D ≃ₐ[R] F) : (map h i).symm = map h.symm i.symm

theorem AlgEquiv.op_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C) : (op f).trans (op g) = op (f.trans g)

@[simp]

theorem AlgEquiv.op_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : op 1 = 1

@[simp]

theorem AlgEquiv.TensorProduct.map_one {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] : map 1 1 = 1

theorem LinearEquiv.TensorProduct.map_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D] [Module R A] [Module R B] [Module R C] [Module R D] (f : A ≃ₗ[R] B) (g : C ≃ₗ[R] D) (x : A) (y : C) : (map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y

noncomputable def AlgEquiv.lTensor {R : Type u_1} {A : Type u_2} {B : Type u_3} (C : Type u_4) [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A ≃ₐ[R] B) : TensorProduct R C A ≃ₐ[R] TensorProduct R C B

Equations

• AlgEquiv.lTensor C f = Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct (LinearEquiv.lTensor C f.toLinearEquiv) ⋯ ⋯

theorem AlgEquiv.lTensor_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A ≃ₐ[R] B) (x : C) (y : A) : (lTensor C f) (x ⊗ₜ[R] y) = x ⊗ₜ[R] f y

theorem AlgEquiv.lTensor_symm_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A ≃ₐ[R] B) (x : C) (y : B) : (lTensor C f).symm (x ⊗ₜ[R] y) = x ⊗ₜ[R] f.symm y