Cross products #

This module defines the cross product of vectors in $R^3$ for $R$ a commutative ring, as a bilinear map.

Main definitions #

• crossProduct is the cross product of pairs of vectors in $R^3$.

Main results #

• triple_product_eq_det
• cross_dot_cross
• jacobi_cross

Notation #

The locale Matrix gives the following notation:

• ×₃ for the cross product

Tags #

crossproduct

def crossProduct {R : Type u_1} [] :
(Fin 3R) →ₗ[R] (Fin 3R) →ₗ[R] Fin 3R

The cross product of two vectors in $R^3$ for $R$ a commutative ring.

Equations
• crossProduct = LinearMap.mk₂ R (fun (a b : Fin 3R) => ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0])
Instances For
Equations
Instances For
theorem cross_apply {R : Type u_1} [] (a : Fin 3R) (b : Fin 3R) :
(crossProduct a) b = ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]
@[simp]
theorem cross_anticomm {R : Type u_1} [] (v : Fin 3R) (w : Fin 3R) :
-(crossProduct v) w = (crossProduct w) v
theorem neg_cross {R : Type u_1} [] (v : Fin 3R) (w : Fin 3R) :
-(crossProduct v) w = (crossProduct w) v

Alias of cross_anticomm.

@[simp]
theorem cross_anticomm' {R : Type u_1} [] (v : Fin 3R) (w : Fin 3R) :
(crossProduct v) w + (crossProduct w) v = 0
@[simp]
theorem cross_self {R : Type u_1} [] (v : Fin 3R) :
(crossProduct v) v = 0
@[simp]
theorem dot_self_cross {R : Type u_1} [] (v : Fin 3R) (w : Fin 3R) :
Matrix.dotProduct v ((crossProduct v) w) = 0

The cross product of two vectors is perpendicular to the first vector.

@[simp]
theorem dot_cross_self {R : Type u_1} [] (v : Fin 3R) (w : Fin 3R) :
Matrix.dotProduct w ((crossProduct v) w) = 0

The cross product of two vectors is perpendicular to the second vector.

theorem triple_product_permutation {R : Type u_1} [] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
Matrix.dotProduct u ((crossProduct v) w) = Matrix.dotProduct v ((crossProduct w) u)

Cyclic permutations preserve the triple product. See also triple_product_eq_det.

theorem triple_product_eq_det {R : Type u_1} [] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
Matrix.dotProduct u ((crossProduct v) w) = Matrix.det ![u, v, w]

The triple product of u, v, and w is equal to the determinant of the matrix with those vectors as its rows.

theorem cross_dot_cross {R : Type u_1} [] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) (x : Fin 3R) :
Matrix.dotProduct ((crossProduct u) v) ((crossProduct w) x) = -

The scalar quadruple product identity, related to the Binet-Cauchy identity.

theorem leibniz_cross {R : Type u_1} [] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
(crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)

The cross product satisfies the Leibniz lie property.

def Cross.lieRing {R : Type u_1} [] :
LieRing (Fin 3R)

The three-dimensional vectors together with the operations + and ×₃ form a Lie ring. Note we do not make this an instance as a conflicting one already exists via LieRing.ofAssociativeRing.

Equations
• Cross.lieRing = let __src := Pi.addCommGroup; LieRing.mk
Instances For
theorem cross_cross {R : Type u_1} [] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
(crossProduct ((crossProduct u) v)) w = (crossProduct u) ((crossProduct v) w) - (crossProduct v) ((crossProduct u) w)
theorem jacobi_cross {R : Type u_1} [] (u : Fin 3R) (v : Fin 3R) (w : Fin 3R) :
(crossProduct u) ((crossProduct v) w) + (crossProduct v) ((crossProduct w) u) + (crossProduct w) ((crossProduct u) v) = 0

Jacobi identity: For a cross product of three vectors, their sum over the three even permutations is equal to the zero vector.