[Merged by Bors] - feat(ring_theory/finiteness): generalize module.finite to noncommutative setting #9860
Conversation
riccardobrasca
added
the
awaiting-review
| lemma of_injective {R M N : Type*} [ring R] [add_comm_group M] [module R M] [add_comm_group N] | ||
| [module R N] [is_noetherian R N] (f : M →ₗ[R] N) |
There was a problem hiding this comment.
It would be straightforward to make this only require semiring R, as far as I can tell the proof just rewrites ker f = \bot back into function.injective f inside fg_of_injective
There was a problem hiding this comment.
linear_map.ker_eq_bot.2 can be replaced by linear_map.ker_eq_bot_of_injective, that works for semiring, but fg_of_injective is for ring. Let me see if it easy to generalize.
There was a problem hiding this comment.
Mmm, this is annoying: fg_of_injective does not have function.injective f as assumption, it has f.ker = ⊥, so I think it is true only over ring. But with function.injective f it would be true over semiring, and over rings f.ker = ⊥ implies function.injective f. I can change fg_of_injective, but it is better to do it in another PR.
There was a problem hiding this comment.
I'm happy to leave that as a follow-up for when (if?) it is needed in the future.
There was a problem hiding this comment.
Yes, the other half of my suggestion is to change fg_of_injective to assume function.injective f. I don't feel strongly about whether this is part of this PR, but I think it would be straightforward.
There was a problem hiding this comment.
I agree it's straightforward, but then a modification will be needed everywhere it is used (a trivial one of course, but maybe in a lot of places). I am trying. If it is in a couple of files I will do it in this PR.
There was a problem hiding this comment.
It's not reasonable to do it here. ring_theory/noetherian can be generalized to semiring at lot, but even if almost all results trivially generalize, there is some work to do for others. I would say this is a job, if needed, for another PR.
There was a problem hiding this comment.
LGTM. I'll let @eric-wieser have the final decision whether the changes to noetherian.lean should be included.
|
I am opening another PR, depending on this one, to fix the problem. |
|
bors merge Thanks! |
github-actions
bot
added
ready-to-merge
…ive setting (#9860) An almost for free generalization of `module.finite` to `semiring`.
bryangingechen
changed the title
|
This was merged, but bors crashed. |
We generalize some of the results in `ring_theory/noetherian` to `semiring`. - [x] depends on: #9860 Co-authored-by: Johan Commelin <johan@commelin.net>
…l using module.finite (#9854) `finite_dimensional K V` is by definition `is_noetherian K V`. We refactor this to use everywhere `finite K V` instead. To keep the PR reasonably small, we don't delete `finite_dimension`, but we define it as `module.finite`. In a future PR we will remove it. - [x] depends on: #9860
eric-wieser
added
the
hacktoberfest-accepted
…ive setting (#9860) An almost for free generalization of `module.finite` to `semiring`.
We generalize some of the results in `ring_theory/noetherian` to `semiring`. - [x] depends on: #9860 Co-authored-by: Johan Commelin <johan@commelin.net>
…l using module.finite (#9854) `finite_dimensional K V` is by definition `is_noetherian K V`. We refactor this to use everywhere `finite K V` instead. To keep the PR reasonably small, we don't delete `finite_dimension`, but we define it as `module.finite`. In a future PR we will remove it. - [x] depends on: #9860
An almost for free generalization of
module.finitetosemiring.