# 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.unitaryGroup is the submonoid of matrices where the star-transpose is the inverse; the group structure (under multiplication) is inherited from a more general unitary construction.
• Matrix.UnitaryGroup.embeddingGL is the embedding Matrix.unitaryGroup n α → GLₙ(α), where GLₙ(α) is LinearMap.GeneralLinearGroup α (n → α).
• Matrix.orthogonalGroup is the submonoid of matrices where the transpose is the inverse.

## Tags #

matrix group, group, unitary group, orthogonal group

@[reducible, inline]
abbrev Matrix.unitaryGroup (n : Type u) [] [] (α : Type v) [] [] :
Submonoid (Matrix n n α)

Matrix.unitaryGroup n is the group of n by n matrices where the star-transpose is the inverse.

Equations
Instances For
theorem Matrix.mem_unitaryGroup_iff {n : Type u} [] [] {α : Type v} [] [] {A : Matrix n n α} :
A A * star A = 1
theorem Matrix.mem_unitaryGroup_iff' {n : Type u} [] [] {α : Type v} [] [] {A : Matrix n n α} :
A star A * A = 1
theorem Matrix.det_of_mem_unitary {n : Type u} [] [] {α : Type v} [] [] {A : Matrix n n α} (hA : A ) :
A.det
instance Matrix.UnitaryGroup.coeMatrix {n : Type u} [] [] {α : Type v} [] [] :
Coe (()) (Matrix n n α)
Equations
• Matrix.UnitaryGroup.coeMatrix = { coe := Subtype.val }
instance Matrix.UnitaryGroup.coeFun {n : Type u} [] [] {α : Type v} [] [] :
CoeFun () fun (x : ()) => nnα
Equations
• Matrix.UnitaryGroup.coeFun = { coe := fun (A : ()) => A }
def Matrix.UnitaryGroup.toLin' {n : Type u} [] [] {α : Type v} [] [] (A : ()) :
(nα) →ₗ[α] 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.toLin' A
Instances For
theorem Matrix.UnitaryGroup.ext_iff {n : Type u} [] [] {α : Type v} [] [] (A : ()) (B : ()) :
A = B ∀ (i j : n), A i j = B i j
theorem Matrix.UnitaryGroup.ext {n : Type u} [] [] {α : Type v} [] [] (A : ()) (B : ()) :
(∀ (i j : n), A i j = B i j)A = B
theorem Matrix.UnitaryGroup.star_mul_self {n : Type u} [] [] {α : Type v} [] [] (A : ()) :
star A * A = 1
@[simp]
theorem Matrix.UnitaryGroup.det_isUnit {n : Type u} [] [] {α : Type v} [] [] (A : ()) :
IsUnit (A).det
@[simp]
theorem Matrix.UnitaryGroup.inv_val {n : Type u} [] [] {α : Type v} [] [] (A : ()) :
A⁻¹ = star A
@[simp]
theorem Matrix.UnitaryGroup.inv_apply {n : Type u} [] [] {α : Type v} [] [] (A : ()) :
A⁻¹ = star A
@[simp]
theorem Matrix.UnitaryGroup.mul_val {n : Type u} [] [] {α : Type v} [] [] (A : ()) (B : ()) :
(A * B) = A * B
@[simp]
theorem Matrix.UnitaryGroup.mul_apply {n : Type u} [] [] {α : Type v} [] [] (A : ()) (B : ()) :
(A * B) = A * B
@[simp]
theorem Matrix.UnitaryGroup.one_val {n : Type u} [] [] {α : Type v} [] [] :
1 = 1
@[simp]
theorem Matrix.UnitaryGroup.one_apply {n : Type u} [] [] {α : Type v} [] [] :
1 = 1
@[simp]
theorem Matrix.UnitaryGroup.toLin'_mul {n : Type u} [] [] {α : Type v} [] [] (A : ()) (B : ()) :
@[simp]
theorem Matrix.UnitaryGroup.toLin'_one {n : Type u} [] [] {α : Type v} [] [] :
= LinearMap.id
def Matrix.UnitaryGroup.toLinearEquiv {n : Type u} [] [] {α : Type v} [] [] (A : ()) :
(nα) ≃ₗ[α] nα

Matrix.unitaryGroup.toLinearEquiv A is matrix multiplication of vectors by A, as a linear equivalence.

Equations
• = let __src := Matrix.toLin' A; { toLinearMap := __src, invFun := , left_inv := , right_inv := }
Instances For
def Matrix.UnitaryGroup.toGL {n : Type u} [] [] {α : Type v} [] [] (A : ()) :

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} [] [] {α : Type v} [] [] (A : ()) :
@[simp]
theorem Matrix.UnitaryGroup.toGL_one {n : Type u} [] [] {α : Type v} [] [] :
@[simp]
theorem Matrix.UnitaryGroup.toGL_mul {n : Type u} [] [] {α : Type v} [] [] (A : ()) (B : ()) :
def Matrix.UnitaryGroup.embeddingGL {n : Type u} [] [] {α : Type v} [] [] :

Matrix.unitaryGroup.embeddingGL is the embedding from Matrix.unitaryGroup n α to LinearMap.GeneralLinearGroup n α.

Equations
• Matrix.UnitaryGroup.embeddingGL = { toFun := fun (A : ()) => , map_one' := , map_mul' := }
Instances For
@[reducible, inline]
abbrev Matrix.specialUnitaryGroup (n : Type u) [] [] (α : Type v) [] [] :
Submonoid (Matrix n n α)

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
Instances For
theorem Matrix.mem_specialUnitaryGroup_iff {n : Type u} [] [] {α : Type v} [] [] {A : Matrix n n α} :
A A.det = 1
@[reducible, inline]
abbrev Matrix.orthogonalGroup (n : Type u) [] [] (β : Type v) [] :
Submonoid (Matrix n n β)

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) [] [] (β : Type v) [] {A : Matrix n n β} :
A * star A = 1
theorem Matrix.mem_orthogonalGroup_iff' (n : Type u) [] [] (β : Type v) [] {A : Matrix n n β} :
star A * A = 1
@[reducible, inline]
abbrev Matrix.specialOrthogonalGroup (n : Type u) [] [] (β : Type v) [] :
Submonoid (Matrix n n β)

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} [] [] {β : Type v} [] {A : Matrix n n β} :
A.det = 1