# Commit 2018-11-05 10:47 a12d5a19

View on Github →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 class
`is_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