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)
:
(Algebra.TensorProduct.map z w) ((Algebra.TensorProduct.map f g) x) = (Algebra.TensorProduct.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)
:
(TensorProduct.map z w) ((TensorProduct.map f g) x) = (TensorProduct.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.
Instances For
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.
Instances For
@[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)
:
(LinearEquiv.TensorProduct.map f g) x = (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)
:
(LinearEquiv.TensorProduct.map f g).symm x = (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)
:
(AlgEquiv.TensorProduct.map f g).toLinearMap = 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)
:
(AlgEquiv.TensorProduct.map h i) ((AlgEquiv.TensorProduct.map f g) x) = (AlgEquiv.TensorProduct.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)
:
(AlgEquiv.TensorProduct.map h i).symm = AlgEquiv.TensorProduct.map h.symm i.symm
@[simp]
theorem
AlgEquiv.op_one
{R : Type u_1}
{A : Type u_2}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
AlgEquiv.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]
:
AlgEquiv.TensorProduct.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)
:
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) ⋯ ⋯