Commit 2021-09-24 06:10 a9cd8c25

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.add_apply
modified theorem linear_map.add_comp
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_add
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_add_le
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