Commit 2018-11-05 10:47 a12d5a19

feat(linear_algebra,ring_theory): refactoring modules (#456) Co-authored with Kenny Lau. See also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20refactoring for discussion. Major changes made:

• semimodule α β and module α β and vector_space α β now take one more argument, that β is an add_comm_group, i.e. before making an instance of a module, you need to prove that it's an abelian group first.
• vector space is no longer over a field, but a discrete field.
• The idiom for making an instance module α β (after proving that β is an abelian group) is module.of_core { smul := sorry, smul_add := sorry, add_smul := sorry, mul_smul := sorry, one_smul := sorry }.
• is_linear_map and linear_map are now both structures, and they are independent, meaning that linear_map is no longer defined as subtype is_linear_map. The idiom for making linear_map from is_linear_map is is_linear_map.mk' (f : M -> N) (sorry : is_linear_map f), and the idiom for making is_linear_map from linear_map is f.is_linear (i.e. linear_map.is_linear f).
• is_linear_map.add etc no longer exist. instead, you can now add two linear maps together, etc.
• the classis_submodule is gone, replaced by the structure submodule which contains a carrier, i.e. if N : submodule R M then N.carrier is a type. And there is an instance module R N in the same situation.
• similarly, the class is_ideal is gone, replaced by the structure ideal, which also contains a carrier.
• endomorphism ring and general linear group are defined.
• submodules form a complete lattice. the trivial ideal is now idiomatically the bottom element, and the universal ideal the top element.
• linear_algebra/quotient_module.lean is deleted, and it's now submodule.quotient (so if N : submodule R M then submodule R N.quotient) Similarly, quotient_ring.quotient is replaced by ideal.quotient. The canonical map from N to N.quotient is submodule.quotient.mk, and the canonical map from the ideal I to I.quotient is ideal.quotient.mk I.
• linear_equiv is now based on a linear map and an equiv, and the difference being that now you need to prove that the inverse is also linear, and there is currently no interface to get around that.
• Everything you want to know about linear independence and basis is now in the newly created file linear_algebra/basis.lean.
• Everything you want to know about linear combinations is now in the newly created file linear_algebra/lc.lean.
• linear_algebra/linear_map_module.lean and linear_algebra/prod_module.lean and linear_algebra/quotient_module.lean and linear_algebra/submodule.lean and linear_algebra/subtype_module.lean are deleted (with their contents placed elsewhere). squashed commits:

• feat(linear_algebra/basic): product modules, cat/lat structure
• feat(linear_algebra/basic): refactoring quotient_module
• feat(linear_algebra/basic): merge in submodule.lean
• feat(linear_algebra/basic): merge in linear_map_module.lean
• refactor(linear_algebra/dimension): update for new modules
• feat(ring_theory/ideals): convert ideals
• refactor tensor product
• simplify local ring proof for Zp
• refactor(ring_theory/noetherian)
• refactor(ring_theory/localization)
• refactor(linear_algebra/tensor_product)
• feat(data/polynomial): lcoeff