The Unitary Group #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
matrix.unitary_groupis the type of matrices where the star-transpose is the inversematrix.unitary_group.groupis the group structure (under multiplication)matrix.unitary_group.embedding_GLis the embeddingunitary_group n α → GLₙ(α)matrix.orthogonal_groupis the type of matrices where the transpose is the inverse
References #
Tags #
matrix group, group, unitary group, orthogonal group
@[reducible]
def
matrix.unitary_group
(n : Type u)
[decidable_eq n]
[fintype n]
(α : Type v)
[comm_ring α]
[star_ring α] :
unitary_group n is the group of n by n matrices where the star-transpose is the inverse.
theorem
matrix.mem_unitary_group_iff
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α]
{A : matrix n n α} :
A ∈ matrix.unitary_group n α ↔ A * has_star.star A = 1
theorem
matrix.mem_unitary_group_iff'
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α]
{A : matrix n n α} :
A ∈ matrix.unitary_group n α ↔ has_star.star A * A = 1
theorem
matrix.det_of_mem_unitary
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α]
{A : matrix n n α}
(hA : A ∈ matrix.unitary_group n α) :
@[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
- matrix.unitary_group.coe_matrix = {coe := subtype.val (λ (x : matrix n n α), x ∈ matrix.unitary_group n α)}
@[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
- matrix.unitary_group.coe_fun = {coe := λ (A : ↥(matrix.unitary_group n α)), A.val}
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 α)) :
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
@[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
@[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
@[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
@[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 α)) :
@[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 α)) :
@[simp]
theorem
matrix.unitary_group.one_val
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
@[simp]
theorem
matrix.unitary_group.one_apply
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
@[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 α)) :
@[simp]
theorem
matrix.unitary_group.to_lin'_one
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
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 α)) :
to_linear_equiv A is matrix multiplication of vectors by A, as a linear equivalence.
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
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 α)) :
@[simp]
theorem
matrix.unitary_group.to_GL_one
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
@[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 α)) :
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
- matrix.unitary_group.embedding_GL = {to_fun := λ (A : ↥(matrix.unitary_group n α)), matrix.unitary_group.to_GL A, map_one' := _, map_mul' := _}
@[reducible]
orthogonal_group n is the group of n by n matrices where the transpose is the inverse.
theorem
matrix.mem_orthogonal_group_iff
(n : Type u)
[decidable_eq n]
[fintype n]
(β : Type v)
[comm_ring β]
{A : matrix n n β} :
A ∈ matrix.orthogonal_group n β ↔ A * has_star.star A = 1
theorem
matrix.mem_orthogonal_group_iff'
(n : Type u)
[decidable_eq n]
[fintype n]
(β : Type v)
[comm_ring β]
{A : matrix n n β} :
A ∈ matrix.orthogonal_group n β ↔ has_star.star A * A = 1