Documentation

Mathlib.LinearAlgebra.UnitaryGroup

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 #

References #

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
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 α) :
    A.det 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 α)) => nnα
    Equations
    def Matrix.UnitaryGroup.toLin' {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : (Matrix.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
    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 α)) :
      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 : (Matrix.unitaryGroup n α)) (B : (Matrix.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 : (Matrix.unitaryGroup n α)) :
      star A * A = 1
      @[simp]
      theorem Matrix.UnitaryGroup.det_isUnit {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : (Matrix.unitaryGroup n α)) :
      IsUnit (A).det
      @[simp]
      theorem Matrix.UnitaryGroup.inv_val {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : (Matrix.unitaryGroup n α)) :
      A⁻¹ = star A
      @[simp]
      theorem Matrix.UnitaryGroup.inv_apply {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : (Matrix.unitaryGroup n α)) :
      A⁻¹ = star A
      @[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 α)) :
      (A * B) = A * B
      @[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 α)) :
      (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'_one {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] :
      def Matrix.UnitaryGroup.toLinearEquiv {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : (Matrix.unitaryGroup n α)) :
      (nα) ≃ₗ[α] nα

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

      Equations
      Instances For
        def Matrix.UnitaryGroup.toGL {n : Type u} [DecidableEq n] [Fintype n] {α : Type v} [CommRing α] [StarRing α] (A : (Matrix.unitaryGroup n α)) :

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

        Equations
        Instances For

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

          Equations
          Instances For
            @[reducible, inline]
            abbrev 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
            Instances For
              @[reducible, inline]
              abbrev Matrix.orthogonalGroup (n : Type u) [DecidableEq n] [Fintype n] (β : Type v) [CommRing β] :
              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) [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 β} :
                @[reducible, inline]
                abbrev Matrix.specialOrthogonalGroup (n : Type u) [DecidableEq n] [Fintype n] (β : Type v) [CommRing β] :
                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