Left DG modules as right modules over the graded opposite #
A left module over an internally graded algebra A determines a right module over the
Koszul-signed graded opposite of A. On homogeneous elements of degrees p and q, the action
is
x * op(a) = (-1) ^ (p * q) • (a • x).
With this action, a DG left module becomes a DG right module over the graded-opposite DG algebra. Its differential obeys the right Leibniz rule with sign determined by the degree of the module element, for arbitrary algebra elements.
Main results #
IsDGLeftModule.gradedOppositeRight: a DG left module is a DG right module over the Koszul-signed graded opposite.
References #
- B. Keller, Deriving DG categories, Section 1.
- B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.
theorem
TauCeti.IsDGLeftModule.gradedOppositeRight
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module A M]
[IsScalarTower R A M]
{G : InternalGrading R A}
{H : InternalGrading R M}
[GradedAlgebra G.piece]
[SetLike.GradedSMul G.piece H.piece]
{d : A →ₗ[R] A}
{hA : IsDGAlgebra G.piece d}
{dM : M →ₗ[R] M}
(hM : IsDGLeftModule hA H.piece dM)
:
IsDGRightModule ⋯ H.piece dM
A differential graded left module over A is a differential graded right module over the
Koszul-signed graded opposite of A, with action GradedOpposite.leftToRightModule.