vector.egi

--
-- Vectors
--

def dotProduct {Ring a} (v1: Tensor a) (v2: Tensor a) : Tensor a := 
  withSymbols [i] v1~i . v2_i

def V.* {Ring a} : Tensor a -> Tensor a -> Tensor a := dotProduct

def crossProductWithFun {Ring a} (fn: a -> a -> a) (a: Vector a) (b: Vector a) : Vector a :=
  [|fn a_2 b_3 - fn a_3 b_2, fn a_3 b_1 - fn a_1 b_3, fn a_1 b_2 - fn a_2 b_1|]

def crossProduct {Ring a} (a: Vector a) (b: Vector a) : Vector a := 
  crossProductWithFun (*) a b

def div {Ring a} (A: Vector a) (xs: Vector a) : a := trace (!∂/∂ A xs)

-- curl: the standard convention (rot A)_i = eps_ijk d(A_k)/d(x_j), so
-- (rot A)_1 = dA_3/dx_2 - dA_2/dx_3.  This is nabla x A, hence the
-- coordinates xs take the first cross-product slot and the derivative
-- is flipped to differentiate the field component by the coordinate.
def rot {Ring a} (A: Vector a) (xs: Vector a) : Vector a :=
  crossProductWithFun (flip ∂/∂) xs A