Commit 2024-06-26 17:56 cf35070b

feat(Data/Matroid/Map): maps between matroids (#13960) This PR creates a new file with the machinery for transferring matroid structures between types. The most important definitions are Matroid.map, which pushes a M : Matroid α along f : α → β to give an N : Matroid β, and Matroid.comap, which pulls N : Matroid β back along f : α → β to get an M : Matroid α. The former requires f to be injective on the ground set of M, but the latter doesn't. The original decision to define matroids with an embedded ground set within a type rather than just a structure on a type came with tradeoffs, and it is in places like this that they show up the most. For this reason, the file also defines several variants of map where the range/domain of the function in question is a coerced set rather than a type. There is nothing mathematically interesting going on with these definitions, and maps and comaps are not central to matroid theory in actual research, but they are very useful in making formalization painless, as they save the work of painstakingly checking matroid axioms in many cases. They will be used in future PRs to define things like direct sums and linearly representable matroids.