Documentation

TauCeti.LinearAlgebra.Matrix.SpecialOrthogonalGroup.CoordinateRotation

Coordinate rotations in the special orthogonal group #

For two distinct coordinates, the signed transposition which sends the first basis vector to the second and the second to the negative of the first is special orthogonal. Its square changes the sign of exactly those two coordinates. These elementary matrices give a convenient, ring-valued interface for arguments with the standard representation of a special orthogonal group.

Main declarations #

References #

source
def TauCeti.Matrix.SpecialOrthogonalGroup.coordinateRotation {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (i j : n) (hij : i ≠ j) :
↥(Matrix.specialOrthogonalGroup n R)

The special orthogonal matrix which sends the i-th basis vector to the j-th basis vector, sends the j-th basis vector to the negative of the i-th basis vector, and fixes the remaining basis vectors.

Equations
Instances For
    source
    theorem TauCeti.Matrix.SpecialOrthogonalGroup.coe_coordinateRotation {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (i j : n) (hij : i ≠ j) :
    ↑(coordinateRotation i j hij) = Matrix.swap R i j * Matrix.diagonal (Function.update 1 j (-1))

    The underlying matrix of a coordinate rotation is the signed swap matrix used in its definition.

    source
    @[simp]
    theorem TauCeti.Matrix.SpecialOrthogonalGroup.coordinateRotation_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (i j : n) (hij : i ≠ j) (w : n → R) (a : n) :
    (↑(coordinateRotation i j hij)).mulVec w a = if a = i then -w j else if a = j then w i else w a

    A coordinate rotation exchanges the selected coordinates with the sign on the first output coordinate.

    source
    @[simp]
    theorem TauCeti.Matrix.SpecialOrthogonalGroup.coordinateRotation_col_left {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (i j : n) (hij : i ≠ j) :
    (↑(coordinateRotation i j hij)).col i = Pi.single j 1

    A coordinate rotation sends the i-th basis vector to the j-th basis vector.

    source
    @[simp]
    theorem TauCeti.Matrix.SpecialOrthogonalGroup.coordinateRotation_col_right {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (i j : n) (hij : i ≠ j) :
    (↑(coordinateRotation i j hij)).col j = -Pi.single i 1

    A coordinate rotation sends the j-th basis vector to the negative of the i-th basis vector.

    source
    def TauCeti.Matrix.SpecialOrthogonalGroup.coordinateHalfTurn {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (i j : n) (hij : i ≠ j) :
    ↥(Matrix.specialOrthogonalGroup n R)

    Squaring a coordinate rotation gives the half-turn which negates the two selected coordinates.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Matrix.SpecialOrthogonalGroup.coordinateHalfTurn_mulVec {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] (i j : n) (hij : i ≠ j) (w : n → R) (a : n) :
      (↑(coordinateHalfTurn i j hij)).mulVec w a = if a = i ∨ a = j then -w a else w a

      A coordinate half-turn negates exactly the two selected coordinates.