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_group
is the type of matrices where the star-transpose is the inversematrix.unitary_group.group
is the group structure (under multiplication)matrix.unitary_group.embedding_GL
is the embeddingunitary_group n α → GLₙ(α)
matrix.orthogonal_group
is 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
.
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 α))
Equations
- matrix.unitary_group.coe_matrix = {coe := subtype.val (λ (x : matrix n n α), x ∈ unitary_submonoid (matrix n n α))}
Equations
- matrix.unitary_group.coe_fun = {F := λ (_x : matrix.unitary_group n α), n → n → α, coe := λ (A : matrix.unitary_group n α), A.val}
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
Equations
- matrix.unitary_group.has_inv = {inv := λ (A : matrix.unitary_group n α), ⟨star A.val, _⟩}
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 := _}
Equations
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 := _, mul_left_inv := _}
to_linear_equiv A
is matrix multiplication of vectors by A
, as a linear equivalence.
to_GL
is the map from the unitary group to the general linear group
Equations
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' := _}
orthogonal_group n
is the group of n
by n
matrices where the transpose is the inverse.