Curved left modules as right modules over the graded opposite

A graded left module over an internally graded algebra A is a right module over the Koszul-signed graded opposite of A, with x * op a = (-1) ^ (|a| * |x|) • (a • x) (TauCeti.GradedOpposite.leftToRightModule). For a curved differential graded algebra (A, d, w) the graded opposite is a curved differential graded algebra of curvature -op w (TauCeti.IsCurvedDGAlgebra.gradedOpposite). This file proves that the curved differential graded left modules over A are exactly the curved differential graded right modules over this graded opposite, on the same graded module and with the same differential.

The curvature is even, so it acts through the graded opposite without a Koszul sign, and the right-module square dM (dM x) = x * (-op w) over the opposite reads dM (dM x) = -(w • x). Thus a left module does not satisfy the right-module square w • x: the sign is the one recorded in TauCeti.IsCurvedDGLeftModule.

Main results

• TauCeti.isCurvedDGLeftModule_iff_gradedOppositeRight: a differential makes a graded left module a curved differential graded left module exactly when it makes it a curved differential graded right module over the graded opposite.
• TauCeti.IsCurvedDGLeftModule.gradedOppositeRight: the forward direction, for dot notation.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 6.2.
• B. Keller, Deriving DG categories, Section 1, for the Koszul-signed opposite.

theorem TauCeti.isCurvedDGLeftModule_iff_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} {w : A} {h : IsCurvedDGAlgebra G.piece d w} {dM : M →ₗ[R] M} : IsCurvedDGLeftModule h H.piece dM ↔ IsCurvedDGRightModule ⋯ H.piece dM

Curved left modules through the graded opposite. A differential dM makes the graded left module M a curved differential graded left module over (A, d, w) exactly when it makes M, with the transported action GradedOpposite.leftToRightModule, a curved differential graded right module over the graded opposite, of curvature -op w. The right-module square dM (dM x) = x * (-op w) over the opposite is the left-module square dM (dM x) = -(w • x).

theorem TauCeti.IsCurvedDGLeftModule.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} {w : A} {h : IsCurvedDGAlgebra G.piece d w} {dM : M →ₗ[R] M} (hM : IsCurvedDGLeftModule h H.piece dM) : IsCurvedDGRightModule ⋯ H.piece dM

A curved differential graded left module over (A, d, w) is a curved differential graded right module over the Koszul-signed graded opposite, of curvature -op w, with action GradedOpposite.leftToRightModule.