mathlib documentation

linear_algebra.unitary_group

The Unitary Group #

This file defines elements of the unitary group unitary_group n α, where α is a star_ring. This consists of all n by n matrices with entries in α such that the star-transpose is its inverse. In addition, we define the group structure on unitary_group n α, and the embedding into the general linear group general_linear_group α (n → α).

We also define the orthogonal group orthogonal_group n β, where β is a comm_ring.

Main Definitions #

References #

Tags #

matrix group, group, unitary group, orthogonal group

source
def matrix.unitary_group (n : Type u) [decidable_eq n] [fintype n] (α : Type v) [comm_ring α] [star_ring α] :
submonoid (matrix n n α)

unitary_group n is the group of n by n matrices where the star-transpose is the inverse.

source
@[protected, instance]
def matrix.unitary_group.coe_matrix {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] :
has_coe ↥(matrix.unitary_group n α) (matrix n n α)
Equations
source
@[protected, instance]
def matrix.unitary_group.coe_fun {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] :
has_coe_to_fun ↥(matrix.unitary_group n α) (λ (_x : ↥(matrix.unitary_group n α)), n → n → α)
Equations
source
def matrix.unitary_group.to_lin' {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A : ↥(matrix.unitary_group n α)) :
(n → α) →ₗ[α] n → α

to_lin' A is matrix multiplication of vectors by A, as a linear map.

After the group structure on unitary_group n is defined, we show in to_linear_equiv that this gives a linear equivalence.

Equations
source
theorem matrix.unitary_group.ext_iff {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A B : ↥(matrix.unitary_group n α)) :
A = B ↔ ∀ (i j : n), ⇑A i j = ⇑B i j
source
@[ext]
theorem matrix.unitary_group.ext {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A B : ↥(matrix.unitary_group n α)) :
(∀ (i j : n), ⇑A i j = ⇑B i j) → A = B
source
@[simp]
theorem matrix.unitary_group.star_mul_self {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A : ↥(matrix.unitary_group n α)) :
(has_star.star ⇑A).mul ⇑A = 1
source
@[simp]
theorem matrix.unitary_group.inv_val {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A : ↥(matrix.unitary_group n α)) :
↑A⁻¹ = has_star.star ⇑A
source
@[simp]
theorem matrix.unitary_group.inv_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A : ↥(matrix.unitary_group n α)) :
⇑A⁻¹ = has_star.star ⇑A
source
@[simp]
theorem matrix.unitary_group.mul_val {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A B : ↥(matrix.unitary_group n α)) :
↑(A * B) = matrix.mul ⇑A ⇑B
source
@[simp]
theorem matrix.unitary_group.mul_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A B : ↥(matrix.unitary_group n α)) :
⇑(A * B) = matrix.mul ⇑A ⇑B
source
@[simp]
theorem matrix.unitary_group.one_val {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] :
↑1 = 1
source
@[simp]
theorem matrix.unitary_group.one_apply {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] :
⇑1 = 1
source
@[simp]
theorem matrix.unitary_group.to_lin'_mul {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A B : ↥(matrix.unitary_group n α)) :
matrix.unitary_group.to_lin' (A * B) = (matrix.unitary_group.to_lin' A).comp (matrix.unitary_group.to_lin' B)
source
@[simp]
theorem matrix.unitary_group.to_lin'_one {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] :
matrix.unitary_group.to_lin' 1 = linear_map.id
source
def matrix.unitary_group.to_linear_equiv {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A : ↥(matrix.unitary_group n α)) :
(n → α) ≃ₗ[α] n → α

to_linear_equiv A is matrix multiplication of vectors by A, as a linear equivalence.

Equations
source
def matrix.unitary_group.to_GL {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A : ↥(matrix.unitary_group n α)) :
linear_map.general_linear_group α (n → α)

to_GL is the map from the unitary group to the general linear group

Equations
source
theorem matrix.unitary_group.coe_to_GL {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A : ↥(matrix.unitary_group n α)) :
↑(matrix.unitary_group.to_GL A) = matrix.unitary_group.to_lin' A
source
@[simp]
theorem matrix.unitary_group.to_GL_one {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] :
matrix.unitary_group.to_GL 1 = 1
source
@[simp]
theorem matrix.unitary_group.to_GL_mul {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] (A B : ↥(matrix.unitary_group n α)) :
matrix.unitary_group.to_GL (A * B) = matrix.unitary_group.to_GL A * matrix.unitary_group.to_GL B
source
def matrix.unitary_group.embedding_GL {n : Type u} [decidable_eq n] [fintype n] {α : Type v} [comm_ring α] [star_ring α] :
↥(matrix.unitary_group n α) →* linear_map.general_linear_group α (n → α)

unitary_group.embedding_GL is the embedding from unitary_group n α to general_linear_group n α.

Equations
source
def matrix.orthogonal_group {n : Type u} [decidable_eq n] [fintype n] (β : Type v) [comm_ring β] :
submonoid (matrix n n β)

orthogonal_group n is the group of n by n matrices where the transpose is the inverse.