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 R, where R 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.

References

• https://en.wikipedia.org/wiki/Unitary_group

Tags

matrix group, group, unitary group, orthogonal group

@[reducible, inline]

abbrev Matrix.unitaryGroup (n : Type u) [DecidableEq n] [Fintype n] (α : Type v) [CommRing α] [StarRing α] : Submonoid (Matrix n n α)

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 α)

theorem Matrix.mem_unitaryGroup_iff {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] {A : Matrix n n α} : A ∈ unitaryGroup n α ↔ A * star A = 1

theorem Matrix.mem_unitaryGroup_iff' {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] {A : Matrix n n α} : A ∈ unitaryGroup n α ↔ star A * A = 1

theorem Matrix.det_of_mem_unitary {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] {A : Matrix n n α} (hA : A ∈ unitaryGroup n α) : A.det ∈ unitary α

theorem Matrix.kronecker_mem_unitary {n : Type u} [DecidableEq n] [Fintype n] {R : Type u_1} {m : Type u_2} [Semiring R] [StarRing R] [Fintype m] [DecidableEq m] {U₁ : Matrix n n R} {U₂ : Matrix m m R} (hU₁ : U₁ ∈ unitary (Matrix n n R)) (hU₂ : U₂ ∈ unitary (Matrix m m R)) : kroneckerMap (fun (x1 x2 : R) => x1 * x2) U₁ U₂ ∈ unitary (Matrix (n × m) (n × m) R)

The kronecker product of two unitary matrices is unitary.

This is stated for unitary instead of unitaryGroup as it holds even for non-commutative coefficients.

