Graded left 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).

The construction applies to additive commutative monoids and preserves both the ground-ring scalar tower and the module grading.

Main definitions

• GradedOpposite.leftToRightModule: the right action of the graded opposite associated to a graded left module.

Main results

• GradedOpposite.leftToRight_smul_of_mem: the action on homogeneous elements is the Koszul-signed original left action.
• GradedOpposite.leftToRight_smul_of_mem_of_even: a homogeneous scalar of even degree acts by the original left action, with no sign.
• GradedOpposite.leftToRight_isScalarTower and GradedOpposite.leftToRight_gradedSMul: compatibility with the ground-ring action and the module grading.
• GradedOpposite.leftToRight_leibniz_iff: a differential satisfies the right graded Leibniz rule for the transported action exactly when it satisfies the left graded Leibniz rule.

The sign convention follows B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.

@[instance_reducible]

noncomputable def TauCeti.GradedOpposite.leftToRightModule {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] (G : InternalGrading R A) (H : InternalGrading R M) : Module (GradedOpposite G)ᵐᵒᵖ M

The right action of the graded opposite associated to a graded left A-module.

It is obtained by restricting scalars along (GradedOpposite G)ᵐᵒᵖ ≃ₐ[R] A and conjugating the result by the quadratic twist of the module grading.

Equations

• TauCeti.GradedOpposite.leftToRightModule G H = AddEquiv.module (TauCeti.GradedOpposite G)ᵐᵒᵖ H.quadraticTwistEquiv.toAddEquiv

@[simp]

theorem TauCeti.GradedOpposite.leftToRight_smul {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] (G : InternalGrading R A) (H : InternalGrading R M) (s : (GradedOpposite G)ᵐᵒᵖ) (x : M) : s • x = H.quadraticTwist ((opAlgEquiv G) s • H.quadraticTwist x)

The graded-opposite action is conjugation of scalar restriction by the quadratic twist.

theorem TauCeti.GradedOpposite.leftToRight_isScalarTower {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (G : InternalGrading R A) (H : InternalGrading R M) : IsScalarTower R (GradedOpposite G)ᵐᵒᵖ M

The ground-ring action commutes with the transported graded-opposite action.

theorem TauCeti.GradedOpposite.leftToRight_smul_of_mem {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (G : InternalGrading R A) (H : InternalGrading R M) [SetLike.GradedSMul G.piece H.piece] {p q : ℤ} {a : A} (ha : a ∈ G.piece p) {x : M} (hx : x ∈ H.piece q) : MulOpposite.op (op G a) • x = ↑↑(p * q).negOnePow • a • x

A homogeneous scalar of degree p acts on a homogeneous module element of degree q by the original left action multiplied by the Koszul sign (-1) ^ (p * q).

theorem TauCeti.GradedOpposite.leftToRight_smul_of_mem_of_even {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (G : InternalGrading R A) (H : InternalGrading R M) [SetLike.GradedSMul G.piece H.piece] {p : ℤ} {a : A} (ha : a ∈ G.piece p) (hp : Even p) (x : M) : MulOpposite.op (op G a) • x = a • x

A homogeneous scalar of even degree acts through the graded opposite by the original left action, on every module element: the Koszul sign (-1) ^ (p * q) is trivial on each homogeneous component.

theorem TauCeti.GradedOpposite.leftToRight_gradedSMul {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (G : InternalGrading R A) (H : InternalGrading R M) [SetLike.GradedSMul G.piece H.piece] : SetLike.GradedSMul (InternalGrading.ofDecomposition (grading G).piece).opposite.piece H.piece

The transported graded-opposite action adds the scalar degree to the module degree.

Differentials

A linear endomorphism dM of a graded left module satisfies the left graded Leibniz rule dM (a • x) = d a • x + (-1) ^ |a| • (a • dM x) exactly when it satisfies the right graded Leibniz rule dM (x * b) = dM x * b + (-1) ^ |x| • (x * d b) for the transported action of the graded opposite. Only the degree laws of d and dM are used, so the comparison serves differential graded and curved differential graded modules alike; the square-zero and curvature laws are added by their respective theories.

theorem TauCeti.GradedOpposite.leftToRight_leibniz_iff {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) [SetLike.GradedSMul G.piece H.piece] {d : A →ₗ[R] A} {dM : M →ₗ[R] M} (hd : ∀ {p : ℤ} {a : A}, a ∈ G.piece p → d a ∈ G.piece (p + 1)) (hdM : ∀ {q : ℤ} {x : M}, x ∈ H.piece q → dM x ∈ H.piece (q + 1)) : (∀ {q : ℤ} {x : M}, x ∈ H.piece q → ∀ (b : GradedOpposite G), dM (MulOpposite.op b • x) = MulOpposite.op b • dM x + q.negOnePow • MulOpposite.op ((differential G d) b) • x) ↔ ∀ {p : ℤ} {a : A}, a ∈ G.piece p → ∀ (x : M), dM (a • x) = d a • x + p.negOnePow • a • dM x

Left and right graded Leibniz rules. For degree-raising d and dM, the differential dM satisfies the right graded Leibniz rule for the action of the graded opposite transported by leftToRightModule, on homogeneous module elements and arbitrary scalars, exactly when it satisfies the left graded Leibniz rule on homogeneous scalars and arbitrary module elements.