to_matrix_of_equiv

This defines the identification $L(M_{n \times m})\cong_{a} M_{n \times m}$ (see linear_map.to_matrix_of_alg_equiv; also see matrix.to_lin_of_alg_equiv).

noncomputable def OrthonormalBasis.toMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} {E : Type u_3} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) : (E →ₗ[𝕜] E) ≃⋆ₐ[𝕜] Matrix n n 𝕜

the star-algebraic isomorphism from E →ₗ[𝕜] E to the matrix ring M_n(𝕜) given by the orthonormal basis b on E

Equations

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

theorem OrthonormalBasis.toMatrix_apply {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) (x : E →ₗ[𝕜] E) (i : n) (j : n) : b.toMatrix x i j = inner (b i) (x (b j))

theorem OrthonormalBasis.toMatrix_symm_apply {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) (x : Matrix n n 𝕜) : b.toMatrix.symm x = ∑ i : n, ∑ j : n, x i j • ↑(((rankOne 𝕜) (b i)) (b j))

theorem OrthonormalBasis.toMatrix_symm_apply' {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) (x : Matrix n n 𝕜) : b.toMatrix.symm x = b.repr.symm.conj (Matrix.toEuclideanLin x)

theorem orthonormalBasis_toMatrix_eq_basis_toMatrix {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_1} {E : Type u_2} [Fintype n] [DecidableEq n] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (b : OrthonormalBasis n 𝕜 E) : LinearMap.toMatrixAlgEquiv b.toBasis = b.toMatrix.toAlgEquiv

def EuclideanSpace.orthonormalBasis (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] : OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)

Alias of EuclideanSpace.basisFun.

---

The basis Pi.basisFun, bundled as an orthornormal basis of EuclideanSpace 𝕜 ι.

Equations

• EuclideanSpace.orthonormalBasis = EuclideanSpace.basisFun

theorem EuclideanSpace.orthonormalBasis.repr_eq_one {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] : (EuclideanSpace.orthonormalBasis n 𝕜).repr = 1

theorem LinearIsometryEquiv.toLinearEquiv_one {R : Type u_1} {E : Type u_2} [_inst_1 : Semiring R] [_inst_25 : SeminormedAddCommGroup E] [_inst_29 : Module R E] : LinearIsometryEquiv.toLinearEquiv 1 = 1

theorem LinearEquiv.one_symm {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] : LinearEquiv.symm 1 = 1

