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
orthonormal_basis.to_matrix
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_1}
{E : Type (max u_2 u_3)}
[fintype n]
[decidable_eq n]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
(b : orthonormal_basis n 𝕜 E) :
the star-algebraic isomorphism from E →ₗ[𝕜] E to the matrix ring M_n(𝕜) given by
the orthonormal basis b on E
Equations
- b.to_matrix = {to_fun := λ (x : E →ₗ[𝕜] E) (k p : n), has_inner.inner (⇑b k) (⇑x (⇑b p)), inv_fun := λ (x : matrix n n 𝕜), finset.univ.sum (λ (i : n), finset.univ.sum (λ (j : n), x i j • ↑(rank_one (⇑b i) (⇑b j)))), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}
theorem
orthonormal_basis.to_matrix_apply
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_1}
{E : Type (max u_2 u_3)}
[fintype n]
[decidable_eq n]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
(b : orthonormal_basis n 𝕜 E)
(x : E →ₗ[𝕜] E)
(i j : n) :
theorem
orthonormal_basis.to_matrix_symm_apply
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_1}
{E : Type (max u_2 u_3)}
[fintype n]
[decidable_eq n]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
(b : orthonormal_basis n 𝕜 E)
(x : matrix n n 𝕜) :
theorem
orthonormal_basis.to_matrix_symm_apply'
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_1}
{E : Type (max u_2 u_3)}
[fintype n]
[decidable_eq n]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
(b : orthonormal_basis n 𝕜 E)
(x : matrix n n 𝕜) :
⇑(b.to_matrix.symm) x = ⇑(b.repr.symm.to_linear_equiv.conj) x.mul_vec_lin
theorem
orthonormal_basis_to_matrix_eq_basis_to_matrix
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_1}
{E : Type (max u_2 u_3)}
[fintype n]
[decidable_eq n]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
(b : orthonormal_basis n 𝕜 E) :
noncomputable
def
euclidean_space.orthonormal_basis
(n : Type u_1)
(𝕜 : Type u_2)
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n] :
orthonormal_basis n 𝕜 (euclidean_space 𝕜 n)
Equations
theorem
euclidean_space.orthonormal_basis.repr_eq_one
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_1}
[fintype n]
[decidable_eq n] :
(euclidean_space.orthonormal_basis n 𝕜).repr = 1
theorem
linear_isometry_equiv.to_linear_equiv_one
{R : Type u_1}
{E : Type u_2}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
1.to_linear_equiv = 1
theorem
linear_equiv.one_symm
{R : Type u_1}
{E : Type u_2}
[semiring R]
[add_comm_monoid E]
[module R E] :
theorem
linear_equiv.to_linear_map_one
{R : Type u_1}
{E : Type u_2}
[semiring R]
[add_comm_monoid E]
[module R E] :
1.to_linear_map = 1
theorem
linear_equiv.refl_conj
{R : Type u_1}
{E : Type u_2}
[comm_semiring R]
[add_comm_monoid E]
[module R E] :
(linear_equiv.refl R E).conj = 1
theorem
linear_equiv.conj_mul
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[comm_semiring R]
[add_comm_monoid E]
[add_comm_monoid F]
[module R E]
[module R F]
(f : E ≃ₗ[R] F)
(x y : module.End R E) :
theorem
linear_equiv.conj_apply_one
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[comm_semiring R]
[add_comm_monoid E]
[add_comm_monoid F]
[module R E]
[module R F]
(f : E ≃ₗ[R] F) :
theorem
linear_equiv.conj_one
{R : Type u_1}
{E : Type u_2}
[comm_semiring R]
[add_comm_monoid E]
[module R E] :
theorem
linear_equiv.one_apply
{R : Type u_1}
{E : Type u_2}
[comm_semiring R]
[add_comm_monoid E]
[module R E]
(x : E) :
theorem
orthonormal_basis.std_to_matrix
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_1}
[fintype n]
[decidable_eq n] :
theorem
matrix.std_basis_repr_eq_reshape
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J] :
(matrix.std_basis R I J).equiv_fun = matrix.reshape
def
linear_equiv.inner_conj
{R : Type u_1}
{E : Type u_2}
{F : Type u_3}
[comm_semiring R]
[add_comm_monoid E]
[add_comm_monoid F]
[module R E]
[module R F]
(ϱ : E ≃ₗ[R] F) :
Equations
- ϱ.inner_conj = alg_equiv.of_linear_equiv ϱ.conj _ _
theorem
linear_map.to_matrix_std_basis_std_basis
{R : Type u_1}
[comm_semiring R]
{I : Type u_2}
{J : Type u_3}
{K : Type u_4}
{L : Type u_5}
[fintype I]
[fintype J]
[fintype K]
[fintype L]
[decidable_eq I]
[decidable_eq J]
(x : matrix I J R →ₗ[R] matrix K L R) :
⇑(linear_map.to_matrix (matrix.std_basis R I J) (matrix.std_basis R K L)) x = ⇑linear_map.to_matrix' (matrix.reshape.to_linear_map.comp (x.comp matrix.reshape.symm.to_linear_map))
theorem
linear_map.to_lin_std_basis_std_basis
{R : Type u_1}
[comm_semiring R]
{I : Type u_2}
{J : Type u_3}
{K : Type u_4}
{L : Type u_5}
[fintype I]
[fintype J]
[fintype K]
[fintype L]
[decidable_eq I]
[decidable_eq J]
(x : matrix (K × L) (I × J) R) :
⇑(matrix.to_lin (matrix.std_basis R I J) (matrix.std_basis R K L)) x = matrix.reshape.symm.to_linear_map.comp ((⇑matrix.to_lin' x).comp matrix.reshape.to_linear_map)
def
linear_map.to_matrix_of_alg_equiv
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J] :
theorem
linear_map.to_matrix_of_alg_equiv_apply
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J]
(x : matrix I J R →ₗ[R] matrix I J R) :
theorem
linear_map.to_matrix_of_alg_equiv_symm_apply
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J]
(x : matrix (I × J) (I × J) R) :
theorem
linear_map.to_matrix_of_alg_equiv_apply'
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J]
(x : matrix I J R →ₗ[R] matrix I J R)
(ij kl : I × J) :
⇑linear_map.to_matrix_of_alg_equiv x ij kl = ⇑x (matrix.std_basis_matrix kl.fst kl.snd 1) ij.fst ij.snd
def
matrix.to_lin_of_alg_equiv
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J] :
theorem
matrix.to_lin_of_alg_equiv_apply
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J]
(x : matrix (I × J) (I × J) R)
(y : matrix I J R) :
⇑(⇑matrix.to_lin_of_alg_equiv x) y = ⇑(matrix.reshape.symm) (⇑(⇑matrix.to_lin_alg_equiv' x) (⇑matrix.reshape y))
def
matrix.rank_one_std_basis
{R : Type u_1}
[comm_semiring R]
{I : Type u_2}
{J : Type u_3}
[decidable_eq I]
[decidable_eq J]
(ij kl : I × J)
(r : R) :
theorem
matrix.rank_one_std_basis_apply
{R : Type u_1}
[comm_semiring R]
{I : Type u_2}
{J : Type u_3}
[decidable_eq I]
[decidable_eq J]
(ij kl : I × J)
(r : R)
(x : matrix I J R) :
⇑(matrix.rank_one_std_basis ij kl r) x = matrix.std_basis_matrix ij.fst ij.snd (r • r • x kl.fst kl.snd)
theorem
matrix.to_lin_of_alg_equiv_eq
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J]
(x : matrix (I × J) (I × J) R) :
⇑matrix.to_lin_of_alg_equiv x = finset.univ.sum (λ (ij : I × J), finset.univ.sum (λ (kl : I × J), x ij kl • matrix.rank_one_std_basis ij kl 1))
theorem
matrix.to_lin_of_alg_equiv_to_matrix_of_alg_equiv
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J]
(x : matrix (I × J) (I × J) R) :
theorem
linear_map.to_matrix_of_alg_equiv_to_lin_of_alg_equiv
{R : Type u_1}
{I : Type u_2}
{J : Type u_3}
[fintype I]
[fintype J]
[comm_semiring R]
[decidable_eq I]
[decidable_eq J]
(x : matrix I J R →ₗ[R] matrix I J R) :
theorem
inner_aut_coord
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_5}
[fintype n]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
theorem
matrix.inner_aut_coord
{𝕜 : Type u_4}
[is_R_or_C 𝕜]
{n : Type u_5}
[fintype n]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(ij kl : n × n) :
⇑linear_map.to_matrix_of_alg_equiv (matrix.inner_aut U) ij kl = ⇑U ij.fst kl.fst * has_star.star (⇑U ij.snd kl.snd)
theorem
inner_aut_inv_coord
{n : Type u_5}
[fintype n]
[decidable_eq n]
(U : ↥(matrix.unitary_group n ℂ))
(ij kl : n × n) :
⇑linear_map.to_matrix_of_alg_equiv (matrix.inner_aut U⁻¹) ij kl = ⇑U kl.snd ij.snd * has_star.star (⇑U kl.fst ij.fst)