tensor_finite #
This file defines the star operation on a tensor product of finite-dimensional star-modules $E,F$, i.e., ${(x \otimes y)}^*=x^* \otimes y^*$ for $x\in{E}$ and $x\in{F}$.
@[protected, instance]
noncomputable
def
tensor_product.has_star
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F] :
has_star (tensor_product 𝕜 E F)
Equations
- tensor_product.has_star = {star := λ (x : tensor_product 𝕜 E F), let b₁ : basis ↥(basis.of_vector_space_index 𝕜 E) 𝕜 E := basis.of_vector_space 𝕜 E, b₂ : basis ↥(basis.of_vector_space_index 𝕜 F) 𝕜 F := basis.of_vector_space 𝕜 F in finset.univ.sum (λ (i : ↥(basis.of_vector_space_index 𝕜 E)), finset.univ.sum (λ (j : ↥(basis.of_vector_space_index 𝕜 F)), has_star.star (⇑(⇑((b₁.tensor_product b₂).repr) x) (i, j)) • has_star.star (⇑b₁ i) ⊗ₜ[𝕜] has_star.star (⇑b₂ j)))}
@[simp]
theorem
tensor_product.star_tmul
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
[star_module 𝕜 E]
[star_module 𝕜 F]
(x : E)
(y : F) :
has_star.star (x ⊗ₜ[𝕜] y) = has_star.star x ⊗ₜ[𝕜] has_star.star y
theorem
tensor_product.star_add
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
(x y : tensor_product 𝕜 E F) :
has_star.star (x + y) = has_star.star x + has_star.star y
def
tensor_product.star_is_involutive
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
[star_module 𝕜 E]
[star_module 𝕜 F] :
@[instance]
noncomputable
def
tensor_product.has_involutive_star
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
[star_module 𝕜 E]
[star_module 𝕜 F] :
has_involutive_star (tensor_product 𝕜 E F)
Equations
- tensor_product.has_involutive_star = {to_has_star := tensor_product.has_star _inst_14, star_involutive := _}
@[instance]
noncomputable
def
tensor_product.star_add_monoid
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
[star_module 𝕜 E]
[star_module 𝕜 F] :
star_add_monoid (tensor_product 𝕜 E F)
Equations
@[instance]
def
tensor_product.star_module
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F] :
star_module 𝕜 (tensor_product 𝕜 E F)
theorem
tensor_product.map_real
{𝕜 : Type u_1}
[field 𝕜]
[star_ring 𝕜]
{A : Type u_2}
{B : Type u_3}
{E : Type u_4}
{F : Type u_5}
[add_comm_group A]
[add_comm_group B]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid A]
[star_add_monoid B]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 A]
[module 𝕜 B]
[module 𝕜 E]
[module 𝕜 F]
[star_module 𝕜 A]
[star_module 𝕜 B]
[star_module 𝕜 E]
[star_module 𝕜 F]
[finite_dimensional 𝕜 A]
[finite_dimensional 𝕜 B]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
(f : E →ₗ[𝕜] F)
(g : A →ₗ[𝕜] B) :
(tensor_product.map f g).real = tensor_product.map f.real g.real
theorem
linear_map.mul'_real
{𝕜 : Type u_1}
[field 𝕜]
[star_ring 𝕜]
(A : Type u_5)
[ring A]
[module 𝕜 A]
[star_ring A]
[star_module 𝕜 A]
[smul_comm_class 𝕜 A A]
[is_scalar_tower 𝕜 A A]
[finite_dimensional 𝕜 A] :
(linear_map.mul' 𝕜 A).real = (linear_map.mul' 𝕜 A).comp (tensor_product.comm 𝕜 A A).to_linear_map
theorem
tensor_product.assoc_real
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[add_comm_group G]
[star_add_monoid E]
[star_add_monoid F]
[star_add_monoid G]
[module 𝕜 E]
[module 𝕜 F]
[module 𝕜 G]
[star_ring 𝕜]
[star_module 𝕜 G]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
[finite_dimensional 𝕜 G]
[star_module 𝕜 E]
[star_module 𝕜 F] :
↑(tensor_product.assoc 𝕜 E F G).real = ↑(tensor_product.assoc 𝕜 E F G)
theorem
tensor_product.comm_real
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[field 𝕜]
[add_comm_group E]
[add_comm_group F]
[star_add_monoid E]
[star_add_monoid F]
[module 𝕜 E]
[module 𝕜 F]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[finite_dimensional 𝕜 F]
[star_module 𝕜 E]
[star_module 𝕜 F] :
↑(tensor_product.comm 𝕜 E F).real = ↑(tensor_product.comm 𝕜 E F)
theorem
tensor_product.lid_real
{𝕜 : Type u_1}
{E : Type u_2}
[field 𝕜]
[add_comm_group E]
[star_add_monoid E]
[module 𝕜 E]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[star_module 𝕜 E] :
↑(tensor_product.lid 𝕜 E).real = ↑(tensor_product.lid 𝕜 E)
theorem
tensor_product.rid_real
{𝕜 : Type u_1}
{E : Type u_2}
[field 𝕜]
[add_comm_group E]
[star_add_monoid E]
[module 𝕜 E]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[star_module 𝕜 E] :
↑(tensor_product.rid 𝕜 E).real = ↑(tensor_product.rid 𝕜 E)
theorem
tensor_op_star_apply
{𝕜 : Type u_1}
{E : Type u_2}
[field 𝕜]
[add_comm_group E]
[star_add_monoid E]
[module 𝕜 E]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[star_module 𝕜 E]
(x : E)
(y : Eᵐᵒᵖ) :
has_star.star (x ⊗ₜ[𝕜] y) = has_star.star x ⊗ₜ[𝕜] ⇑op (has_star.star (⇑unop y))
theorem
ten_swap_star
{𝕜 : Type u_1}
{E : Type u_2}
[field 𝕜]
[add_comm_group E]
[star_add_monoid E]
[module 𝕜 E]
[star_ring 𝕜]
[finite_dimensional 𝕜 E]
[star_module 𝕜 E]
(x : tensor_product 𝕜 E Eᵐᵒᵖ) :
has_star.star (⇑ten_swap x) = ⇑ten_swap (has_star.star x)