Commit 2021-09-24 06:10 a9cd8c25

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, 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 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.