-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - [Merged by Bors] - feat(ring_theory/finiteness): prove that a surjective endomorphism of a finite module over a comm ring is injective #10944
Conversation
… a finite module over a comm ring is injective
src/ring_theory/finiteness.lean
Outdated
obtain ⟨y, rfl⟩ := f_surj a, | ||
rw [← X_mul y], | ||
exact submodule.smul_mem_smul (ideal.mem_span_singleton.mpr (dvd_refl _)) trivial, }, | ||
haveI : is_scalar_tower R (polynomial R) M := ⟨λ x y z, by simp⟩, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it would be good to have this as a lemma after module_polynomial_ring_endo
. Just to indicate it as a natural API piece. I would also move this haveI
to directly after the letI
that introduces the module structure.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah the issue is I'm not really sure how to state this properly as a lemma.
The type depends on the typeclases inferred, and this depends on f, I've pushed by best attempt but its quite unsatisfying as a lemma to me. Maybe its ok though.
Thanks 🎉 bors merge |
Pull request successfully merged into master. Build succeeded: |
Pull request successfully merged into master. Build succeeded: |
Using an approach of Vasconcelos, treating the module as a module over the polynomial ring, with action induced by the endomorphism.
This result was rescued from #1822.
I'm not sure of the best location for
module_polynomial_ring_endo
/ whether we want more lemmata for it, I only needed the autognerated simp lemams