[Merged by Bors] - feat(linear_algebra/free_module): add lemmas #7950
Conversation
riccardobrasca
added
the
awaiting-review
|
|
||
| lemma linear_independent_std_basis [decidable_eq η] | ||
| (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) : | ||
| lemma linear_independent_std_basis [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)] |
There was a problem hiding this comment.
This file is essentially the same as before, i just generalized it to semiring, except linear_independent_std_basis that does not work. I didn't touch any proof.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…hlib into free_mod_lemmas
|
|
||
| /-- The direct sum of free modules is free. | ||
|
|
||
| Note that while this is stated for `dfinsupp` not `direct_sum`, the types are defeq. -/ |
There was a problem hiding this comment.
Do you know why we have module instances for both dfinsupp and direct_sum? Should the second one become notation perhaps?
There was a problem hiding this comment.
My mental model is that finsupp is to dfinsupp as monoid_algebra is to direct_sum.
There was a problem hiding this comment.
No idea why direct_sum is a def rather than notation, but I was indeed slightly confused by this the first time I saw it.
There was a problem hiding this comment.
The way I understand monoid_algebra is as a type synonym for finsupp that chooses * to be the convolution product (rather than the pointwise product). But the direct sum of modules doesn't have a product, right?
There was a problem hiding this comment.
Mathematically they work in different categories, monoid_algebra is the left/right (I always forget) adjoint to the forgetful functor algebras → monoids, so it is like free modules (that is the adjoint to the forgetful modules → sets). The direct sum is the coproduct in R-mod, and the analogue for algebras is tensor product.
There was a problem hiding this comment.
But the direct sum of modules doesn't have a product, right?
If those modules are submodules of the same algebra, then direct_sum.ring provides a convolutional product mirroring monoid_algebra via direct_sum.gmonoid.of_submodules
|
✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
bors r+ |
Easy results about free modules.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Easy results about free modules.