Commit 2021-09-24 06:10 a9cd8c25View on Github →
linear_equiv to be semilinear (#9272)
This PR redefines
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
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
σ₂₁ 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/ring/basic.lean for the
ring_hom typeclasses). The changes in other files fall into the following categories:
- When defining a regular linear map directly using the structure (i.e. when specifying
map_smul'and so on), there is a
ring_hom.idthat shows up in
map_smul'. This mostly involves dsimping it away.
- Elaboration seems slightly more brittle, and it fails a little bit more often than before. For example, when
fis a linear map and
gis something that can be coerced to a linear map (say a linear equiv), one has to write
f.comp ↑gwork, or sometimes even to add a type annotation. This also occurs when using
e₁.trans (e₂.trans e₃)). In those places, we use the notation defined in #8857
- 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.
- The PR triggered a few timeouts in proofs that were already close to the edge. Those were sped up.
- A few random other issues that didn't arise often enough to see a pattern.