The Unitary Group #
This file defines elements of the unitary group
unitary_group n α, where
α is a
This consists of all
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
Main Definitions #
matrix.unitary_groupis the type of matrices where the star-transpose is the inverse
matrix.unitary_group.groupis the group structure (under multiplication)
matrix.unitary_group.embedding_GLis the embedding
unitary_group n α → GLₙ(α)
matrix.orthogonal_groupis the type of matrices where the transpose is the inverse
matrix group, group, unitary group, orthogonal group
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.
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
unitary_group.embedding_GL is the embedding from
unitary_group n α
general_linear_group n α.