Documentation

TauCeti.LinearAlgebra.Matrix.OrthogonalGroup.Basic

Scalar, diagonal and determinant facts for orthogonal matrices #

A scalar matrix c • 1 over a nonempty index type lies in the orthogonal group of the standard symmetric form only when c ^ 2 = 1. For an empty index type every scalar qualifies.

Over a ring without zero divisors an orthogonal matrix has determinant 1 or -1, and both values occur as soon as the index type is nonempty: the diagonal reflection negating one coordinate is an orthogonal matrix of determinant -1.

Permutation matrices are orthogonal, and a matrix is orthogonal exactly when it preserves the dot product. The columns of an orthogonal matrix are orthonormal for the dot product. For a trivial star operation the unitary elements of the general linear group are the orthogonal matrices.

Main definitions #

Main declarations #

source
theorem TauCeti.sq_eq_one_of_smul_one_mem_orthogonalGroup {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {R : Type u_2} [CommRing R] {c : R} (h : c • 1 ∈ Matrix.orthogonalGroup n R) :
c ^ 2 = 1

A scalar matrix preserving the standard symmetric form has scalar a square root of one, provided the index type is nonempty: the orthogonality relation reads c ^ 2 • 1 = 1.

source
theorem TauCeti.det_eq_one_or_neg_one_of_mem_orthogonalGroup {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] [NoZeroDivisors R] {A : Matrix n n R} (hA : A ∈ Matrix.orthogonalGroup n R) :
A.det = 1 ∨ A.det = -1

Over a ring without zero divisors, the determinant of an orthogonal matrix is 1 or -1: the orthogonality relation Aᵀ * A = 1 gives det A * det A = 1.

source
def TauCeti.orthogonalDiagonalReflection {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] (i : n) :
↥(Matrix.orthogonalGroup n R)

The diagonal reflection negating the coordinate i: the diagonal matrix with entry -1 at i and 1 elsewhere, an orthogonal matrix of determinant -1 (TauCeti.det_orthogonalDiagonalReflection).

Instances For
    source
    @[simp]
    theorem TauCeti.coe_orthogonalDiagonalReflection {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] (i : n) :
    ↑(orthogonalDiagonalReflection R i) = Matrix.diagonal (Function.update 1 i (-1))

    The diagonal reflection negating the coordinate i has underlying matrix the diagonal matrix with entry -1 at i and 1 elsewhere.

    source
    theorem TauCeti.det_orthogonalDiagonalReflection {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] (i : n) :
    (↑(orthogonalDiagonalReflection R i)).det = -1

    The diagonal reflection negating one coordinate has determinant -1.

    source
    theorem Matrix.permMatrix_mem_orthogonalGroup {n : Type u_1} [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] (σ : Equiv.Perm n) :
    Equiv.Perm.permMatrix R σ ∈ orthogonalGroup n R

    A permutation matrix is orthogonal. This is Matrix.permMatrix_mem_unitaryGroup for the trivial star operation starRingOfComm, which defines Matrix.orthogonalGroup.

    source
    theorem Matrix.mem_orthogonalGroup_iff_dotProduct_mulVec {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {A : Matrix n n R} :
    A ∈ orthogonalGroup n R ↔ ∀ (x y : n → R), A.mulVec x ⬝ᵥ A.mulVec y = x ⬝ᵥ y

    A square matrix is orthogonal exactly when it preserves the dot product.

    source
    theorem Matrix.col_dotProduct_col_of_mem_orthogonalGroup {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {A : Matrix n n R} (hA : A ∈ orthogonalGroup n R) (i j : n) :
    A.col i ⬝ᵥ A.col j = 1 i j

    The columns of an orthogonal matrix are orthonormal for the dot product: the dot product of columns i and j is the (i, j) entry of the identity matrix.

    source
    theorem Matrix.GeneralLinearGroup.mem_unitarySubgroup_iff_mem_orthogonalGroup {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] [TrivialStar R] {M : GL n R} :
    M ∈ unitarySubgroup (GL n R) ↔ ↑M ∈ orthogonalGroup n R

    For a trivial star operation, the unitary elements of GL n R are the orthogonal matrices.