[Merged by Bors] - feat(Data/Polynomial/Module) : define an R[X] module, given a linear map.

[rmhi]

Given an element a in an R-algebra A and an A-module M,
define an R[X]-module Module.AEval R M a, whose elements correspond to
elements of M, and where the action of f : R[X] is f • m = aeval a f • m.
Equivalently, X • m = a • m.

This module is abbreviated to Module.AEval' φ in the special case that A is the algebra of R-linear maps and φ : M → M is an R-linear map.

This is needed in #7419.

---

[alexjbest]

This sounds like it has the same goal as https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/FiniteType.html#modulePolynomialOfEndo, this PR should redefine that material in terms of this I think. (I think using a type synonym is probably a nicer way to go, and it looks like you added more api here)

[riccardobrasca]

This sounds like it has the same goal as https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/FiniteType.html#modulePolynomialOfEndo, this PR should redefine that material in terms of this I think. (I think using a type synonym is probably a nicer way to go, and it looks like you added more api here)

Why is this in Mathlib.RingTheory.FiniteType?! Nice found BTW.

[alexjbest]

I think because its only used to prove the result below! But it really shouldn't be indeed

[alexjbest]

It took me a minute to work out how these proofs even work, I think using inferInstanceAs (AddCommMonoid M) is probably cleaner

[rmhi]

Thanks for showing me that; it is much clearer.

[rmhi]

This sounds like it has the same goal as https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/FiniteType.html#modulePolynomialOfEndo, this PR should redefine that material in terms of this I think. (I think using a type synonym is probably a nicer way to go, and it looks like you added more api here)

Thanks very much for that; I didn't think it was already in Mathlib. I'll try doing what you suggest.

[alexjbest]

I think it should still go in Polynomial/Module if that works though, just add an import to that from the finitetype file, as Riccardo says FiniteType is a non-obvious place for this construction to live

[rmhi]

I think it should still go in Polynomial/Module if that works though, just add an import to that from the finitetype file, as Riccardo says FiniteType is a non-obvious place for this construction to live

Thanks, I've switched that around now. I also needed to swap the imports, so that now FiniteType imports Polynomial/Module, whereas previously it was the other way around. I've moved my code to the start of Polynomial/Module, because it is now used later down that file. I have left Vasconcelos' theorem in FiniteType, but its proof now uses AEval' instead of ModulePolynomialOfEndo. This avoids the creation of instances at the start of the proof, and also a have statement, which is a lemma for AEval'.

[rmhi]

Many thanks for all you help!

[riccardobrasca]

Sorry again for the long review time, but this is very good now, thanks! (I've left a couple of trivial comments.)

bors d+

[bors]

✌️ rmhi can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[rmhi]

bors r+

[bors]

Canceled.

[rmhi]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style