generalizing docs#crossProduct over input types

Stream: Is there code for X?

[Vedant Gupta]

Currently, the definition of CrossProduct only works with input/output type (Fin 3 -> Real). I think it would be useful to generalise this definition so that it also works with types such as EuclideanSpace ℝ (Fin 3) (at present, using EuclideanSpace ℝ (Fin 3) as input still yields a Fin 3 -> Real as output, which can make it harder to get the L2 norm of the cross product...). I'm not sure what the right way would be to write such a generalised definition. Any help would be very appreciated!
For more details on why this is relevant see #20920

[Eric Wieser]

I don't have an answer to this generalization, but I left a comment on the PR showing how you can make do without it for now

[Eric Wieser]

Ok, here's the generalization I'd suggest:

-- in the existing file
class CrossProduct (R : outParam Type*) (V3 : Type*) [AddCommGroup V3] [Module R V3] where
   crossProduct : V3 →ₗ[R] V3 →ₗ[R] V3
   -- all the lie axioms
   crossProduct_self : sorry
   liebniz_crossProduct : sorry

export CrossProduct (crossProduct)

-- theorems about cross products only, from the lie structure

instance : CrossProduct R (Fin 3 -> R) := ...

-- theorems about `Fin 3 -> R` and `Matrix.dotProduct` and `![x, y, z]`

-- in a new file
instance : CrossProduct R (EuclideanSpace (Fin 3) R) := ...

-- theorems about `EuclideanSpace` and `inner` and `!₂[x, y, z]`

-- theorems linking the two spellings via `WithLP.equiv`

[Kevin Buzzard]

Just to remark that probably if phi:V_3->V_3 is any linear isomorphism then my guess is that phi \circ crossProduct probably also satisfies the axioms so this is an extremely weak structure to be allowed the name CrossProduct.

[Eric Wieser]

That doesn't sound like a problem to me, the same comment about composing with linear morphisms applies to choices of norm, and we don't attempt to encode the choice in NormedSpace

[Eric Wieser]

Really the typeclass only needs to exist to 1) provide notation and 2) save us from copying the first 10 or so lemmas

[Jz Pan]

Eric Wieser said:

Ok, here's the generalization I'd suggest:

-- in the existing file
class CrossProduct (R : outParam Type*) (V3 : Type*) [AddCommGroup V3] [Module R V3] where
   crossProduct : V3 →ₗ[R] V3 →ₗ[R] V3
   -- all the lie axioms
   crossProduct_self : sorry
   liebniz_crossProduct : sorry

Isn't it Lie bracket?

[Michael Stoll]

Eric Wieser said:

liebniz_crossProduct

The guy was called Leibniz :smile: :flag_germany:

[Damiano Testa]

Eric Weiser must have developed an incompatible muscle memory...

[Kevin Buzzard]

Eric Wieser said:

That doesn't sound like a problem to me, the same comment about composing with linear morphisms applies to choices of norm, and we don't attempt to encode the choice in NormedSpace

Sure, but what I'm saying is "the cross product" is a special canonical thing on $\R^3$, there aren't lots of choices of "the cross product", so I'm objecting to the name CrossProduct for something which there might be many of (for example it would I think be quite odd to mathematicians if $0$ was a cross product).

However to be honest I don't really understand the Leibniz rule conceptually. The first axiom just says that you have a linear map $\Lambda^2(V_3)\to V_3$ sending $a\wedge b$ to $[a,b]$, but $[[a,b],c]+[[b,c],a]+[[c,a],b]=0$ might put a lot of constraints on it which I don't understand. It's not going to rule out the zero map though. In short I'm just suggesting that the class might need a different name.

[Oliver Nash]

I'm not convinced about a typeclass for the cross product. Maybe I could be persuaded if I can find time to appreciate the issue here but it's just the Lie algebra 𝔰𝔬(3).

[Oliver Nash]

If we can get branch#morrison-daniel/hodge-star merged (which is blocked by our #11155) then we'll be able to define a cross product on any three-dim space with orientation and metric. That's probably the right generality.

[Eric Wieser]

I think the typeclass proposed above is an improvement over the current crossProduct, but indeed removing crossProduct in its current form entirely in favor of what you define would probably be better

[Vedant Gupta]

Eric Wieser said:

I don't have an answer to this generalization, but I left a comment on the PR showing how you can make do without it for now

Thanks everyone! Would it makes sense for me to move ahead with #20920 using this makeshift solution @Eric Wieser? If not, how would y'all recommend I move ahead given there are a couple options here?

[Eric Wieser]

I think you should wrap up #20920 with the ugly-but-type-correct WithLp.equivs for now. As a follow up, we can see if Oliver can be convinced that CrossProduct is a useful intermediate step, or can convince me that it is not!