Euclidean space is oriented

Stream: mathlib4

[Yaël Dillies]

How far are we from showing that Euclidean space is oriented? Eg something like

import Mathlib

instance (n : Type*) [Fintype n] : Module.Oriented ℝ (EuclideanSpace ℝ n) n := sorry

cc @Joseph Myers

[Eric Wieser]

I think this is a one-liner, but also perhaps a bad global instance

[Eric Wieser]

import Mathlib

noncomputable instance (n : Type*) [Fintype n] [DecidableEq n] : Module.Oriented ℝ (EuclideanSpace ℝ n) n :=
  ⟨Basis.orientation <| Pi.basisFun _ _⟩

[Jireh Loreaux]

Why do you think it's a bad global instance?

[Eric Wieser]

I don't remember, I just remember thinking that in the past

[Yaël Dillies]

Oh that was easy. I somehow assumed it would be harder due to the rays involved. But I guess docs#Basis.orientation already does the heavy lifting

[Antoine Chambert-Loir]

Is it a good thing to force people to use that precise orientation?

[Yaël Dillies]

I would personally be happy with a Nonempty (Module.Oriented ℝ (EuclideanSpace ℝ n) n) instance

[Eric Wieser]

I'm not sure I even understand which orientation that chooses for n = Fin m

[Yury G. Kudryashov]

Note that Nonempty (Module.Oriented ...) just says that the dimension of a space is at least Fintype.card ι.

[Yury G. Kudryashov]

Eric Wieser said:

I'm not sure I even understand which orientation that chooses for n = Fin m

The one that's positive on the Pi.single basis, I guess.

[Yury G. Kudryashov]

BTW, there are no nontrivial instances of Module.Oriented at the moment.

[Yury G. Kudryashov]

E.g., we have no Module.Oriented R R (Fin 1) (or should we use PUnit?)

[Yaël Dillies]

Yury G. Kudryashov said:

Note that Nonempty (Module.Oriented ...) just says that the dimension of a space is at least Fintype.card ι.

I am not saying it says much mathematically. However that doesn't mean we shouldn't have it!

[Yury G. Kudryashov]

If we're talking about Prod/Pi/PiLp instances, then we have the following issue:

• If we have Module.Oriented R M ι and Module.Oriented R N ι', then we can have Module.Oriented R (M × N) (ι ⊕ ι');
• however, if ι = Fin k and ι' = Fin l, then we get Fin k ⊕ Fin l, not Fin (k + l). Should we have an instance with Fin (k + l) too?
• similarly, for ∀ i : ι, E i with ∀ i, Oriented R (E i) (σ i), we get Oriented R (∀ i, E i) (Σ i, σ i)
• this time, we need an order (or FinEnum) on ι to get from ∀ i, Oriented R (E i) (Fin (d i)) to Oriented R (∀ i, E i) (Fin (∑ i, d i)).
• in the special case ι → E, we can have Oriented R (ι → E) (ι × σ); should we?
• we can have [Oriented R E (Fin d)] : Oriented R (ι → E) (Fin (Fintype.card ι * d)), if we have an order on ι.

[Yury G. Kudryashov]

Yaël Dillies said:

Yury G. Kudryashov said:

Note that Nonempty (Module.Oriented ...) just says that the dimension of a space is at least Fintype.card ι.

I am not saying it says much mathematically. However that doesn't mean we shouldn't have it!

If we want to talk about it, then IMHO we should have a more readable typeclass (e.g., LERank R M d).

[Eric Wieser]

Yury G. Kudryashov said:

• Should we have an instance with Fin (k + l) too?

I don't think we need to worry about this, because the index type is not an outparam

[Eric Wieser]

So we can have as many alternative indices as we like

[Antoine Chambert-Loir]

If you have an orientation on Fin (k + l), playing with add_comm will sometimes give the right one on Fin (l + k), sometimes not…

[Aaron Liu]

Can you give an example?

[Aaron Liu]

I think if l and k are both odd, and you mix docs#Fin.cast with docs#finAddFlip, you will get the opposite orientation.

[Aaron Liu]

But why would you do that

[Jireh Loreaux]

Antoine, I think you need three variables in the sum for that to be the case. With two you always get a cyclic permutation.

[Eric Wieser]

I don't really understand the problem here; if you start rewriting arguments to typeclasses you're usually going to end up in a mess; for instance, unfolding Matrix into a function types is going to leave you with nonsense Mul instances on functions.

[Yury G. Kudryashov]

Antoine Chambert-Loir said:

If you have an orientation on Fin (k + l), playing with add_comm will sometimes give the right one on Fin (l + k), sometimes not…

I don't understand this. If you have [Oriented R E (Fin 2)] [Oriented R F (Fin 3)], then you get some specific orientation for Oreinted R (E × F) (Fin 5). Note that F × E is a different space, so it doesn't matter (for typeclass diamonds) if Equiv.prodComm is not an orientation-preserving map.

[Yury G. Kudryashov]

BTW, should we have [Module Complex E] : Oriented Real E ??? for some ????

[Yury G. Kudryashov]

Here ??? is equivalent to Fin (2 * finrank Complex E).

[Yury G. Kudryashov]

But we may want to use a different type to avoid diamonds for specific low dimensions.

[Joseph Myers]

Note that we don't yet have any of the definitions mapping from orientations of individual spaces to an orientation of a pairwise or indexed product space, which you need as defs on Orientation before you use them to construct any possible Module.Oriented instances.

[Joseph Myers]

(I think such definitions only make sense - that is, are canonical - when the index types have cardinality equal to the dimensions (which is the intended use case of Orientation, but the definition of Orientation doesn't require the right cardinality).)

[Joseph Myers]

If we don't have those definitions when I get to setting up the relation between incenter of a simplex and angle bisectors in general dimensions, I may add them at that point, since I think such definitions will be of use in e.g. saying what's a consistent collection of orientations of the faces of a simplex (in order then to say what's an internal / external bisector between two faces). The map in the reverse direction (given an orientation of a product space indexed by a sum type, and an orientation of one of the two spaces, get the corresponding orientation of the other space) may also be useful.

[Joseph Myers]

I don't think of the Fin (k + l) orientation as being particularly canonical, it's more what you get if you use Orientation.reindex with a particular choice of equivalence between the sum type and that Fin type.

[Eric Wieser]

Eric Wieser said:

import Mathlib

noncomputable instance (n : Type*) [Fintype n] [DecidableEq n] : Module.Oriented ℝ (EuclideanSpace ℝ n) n :=
  ⟨Basis.orientation <| Pi.basisFun _ _⟩

Just to check @Joseph Myers, do you think this instance is a good idea, or do you have reservations?

[Eric Wieser]

I think my reservation was mainly "Joseph would surely have added this instance if he felt it was a good idea, so its absence suggests it may not be"

[Joseph Myers]

I think it's a reasonable instance. I don't think I was considering the concrete EuclideanSpace at all when setting up orientations, just general spaces of a given dimension where an orientation might be assumed as a type class hypothesis where needed for a statement, or an (arbitrary) instance constructed inside a proof where only needed for the proof and not the statement of the result.