-
Notifications
You must be signed in to change notification settings - Fork 298
/
cross_product.lean
134 lines (106 loc) · 4.38 KB
/
cross_product.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
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