instance Matrix.UnitaryGroup.coeMatrix {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : Coe (↥(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 ↥(unitaryGroup n α) fun (x : ↥(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 : ↥(unitaryGroup n α)) : (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.UnitaryGroup.toLin' A = Matrix.toLin' ↑A

theorem Matrix.UnitaryGroup.ext_iff {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A B : ↥(unitaryGroup n α)) : A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j

theorem Matrix.UnitaryGroup.ext {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A B : ↥(unitaryGroup n α)) : (∀ (i j : n), ↑A i j = ↑B i j) → A = B

theorem Matrix.UnitaryGroup.star_mul_self {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(unitaryGroup n α)) : star ↑A * ↑A = 1

@[simp]

theorem Matrix.UnitaryGroup.det_isUnit {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(unitaryGroup n α)) : IsUnit (↑A).det

@[simp]

theorem Matrix.UnitaryGroup.inv_val {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(unitaryGroup n α)) : ↑A⁻¹ = star ↑A

@[simp]

theorem Matrix.UnitaryGroup.inv_apply {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(unitaryGroup n α)) : ↑A⁻¹ = star ↑A

@[simp]

theorem Matrix.UnitaryGroup.mul_val {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A B : ↥(unitaryGroup n α)) : ↑(A * B) = ↑A * ↑B

@[simp]

theorem Matrix.UnitaryGroup.mul_apply {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A B : ↥(unitaryGroup n α)) : ↑(A * B) = ↑A * ↑B

@[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 B : ↥(unitaryGroup n α)) : toLin' (A * B) = toLin' A ∘ₗ toLin' B

@[simp]

theorem Matrix.UnitaryGroup.toLin'_one {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : toLin' 1 = LinearMap.id

def Matrix.UnitaryGroup.toLinearEquiv {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(unitaryGroup n α)) : (n → α) ≃ₗ[α] n → α

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

Equations

• Matrix.UnitaryGroup.toLinearEquiv A = { toLinearMap := Matrix.toLin' ↑A, invFun := ⇑(Matrix.UnitaryGroup.toLin' A⁻¹), left_inv := ⋯, right_inv := ⋯ }

def Matrix.UnitaryGroup.toGL {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(unitaryGroup n α)) : LinearMap.GeneralLinearGroup α (n → α)

Matrix.unitaryGroup.toGL is the map from the unitary group to the general linear group

Equations

• Matrix.UnitaryGroup.toGL A = LinearMap.GeneralLinearGroup.ofLinearEquiv (Matrix.UnitaryGroup.toLinearEquiv A)

theorem Matrix.UnitaryGroup.coe_toGL {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(unitaryGroup n α)) : ↑(toGL A) = toLin' A

@[simp]

theorem Matrix.UnitaryGroup.toGL_one {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : toGL 1 = 1

@[simp]

theorem Matrix.UnitaryGroup.toGL_mul {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A B : ↥(unitaryGroup n α)) : toGL (A * B) = toGL A * toGL B

def Matrix.UnitaryGroup.embeddingGL {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : ↥(unitaryGroup n α) →* LinearMap.GeneralLinearGroup α (n → α)

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

Equations

• Matrix.UnitaryGroup.embeddingGL = { toFun := fun (A : ↥(Matrix.unitaryGroup n α)) => Matrix.UnitaryGroup.toGL A, map_one' := ⋯, map_mul' := ⋯ }

def Matrix.specialUnitaryGroup (n : Type u) [DecidableEq n] [Fintype n] (α : Type v) [CommRing α] [StarRing α] : 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

• Matrix.specialUnitaryGroup n α = Matrix.unitaryGroup n α ⊓ MonoidHom.mker Matrix.detMonoidHom

theorem Matrix.specialUnitaryGroup_le_unitaryGroup {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : specialUnitaryGroup n α ≤ unitaryGroup n α

theorem Matrix.mem_specialUnitaryGroup_iff {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] {A : Matrix n n α} : A ∈ specialUnitaryGroup n α ↔ A ∈ unitaryGroup n α ∧ A.det = 1

instance Matrix.instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : StarMul ↥(specialUnitaryGroup n α)

Equations

• Matrix.instStarMulSubtypeMemSubmonoidSpecialUnitaryGroup = { star := fun (A : ↥(Matrix.specialUnitaryGroup n α)) => ⟨star ↑A, ⋯⟩, star_involutive := ⋯, star_mul := ⋯ }

@[simp]

theorem Matrix.specialUnitaryGroup.coe_star {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(specialUnitaryGroup n α)) : ↑(star A) = star ↑A

instance Matrix.instInvSubtypeMemSubmonoidSpecialUnitaryGroup {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : Inv ↥(specialUnitaryGroup n α)

Equations

• Matrix.instInvSubtypeMemSubmonoidSpecialUnitaryGroup = { inv := star }

theorem Matrix.star_eq_inv {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : ↥(specialUnitaryGroup n α)) : star A = A⁻¹

instance Matrix.instGroupSubtypeMemSubmonoidSpecialUnitaryGroup {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] : Group ↥(specialUnitaryGroup n α)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Matrix.orthogonalGroup (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] : Submonoid (Matrix n n R)

Matrix.orthogonalGroup n is the group of n by n matrices where the transpose is the inverse.

Equations

• Matrix.orthogonalGroup n R = Matrix.unitaryGroup n R

theorem Matrix.mem_orthogonalGroup_iff (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] {A : Matrix n n R} : A ∈ orthogonalGroup n R ↔ A * A.transpose = 1

theorem Matrix.mem_orthogonalGroup_iff' (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] {A : Matrix n n R} : A ∈ orthogonalGroup n R ↔ A.transpose * A = 1

@[reducible, inline]

abbrev Matrix.specialOrthogonalGroup (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] : Submonoid (Matrix n n R)

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

• Matrix.specialOrthogonalGroup n R = Matrix.specialUnitaryGroup n R

theorem Matrix.mem_specialOrthogonalGroup_iff {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {A : Matrix n n R} : A ∈ specialOrthogonalGroup n R ↔ A ∈ orthogonalGroup n R ∧ A.det = 1

@[simp]

theorem Matrix.of_mem_specialOrthogonalGroup_fin_two_iff {R : Type v} [CommRing R] {a b c d : R} : !![a, b; c, d] ∈ specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1

theorem Matrix.mem_specialOrthogonalGroup_fin_two_iff {R : Type v} [CommRing R] {M : Matrix (Fin 2) (Fin 2) R} : M ∈ specialOrthogonalGroup (Fin 2) R ↔ M 0 0 = M 1 1 ∧ M 0 1 = -M 1 0 ∧ M 0 0 ^ 2 + M 0 1 ^ 2 = 1