Inner automorphisms #
This file defines the inner automorphism of a unitary matrix U as U x U⁻¹ and proves that any star-algebraic automorphism on Mₙ(ℂ) is an inner automorphism.
def
unitary.inner_aut_star_alg
(K : Type u_1)
{R : Type u_2}
[comm_semiring K]
[semiring R]
[star_semigroup R]
[algebra K R]
(a : ↥(unitary R)) :
Equations
- unitary.inner_aut_star_alg K a = let _inst : invertible ↑a := {inv_of := has_star.star ↑a, inv_of_mul_self := _, mul_inv_of_self := _} in star_alg_equiv.of_alg_equiv (algebra.aut_inner ↑a) _
theorem
unitary.inner_aut_star_alg_apply
{K : Type u_1}
{R : Type u_2}
[comm_semiring K]
[semiring R]
[star_semigroup R]
[algebra K R]
(U : ↥(unitary R))
(x : R) :
⇑(unitary.inner_aut_star_alg K U) x = ↑U * x * ↑(has_star.star U)
theorem
unitary.inner_aut_star_alg_apply'
{K : Type u_1}
{R : Type u_2}
[comm_semiring K]
[semiring R]
[star_semigroup R]
[algebra K R]
(U : ↥(unitary R))
(x : R) :
theorem
unitary.inner_aut_star_alg_symm_apply
{K : Type u_1}
{R : Type u_2}
[comm_semiring K]
[semiring R]
[star_semigroup R]
[algebra K R]
(U : ↥(unitary R))
(x : R) :
⇑((unitary.inner_aut_star_alg K U).symm) x = ↑(has_star.star U) * x * ↑U
theorem
unitary.inner_aut_star_alg_symm_apply'
{K : Type u_1}
{R : Type u_2}
[comm_semiring K]
[semiring R]
[star_semigroup R]
[algebra K R]
(U : ↥(unitary R))
(x : R) :
theorem
unitary.inner_aut_star_alg_symm
{K : Type u_1}
{R : Type u_2}
[comm_semiring K]
[semiring R]
[star_semigroup R]
[algebra K R]
(U : ↥(unitary R)) :
@[simp]
theorem
matrix.unitary_group.mul_star_self
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(a : ↥(matrix.unitary_group n 𝕜)) :
matrix.mul ⇑a (has_star.star ⇑a) = 1
@[simp]
theorem
matrix.unitary_group.star_coe_eq_coe_star
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
has_star.star ⇑U = ⇑(has_star.star U)
def
matrix.inner_aut_star_alg
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(a : ↥(matrix.unitary_group n 𝕜)) :
given a unitary $U$, we have the inner algebraic automorphism, given by $x \mapsto UxU^*$ with its inverse given by $x \mapsto U^* x U$
Equations
theorem
matrix.inner_aut_star_alg_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut_star_alg U) x = (matrix.mul ⇑U x).mul ⇑(has_star.star U)
theorem
matrix.inner_aut_star_alg_apply'
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut_star_alg U) x = (matrix.mul ⇑U x).mul ⇑U⁻¹
theorem
matrix.inner_aut_star_alg_symm_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑((matrix.inner_aut_star_alg U).symm) x = (matrix.mul ⇑(has_star.star U) x).mul ⇑U
theorem
matrix.inner_aut_star_alg_symm_apply'
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑((matrix.inner_aut_star_alg U).symm) x = (matrix.mul ⇑U⁻¹ x).mul ⇑U
@[simp]
theorem
matrix.inner_aut_star_alg_symm
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
def
matrix.inner_aut
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
inner automorphism (matrix.inner_aut_star_alg), but as a linear map
Equations
@[simp]
theorem
matrix.inner_aut_coe
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
@[simp]
theorem
matrix.inner_aut_inv_coe
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
⇑(matrix.inner_aut U⁻¹) = ⇑((matrix.inner_aut_star_alg U).symm)
theorem
matrix.inner_aut_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut U) x = (matrix.mul ⇑U x).mul ⇑U⁻¹
theorem
matrix.inner_aut_apply'
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut U) x = (matrix.mul ⇑U x).mul ⇑(has_star.star U)
theorem
matrix.inner_aut_inv_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut U⁻¹) x = (matrix.mul ⇑U⁻¹ x).mul ⇑U
theorem
matrix.inner_aut_star_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut (has_star.star U)) x = (matrix.mul ⇑(has_star.star U) x).mul ⇑U
theorem
matrix.inner_aut_conj_transpose
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
(⇑(matrix.inner_aut U) x).conj_transpose = ⇑(matrix.inner_aut U) x.conj_transpose
theorem
matrix.inner_aut_comp_inner_aut
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U₁ U₂ : ↥(matrix.unitary_group n 𝕜)) :
(matrix.inner_aut U₁).comp (matrix.inner_aut U₂) = matrix.inner_aut (U₁ * U₂)
theorem
matrix.inner_aut_apply_inner_aut
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U₁ U₂ : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut U₁) (⇑(matrix.inner_aut U₂) x) = ⇑(matrix.inner_aut (U₁ * U₂)) x
theorem
matrix.inner_aut_eq_iff
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x y : matrix n n 𝕜) :
⇑(matrix.inner_aut U) x = y ↔ x = ⇑(matrix.inner_aut U⁻¹) y
theorem
matrix.unitary_group.to_linear_equiv_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : n → 𝕜) :
⇑(matrix.unitary_group.to_linear_equiv U) x = ↑U.mul_vec x
theorem
matrix.unitary_group.to_linear_equiv_eq
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : n → 𝕜) :
theorem
matrix.unitary_group.to_lin'_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : n → 𝕜) :
⇑(matrix.unitary_group.to_lin' U) x = ↑U.mul_vec x
theorem
matrix.unitary_group.to_lin'_eq
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : n → 𝕜) :
⇑(matrix.unitary_group.to_lin' U) x = ⇑(⇑matrix.to_lin' ⇑U) x
theorem
matrix.inner_aut.spectrum_eq
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
spectrum 𝕜 (⇑matrix.to_lin' (⇑(matrix.inner_aut U) x)) = spectrum 𝕜 (⇑matrix.to_lin' x)
the spectrum of $U x U^*$ for any unitary $U$ is equal to the spectrum of $x$
theorem
matrix.inner_aut_one
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n] :
matrix.inner_aut 1 = 1
theorem
matrix.inner_aut_comp_inner_aut_inv
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
(matrix.inner_aut U).comp (matrix.inner_aut U⁻¹) = 1
theorem
matrix.inner_aut_apply_inner_aut_inv
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U₁ U₂ : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut U₁) (⇑(matrix.inner_aut U₂⁻¹) x) = ⇑(matrix.inner_aut (U₁ * U₂⁻¹)) x
theorem
matrix.inner_aut_apply_inner_aut_inv_self
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut U) (⇑(matrix.inner_aut U⁻¹) x) = x
theorem
matrix.inner_aut_inv_apply_inner_aut_self
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut U⁻¹) (⇑(matrix.inner_aut U) x) = x
theorem
matrix.inner_aut_apply_zero
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
⇑(matrix.inner_aut U) 0 = 0
theorem
matrix.inner_aut_conj_spectrum_eq
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜 →ₗ[𝕜] matrix n n 𝕜) :
spectrum 𝕜 ((matrix.inner_aut U⁻¹).comp (x.comp (matrix.inner_aut U))) = spectrum 𝕜 x
the spectrum of a linear map $x$ equals the spectrum of
$f_U^{-1} x f_U$ for some unitary $U$ and $f_U$ is
the inner automorphism (matrix.inner_aut)
theorem
matrix.inner_aut_apply_one
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
⇑(matrix.inner_aut U) 1 = 1
the inner automorphism is unital
theorem
matrix.inner_aut_star_alg_apply_eq_inner_aut_apply
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
⇑(matrix.inner_aut_star_alg U) x = ⇑(matrix.inner_aut U) x
theorem
matrix.inner_aut.map_mul
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x y : matrix n n 𝕜) :
⇑(matrix.inner_aut U) (x.mul y) = (⇑(matrix.inner_aut U) x).mul (⇑(matrix.inner_aut U) y)
theorem
matrix.inner_aut.map_star
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
has_star.star (⇑(matrix.inner_aut U) x) = ⇑(matrix.inner_aut U) (has_star.star x)
theorem
matrix.inner_aut_inv_eq_star
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
{x : ↥(matrix.unitary_group n 𝕜)} :
theorem
matrix.unitary_group.coe_inv
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
theorem
matrix.inner_aut.map_inv
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
(⇑(matrix.inner_aut U) x)⁻¹ = ⇑(matrix.inner_aut U) x⁻¹
theorem
matrix.inner_aut_apply_trace_eq
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
(⇑(matrix.inner_aut U) x).trace = x.trace
the trace of $f_U(x)$ is equal to the trace of $x$
theorem
matrix.exists_inner_aut_iff_exists_inner_aut_inv
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
{P : matrix n n 𝕜 → Prop}
(x : matrix n n 𝕜) :
(∃ (U : ↥(matrix.unitary_group n 𝕜)), P (⇑(matrix.inner_aut U) x)) ↔ ∃ (U : ↥(matrix.unitary_group n 𝕜)), P (⇑(matrix.inner_aut U⁻¹) x)
theorem
matrix.inner_aut.is_injective
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
theorem
matrix.is_hermitian.inner_aut_iff
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
x.is_hermitian ↔ (⇑(matrix.inner_aut U) x).is_hermitian
$x$ is Hermitian if and only if $f_U(x)$ is Hermitian
theorem
matrix.pos_semidef.inner_aut
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
(U : ↥(matrix.unitary_group n 𝕜))
{a : matrix n n 𝕜} :
(⇑(matrix.inner_aut U) a).pos_semidef ↔ a.pos_semidef
theorem
matrix.pos_def.inner_aut
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
(⇑(matrix.inner_aut U) x).pos_def ↔ x.pos_def
$f_U(x)$ is positive definite if and only if $x$ is positive definite
theorem
matrix.is_almost_hermitian.schur_decomp
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{A : matrix n n 𝕜}
(hA : A.is_almost_hermitian) :
∃ (D : n → 𝕜) (U : ↥(matrix.unitary_group n 𝕜)), ⇑(matrix.inner_aut U) (matrix.diagonal D) = A
Schur decomposition, but only for almost Hermitian matrices: given an almost Hermitian matrix $A$, there exists a diagonal matrix $D$ and a unitary matrix $U$ such that $UDU^*=A$
theorem
matrix.star_alg_equiv.of_matrix_is_inner
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
(f : matrix n n 𝕜 ≃⋆ₐ[𝕜] matrix n n 𝕜) :
∃ (U : ↥(matrix.unitary_group n 𝕜)), matrix.inner_aut_star_alg U = f
any $^*$-isomorphism on $M_n$ is an inner automorphism
noncomputable
def
matrix.star_alg_equiv.unitary
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
(f : matrix n n 𝕜 ≃⋆ₐ[𝕜] matrix n n 𝕜) :
↥(matrix.unitary_group n 𝕜)
Equations
- matrix.star_alg_equiv.unitary f = (λ (_x : matrix.inner_aut_star_alg (classical.some _) = f), classical.some _) _
def
matrix.star_alg_equiv.eq_inner_aut
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
(f : matrix n n 𝕜 ≃⋆ₐ[𝕜] matrix n n 𝕜) :
theorem
matrix.is_hermitian.spectral_theorem'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{x : matrix n n 𝕜}
(hx : x.is_hermitian) :
x = ⇑(matrix.inner_aut ⟨hx.eigenvector_matrix, _⟩) (matrix.diagonal (coe ∘ hx.eigenvalues))
theorem
matrix.coe_diagonal_eq_diagonal_coe
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq n]
(x : n → ℝ) :
matrix.diagonal (coe ∘ x) = coe ∘ matrix.diagonal x
theorem
matrix.diagonal.spectrum
{𝕜 : Type u_1}
{n : Type u_2}
[field 𝕜]
[fintype n]
[decidable_eq n]
(A : n → 𝕜) :
spectrum 𝕜 (⇑matrix.to_lin' (matrix.diagonal A)) = {x : 𝕜 | ∃ (i : n), A i = x}
theorem
matrix.is_hermitian.spectrum
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{x : matrix n n 𝕜}
(hx : x.is_hermitian) :
spectrum 𝕜 (⇑matrix.to_lin' x) = {x_1 : 𝕜 | ∃ (i : n), ↑(hx.eigenvalues i) = x_1}
theorem
matrix.is_hermitian.has_eigenvalue_iff
{n : Type u_1}
[fintype n]
[decidable_eq n]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
{x : matrix n n 𝕜}
(hx : x.is_hermitian)
(α : 𝕜) :
module.End.has_eigenvalue (⇑matrix.to_lin' x) α ↔ ∃ (i : n), ↑(hx.eigenvalues i) = α
theorem
matrix.inner_aut_commutes_with_map_lid_symm
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
(tensor_product.map 1 (matrix.inner_aut U)).comp (tensor_product.lid 𝕜 (matrix n n 𝕜)).symm.to_linear_map = (tensor_product.lid 𝕜 (matrix n n 𝕜)).symm.to_linear_map.comp (matrix.inner_aut U)
theorem
matrix.inner_aut_commutes_with_lid_comm
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
(tensor_product.lid 𝕜 (matrix n n 𝕜)).to_linear_map.comp ((tensor_product.comm 𝕜 (matrix n n 𝕜) 𝕜).to_linear_map.comp (tensor_product.map (matrix.inner_aut U) 1)) = (matrix.inner_aut U).comp ((tensor_product.lid 𝕜 (matrix n n 𝕜)).to_linear_map.comp (tensor_product.comm 𝕜 (matrix n n 𝕜) 𝕜).to_linear_map)
theorem
matrix.unitary_group.conj_mem
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
def
matrix.unitary_group.conj
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
↥(matrix.unitary_group n 𝕜)
Equations
- matrix.unitary_group.conj U = ⟨matrix.conj ⇑U, _⟩
@[norm_cast]
theorem
matrix.unitary_group.conj_coe
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜)) :
theorem
matrix.inner_aut.conj
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
(U : ↥(matrix.unitary_group n 𝕜))
(x : matrix n n 𝕜) :
(⇑(matrix.inner_aut U) x).conj = ⇑(matrix.inner_aut (matrix.unitary_group.conj U)) x.conj
theorem
matrix.kronecker_mem_unitary_group
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
{p : Type u_3}
[fintype p]
[decidable_eq p]
(U₁ : ↥(matrix.unitary_group n 𝕜))
(U₂ : ↥(matrix.unitary_group p 𝕜)) :
matrix.kronecker_map has_mul.mul ⇑U₁ ⇑U₂ ∈ matrix.unitary_group (n × p) 𝕜
def
matrix.unitary_group.kronecker
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
{p : Type u_3}
[fintype p]
[decidable_eq p]
(U₁ : ↥(matrix.unitary_group n 𝕜))
(U₂ : ↥(matrix.unitary_group p 𝕜)) :
↥(matrix.unitary_group (n × p) 𝕜)
Equations
- matrix.unitary_group.kronecker U₁ U₂ = ⟨matrix.kronecker_map has_mul.mul ⇑U₁ ⇑U₂, _⟩
theorem
matrix.unitary_group.kronecker_coe
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
{p : Type u_3}
[fintype p]
[decidable_eq p]
(U₁ : ↥(matrix.unitary_group n 𝕜))
(U₂ : ↥(matrix.unitary_group p 𝕜)) :
⇑(matrix.unitary_group.kronecker U₁ U₂) = matrix.kronecker_map has_mul.mul ⇑U₁ ⇑U₂
theorem
matrix.inner_aut_kronecker
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[field 𝕜]
[star_ring 𝕜]
[decidable_eq n]
{p : Type u_3}
[fintype p]
[decidable_eq p]
(U₁ : ↥(matrix.unitary_group n 𝕜))
(U₂ : ↥(matrix.unitary_group p 𝕜))
(x : matrix n n 𝕜)
(y : matrix p p 𝕜) :
matrix.kronecker_map has_mul.mul (⇑(matrix.inner_aut U₁) x) (⇑(matrix.inner_aut U₂) y) = ⇑(matrix.inner_aut (matrix.unitary_group.kronecker U₁ U₂)) (matrix.kronecker_map has_mul.mul x y)
theorem
matrix.pos_semidef.kronecker
{𝕜 : Type u_1}
{n : Type u_2}
{p : Type u_3}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
[fintype n]
[fintype p]
[decidable_eq n]
[decidable_eq p]
{x : matrix n n 𝕜}
{y : matrix p p 𝕜}
(hx : x.pos_semidef)
(hy : y.pos_semidef) :
theorem
matrix.pos_def.kronecker
{𝕜 : Type u_1}
{n : Type u_2}
{p : Type u_3}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
[fintype n]
[fintype p]
[decidable_eq n]
[decidable_eq p]
{x : matrix n n 𝕜}
{y : matrix p p 𝕜}
(hx : x.pos_def)
(hy : y.pos_def) :
theorem
matrix.inner_aut_star_alg_equiv_to_linear_map
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[decidable_eq n]
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
(U : ↥(matrix.unitary_group n 𝕜)) :
theorem
matrix.inner_aut_star_alg_equiv_symm_to_linear_map
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[decidable_eq n]
[is_R_or_C 𝕜]
(U : ↥(matrix.unitary_group n 𝕜)) :
theorem
matrix.inner_aut.comp_inj
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[decidable_eq n]
[is_R_or_C 𝕜]
(U : ↥(matrix.unitary_group n 𝕜))
(S T : matrix n n 𝕜 →ₗ[𝕜] matrix n n 𝕜) :
S = T ↔ (matrix.inner_aut U).comp S = (matrix.inner_aut U).comp T
theorem
matrix.inner_aut.inj_comp
{n : Type u_1}
{𝕜 : Type u_2}
[fintype n]
[decidable_eq n]
[is_R_or_C 𝕜]
(U : ↥(matrix.unitary_group n 𝕜))
(S T : matrix n n 𝕜 →ₗ[𝕜] matrix n n 𝕜) :
S = T ↔ S.comp (matrix.inner_aut U) = T.comp (matrix.inner_aut U)