The Unitary Group #
This file defines elements of the unitary group Matrix.unitaryGroup n α, where α is a
StarRing. 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
Matrix.unitaryGroup n α, and the embedding into the general linear group
LinearMap.GeneralLinearGroup α (n → α).
We also define the orthogonal group Matrix.orthogonalGroup n β, where β is a CommRing.
Main Definitions #
Matrix.unitaryGroupis the submonoid of matrices where the star-transpose is the inverse; the group structure (under multiplication) is inherited from a more generalunitaryconstruction.Matrix.UnitaryGroup.embeddingGLis the embeddingMatrix.unitaryGroup n α → GLₙ(α), whereGLₙ(α)isLinearMap.GeneralLinearGroup α (n → α).Matrix.orthogonalGroupis the submonoid of matrices where the transpose is the inverse.
References #
- https://en.wikipedia.org/wiki/Unitary_group
Tags #
matrix group, group, unitary group, orthogonal group
@[inline, reducible]
abbrev
Matrix.unitaryGroup
(n : Type u)
[DecidableEq n]
[Fintype n]
(α : Type v)
[CommRing α]
[StarRing α]
:
Matrix.unitaryGroup n is the group of n by n matrices where the star-transpose is the
inverse.
Equations
- Matrix.unitaryGroup n α = unitary (Matrix n n α)
Instances For
theorem
Matrix.mem_unitaryGroup_iff
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
{A : Matrix n n α}
:
theorem
Matrix.mem_unitaryGroup_iff'
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
{A : Matrix n n α}
:
theorem
Matrix.det_of_mem_unitary
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
{A : Matrix n n α}
(hA : A ∈ Matrix.unitaryGroup n α)
:
Matrix.det A ∈ unitary α
instance
Matrix.UnitaryGroup.coeMatrix
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
:
Coe (↥(Matrix.unitaryGroup n α)) (Matrix n n α)
Equations
- Matrix.UnitaryGroup.coeMatrix = { coe := Subtype.val }
instance
Matrix.UnitaryGroup.coeFun
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
:
CoeFun ↥(Matrix.unitaryGroup n α) fun (x : ↥(Matrix.unitaryGroup n α)) => n → n → α
Equations
- Matrix.UnitaryGroup.coeFun = { coe := fun (A : ↥(Matrix.unitaryGroup n α)) => ↑A }
def
Matrix.UnitaryGroup.toLin'
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
:
Matrix.UnitaryGroup.toLin' A is matrix multiplication of vectors by A, as a linear map.
After the group structure on Matrix.unitaryGroup n is defined, we show in
Matrix.UnitaryGroup.toLinearEquiv that this gives a linear equivalence.
Equations
- Matrix.UnitaryGroup.toLin' A = Matrix.toLin' ↑A
Instances For
theorem
Matrix.UnitaryGroup.ext_iff
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
(B : ↥(Matrix.unitaryGroup n α))
:
theorem
Matrix.UnitaryGroup.ext
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
(B : ↥(Matrix.unitaryGroup n α))
:
theorem
Matrix.UnitaryGroup.star_mul_self
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
:
@[simp]
theorem
Matrix.UnitaryGroup.inv_val
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
:
@[simp]
theorem
Matrix.UnitaryGroup.inv_apply
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
:
@[simp]
theorem
Matrix.UnitaryGroup.mul_val
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
(B : ↥(Matrix.unitaryGroup n α))
:
@[simp]
theorem
Matrix.UnitaryGroup.mul_apply
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
(B : ↥(Matrix.unitaryGroup n α))
:
@[simp]
theorem
Matrix.UnitaryGroup.one_val
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
:
↑1 = 1
@[simp]
theorem
Matrix.UnitaryGroup.one_apply
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
:
↑1 = 1
@[simp]
theorem
Matrix.UnitaryGroup.toLin'_mul
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
(B : ↥(Matrix.unitaryGroup n α))
:
@[simp]
theorem
Matrix.UnitaryGroup.toLin'_one
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
:
Matrix.UnitaryGroup.toLin' 1 = LinearMap.id
def
Matrix.UnitaryGroup.toLinearEquiv
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
:
Matrix.unitaryGroup.toLinearEquiv A is matrix multiplication of vectors by A, as a linear
equivalence.
Equations
- Matrix.UnitaryGroup.toLinearEquiv A = let __src := Matrix.toLin' ↑A; { toLinearMap := __src, invFun := ⇑(Matrix.UnitaryGroup.toLin' A⁻¹), left_inv := ⋯, right_inv := ⋯ }
Instances For
def
Matrix.UnitaryGroup.toGL
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
:
LinearMap.GeneralLinearGroup α (n → α)
Matrix.unitaryGroup.toGL is the map from the unitary group to the general linear group
Equations
Instances For
theorem
Matrix.UnitaryGroup.coe_toGL
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
:
@[simp]
theorem
Matrix.UnitaryGroup.toGL_one
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
:
@[simp]
theorem
Matrix.UnitaryGroup.toGL_mul
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
(A : ↥(Matrix.unitaryGroup n α))
(B : ↥(Matrix.unitaryGroup n α))
:
def
Matrix.UnitaryGroup.embeddingGL
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
:
↥(Matrix.unitaryGroup n α) →* LinearMap.GeneralLinearGroup α (n → α)
Matrix.unitaryGroup.embeddingGL is the embedding from Matrix.unitaryGroup n α to
LinearMap.GeneralLinearGroup n α.
Equations
- Matrix.UnitaryGroup.embeddingGL = { toOneHom := { toFun := fun (A : ↥(Matrix.unitaryGroup n α)) => Matrix.UnitaryGroup.toGL A, map_one' := ⋯ }, map_mul' := ⋯ }
Instances For
@[inline, reducible]
abbrev
Matrix.specialUnitaryGroup
(n : Type u)
[DecidableEq n]
[Fintype n]
(α : Type v)
[CommRing α]
[StarRing α]
:
Matrix.specialUnitaryGroup is the group of unitary n by n matrices where the determinant
is 1. (This definition is only correct if 2 is invertible.)
Equations
- Matrix.specialUnitaryGroup n α = Matrix.unitaryGroup n α ⊓ MonoidHom.mker Matrix.detMonoidHom
Instances For
theorem
Matrix.mem_specialUnitaryGroup_iff
{n : Type u}
[DecidableEq n]
[Fintype n]
{α : Type v}
[CommRing α]
[StarRing α]
{A : Matrix n n α}
:
A ∈ Matrix.specialUnitaryGroup n α ↔ A ∈ Matrix.unitaryGroup n α ∧ Matrix.det A = 1
@[inline, reducible]
Matrix.orthogonalGroup n is the group of n by n matrices where the transpose is the
inverse.
Equations
Instances For
theorem
Matrix.mem_orthogonalGroup_iff
(n : Type u)
[DecidableEq n]
[Fintype n]
(β : Type v)
[CommRing β]
{A : Matrix n n β}
:
theorem
Matrix.mem_orthogonalGroup_iff'
(n : Type u)
[DecidableEq n]
[Fintype n]
(β : Type v)
[CommRing β]
{A : Matrix n n β}
:
@[inline, reducible]
abbrev
Matrix.specialOrthogonalGroup
(n : Type u)
[DecidableEq n]
[Fintype n]
(β : Type v)
[CommRing β]
:
Matrix.specialOrthogonalGroup n is the group of orthogonal n by n where the determinant
is one. (This definition is only correct if 2 is invertible.)
Equations
Instances For
theorem
Matrix.mem_specialOrthogonalGroup_iff
{n : Type u}
[DecidableEq n]
[Fintype n]
{β : Type v}
[CommRing β]
{A : Matrix n n β}
:
A ∈ Matrix.specialOrthogonalGroup n β ↔ A ∈ Matrix.orthogonalGroup n β ∧ Matrix.det A = 1