theorem LinearEquiv.toLinearMap_one {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [Module R E] : ↑1 = 1

theorem LinearEquiv.refl_conj {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommMonoid E] [Module R E] : (LinearEquiv.refl R E).conj = 1

theorem LinearEquiv.conj_hMul {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (f : E ≃ₗ[R] F) (x : Module.End R E) (y : Module.End R E) : f.conj (x * y) = f.conj x * f.conj y

theorem LinearEquiv.conj_apply_one {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (f : E ≃ₗ[R] F) : f.conj 1 = 1

theorem LinearEquiv.conj_one {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommMonoid E] [Module R E] : LinearEquiv.conj 1 = 1

theorem LinearEquiv.one_apply {R : Type u_1} {E : Type u_2} [CommSemiring R] [AddCommMonoid E] [Module R E] (x : E) : 1 x = x

theorem OrthonormalBasis.std_toMatrix {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] : (EuclideanSpace.orthonormalBasis n 𝕜).toMatrix.symm.toLinearEquiv = Matrix.toEuclideanLin

theorem Matrix.stdBasis_repr_eq_reshape {R : Type u_1} {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] : (Matrix.stdBasis R I J).equivFun = Matrix.reshape

def LinearEquiv.innerConj {R : Type u_1} {E : Type u_2} {F : Type u_3} [CommSemiring R] [AddCommMonoid E] [AddCommMonoid F] [Module R E] [Module R F] (ϱ : E ≃ₗ[R] F) : (E →ₗ[R] E) ≃ₐ[R] F →ₗ[R] F

Equations

• ϱ.innerConj = AlgEquiv.ofLinearEquiv ϱ.conj ⋯ ⋯

theorem LinearMap.toMatrix_stdBasis_stdBasis {R : Type u_5} [CommSemiring R] {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} [Fintype I] [Fintype J] [Fintype K] [Fintype L] [DecidableEq I] [DecidableEq J] (x : Matrix I J R →ₗ[R] Matrix K L R) : (LinearMap.toMatrix (Matrix.stdBasis R I J) (Matrix.stdBasis R K L)) x = LinearMap.toMatrix' (↑Matrix.reshape ∘ₗ x ∘ₗ ↑Matrix.reshape.symm)

theorem LinearMap.toLin_stdBasis_stdBasis {R : Type u_5} [CommSemiring R] {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} [Fintype I] [Fintype J] [Fintype K] [Fintype L] [DecidableEq I] [DecidableEq J] (x : Matrix (K × L) (I × J) R) : (Matrix.toLin (Matrix.stdBasis R I J) (Matrix.stdBasis R K L)) x = ↑Matrix.reshape.symm ∘ₗ Matrix.toLin' x ∘ₗ ↑Matrix.reshape

def LinearMap.toMatrixOfAlgEquiv {R : Type u_1} {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] : (Matrix I J R →ₗ[R] Matrix I J R) ≃ₐ[R] Matrix (I × J) (I × J) R

Equations

• LinearMap.toMatrixOfAlgEquiv = Matrix.reshape.innerConj.trans LinearMap.toMatrixAlgEquiv'

theorem LinearMap.toMatrixOfAlgEquiv_apply {R : Type u_1} {I : Type u_3} {J : Type u_2} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix I J R →ₗ[R] Matrix I J R) : LinearMap.toMatrixOfAlgEquiv x = LinearMap.toMatrixAlgEquiv' (↑Matrix.reshape ∘ₗ x ∘ₗ ↑Matrix.reshape.symm)

theorem LinearMap.toMatrixOfAlgEquiv_symm_apply {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) : LinearMap.toMatrixOfAlgEquiv.symm x = ↑Matrix.reshape.symm ∘ₗ LinearMap.toMatrixAlgEquiv'.symm x ∘ₗ ↑Matrix.reshape

theorem LinearMap.toMatrixOfAlgEquiv_apply' {R : Type u_1} {I : Type u_3} {J : Type u_2} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix I J R →ₗ[R] Matrix I J R) (ij : I × J) (kl : I × J) : LinearMap.toMatrixOfAlgEquiv x ij kl = x (Matrix.stdBasisMatrix kl.1 kl.2 1) ij.1 ij.2

def Matrix.toLinOfAlgEquiv {R : Type u_1} {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] : Matrix (I × J) (I × J) R ≃ₐ[R] Matrix I J R →ₗ[R] Matrix I J R

Equations

• Matrix.toLinOfAlgEquiv = LinearMap.toMatrixOfAlgEquiv.symm

theorem Matrix.toLinOfAlgEquiv_apply {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) (y : Matrix I J R) : (Matrix.toLinOfAlgEquiv x) y = Matrix.reshape.symm ((Matrix.toLinAlgEquiv' x) (Matrix.reshape y))

def Matrix.rankOneStdBasis {R : Type u_1} [CommSemiring R] {I : Type u_2} {J : Type u_3} [DecidableEq I] [DecidableEq J] (ij : I × J) (kl : I × J) (r : R) : Matrix I J R →ₗ[R] Matrix I J R

Equations

• Matrix.rankOneStdBasis ij kl r = { toFun := fun (x : Matrix I J R) => Matrix.stdBasisMatrix ij.1 ij.2 (r • r • x kl.1 kl.2), map_add' := ⋯, map_smul' := ⋯ }

theorem Matrix.rankOneStdBasis_apply {R : Type u_3} [CommSemiring R] {I : Type u_1} {J : Type u_2} [DecidableEq I] [DecidableEq J] (ij : I × J) (kl : I × J) (r : R) (x : Matrix I J R) : (Matrix.rankOneStdBasis ij kl r) x = Matrix.stdBasisMatrix ij.1 ij.2 (r • r • x kl.1 kl.2)

theorem Matrix.toLinOfAlgEquiv_eq {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) : Matrix.toLinOfAlgEquiv x = ∑ ij : I × J, ∑ kl : I × J, x ij kl • Matrix.rankOneStdBasis ij kl 1

theorem Matrix.toLinOfAlgEquiv_toMatrixOfAlgEquiv {R : Type u_3} {I : Type u_2} {J : Type u_1} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix (I × J) (I × J) R) : LinearMap.toMatrixOfAlgEquiv (Matrix.toLinOfAlgEquiv x) = x

theorem LinearMap.toMatrixOfAlgEquiv_toLinOfAlgEquiv {R : Type u_1} {I : Type u_3} {J : Type u_2} [Fintype I] [Fintype J] [CommSemiring R] [DecidableEq I] [DecidableEq J] (x : Matrix I J R →ₗ[R] Matrix I J R) : Matrix.toLinOfAlgEquiv (LinearMap.toMatrixOfAlgEquiv x) = x

theorem innerAut_toMatrix {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) : LinearMap.toMatrixOfAlgEquiv (Matrix.innerAut U) = Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) (↑U) (↑U).conj

theorem innerAut_coord {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n 𝕜)) (ij : n × n) (kl : n × n) : LinearMap.toMatrixOfAlgEquiv (Matrix.innerAut U) ij kl = ↑U ij.1 kl.1 * star (↑U ij.2 kl.2)

theorem innerAut_inv_coord {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) (ij : n × n) (kl : n × n) : LinearMap.toMatrixOfAlgEquiv (Matrix.innerAut U⁻¹) ij kl = ↑U kl.2 ij.2 * star (↑U kl.1 ij.1)