[Merged by Bors] - feat(linear_algebra/{cross_product,vectors}): cross product

src/linear_algebra/cross_product.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2021 Martin Dvorak. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Dvorak, Kyle Miller, Eric Wieser
+-/
+
+import linear_algebra.bilinear_map
+import linear_algebra.matrix.determinant
+import linear_algebra.vectors
+import algebra.lie.basic
+
+/-!
+# Cross products
+
+This module defines the cross product of vectors in $R^3$ for $R$ a commutative ring.
+
+## Main definitions
+
+* `cross_product` is the cross product of pairs of vectors in $R^3$.
+
+## Main results
+
+* `triple_product_eq_det`
+* `jacobi_identity`
+
+## Notation
+
+The locale `vectors` gives the following notation:
+
+* `×₃` for the cross product
+
+## Tags
+
+crossproduct
+-/
+
+open_locale vectors
+
+variables {R : Type*} [comm_ring R]
+
+/-- The cross product of two vectors in $R^3$ for $R$ a commutative ring. -/
+def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
+begin
+  apply linear_map.mk₂ R (λ (a b : fin 3 → R),
+    ![ (a 1)*(b 2) - (a 2)*(b 1) ,
+       (a 2)*(b 0) - (a 0)*(b 2) ,
+       (a 0)*(b 1) - (a 1)*(b 0) ]);
+  intros;
+  simp only [vec3_add,
+    pi.add_apply, smul_eq_mul, matrix.smul_cons, matrix.smul_empty, pi.smul_apply];
+  apply vec3_eq;
+  ring,
+end
+
+localized "infixl ` ×₃ `: 68 := cross_product" in vectors
+
+lemma cross_product_apply (a b : fin 3 → R) :
+  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) ] :=
+rfl
+
+lemma cross_product_anticomm (v w : fin 3 → R) :
+  - (v ×₃ w) = w ×₃ v :=
+by simp [cross_product_apply, mul_comm]
+
+lemma cross_product_anticomm' (v w : fin 3 → R) :
+  v ×₃ w + w ×₃ v = 0 :=
+by rw [add_eq_zero_iff_eq_neg, cross_product_anticomm]
+
+lemma cross_product_self (v : fin 3 → R) :
+  v ×₃ v = 0 :=
+by simp [cross_product_apply, mul_comm]
+
+/-- The cross product of two vectors is perpendicular to the first vector. -/
+lemma dot_self_cross_product (v w : fin 3 → R) :
+  v ⬝ (v ×₃ w) = 0 :=
+by simp [cross_product_apply, vec3_dot_product, mul_sub, mul_assoc, mul_left_comm]
+
+/-- The cross product of two vectors is perpendicular to the second vector. -/
+lemma dot_cross_product_self (v w : fin 3 → R) :
+  w ⬝ (v ×₃ w) = 0 :=
+by rw [← cross_product_anticomm, matrix.dot_product_neg, dot_self_cross_product, neg_zero]
+
+/-- Cyclic permutations preserve the triple product. See also `triple_product_eq_det`. -/
+lemma triple_product_permutation (u v w : fin 3 → R) :
+  u ⬝ (v ×₃ w) = v ⬝ (w ×₃ u) :=
+begin
+  simp only [cross_product_apply, vec3_dot_product,
+    matrix.head_cons, matrix.cons_vec_bit0_eq_alt0, matrix.empty_append, matrix.cons_val_one,
+    matrix.cons_vec_alt0, matrix.cons_append, matrix.cons_val_zero],
+  ring,
+end
+
+/-- The triple product of `u`, `v`, and `w` is equal to the determinant of the matrix
+    with those vectors as its rows. -/
+theorem triple_product_eq_det (u v w : fin 3 → R) :
+  u ⬝ (v ×₃ w) = matrix.det ![u, v, w] :=
+begin
+  simp only [vec3_dot_product, cross_product_apply, matrix.det_fin_three,
+    matrix.head_cons, matrix.cons_vec_bit0_eq_alt0, matrix.empty_vec_alt0, matrix.cons_vec_alt0,
+    matrix.vec_head_vec_alt0, fin.fin_append_apply_zero, matrix.empty_append, matrix.cons_append,
+    matrix.cons_val', matrix.cons_val_one, matrix.cons_val_zero],
+  ring,
+end
+
+/-- The cross product satisfies the Leibniz lie property
+    `∀ (x y z : L) : ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆` from `algebra.lie.basic.lie_ring`.
+    It is equivalent to the Jacobi identity in the presence of the other Lie ring axioms. -/
+lemma leibniz_cross (u v w : fin 3 → R) :
+  u ×₃ (v ×₃ w) = (u ×₃ v) ×₃ w + v ×₃ (u ×₃ w) :=
+begin
+  dsimp only [has_bracket.bracket, cross_product_apply],
+  ext i,
+  fin_cases i; norm_num; ring,
+end
+
+/-- The three-dimensional vectors together with the operations + and ×₃ form a Lie ring. -/
+def cross_product.lie_ring : lie_ring (fin 3 → R) :=
+{ bracket := λ u v, u ×₃ v,
+  add_lie := linear_map.map_add₂ _,
+  lie_add := λ u, linear_map.map_add _,
+  lie_self := cross_product_self,
+  leibniz_lie := leibniz_cross,
+  ..pi.add_comm_group }
+
+local attribute [instance] cross_product.lie_ring
+
+/-- For a cross product of three vectors, their sum over the three even permutations is equal
+    to the zero vector. -/
+theorem jacobi_identity (u v w : fin 3 → R) :
+  u ×₃ (v ×₃ w) + v ×₃ (w ×₃ u) + w ×₃ (u ×₃ v) = 0 :=
+lie_jacobi u v w

src/linear_algebra/vectors.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2021 Martin Dvorak. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Martin Dvorak, Kyle Miller
+-/
+
+import data.matrix.basic
+import data.matrix.notation
+import tactic.fin_cases
+
+/-!
+# Vectors
+
+This module provides lemmata to more easily manipulate explicit vectors in $R^2$ and $R^3$
+for $R$ a commutative ring.
+
+## Notation
+
+The locale `vectors` gives the following notation:
+
+* `⬝` for dot products
+
+## Tags
+
+vectors
+-/
+
+variable {R : Type*}
+
+lemma vec2_eq {a₀ a₁ b₀ b₁ : R} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) :
+  ![a₀, a₁] = ![b₀, b₁] :=
+by { ext x, fin_cases x; assumption }
+
+lemma vec3_eq {a₀ a₁ a₂ b₀ b₁ b₂ : R} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) :
+  ![a₀, a₁, a₂] = ![b₀, b₁, b₂] :=
+by { ext x, fin_cases x; assumption }
+
+variable [comm_ring R]
+
+lemma vec2_add {a₀ a₁ b₀ b₁ : R} :
+  ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁] :=
+by { ext x, fin_cases x; refl }
+
+lemma vec3_add {a₀ a₁ a₂ b₀ b₁ b₂ : R} :
+  ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂] :=
+by { ext x, fin_cases x; refl }
+
+localized "infix  ` ⬝ ` : 67 := matrix.dot_product" in vectors
+
+lemma vec2_dot_product (v w : fin 2 → R) :
+  v ⬝ w = v 0 * w 0 + v 1 * w 1 :=
+by simp [matrix.dot_product, add_assoc, fin.sum_univ_succ]
+
+lemma vec3_dot_product (v w : fin 3 → R) :
+  v ⬝ w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2 :=
+by simp [matrix.dot_product, add_assoc, fin.sum_univ_succ]