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 #
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
In a star_monoid M, unitary_submonoid M is the submonoid consisting of all the elements of
M such that star A * A = 1.
@[instance]
def
matrix.unitary_group.monoid
(n : Type u)
[decidable_eq n]
[fintype n]
(α : Type v)
[comm_ring α]
[star_ring α] :
monoid (matrix.unitary_group n α)
def
matrix.unitary_group
(n : Type u)
[decidable_eq n]
[fintype n]
(α : Type v)
[comm_ring α]
[star_ring α] :
Type (max u v)
unitary_group n is the group of n by n matrices where the star-transpose is the inverse.
Equations
- matrix.unitary_group n α = ↥(unitary_submonoid (matrix n n α))
theorem
matrix.unitary_submonoid.star_mem
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α]
{A : matrix n n α}
(h : A ∈ unitary_submonoid (matrix n n α)) :
star A ∈ unitary_submonoid (matrix n n α)
@[simp]
theorem
matrix.unitary_submonoid.star_mem_iff
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α]
{A : matrix n n α} :
star A ∈ unitary_submonoid (matrix n n α) ↔ A ∈ unitary_submonoid (matrix n n α)
@[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 ∈ unitary_submonoid (matrix n n α))}
@[instance]
def
matrix.unitary_group.coe_fun
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
Equations
- matrix.unitary_group.coe_fun = {F := λ (_x : matrix.unitary_group n α), n → n → α, 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
- A.to_lin' = ⇑matrix.to_lin' ⇑A
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 α) :
@[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 α) :
@[instance]
def
matrix.unitary_group.has_inv
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
has_inv (matrix.unitary_group n α)
Equations
- matrix.unitary_group.has_inv = {inv := λ (A : matrix.unitary_group n α), ⟨star A.val, _⟩}
@[instance]
def
matrix.unitary_group.star_monoid
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
Equations
- matrix.unitary_group.star_monoid = {to_has_involutive_star := {to_has_star := {star := λ (A : matrix.unitary_group n α), ⟨star A.val, _⟩}, star_involutive := _}, star_mul := _}
@[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 α) :
@[instance]
def
matrix.unitary_group.inhabited
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
Equations
@[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 α) :
@[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 α) :
@[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 α] :
@[instance]
def
matrix.unitary_group.group
{n : Type u}
[decidable_eq n]
[fintype n]
{α : Type v}
[comm_ring α]
[star_ring α] :
group (matrix.unitary_group n α)
Equations
- matrix.unitary_group.group = {mul := monoid.mul (matrix.unitary_group.monoid n α), mul_assoc := _, one := monoid.one (matrix.unitary_group.monoid n α), one_mul := _, mul_one := _, npow := npow (matrix.unitary_group.monoid n α), npow_zero' := _, npow_succ' := _, inv := has_inv.inv matrix.unitary_group.has_inv, div := div_inv_monoid.div._default monoid.mul matrix.unitary_group.group._proof_6 monoid.one matrix.unitary_group.group._proof_7 matrix.unitary_group.group._proof_8 npow matrix.unitary_group.group._proof_9 matrix.unitary_group.group._proof_10 has_inv.inv, div_eq_mul_inv := _, gpow := div_inv_monoid.gpow._default monoid.mul matrix.unitary_group.group._proof_12 monoid.one matrix.unitary_group.group._proof_13 matrix.unitary_group.group._proof_14 npow matrix.unitary_group.group._proof_15 matrix.unitary_group.group._proof_16 has_inv.inv, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_left_inv := _}
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
Equations
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 α), A.to_GL, map_one' := _, map_mul' := _}
def
matrix.orthogonal_group
{n : Type u}
[decidable_eq n]
[fintype n]
(β : Type v)
[comm_ring β] :
Type (max u v)
orthogonal_group n is the group of n by n matrices where the transpose is the inverse.