mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/module/polynomial): Modules over `R[X]`

Open pbazin opened this issue 3 years ago • 4 comments

A R[X]-module is a R-module with the additional data of a R-linear endomorphism, describing the action of X.

Open in Gitpod

pbazin avatar Jun 10 '22 10:06 pbazin

I added a similar construction in #10944, it would be good to de-duplicate that material, and write that proof in terms of your new construction I think

alexjbest avatar Jun 10 '22 14:06 alexjbest

This feels like it likely overlaps with the representation theory stuff too

eric-wieser avatar Jun 11 '22 01:06 eric-wieser

This feels like it likely overlaps with the representation theory stuff too

Well module_with_End E can indeed also be viewed as a representation R (multiplicative ℕ) M (with E being the action of of_add 1). The representation stuff then gives a module (monoid_algebra R $ multiplicative ℕ) (module_with_End E), which is indeed the same structure as the module R[X] (module_with_End E) modulo the natural isomorphism (monoid_algebra R $ multiplicative ℕ) ≃ₐ[R] R[X]. However, I'm not sure if it's easier to implement it this way.

pbazin avatar Jun 13 '22 16:06 pbazin

what's happening here ?

pbazin avatar Jun 29 '22 09:06 pbazin