Monlib.LinearAlgebra.TensorProduct.Submodule

source

noncomputable def Submodule.tensorProduct {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (V : Submodule R E) (W : Submodule R F) :

Submodule R (TensorProduct R E F)

Equations

V.tensorProduct W = LinearMap.range (TensorProduct.mapIncl V W)

Instances For

source

theorem Submodule.tensorProduct_mem {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] {V : Submodule R E} {W : Submodule R F} (x : TensorProduct R ↥V ↥W) :

(TensorProduct.mapIncl V W) x ∈ V.tensorProduct W

source

noncomputable def Submodule.mem_tensorProduct {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] {V : Submodule R E} {W : Submodule R F} (vw : ↥(V.tensorProduct W)) :

TensorProduct R ↥V ↥W

Equations

Submodule.mem_tensorProduct vw = Exists.choose ⋯

Instances For

source

theorem Submodule.mem_tensorProduct_eq {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] {V : Submodule R E} {W : Submodule R F} (vw : ↥(V.tensorProduct W)) :

(TensorProduct.mapIncl V W) (Submodule.mem_tensorProduct vw) = ↑vw

source

theorem TensorProduct.mapIncl_isInjective {R : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike R] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace R E] [InnerProductSpace R F] [FiniteDimensional R E] [FiniteDimensional R F] {V : Submodule R E} {W : Submodule R F} :

Function.Injective ⇑(TensorProduct.mapIncl V W)

source

theorem Submodule.mapIncl_mem_tensorProduct {R : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike R] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace R E] [InnerProductSpace R F] [FiniteDimensional R E] [FiniteDimensional R F] {V : Submodule R E} {W : Submodule R F} (v : TensorProduct R ↥V ↥W) :

Submodule.mem_tensorProduct ⟨(TensorProduct.mapIncl V W) v, ⋯⟩ = v

source

theorem norm_tmul {𝕜 : Type u_4} {B : Type u_5} {C : Type u_6} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (x : B) (y : C) :

‖x ⊗ₜ[𝕜] y‖ = ‖x‖ * ‖y‖

source

