mathlib

a9cd8c25 - feat(linear_algebra): redefine `linear_map` and `linear_equiv` to be semilinear (#9272)

feat(linear_algebra): redefine `linear_map` and `linear_equiv` to be semilinear (#9272) 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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Semilinear.20maps), 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 #8857 `∘ₗ` and `≪≫ₗ`. 3. It seems to exacerbate the bug discussed [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/odd.20repeated.20type.20class.20search) 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 Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com> Co-authored-by: Scott Morrison <scott@tqft.net>