cross product

Stream: general

[Johan Commelin]

One of the targets on https://github.com/leanprover-community/mathlib/wiki/Undergrad-TODO-trivial-targets is the cross product. I agree that it is quite easy to define the cross product on fin 3 → ℝ. But presumably that is not the correct generality, and we want to define it on arbitrary 3-dimensional oriented Euclidean spaces, or something like that.
Maybe that's not even the right generality, and we want something else in fact...

If you have an opinion on what the cross product in Lean should look like, please share it here.

[Yaël Dillies]

<insert some property> Lie bracket?

[Patrick Massot]

I don't think we should waste time here. If nobody is interested in the generalization then let's do the specific undergrad case and it will be refactored if anyone needs a generalization in the future. The optimal thing to do now is probably the case of an oriented three dimensional real inner product space, and it would be nice to make sure this applies to fin 3 → ℝ.

[Eric Wieser]

Would the binary exterior product be a sensible thing to formalize relating to this?

[Eric Wieser]

Maybe the binary specialization isn't as useful for the exterior product as it is for the tensor product.

[Eric Wieser]

I think it would be good to have cross_alternating : alternating_map R V V (fin 2) somewhere.

[Johan Commelin]

@Patrick Massot Would it be good enough to only deal with the case fin 3 → ℝ?

[Johan Commelin]

(To be honest, I don't think I've ever used the cross product after some example sheet in my 1st year LinAlg course.)

[Eric Wieser]

I agree we should probably have the generalization to an inner product space

[Eric Wieser]

Otherwise we can't use it to talk about the model of polar coordinates (r, θ, ψ) without forcing the user to go via an equiv

[Patrick Massot]

Honestly, I think we could get away with doing only fin 3 → ℝ. This definition is really nothing important.

[Eric Wieser]

If we don't do the full generalization, we may as well do fin 3 → R so that we can take a cross product of integer vectors, right?

[Johan Commelin]

You need some sin(θ) in the definition, right?

[Joseph Myers]

If you define it for a given basis, an arbitrary comm_ring should work.

If you define it for an orientation without specifying a choice of basis, you need extra structure (such as the real inner product) to make the result (as a vector in the same space as the arguments) depend only on the orientation.

I guess that means that the cross product with respect to a given basis is a sensible thing to define, whether or not we also define it with respect to an orientation and prove how it relates to sin in a real inner product space.

We don't yet have "given an orientation of a real inner product space, there exists an orthonormal basis corresponding to that orientation" (but that's something #10737 is aiming towards, being able to describe how concrete basis / alternating map manipulations relate to orientations).

[Kevin Buzzard]

Johan Commelin said:

You need some sin(θ) in the definition, right?

Johan -- the definition is \lam i, if i = 0 then a(1)*b(1)-a(2)*b(2) else if i = 1 then a(2)*b(0)-a(0)*b(2) else a(0)*b(1)-a(1)*b(0)

[Johan Commelin]

Good point!

[Eric Wieser]

Probably better with ![_, _, _]

[Kalle Kytölä]

Is it meaningful to make the cross-product an instance of docs#lie_ring on the type fin 3 → R for [add_comm_group R]?

[Kalle Kytölä]

I don't know if that plays well with nice notation, though.

[Eric Rodriguez]

wouldn't you need (comm_)ring? but yes, I'd agree that's sensible and then makes it very easy to state at any level of generality

[Kalle Kytölä]

I'm not very familiar with the implementation of lie_ring, but I think it has add_comm_group assumption.

By the way, I agree with much of the previous discussion that it is not obvious what generalizations we would care about. The cross product is mathematically a bit odd; I think it is something of a "law of small numbers" that there are not too many antisymmetric bilinear gadgets with Jacobi identity on merely 3 dimensional spaces, and therefore the cross product coincides with many conceptually different things.

But allowing e.g. integer entries seems meaningful, as Eric Wieser pointed out.

[Kevin Buzzard]

The cross product is an isomorphism of $\mathbb{R}^3$ with $\Lambda^2(\mathbb{R}^3)$ and its existence comes from the coincidence that 3 choose 2 is 3 again.

[Kalle Kytölä]

One of the coincidences I had in mind, indeed.

[Kalle Kytölä]

To me, the implementation of cross product as an instance of docs#lie_ring would involve only two potential drawbacks:

• competing instances of lie_ring on fin 3 → R (although I don't currently see serious competitors)
• difficulty to use nice notation (or would ⁅u, v⁆ be acceptable as such for the cross product?).

[Eric Rodriguez]

I meant the definition as Kevin wrote above to work, you need + and * so comm_ring seems like the sensible way to create the instance. The instance could be localised, too

[Johan Commelin]

Every ring R is a Lie algebra, so fin 3 → R would be the Lie algebra $R^{⊕ 3}$.

[Johan Commelin]

I think that's what mathlib currently assumes it to be.

[Patrick Massot]

I don't think we should have a globally registered notation for cross product. This is too specialized.

[Eric Wieser]

×₃ as locale notation?

[Martin Dvořák]

Is anybody working on it? If not, I'd like to take this task. Since I am a beginner, this looks good for me because it is probably the easiest-to-implement TODO in mathlib right now.

[Martin Dvořák]

I suppose I would define cross product as a function of the type (fin 3 → α) → (fin 3 → α) and I would prove some trivial properties of it (like anticommutativity). Is there something I should be aware of before I start?

[Johan Commelin]

I think you should be aware of the above discussion :wink: (There are a tonne of generalizations, but I think the consensus is that it's ok to focus on fin 3 → R for now.)

[Johan Commelin]

Also, please use R instead of α. It is a useful signal to the reader that R is not some random type, but caries a ring-like structure.

[Martin Dvořák]

Thank you! So you mean R not ℝ right?

[Martin Dvořák]

Thanks! Imma do it! I think it will be a great exercise to start with and experience the whole mathlib workflow before I dive into something complicated.

[Joseph Myers]

Maybe at least bilinearity should be bundled (so (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R))?

[Eric Wieser]

Should we be calling star on the output and requiring star_ring R? https://math.stackexchange.com/q/129227/1896 suggests we probably should.

[Martin Dvořák]

Joseph Myers said:

Maybe at least bilinearity should be bundled (so (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R))?

What does it mean?

[Eric Wieser]

It means exactly what Joseph said, that the map is bilinear

[Eric Wieser]

i.e. linear in both arguments

[Martin Dvořák]

Yes but what is the syntax →ₗ[R] for?

[Yury G. Kudryashov]

docs#linear_map

[Eric Wieser]

If you type in the full type as above, you can hover over it in vs-code to find out what the syntax means

[Martin Dvořák]

Thank yall for helping the n00b!

[Martin Dvořák]

Can I get your feedback on my wip please? This is my first time contributing (not only to Lean/mathlib but also to any open source).
https://github.com/madvorak/mathlib/blob/master/src/linear_algebra/cross_product.lean

[Andrew Yang]

A quick golf

/-- cross product is anti-commutative -/
lemma cross_product_anticomm (v w : fin 3 → R) :
  v ×₃ w = - (w ×₃ v) :=
begin
  simp [cross_product, mul_comm (v _) (w _)]
end

[Martin Dvořák]

Andrew Yang said:

A quick golf

/-- cross product is anti-commutative -/
lemma cross_product_anticomm (v w : fin 3 → R) :
  v ×₃ w = - (w ×₃ v) :=
begin
  simp [cross_product, mul_comm (v _) (w _)]
end

Thanks a lot!!!!!

I will try to write more proofs in a similar manner.

[Kyle Miller]

Going back to the Dec 18 discussion, regarding the correct generalization: I think the cross product is commonly regarded as being a bilinear map on $\mathbb{R}^3$, and anyone who uses generalizations tends not to use the cross product itself.

The property that completely determines the cross product is the triple product: $(u \times v)\cdot w=\det[u\ v\ w]$. The idea is that $w\mapsto \det[u\ v\ w]$ is an element of $(\mathbb{R}^3)^*$, and the dot product lets you take this dual vector and turn it back into a vector.

A general version is that if you have some fixed $\omega\in \Lambda^{k+1}(V)$ when $V$ is an inner product space, you can take vectors $v_1,\dots,v_k\in V$, compute the iterated interior multiplication $i_{v_k}i_{v_{k-1}}\cdots i_{v_1}(\omega)\in V^*$, then dualize using the inner product to get an element of $V$. This defines an alternating linear map $\Lambda^k V\to V$. The $k=2$ case when $\omega$ is the determinant form gives the cross product.

[Martin Dvořák]

Andrew Yang said:

A quick golf

/-- cross product is anti-commutative -/
lemma cross_product_anticomm (v w : fin 3 → R) :
  v ×₃ w = - (w ×₃ v) :=
begin
  simp [cross_product, mul_comm (v _) (w _)]
end

Is the part (v _) (w _) needed?

[Andrew Yang]

Seems that it's not. Lean is smarter than I thought.

[Martin Dvořák]

Andrew Yang said:

Seems that it's not. Lean is smarter than I thought.

What is the process of finding out that simp with my definition and the only lemma mul_comm is enough?

[Andrew Yang]

after simp [cross_product], you will see that the two sides of the equation only differs by some mul_comm.

[Kyle Miller]

Importantly, even though you could rewrite with mul_comm repeatedly forever, simp will put things into a normal form.

[Martin Dvořák]

Oh! Now I see that sequence

dsimp [cross_product],
simp [mul_comm],

accomplishes the goal as well!

[Kyle Miller]

Btw, you can get it down to just one line with

lemma cross_product_anticomm (v w : fin 3 → R) :
  v ×₃ w = - (w ×₃ v) :=
by simp [cross_product, mul_comm]

Here's another:

lemma cross_product_anticomm' (v w : fin 3 → R) :
  v ×₃ w + w ×₃ v = 0 :=
by simp [cross_product, add_eq_zero_iff_eq_neg, mul_comm]

[Kyle Miller]

If you add spaces around the notation, you'll get somewhat more legible output in the goal window:

local infix ` ×₃ `: 68 := cross_product
local infix ` ⬝ ` : 67 := matrix.dot_product

[Martin Dvořák]

Kyle Miller said:

Going back to the Dec 18 discussion, regarding the correct generalization: I think the cross product is commonly regarded as being a bilinear map on $\mathbb{R}^3$, and anyone who uses generalizations tends not to use the cross product itself.

The property that completely determines the cross product is the triple product: $(u \times v)\cdot w=\det[u\ v\ w]$. The idea is that $w\mapsto \det[u\ v\ w]$ is an element of $(\mathbb{R}^3)^*$, and the dot product lets you take this dual vector and turn it back into a vector.

A general version is that if you have some fixed $\omega\in \Lambda^{k+1}(V)$ when $V$ is an inner product space, you can take vectors $v_1,\dots,v_k\in V$, compute the iterated interior multiplication $i_{v_k}i_{v_{k-1}}\cdots i_{v_1}(\omega)\in V^*$, then dualize using the inner product to get an element of $V$. This defines an alternating linear map $\Lambda^k V\to V$. The $k=2$ case when $\omega$ is the determinant form gives the cross product.

Oh! That is a beautiful motivation!

[Martin Dvořák]

BTW should we fork this conversation — move my n00bish implementation question to a separate thread?

[Kyle Miller]

@Martin Dvořák More golfing using a lemma with a questionable proof (it perhaps depends on the definition of finset.sum a bit too much?)

lemma dot_product_unfold' (v w : fin 3 → R) :
  v ⬝ w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2 :=
begin
  simp [matrix.dot_product, add_assoc],
  rw ← add_zero (v 2 * w 2),
  refl,
end

lemma cross_product_perpendicular_first_arg (v w : fin 3 → R) :
  v ⬝ (v ×₃ w) = 0 :=
begin
  simp only [cross_product, dot_product_unfold'],
  simp [mul_sub, mul_assoc, mul_left_comm],
end

[Kyle Miller]

There's a nonterminal simp here, but that lemma is useful for the triple product permutation lemma:

lemma triple_product_equality (u v w : fin 3 → R) :
  u ⬝ (v ×₃ w) = v ⬝ (w ×₃ u) :=
begin
  simp only [cross_product, dot_product_unfold'],
  simp [mul_sub, mul_assoc, mul_left_comm, mul_comm],
  ring,
end

[Yakov Pechersky]

You can always use docs#finset.sum_univ_succ or whatever it's called

[Kyle Miller]

This works, too:

lemma triple_product_equality (u v w : fin 3 → R) :
  u ⬝ (v ×₃ w) = v ⬝ (w ×₃ u) :=
begin
  simp only [cross_product, dot_product_unfold',
    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

[Kyle Miller]

@Yakov Pechersky Great:

lemma dot_product_unfold' (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]

[Martin Dvořák]

Do you still want me to create the PR in the end, even tho most of the code is yours?

[Martin Dvořák]

Ye deserve the credit but I actually wanted to experience the whole workflow with Lean/mathlib. So I don't know now.

[Arthur Paulino]

Martin Dvořák said:

Ye deserve the credit but I actually wanted to experience the whole workflow with Lean/mathlib. So I don't know now.

There's an "Authors" field at the top of mathlib files. You can credit Kyle and yourself there in alphabetic order. I've done if before and it was fine :smile:

[Martin Dvořák]

OK! And copyright goes to?

[Kyle Miller]

@Martin Dvořák Please create the PR! Creating the PR and shepherding it through the review process is a large part of the work.

[Arthur Paulino]

Martin Dvořák said:

OK! And copyright goes to?

You're creating the file so I think it's you :+1:

[Martin Dvořák]

OK ok. But I should sort out the →ₗ[R] first, right?

[Kyle Miller]

@Martin Dvořák A possible framework. I don't know this part of the library well enough to know if this is the best way to do it though:

def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
{ to_fun := λ a,
  { to_fun := λ 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) ],
    map_add' := λ a b, begin
      sorry
    end,
    map_smul' := λ c a, begin
      sorry
    end },
  map_add' := λ a b, begin
    sorry
  end,
  map_smul' := λ c a, begin
    sorry
  end }

[Martin Dvořák]

I made progress.
https://github.com/madvorak/mathlib/blob/master/src/linear_algebra/cross_product.lean

My current problem is that I don't know how to attack goals of this form:

⊢ {to_fun := λ (b : fin 3 → R),
  ![(c • a) 1 * b 2 - (c • a) 2 * b 1, (c • a) 2 * b 0 - (c • a) 0 * b 2, (c • a) 0 * b 1 - (c • a) 1 * b 0],
  map_add' := _, map_smul' := _}
 = ⇑(ring_hom.id R)
  c • {to_fun := λ (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],
  map_add' := _, map_smul' := _}

[Martin Dvořák]

Unless I am mistaken, I am on the outside level, hence I need to prove equality of two functions of the type (fin 3 → R) →ₗ[R] (fin 3 → R).

[Yaël Dillies]

Have you tried ext?

[Yury G. Kudryashov]

BTW, we have https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_map.html#linear_map.mk%E2%82%82 for creating bilinear maps.

[Martin Dvořák]

After ext I see the following goal, which I understand even less:

⊢ ⇑{to_fun := λ (b : fin 3 → R), ![(c • a) 1 * b 2 - (c • a) 2 * b 1, (c • a) 2 * b 0 - (c • a) 0 * b 2, (c • a) 0 * b 1 - (c • a) 1 * b 0], map_add' := _, map_smul' := _} x x_1 = ⇑(⇑(ring_hom.id R) c • {to_fun := λ (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], map_add' := _, map_smul' := _}) x x_1

image.png

[Yaël Dillies]

Clean it up for you own eyes using dsimp.

[Martin Dvořák]

Yury G. Kudryashov said:

BTW, we have https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_map.html#linear_map.mk%E2%82%82 for creating bilinear maps.

I don't understand the code. Can I somehow use it to just prove the linearity in the second argument and use the "symmetry"?

[Yury G. Kudryashov]

No, it's not about (anti)symmetric maps. You can use

def cross_product : (fin 3 → R) →ₗ[R] (fin 3 → R) →ₗ[R] (fin 3 → R) :=
linear_map.mk₂
  (λ a b, ![...]) -- same is in your code
  _
  _
  _
  _

This way you don't need to use linear_map.ext

[Martin Dvořák]

[crowdproving]
Well, this is my current state of the proof:

⊢ ![c * (a 1 * b 2 - a 2 * b 1), c * (a 2 * b 0 - a 0 * b 2), c * (a 0 * b 1 - a 1 * b 0)] x
= c * ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0] x

On the LHS, the vector gets first multiplied and then the element gets selected.
On the RHS, the element first gets selected and then it is multiplied.
image.png
Any idea how to close the goal?

[Yaël Dillies]

Move multiplication inside, then use extensionality.

[Martin Dvořák]

What do you mean by "inside" please?

[Yaël Dillies]

inside the vector

[Martin Dvořák]

I should probably be trivial, but I am lost. I am probably too tired. Imma continue tomorrow.

[Eric Rodriguez]

Can you post your code again? A few incantations of simp should really get you there.

[Yaël Dillies]

Try rw pi.const_mul or something.

[Eric Wieser]

fin_cases x; simp ought to work

[Joseph Myers]

Rather than using ![] I'd suggest λ i, a (i + 1) * b (i + 2) - a (i + 2) * b (i + 1) and then hopefully you don't need to use fin_cases.

[Martin Dvořák]

Eric Wieser said:

fin_cases x; simp ought to work

It works! Awesome! Thanks a lot!

Also fin_cases x; refl, works as well, so I will keep the latter.

[Martin Dvořák]

With your great help, I finished the proofs! What do you think?

https://github.com/madvorak/mathlib/blob/master/src/linear_algebra/cross_product.lean

[Martin Dvořák]

In the lemmata (everything that follows after line 58), I should rename the arguments to x and y in order to comply with the mathlib's manual of style, right?

[Martin Dvořák]

However, I don't understand what Jeremy Avigad meant by writing that a, b, c are for propositions.
https://leanprover-community.github.io/contribute/style.html

[Arthur Paulino]

On formatting style, check how curly brackets are used in other proofs.
I also see some glossary#non-terminal-simp usages, which is avoided in mathlib

[Martin Dvořák]

Thank you! I will revise it.

[Arthur Paulino]

This link contains some useful information about documentation: https://leanprover-community.github.io/contribute/doc.html
Your file is currently missing a module documentation, which summarizes what you're exploring, a somewhat precise overview of the main definitions you're proposing and, if applicable, a few #TODO items for next steps.

We usually don't add documentation for lemmas/theorems, although I think this is not forbidden. The motivation is that we try to make the lemmas names precise and explicit enough.

[Patrick Massot]

Arthur Paulino said:

We usually don't add documentation for lemmas/theorems

I think you got this impression from reading only elementary lemmas in mathlib.

[Patrick Massot]

What is useless is adding a docstring which takes longer to read than the actual statement.

[Martin Dvořák]

Did I name my lemmata well?

[Patrick Massot]

Arthur, you can have a look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/parametric_interval_integral.html for instance. Lemmas there have quite a number of assumptions and docstrings help a bit.

[Patrick Massot]

Looking at this page myself, I have a question for @Rob Lewis: why do we get all those «μ» instead of μ?

[Arthur Paulino]

Patrick Massot said:

Arthur, you can have a look at https://leanprover-community.github.io/mathlib_docs/analysis/calculus/parametric_interval_integral.html for instance. Lemmas there have quite a number of assumptions and docstrings help a bit.

Nice! There's even an explanation for the reasoning behind the proof itself. I was wondering if it was a thing in mathlib

[Arthur Paulino]

Oh wait, the docstring doesn't explain the proof. Nevermind. But it does help understanding the assumptions

[Patrick Massot]

We also have complicated proofs having comments explaining the strategy (and such comments can also be found in module docstrings).

[Patrick Massot]

Have a look at https://github.com/leanprover-community/mathlib/blob/2ceda7850a0aaa35f31697072c755fb3de3dbaa7/src/topology/metric_space/baire.lean#L42 for instance.

[Eric Wieser]

The weird brackets are because somewhere μ is defined as notation, and the brackets say "not the notation"

[Patrick Massot]

But this notation is clearly not in scope here.

[Eric Wieser]

All open_locale notation is in scope in doc-gen

[Kyle Miller]

@Martin Dvořák I got rid of the nonterminal simps and got things somewhat more mathlib ready. I tried speeding up some of the proofs using some specialized lemmas for operations on 3-vectors (vec3_eq, vec3_add, and so on). I also switched the definition of cross_product to Yury's suggestion and created a locale for vector notation.

There's also the determinant characterization of the triple product:

lemma triple_product_eq_det (u v w : fin 3 → R) : u ⬝ (v ×₃ w) = matrix.det ![ u, v, w ]

Code:

/-
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, Andrew Yang
-/

import data.matrix.basic
import data.matrix.notation
import tactic.fin_cases
import linear_algebra.bilinear_map
import linear_algebra.matrix.determinant

/-!
# Cross products

This module defines the cross product of vectors in $R^3$ for $R$ a commutive ring.

## Main definitions

* `cross_product` is the cross product of pairs of vectors in $R^3$.

## Main results

* `triple_product_eq_det`

## Notation

The locale `vectors` gives the following notations:

* `×₃` for the cross product
* `⬝` for dot products

## Tags

cross product

-/

variables {R : Type*}

lemma vec3_eq {a b : fin 3 → R}
  (h0 : a 0 = b 0) (h1 : a 1 = b 1) (h2 : a 2 = b 2) :
  a = b :=
by { ext x, fin_cases x; assumption }

lemma vec3_eq' {a0 a1 a2 b0 b1 b2 : R}
  (h0 : a0 = b0) (h1 : a1 = b1) (h2 : a2 = b2) :
  ![a0, a1, a2] = ![b0, b1, b2] :=
by rw [h0, h1, h2]

variables [comm_ring R]

lemma vec3_add {a b : fin 3 → R} :
  a + b = ![a 0 + b 0, a 1 + b 1, a 2 + b 2] :=
by { apply vec3_eq; refl }

lemma vec3_add' {a0 a1 a2 b0 b1 b2 : R} :
  ![a0, a1, a2] + ![b0, b1, b2] = ![a0 + b0, a1 + b1, a2 + b2] :=
by { rw vec3_add, refl }

/-- 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, algebra.id.smul_eq_mul, matrix.smul_cons,
    matrix.smul_empty, pi.smul_apply];
  apply vec3_eq';
  ring
end

localized "infixl ` ×₃ `: 68 := cross_product" in vectors
localized "infix ` ⬝ ` : 67 := matrix.dot_product" in vectors

lemma cross_product_def (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_def, 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_eq_zero_vector (v : fin 3 → R) :
  v ×₃ v = 0 :=
by simp [cross_product_def, mul_comm]

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]

lemma dot_self_cross_product_eq_zero (v w : fin 3 → R) :
  v ⬝ (v ×₃ w) = 0 :=
by simp [cross_product_def, vec3_dot_product, mul_sub, mul_assoc, mul_left_comm]

lemma dot_cross_product_self_eq_zero (v w : fin 3 → R) :
  w ⬝ (v ×₃ w) = 0 :=
by rw [cross_product_anticomm, matrix.dot_product_neg, dot_self_cross_product_eq_zero, neg_zero]

/-- Cyclic permutations preserve 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_def, 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

lemma 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_def, 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

[Kyle Miller]

By the way, is there a way to make cross_product pretty print properly? The expression v ×₃ w = - (w ×₃ v) prints as ⇑(⇑cross_product v) w = -⇑(⇑cross_product w) v.

[Anne Baanen]

You'll probably want to write out the coe_fn/⇑ in the notation, so something like (untested):

notation v ` ×₃ ` w := ⇑(⇑cross_product v) w

[Kyle Miller]

I haven't been able to get that to work or any number of permutations... Did you manage, @Eric Wieser?

[Eric Wieser]

No, I didn't. Is this in a branch / PR somewhere?

[Kyle Miller]

There's a code snippet of a complete module I posted two messages up.

[Anne Baanen]

I'm having trouble too. How does src#linear_map.comp do it?

[Eric Wieser]

My point is that I think this is mature enough that zulip is probably no longer the best place to discuss it, and it would probably make sense for @Martin Dvořák to make a PR

[Anne Baanen]

Ah right, that's not bundled.

[Martin Dvořák]

Thank you very much for your helps! I will take care of the PR.

[Martin Dvořák]

If you say that triple_product_eq_det is the main result, should I denote it as a theorem instead?

[Kyle Miller]

You can put other main results, too. I just wanted to be sure to include that since it's theoretically important.

[Martin Dvořák]

Can we keep the identifiers u, v, w as name of vectors (even tho they are probably standard names for universes in Lean/mathlib)?

[Martin Dvořák]

Kyle Miller said:

You can put other main results, too. I just wanted to be sure to include that since it's theoretically important.

I don't want to exaggerate the importance of the other results. I just wanted to denote it as a theorem unless you are opposed to it.

[Kyle Miller]

data.fin.vec_notation seems to use u and v for vectors

[Martin Dvořák]

Kyle Miller said:

data.fin.vec_notation seems to use u and v for vectors

Oh, that's weird. In this file, the identifier u is used in both meanings (globally universe; in arguments a vector).

[Kyle Miller]

I'm not sure it matters whether it's a theorem or not -- in the docs everything seems to be a theorem anyway -- so feel free to choose how you want.

[Martin Dvořák]

BTW how did you generate the long list of all lemmata used in the last simp?

[Kyle Miller]

In data.fin.vec_notation, u is used as both a universe variable and an argument, too.

[Kyle Miller]

simp?

[Martin Dvořák]

simp only [vec3_dot_product, cross_product_def, 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],

[Kyle Miller]

Yeah, I seeded it with the first three and then did simp? [vec3_dot_product, cross_product_def, matrix.det_fin_three]

[Martin Dvořák]

I suppose you didn't write it by hand. Can I first call just simp and then get the list of all used lemmata in it?

[Martin Dvořák]

Thanks!

[Martin Dvořák]

And is there any semantics in which lemmata you placed on the same line?

[Kyle Miller]

I mostly made sure the three main ones came first in case someone wanted to regenerate it later, and any other rearrangements I might have made don't matter.

[Damiano Testa]

Just a very minor comment: should

lemma cross_product_anticomm (v w : fin 3 → R) :
  v ×₃ w = - (w ×₃ v) :=

be formulated with the minus sign on the other side of the equality?

--  The right-hand side is "easier" than the left-hand side
lemma cross_product_anticomm (v w : fin 3 → R) :
  - (v ×₃ w) = w ×₃ v :=

[Yaël Dillies]

That seems nicer, yeah.

[Martin Dvořák]

Thanks for the suggestion! I updated the pull request.

[Martin Dvořák]

Anne Baanen said:

You'll probably want to write out the coe_fn/⇑ in the notation, so something like (untested):

notation v ` ×₃ ` w := ⇑(⇑cross_product v) w

Should I change the notation for ×₃ to the above? I don't know what coe_fn and ⇑ mean.

[Martin Dvořák]

This is the pull request: https://github.com/leanprover-community/mathlib/pull/11181

[Anne Baanen]

I understood that my suggestion did not work. Does cross_product v w pretty-print as v ×₃ w now?

[Martin Dvořák]

No, it doesn't. And it is weird. I think that it did pretty print a few commits ago...

[Martin Dvořák]

It worked when it was written as:

local infix ` ×₃ `: 68 := cross_product

No it doesn't work when it is written as:

localized "infixl ` ×₃ `: 68 := cross_product" in vectors

[Martin Dvořák]

I don't know how it works so it is still possible that the pretty print stopped due to some other change.

[Martin Dvořák]

Should I experiment with that? Or do you see it from your knowledge?

[Anne Baanen]

I don't know much about the pretty-printer, and can't think of any other tricks to experiment with. I guess let's just keep it as it is.

[Kyle Miller]

@Martin Dvořák I'm pretty sure it stopped working when we made cross_product be a multilinear map rather than a plain function.

All localized really does is store the quoted code so that when you later do open_locale vectors it will automatically run local infixl ×₃ : 68 := cross_product, so I'd be surprised if that's the cause.

[Martin Dvořák]

Kyle Miller said:

Martin Dvořák I'm pretty sure it stopped working when we made cross_product be a multilinear map rather than a plain function.

Oh, you are absolutely right!

[Eric Wieser]

Instead of providing a bilinear map, would it make more sense to provide the cross product as a lie_ring instance?

[Johan Commelin]

There is already a lie_ring instance on fin 3 → ℝ. (And it's not propeq to the cross product.)

[Eric Wieser]

Something like:

instance vec3_has_bracket : has_bracket (fin 3 → R) (fin 3 → R) :=
{ bracket := λ u v, u ×₃ v }

instance vec3_lie_ring : lie_ring (fin 3 → R) :=
{ add_lie := linear_map.map_add₂ _,
  lie_add := λ u, linear_map.map_add _,
  lie_self := cross_product_self,
  leibniz_lie := λ u v w, begin
    dsimp only [has_bracket.bracket, cross_product_apply],
    ext i,
    fin_cases i; norm_num; ring,
  end,
  ..pi.add_comm_group }

-- pretty printer can't use this unfortunately
localized "infixl ` ×₃ `: 68 := @has_bracket.bracket _ _ vec3_has_bracket" in vectors

[Eric Wieser]

Johan Commelin said:

There is already a lie_ring instance on fin 3 → ℝ.

Where? apply_instance didn't find it for me.

[Johan Commelin]

Weird. Maybe lie_ring.pi is missing from mathlib? But it certainly exists in the platonic ideal of mathlib.

[Eric Wieser]

Ah, missing import

[Eric Wieser]

docs#lie_ring.of_associative_ring

[Damiano Testa]

This seems a situation where a human being told of a Lie bracket on fin 3 → ℝ would not choose the one coming from the instance... or where they would at least ask "Are you really sure that you want the zero Lie-bracket?" :smile:

[Damiano Testa]

Is it possible to override the instance when the associative ring is also commutative?

[Johan Commelin]

I'm afraid that's non-trivial.

[Oliver Nash]

And not desirable; we want to be able to make statements like docs#commutative_ring_iff_abelian_lie_ring

[Eric Wieser]

I guess a type synonym would solve the problem here

[Eric Wieser]

Do people agree that working with a lie structure would be better than just having a bilinear map?

[Oliver Nash]

It's such a specific case that it's hard to have strong feelings. Regarding the cross product as a Lie bracket is mostly just a curiosity. I'd be happy either way.

[Johan Commelin]

I have never used the cross product apart from the Intro to Calculus course. So I wouldn't put it high up my prio list. But I'm just one anecdote.

[Damiano Testa]

I also do not have strong opinions, really. If someone asked me to provide a Lie bracket on ℝ^3, my first reaction would probably be "What a weird question". Then I would think about the cross-product. Finally I would think of the zero Lie bracket.

[Oliver Nash]

I look forward to a long thread about the seven-dimensional cross product once we finish here :-)

[Ruben Van de Velde]

But that's the last one, right?

[Johan Commelin]

Damiano Testa said:

If someone asked me to provide a Lie bracket on ℝ^3,

The standard $\mathfrak{sl}_2$-triple with basis $(X,H,Y)$.

[Damiano Testa]

Oh, but that is $\mathfrak{sl}_2$, nor $\mathbb{R}^3$: as the notation suggests, they are not the same! :upside_down:

[Johan Commelin]

Sure, I completely agree. But still, if you ask me to put a Lie algebra structure on a 3-dimensional space with a distinguished basis, this is the one I would pick :smile:

[Kyle Miller]

Oliver Nash said:

It's such a specific case that it's hard to have strong feelings. Regarding the cross product as a Lie bracket is mostly just a curiosity. I'd be happy either way.

I think it's sort of a curiosity, too, a sort of "law of small numbers" (that there are interesting coincidences for things of small cardinality or dimension).

It does have some sense to it, but it takes a few isomorphisms. We start with $V=\mathbb{R}^3$ as the fundamental $\mathfrak{so}(3)$-module. The adjoint representation is $\Lambda^2 V$, which is isomorphic to $\mathfrak{so}(3)$ since it may be regarded as being antisymmetric matrices (we identify $V$ with $V^*$ using the inner product from the definition for $\mathfrak{so}(3)$). Then, the Hodge star gives an isomorphism $V=\Lambda^2 V$. Through these isomorphims you can transport the Lie bracket for $\mathfrak{so}(3)$ to $\mathbb{R}^3$.

You can also consider the constant part of differential forms on $\mathbb{R}^3$ under wedge product, using the Hodge star to identify 2-forms with 1-forms. This is the significance of cross products in 3D vector calculus.

[Kyle Miller]

@Johan Commelin What, you wouldn't choose the Heisenberg Lie algebra? :smile:

[Johan Commelin]

Nah, I'm a semisimple guy

[Kalle Kytölä]

I almost thought "simple guy" based on the $\R^3 = \mathfrak{sl}_2$ example above, until... :light_bulb: I remembered that we should strive for the mathlib level of generality.

[Kalle Kytölä]

Ok, bad jokes aside... (Unless the following is yet another one...)

I originally suggested lie_ring for the cross product, because I thought one would then nicely get for free any API consequences of antisymmetry and Jacobi identity. The problems pointed out back then were at least competing instances (the zero bracket, which I think indeed begs the "are you sure?" question to humans) and perhaps notation (I wasn't sure about it). Also the later proposal of implementing the cross product as a bilinear map for sure gives a substantial amount of API for free.

But in fact lie_algebra R (for [comm_ring R]) should in principle give all API of bilinearity, antisymmetry, and Jacobi identity. So in terms of reusing the maximal amount of existing API, wouldn't it be close to optimal? Except, of course, if getting access to the API requires that lie_algebra is an instance, in which case we only get all the consequences of bilinearity, antisymmetry, and Jacobi identity for the the zero Lie bracket ("for free" :smiley:).

[Kalle Kytölä]

Just to clarify, that is not a proposal to change anything implemented right now! But since Eric Wieser brought up the possibility of lie_ring implementation again, I thought it might be worth still clarifying what are the merits of the different choices.

[Eric Wieser]

@Kalle Kytölä, I didn't see your original suggestion, but your comment above nicely summarizes why I think using the lie spelling might be a good idea. Indeed, there's no need to change the approach in the current PR, but it certainly gives us a large pile of reusable lemmas.

[Kyle Miller]

@Eric Wieser What do you mean specifically by a "lie spelling"?

@Kalle Kytölä Are you aware that the current version of #11181 contains a lie_ring implementation as a local instance? Design-wise, I think it's a nice idea to use the lie_ring instance to prove lemmas that are generally true for Lie rings, but in terms of cross product notation.

I think it's good to consider the principle "just because something is something doesn't mean that it is something." I don't see any benefit to be had defining the cross product through the $\mathfrak{so}(3)$ or $\mathfrak{sl}(2)$ exceptional isomorphisms, or requiring that $\mathbb{R}^3$ be a Lie ring and that the cross product needs to be rendered as a Lie bracket. Similarly, the cross product corresponds to the imaginary part of one of the Hurwitz algebras (equivalently: the imaginary part for the quaternions), but do we need to give $\mathbb{R}^3$ a has_mul for a nonunital nonassociative algebra structure? (That would conflict with the has_mul from the pi instance anyway.)

[Kyle Miller]

There are some exceptional identities involving cross products and dot products that would be nice to have at some point. You can understand them as coming from the representation theory of $\mathbb{R}^3$ as a Lie algebra, but they're also straightforward to prove by algebraic manipulation.

Edit: The main one would be $(u\times v)\cdot (w\times x) = (u\cdot w)(v\cdot x) - (u\cdot x)(v\cdot w)$

[Eric Wieser]

Kyle Miller said:

Eric Wieser What do you mean specifically by a "lie spelling"?

I mean introduce a type synonym such that instead of having terms of the form ⇑(⇑cross_product v) w we have terms of the form ⁅v, w⁆. Neither pretty-prints in the nice ×₃ way anyway, but the latter has more existing lemmas than the former, and is shorter.

[Eric Wieser]

Perhaps we can reuse the docs#euclidean_space docs#pi_Lp synonym?

[Eric Wieser]

With the rationale being; pi_Lp replaces the elementwise norm with the Lp norm, just as we want to replace the elementwise bracket with the geometrically meaningful one

[Kalle Kytölä]

Kyle Miller said:

Kalle Kytölä Are you aware that the current version of #11181 contains a lie_ring implementation as a local instance? Design-wise, I think it's a nice idea to use the lie_ring instance to prove lemmas that are generally true for Lie rings, but in terms of cross product notation.

Oh, sorry, I had not noticed this! I don't have experience with local instances yet, but I think it is great if this gives access to the lie_ring API. I suppose that since bilinearity is currently more directly built in, a local instance of lie_algebra would not add much? (EDIT: Or would it? With scalars in docs#lie_algebra anything that theR in fin 3 → R is a module over. Might it make a different part of API available, still?)

Kyle Miller said:

I think it's good to consider the principle "just because something is something doesn't mean that it is something."

I fully agree! It is only for "free API" reasons I thought the lie_ring or lie_algebra might be appropriate. I have no strong opinions of what the cross product should be fundamentally, but I agree that it is not particularly fundamentally a Lie bracket.