Theorems · Inductive type · commutative algebra

PolynomialModule

(R : Type u_1) → (M : Type u_2) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Type u_2

The R[X]-module M[X] for an R-module M. This is isomorphic (as an R-module) to M[X] when M is a ring. We require all the module instances Module S (PolynomialModule R M) to factor through R except Module R[X] (PolynomialModule R M). In this constraint, we have the following instances for example : - R acts on PolynomialModule R R[X] - R[X] acts on PolynomialModule R R[X] as R[Y] acting on R[X][Y] - R acts on PolynomialModule R[X] R[X] - R[X] acts on PolynomialModule R[X] R[X] as R[X] acting on R[X][Y] - R[X][X] acts on PolynomialModule R[X] R[X] as R[X][Y] acting on itself This is also the reason why R is included in the alias, or else there will be two different instances of Module R[X] (PolynomialModule R[X]). See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315065.20polynomial.20modules for the full discussion.

Defined in

Mathlib.Algebra.Polynomial.Module.Basic

Cited by

76 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingAddCommGroupModule