Mathlib v3 is deprecated. Go to Mathlib v4

Commit2021-09-24 06:10a9cd8c25

View on Github →

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.

Estimated changes

modified theorem linear_map.coe_comp
modified theorem linear_map.coe_injective
modified def linear_map.comp
modified theorem linear_map.comp_apply
modified theorem linear_map.ext_ring
modified theorem linear_map.ext_ring_iff
modified def linear_map.inverse
modified theorem linear_map.is_linear
modified theorem linear_map.map_smul
modified theorem linear_map.mk_coe
modified structure linear_map
modified theorem finsupp.smul_sum
modified theorem linear_equiv.coe_zero
modified theorem linear_equiv.ker_comp
modified theorem linear_equiv.map_eq_comap
modified theorem linear_equiv.range_comp
modified theorem linear_equiv.zero_apply
modified theorem linear_equiv.zero_symm
modified theorem linear_map.coe_dfinsupp_sum
modified theorem linear_map.coe_finsupp_sum
modified theorem linear_map.coe_fn_sum
modified theorem linear_map.coe_smul_right
modified theorem linear_map.comap_injective
modified theorem linear_map.comp_assoc
modified theorem linear_map.comp_ker_subtype
modified theorem linear_map.comp_neg
modified theorem linear_map.comp_sub
modified theorem linear_map.comp_zero
modified theorem linear_map.default_def
modified theorem linear_map.disjoint_ker
modified theorem linear_map.eq_on_span'
modified theorem linear_map.eq_on_span
modified theorem linear_map.ext_on
modified theorem linear_map.ext_on_range
modified def linear_map.ker
modified theorem linear_map.ker_cod_restrict
modified theorem linear_map.ker_comp
modified theorem linear_map.ker_eq_bot'
modified theorem linear_map.ker_eq_top
modified theorem linear_map.ker_le_iff
modified theorem linear_map.ker_le_ker_comp
modified theorem linear_map.ker_le_range_iff
modified theorem linear_map.ker_zero
modified theorem linear_map.le_ker_iff_map
modified theorem linear_map.map_cod_restrict
modified theorem linear_map.map_coe_ker
modified theorem linear_map.map_dfinsupp_sum
modified theorem linear_map.map_eq_top_iff
modified theorem linear_map.map_finsupp_sum
modified theorem linear_map.map_injective
modified theorem linear_map.map_le_map_iff'
modified theorem linear_map.map_le_map_iff
modified theorem linear_map.map_le_range
modified theorem linear_map.mem_ker
modified theorem linear_map.mem_range
modified theorem linear_map.mem_range_self
modified def linear_map.range
modified theorem linear_map.range_coe
modified theorem linear_map.range_comp
modified theorem linear_map.range_eq_bot
modified theorem linear_map.range_eq_map
modified theorem linear_map.range_eq_top
modified theorem linear_map.range_le_bot_iff
modified theorem linear_map.range_le_ker_iff
modified theorem linear_map.range_mkq_comp
modified theorem linear_map.range_zero
modified def linear_map.smul_right
modified theorem linear_map.smul_right_apply
modified theorem linear_map.sub_comp
modified theorem linear_map.sum_apply
modified theorem linear_map.zero_apply
modified theorem linear_map.zero_comp
modified theorem pi_eq_sum_univ
modified theorem submodule.apply_coe_mem_map
modified def submodule.comap
modified theorem submodule.comap_bot
modified theorem submodule.comap_coe
modified theorem submodule.comap_comp
modified theorem submodule.comap_inf
modified theorem submodule.comap_infi
modified theorem submodule.comap_liftq
modified theorem submodule.comap_map_eq
modified theorem submodule.comap_map_eq_self
modified theorem submodule.comap_mono
modified theorem submodule.comap_top
modified theorem submodule.comap_zero
modified theorem submodule.gc_map_comap
modified theorem submodule.ker_liftq
modified theorem submodule.ker_liftq_eq_bot
modified theorem submodule.le_comap_map
modified def submodule.liftq
modified theorem submodule.liftq_apply
modified theorem submodule.liftq_mkq
modified theorem submodule.linear_map_qext
modified def submodule.map
modified theorem submodule.map_bot
modified theorem submodule.map_coe
modified theorem submodule.map_comap_eq
modified theorem submodule.map_comap_eq_self
modified theorem submodule.map_comap_le
modified theorem submodule.map_comp
modified theorem submodule.map_id
modified theorem submodule.map_liftq
modified theorem submodule.map_mono
modified theorem submodule.map_span
modified theorem submodule.map_sup
modified theorem submodule.map_supr
modified theorem submodule.map_top
modified theorem submodule.map_zero
modified def submodule.mapq
modified theorem submodule.mapq_apply
modified def submodule.mapq_linear
modified theorem submodule.mapq_mkq
modified theorem submodule.mem_comap
modified theorem submodule.mem_map
modified theorem submodule.mem_map_equiv
modified theorem submodule.mem_map_of_mem
modified theorem submodule.mem_prod
modified theorem submodule.mem_supr
modified theorem submodule.mem_supr_of_chain
modified def submodule.prod
modified theorem submodule.prod_bot
modified theorem submodule.prod_inf_prod
modified theorem submodule.prod_mono
modified theorem submodule.prod_sup_prod
modified theorem submodule.prod_top
modified theorem submodule.range_liftq
modified theorem submodule.span_image
modified theorem submodule.span_preimage_eq
modified theorem submodule.span_preimage_le
modified theorem submodule.span_prod_le
modified theorem submodule.supr_eq_span