Commit 2021-12-03 07:10 f8f28da0

feat(linear_algebra/orientation): orientations of modules and rays in modules (#10306) Define orientations of modules, along the lines of a definition suggested by @hrmacbeth: equivalence classes of nonzero alternating maps. See: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/adding.20angles/near/243856522 Rays are defined in an arbitrary module over an ordered_comm_semiring, then orientations are considered as the case of rays for the space of alternating maps. That definition uses an arbitrary index type; the motivating use case is where this has the cardinality of a basis (two-dimensional use cases will use an index type that is definitionally fin 2, for example). The motivating use case is over the reals, but the definitions and lemmas are for ordered_comm_semiring, ordered_comm_ring, linear_ordered_comm_ring or linear_ordered_field as appropriate (a nontrivial ordered_comm_semiring looks like it's the weakest case for which much useful can be done with this definition). Given an intended use case (oriented angles for Euclidean geometry) where it will make sense for many proofs (and notation) to fix a choice of orientation throughout, there is also a module.oriented type class so the choice of orientation can be implicit in such proofs and the lemmas they use. However, nothing yet makes use of the type class; everything so far is for explicit rays or orientations. I expect more definitions and lemmas about orientations will need adding to make much use of orientations. In particular, I expect to need to add more about orientations in relation to bases (e.g. extracting a basis that gives a given orientation, in positive dimension).