Coordinate action of unitary matrices

Matrix.UnitaryGroup.toLinearEquiv_apply describes the linear equivalence associated to a unitary matrix by its matrix-vector action, and Matrix.permMatrix_mem_unitaryGroup records that permutation matrices are unitary. Accordingly Matrix.permutationUnitary is Matrix.permMatrixHom with values in the unitary group.

Matrix.conjTranspose_mul_mul_mem_unitary transfers unitarity along a possibly rectangular matrix whose conjugate transpose is a two-sided inverse.

Matrix.diagonal_update_one_mem_unitary_iff says that a diagonal matrix with all diagonal entries 1 except one is unitary exactly when that entry is.

@[simp]

theorem Matrix.UnitaryGroup.toLinearEquiv_apply {R : Type u} [CommRing R] [StarRing R] {n : Type v} [Fintype n] [DecidableEq n] (U : ↥(unitaryGroup n R)) (x : n → R) : (toLinearEquiv U) x = (Matrix.toLin' ↑U) x

The linear equivalence associated to a unitary matrix acts by matrix-vector multiplication.

theorem Matrix.conjTranspose_mul_mul_mem_unitary {R : Type u_1} {m : Type u_2} {n : Type u_3} [Semiring R] [StarRing R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (P : Matrix m n R) (hP : P.conjTranspose * P = 1) (hP' : P * P.conjTranspose = 1) {X : Matrix m m R} (hX : X ∈ unitary (Matrix m m R)) : P.conjTranspose * X * P ∈ unitary (Matrix n n R)

Conjugation by a possibly rectangular matrix with conjugate-transpose inverse preserves unitarity over a possibly noncommutative star semiring.

theorem Matrix.diagonal_update_one_mem_unitary_iff {n : Type u_1} {α : Type u_2} [Fintype n] [DecidableEq n] [Semiring α] [StarRing α] {a : α} {i : n} : diagonal (Function.update 1 i a) ∈ unitary (Matrix n n α) ↔ a ∈ unitary α

A diagonal matrix whose diagonal entries are all 1 except the i-th one is unitary exactly when its i-th diagonal entry is unitary.

theorem Matrix.permMatrix_mem_unitaryGroup {R : Type u} [CommRing R] [StarRing R] {n : Type v} [Fintype n] [DecidableEq n] (σ : Equiv.Perm n) : Equiv.Perm.permMatrix R σ ∈ unitaryGroup n R

A permutation matrix is unitary: its conjugate transpose is the permutation matrix of the inverse permutation.

def Matrix.permutationUnitary {R : Type u} [CommRing R] [StarRing R] {n : Type v} [Fintype n] [DecidableEq n] : Equiv.Perm n →* ↥(unitaryGroup n R)

A permutation as a unitary matrix: permutationUnitary σ is the permutation matrix of σ⁻¹, which makes this a homomorphism with Mathlib's convention for multiplication in Equiv.Perm.

@[simp]

theorem Matrix.coe_permutationUnitary {R : Type u} [CommRing R] [StarRing R] {n : Type v} [Fintype n] [DecidableEq n] (σ : Equiv.Perm n) : ↑(permutationUnitary σ) = Equiv.Perm.permMatrix R σ⁻¹

The matrix underlying permutationUnitary σ is the permutation matrix of σ⁻¹.