theorem TensorProduct.mapIncl_norm_map {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (V : Submodule 𝕜 E) (W : Submodule 𝕜 F) (x : TensorProduct 𝕜 ↥V ↥W) :

‖(TensorProduct.mapIncl V W) x‖ = ‖x‖

source

noncomputable def Submodule.tensorProduct_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (V : Submodule 𝕜 E) (W : Submodule 𝕜 F) :

TensorProduct 𝕜 ↥V ↥W ≃ₗᵢ[𝕜] ↥(V.tensorProduct W)

Equations

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

Instances For

source

noncomputable def Submodule.tensorProduct_orthonormalBasis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {V : Submodule 𝕜 E} {W : Submodule 𝕜 F} {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (v : OrthonormalBasis ι₁ 𝕜 ↥V) (w : OrthonormalBasis ι₂ 𝕜 ↥W) :

OrthonormalBasis (ι₁ × ι₂) 𝕜 ↥(V.tensorProduct W)

Equations

Submodule.tensorProduct_orthonormalBasis v w = (v.tensorProduct w).map (V.tensorProduct_linearIsometryEquiv W)

Instances For

source

theorem Submodule.tensorProduct_orthonormalBasis_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {V : Submodule 𝕜 E} {W : Submodule 𝕜 F} {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (v : OrthonormalBasis ι₁ 𝕜 ↥V) (w : OrthonormalBasis ι₂ 𝕜 ↥W) (i : ι₁ × ι₂) :

↑((Submodule.tensorProduct_orthonormalBasis v w) i) = ↑(v i.1) ⊗ₜ[𝕜] ↑(w i.2)

source

theorem Submodule.tensorProduct_finrank {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {V : Submodule 𝕜 E} {W : Submodule 𝕜 F} :

Module.finrank 𝕜 ↥(V.tensorProduct W) = Module.finrank 𝕜 ↥V * Module.finrank 𝕜 ↥W

source

theorem orthogonalProjection_map_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (V : Submodule 𝕜 E) (W : Submodule 𝕜 F) :

TensorProduct.map ↑(orthogonalProjection' V) ↑(orthogonalProjection' W) = ↑(orthogonalProjection' (V.tensorProduct W))

source

theorem TensorProduct.submodule_exists_le_tensorProduct {R : Type u_4} {M : Type u_5} {N : Type u_6} [Field R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (U : Submodule R (TensorProduct R M N)) (hU : Module.Finite R ↥U) :

∃ (M' : Submodule R M) (N' : Submodule R N) (_ : Module.Finite R ↥M') (_ : Module.Finite R ↥N'), U ≤ M'.tensorProduct N'

source

theorem orthogonalProjection'_ortho_eq {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [HasOrthogonalProjection K] :

orthogonalProjection' Kᗮ = ContinuousLinearMap.id 𝕜 E - orthogonalProjection' K

source

theorem TensorProduct.submodule_exists_le_tensorProduct_ofFiniteDimensional {R : Type u_4} {M : Type u_5} {N : Type u_6} [Field R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] (U : Submodule R (TensorProduct R M N)) :

∃ (M' : Submodule R M) (N' : Submodule R N), U ≤ M'.tensorProduct N'

source

theorem orthogonalProjection_of_tensorProduct {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℂ E] [InnerProductSpace ℂ F] [FiniteDimensional ℂ E] [FiniteDimensional ℂ F] {A : TensorProduct ℂ E F →ₗ[ℂ ] TensorProduct ℂ E F} (hA : ∃ (U : Submodule ℂ E) (V : Submodule ℂ F), ↑(orthogonalProjection' (U.tensorProduct V)) = A) :

∃ (U : Submodule ℂ (TensorProduct ℂ E F)), ↑(orthogonalProjection' U) = A

source

def piProdUnitEquivPi {R : Type u_4} {n : Type u_5} [Semiring R] :

(n × Unit → R) ≃ₗ[R] n → R

Equations

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

Instances For

source

def Matrix.ofCol {R : Type u_4} {n : Type u_5} [Semiring R] :

Matrix n Unit R ≃ₗ[R] n → R

matrix.col written as a linear equivalence

Equations

Matrix.ofCol = Matrix.reshape ≪≫ₗ piProdUnitEquivPi

Instances For

source

def matrixProdUnitRight {R : Type u_4} {n : Type u_5} {m : Type u_6} [Semiring R] :

Matrix n (m × Unit) R ≃ₗ[R] Matrix n m R

Equations

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

Instances For

source

theorem col_hMul_col_conjTranspose_is_kronecker_of_vectors {R : Type u_4} {m : Type u_5} {n : Type u_6} [Semiring R] (x : m → R) (y : n → R) :

Matrix.vecMulVec x y = Matrix.reshape.symm (Matrix.ofCol (matrixProdUnitRight (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (Matrix.col Unit x) (Matrix.col Unit y))))

vec_mulVec x y written as a kronecker product

source

noncomputable def PiLp_tensorEquiv {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] :

TensorProduct 𝕜 (PiLp 2 M₁) (PiLp 2 M₂) ≃ₗ[𝕜] PiLp 2 fun (i : ι₁ × ι₂) => TensorProduct 𝕜 (M₁ i.1) (M₂ i.2)

Equations

PiLp_tensorEquiv = directSumTensor

Instances For

source

@[simp]

theorem PiLp_tensorEquiv_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] (a : (i : ι₁ × ι₂) → TensorProduct 𝕜 (M₁ i.1) (M₂ i.2)) :

PiLp_tensorEquiv.symm a = directSumTensorInvFun a

source

@[simp]

theorem PiLp_tensorEquiv_apply {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] (a : TensorProduct 𝕜 ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) (i : ι₁ × ι₂) :

PiLp_tensorEquiv a i = directSumTensorToFun a i

source

theorem PiLp_tensorEquiv_tmul {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] (x : PiLp 2 M₁) (y : PiLp 2 M₂) (i : ι₁ × ι₂) :

PiLp_tensorEquiv (x ⊗ₜ[𝕜] y) i = x i.1 ⊗ₜ[𝕜] y i.2

source

@[simp]

theorem PiLp_tensorEquiv_norm_map {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] [∀ (i : ι₁), FiniteDimensional 𝕜 (M₁ i)] [∀ (i : ι₂), FiniteDimensional 𝕜 (M₂ i)] (x : TensorProduct 𝕜 (PiLp 2 M₁) (PiLp 2 M₂)) :

‖PiLp_tensorEquiv x‖ = ‖x‖

source

@[reducible, inline]

noncomputable abbrev PiLp_tensorLinearIsometryEquiv {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] [∀ (i : ι₁), FiniteDimensional 𝕜 (M₁ i)] [∀ (i : ι₂), FiniteDimensional 𝕜 (M₂ i)] :

TensorProduct 𝕜 (PiLp 2 M₁) (PiLp 2 M₂) ≃ₗᵢ[𝕜] PiLp 2 fun (i : ι₁ × ι₂) => TensorProduct 𝕜 (M₁ i.1) (M₂ i.2)

Equations

PiLp_tensorLinearIsometryEquiv = { toLinearEquiv := PiLp_tensorEquiv, norm_map' := ⋯ }

Instances For

source

@[simp]

theorem PiLp_tensorLinearIsometryEquiv_invFun {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] [∀ (i : ι₁), FiniteDimensional 𝕜 (M₁ i)] [∀ (i : ι₂), FiniteDimensional 𝕜 (M₂ i)] (a : (i : ι₁ × ι₂) → TensorProduct 𝕜 (M₁ i.1) (M₂ i.2)) :

PiLp_tensorLinearIsometryEquiv.invFun a = directSumTensorInvFun a

source

@[simp]

theorem PiLp_tensorLinearIsometryEquiv_toFun {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] [∀ (i : ι₁), FiniteDimensional 𝕜 (M₁ i)] [∀ (i : ι₂), FiniteDimensional 𝕜 (M₂ i)] (a : TensorProduct 𝕜 ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) (i : ι₁ × ι₂) :

PiLp_tensorLinearIsometryEquiv a i = directSumTensorToFun a i

source

@[simp]

theorem PiLp_tensorLinearIsometryEquiv_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] [∀ (i : ι₁), FiniteDimensional 𝕜 (M₁ i)] [∀ (i : ι₂), FiniteDimensional 𝕜 (M₂ i)] (a : (i : ι₁ × ι₂) → TensorProduct 𝕜 (M₁ i.1) (M₂ i.2)) :

PiLp_tensorLinearIsometryEquiv.symm a = directSumTensorInvFun a

source

@[simp]

theorem PiLp_tensorLinearIsometryEquiv_apply {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] [∀ (i : ι₁), FiniteDimensional 𝕜 (M₁ i)] [∀ (i : ι₂), FiniteDimensional 𝕜 (M₂ i)] (a : TensorProduct 𝕜 ((i : ι₁) → M₁ i) ((i : ι₂) → M₂ i)) (i : ι₁ × ι₂) :

PiLp_tensorLinearIsometryEquiv a i = directSumTensorToFun a i

source

theorem PiLp_tensorLinearIsometryEquiv_tmul {𝕜 : Type u_1} [RCLike 𝕜] {ι₁ : Type u_4} {ι₂ : Type u_5} [DecidableEq ι₁] [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type u_6} {M₂ : ι₂ → Type u_7} [(i₁ : ι₁) → NormedAddCommGroup (M₁ i₁)] [(i₂ : ι₂) → NormedAddCommGroup (M₂ i₂)] [(i₁ : ι₁) → InnerProductSpace 𝕜 (M₁ i₁)] [(i₂ : ι₂) → InnerProductSpace 𝕜 (M₂ i₂)] [∀ (i : ι₁), FiniteDimensional 𝕜 (M₁ i)] [∀ (i : ι₂), FiniteDimensional 𝕜 (M₂ i)] (x : PiLp 2 M₁) (y : PiLp 2 M₂) (i : ι₁ × ι₂) :

PiLp_tensorLinearIsometryEquiv (x ⊗ₜ[𝕜] y) i = x i.1 ⊗ₜ[𝕜] y i.2

source

@[reducible, inline]

noncomputable abbrev euclideanSpaceTensor {R : Type u_4} [RCLike R] {ι₁ : Type u_5} {ι₂ : Type u_6} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] :

TensorProduct R (EuclideanSpace R ι₁) (EuclideanSpace R ι₂) ≃ₗᵢ[R] EuclideanSpace (TensorProduct R R R) (ι₁ × ι₂)

Equations

euclideanSpaceTensor = PiLp_tensorLinearIsometryEquiv

Instances For

source

theorem euclideanSpaceTensor_apply {R : Type u_4} [RCLike R] {ι₁ : Type u_5} {ι₂ : Type u_6} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (x : EuclideanSpace R ι₁) (y : EuclideanSpace R ι₂) (i : ι₁ × ι₂) :

euclideanSpaceTensor (x ⊗ₜ[R] y) i = x i.1 ⊗ₜ[R] y i.2

source

noncomputable def TensorProduct.lid_linearIsometryEquiv (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

TensorProduct 𝕜 𝕜 E ≃ₗᵢ[𝕜] E

Equations

TensorProduct.lid_linearIsometryEquiv 𝕜 E = { toLinearEquiv := TensorProduct.lid 𝕜 E, norm_map' := ⋯ }

Instances For

source

@[simp]

theorem TensorProduct.lid_linearIsometryEquiv_apply (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

∀ (a : TensorProduct 𝕜 𝕜 E), (TensorProduct.lid_linearIsometryEquiv 𝕜 E) a = (TensorProduct.liftAux (LinearMap.lsmul 𝕜 E)) a

source

@[simp]

theorem TensorProduct.lid_linearIsometryEquiv_invFun (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (a : E) :

(TensorProduct.lid_linearIsometryEquiv 𝕜 E).invFun a = 1 ⊗ₜ[𝕜] a

source

@[simp]

theorem TensorProduct.lid_linearIsometryEquiv_symm_apply (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (a : E) :

(TensorProduct.lid_linearIsometryEquiv 𝕜 E).symm a = 1 ⊗ₜ[𝕜] a

source

@[simp]

theorem TensorProduct.lid_linearIsometryEquiv_toFun (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

∀ (a : TensorProduct 𝕜 𝕜 E), (TensorProduct.lid_linearIsometryEquiv 𝕜 E) a = (TensorProduct.liftAux (LinearMap.lsmul 𝕜 E)) a

source

@[reducible, inline]

noncomputable abbrev euclideanSpaceTensor' {R : Type u_4} [RCLike R] {ι₁ : Type u_5} {ι₂ : Type u_6} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] :

TensorProduct R (EuclideanSpace R ι₁) (EuclideanSpace R ι₂) ≃ₗᵢ[R] EuclideanSpace R (ι₁ × ι₂)

Equations

euclideanSpaceTensor' = euclideanSpaceTensor.trans (LinearIsometryEquiv.piLpCongrRight 2 fun (x : ι₁ × ι₂) => TensorProduct.lid_linearIsometryEquiv R R)

Instances For

source

theorem euclideanSpaceTensor'_apply {R : Type u_4} [RCLike R] {ι₁ : Type u_5} {ι₂ : Type u_6} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (x : EuclideanSpace R ι₁) (y : EuclideanSpace R ι₂) (i : ι₁ × ι₂) :

euclideanSpaceTensor' (x ⊗ₜ[R] y) i = x i.1 * y i.2

source

theorem LinearIsometryEquiv.linearMap_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {f : E ≃ₗᵢ[𝕜] F} :

LinearMap.adjoint ↑f.toLinearEquiv = ↑f.symm.toLinearEquiv

source

theorem TensorProduct.ring_tmul {R : Type u_4} [CommRing R] (x : TensorProduct R R R) :

∃ (a : R) (b : R), x = a ⊗ₜ[R] b

source

theorem submodule_neq_tensorProduct_of {R : Type u_4} [RCLike R] {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace R E] [InnerProductSpace R F] [FiniteDimensional R E] [FiniteDimensional R F] (U : Submodule R (TensorProduct R E F)) {p : ℕ} (hp : Nat.Prime p) (hU : Module.finrank R ↥U = p) :

¬∃ (V : Submodule R E) (W : Submodule R F) (_ : 1 < Module.finrank R ↥V) (_ : 1 < Module.finrank R ↥W), U = V.tensorProduct W