[Merged by Bors] - feat(linear_algebra): redefine linear_map and linear_equiv to be semilinear

[dupuisf]

This PR redefines linear_map and linear_equiv to be semilinear maps/equivs.

A semilinear map f is a map from an R-module to an S-module with a ring homomorphism σ between R and S, such that f (c • x) = (σ c) • (f x). If we plug in the identity into σ, we get regular linear maps, and if we plug in the complex conjugate, we get conjugate linear maps. There are also other examples (e.g. Frobenius-linear maps) where this is useful which are covered by this general formulation. This was discussed on Zulip here, and a few preliminaries for this have already been merged.

The main issue that we had to overcome involved composition of semilinear maps, and symm for linear equivalences: having things like σ₂₃.comp σ₁₂ in the types of semilinear maps creates major problems. For example, we want the composition of two conjugate-linear maps to be a regular linear map, not a conj.comp conj-linear map. To solve this issue, following a discussion from back in January, we created two typeclasses to make Lean infer the right ring hom. The first one is [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] which expresses the fact that σ₂₃.comp σ₁₂ = σ₁₃, and the second one is [ring_hom_inv_pair σ₁₂ σ₂₁] which states that σ₁₂ and σ₂₁ are inverses of each other. There is also [ring_hom_surjective σ], which is a necessary assumption to generalize some basic lemmas (such as submodule.map). Note that we have introduced notation to ensure that regular linear maps can still be used as before, i.e. M →ₗ[R] N still works as before to mean a regular linear map.

The main changes are in algebra/module/linear_map.lean, data/equiv/module.lean and linear_algebra/basic.lean (and algebra/ring/basic.lean for the ring_hom typeclasses). The changes in other files fall into the following categories:

1. When defining a regular linear map directly using the structure (i.e. when specifying to_fun, map_smul' and so on), there is a ring_hom.id that shows up in map_smul'. This mostly involves dsimping it away.
2. Elaboration seems slightly more brittle, and it fails a little bit more often than before. For example, when f is a linear map and g is something that can be coerced to a linear map (say a linear equiv), one has to write ↑g to make f.comp ↑g work, or sometimes even to add a type annotation. This also occurs when using trans twice (i.e. e₁.trans (e₂.trans e₃)). In those places, we use the notation defined in [Merged by Bors] - feat(linear_algebra): introduce notation for linear_map.comp and linear_equiv.trans #8857 ∘ₗ and ≪≫ₗ.
3. It seems to exacerbate the bug discussed here for reasons that we don't understand all that well right now. It manifests itself in very slow calls to the tactic ext, and the quick fix is to manually use the right ext lemma.
4. The PR triggered a few timeouts in proofs that were already close to the edge. Those were sped up.
5. A few random other issues that didn't arise often enough to see a pattern.

Co-authored-by: @hrmacbeth @robertylewis

---

[sgouezel]

That's an amazing work! It looks globally very nice to me. I am just a little bit afraid that you have changed liberally a lot of simp only to simp, which might be significantly slower. And a few minor comments. But given how little it breaks, this clearly looks like a very good move to me!

Also, it might be worth expanding significantly one of the file-level docstrings on the design, mentioning in particular out_params and what instances you choose to include.

[bryangingechen]

(I've moved most of the PR comment "above the line" so that it will be included in the final commit message - the info is valuable and a detailed explanation is totally appropriate for a PR like this.)

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests