Commit 2020-05-30 16:24 67f1951b

View on Github →

refactor(algebra/module): change module into an abbreviation for semimodule (#2848) The file algebra/module.lean contains the lines

There were several attempts to make `module` an abbreviation of `semimodule` but this makes
  class instance search too hard for Lean 3.

It turns out that this was too hard for Lean 3 until recently, but this is not too hard for Lean 3.14. This PR removes these two lines, and changes the files accordingly. This means that the basic objects of linear algebra are now semimodules over semiring, making it possible to talk about matrices with natural number coefficients or apply general results on multilinear maps to get the binomial or the multinomial formula. A linear map is now defined over semirings, between semimodules which are add_comm_monoids. For some statements, you need to have an add_comm_group, and a ring or a comm_semiring or a comm_ring. I have not tried to lower the possible typeclass assumptions like this in all files, but I have done it carefully in the following files:

  • algebra/module
  • linear_algebra/basic
  • linear_algebra/multilinear
  • topology/algebra/module
  • topology/algebra/multilinear Other files can be optimised later in the same way when needed, but this PR is already big enough. I have also fixed the breakage in all the other files. It was sometimes completely mysterious (in tensor products, I had to replace several times with linear_map.flip, but globally all right. I have tweaked a few instance priorities to make sure that things don't go too bad: there are often additional steps in typeclass inference, going from ring to semiring and from add_comm_group to add_comm_monoid, so I have increased their priority (putting it strictly between 100 and 1000), and adjusted some other priorities to get more canonical instance paths, fixing some preexisting weirdnesses (notably in multilinear maps). One place where I really had to help Lean is with normed spaces of continuous multilinear maps, where instance search is just too big. I am aware that this will be a nightmare to refer, but as often with big refactor it's an "all or nothing" PR, impossible to split in tiny pieces.

Estimated changes

modified theorem is_linear_map.map_neg
modified def
modified theorem linear_map.id_apply
modified theorem linear_map.map_sum
deleted structure module.core
modified theorem module.gsmul_eq_smul_cast
deleted def module.of_core
added def module
deleted def ring_hom.to_module
added structure semimodule.core
modified theorem smul_neg
modified theorem submodule.add_mem_iff_left
modified theorem submodule.add_mem_iff_right
modified theorem submodule.neg_mem_iff
modified structure submodule
modified def subspace
modified def vector_space