Curved differential graded left modules

A curved differential graded left module over a curved differential graded algebra (A, d, w) has a degree-one differential satisfying the graded Leibniz rule

dM (a • x) = d a • x + (-1) ^ |a| • (a • dM x)

and the curvature equation dM (dM x) = -(w • x).

The curvature w is stored in the right-module convention d (d a) = a * w - w * a, under which a right curved module satisfies dM (dM x) = x * w. A left module is the same thing as a right module over the Koszul-signed graded opposite, whose curvature is -op w; reading the right-module square there gives the left-module square -(w • x), not w • x. This comparison is TauCeti.isCurvedDGLeftModule_iff_gradedOppositeRight. In Positselski's convention, with curvature h = -w, the left-module equation is his d² (m) = h * m.

Main definitions

• TauCeti.IsCurvedDGLeftModule: the curved differential graded left-module axioms.

Main results

• TauCeti.IsCurvedDGLeftModule.map_curvature_smul: the curvature action commutes with the module differential.
• TauCeti.IsCurvedDGLeftModule.toIsDGLeftModule_of_curvature_eq_zero: zero curvature turns a curved left module into an ordinary differential graded left module.
• TauCeti.isCurvedDGLeftModule_zero_iff: the curved and ordinary notions agree at curvature zero.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 6.2. His curvature is the negative of the right-module curvature used here.

structure TauCeti.IsCurvedDGLeftModule {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} [IsScalarTower R A M] (h : IsCurvedDGAlgebra 𝒜 d w) (ℳ : ℤ → Submodule R M) [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ] (dM : M →ₗ[R] M) : Prop

A curved differential graded left module over the curved differential graded algebra (𝒜, d, w). Its differential raises degree by one, obeys the left graded Leibniz rule, and squares to minus left multiplication by the curvature: the curvature w is stored in the right-module convention, and the left-module square carries the opposite sign.

• isHomogeneous : LinearMap.IsHomogeneous dM ℳ ℳ 1

  The differential raises degree by one.

• leibniz {p : ℤ} {a : A} : a ∈ 𝒜 p → ∀ (x : M), dM (a • x) = d a • x + p.negOnePow • a • dM x

  The graded left Leibniz rule for a scalar of degree p.

• sq_eq (x : M) : dM (dM x) = -(w • x)

  The differential squares to minus left multiplication by the curvature.

@[simp]

theorem TauCeti.IsCurvedDGLeftModule.map_decompose {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] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} (hM : IsCurvedDGLeftModule h ℳ dM) (p : ℤ) (x : M) : dM ↑(((DirectSum.decompose ℳ) x) p) = ↑(((DirectSum.decompose ℳ) (dM x)) (p + 1))

The differential of a curved differential graded left module commutes with homogeneous projections, up to its degree-one shift.

theorem TauCeti.IsCurvedDGLeftModule.leibniz_of_map_eq_zero {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] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} (hM : IsCurvedDGLeftModule h ℳ dM) (a : A) {x : M} (hx : dM x = 0) : dM (a • x) = d a • x

The left Leibniz rule against a module element killed by the differential. The signed term vanishes, so the scalar need not be homogeneous.

theorem TauCeti.IsCurvedDGLeftModule.map_curvature_smul {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] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} (hM : IsCurvedDGLeftModule h ℳ dM) (x : M) : dM (w • x) = w • dM x

The curvature action commutes with the module differential: the curvature is a cycle of even degree.

theorem TauCeti.IsCurvedDGLeftModule.toIsDGLeftModule_of_curvature_eq_zero {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] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} (hM : IsCurvedDGLeftModule h ℳ dM) (hw : w = 0) : IsDGLeftModule ⋯ ℳ dM

A curved differential graded left module whose curvature is zero is an ordinary differential graded left module.

theorem TauCeti.IsDGLeftModule.isCurvedDGLeftModule_zero {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] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} {hDG : IsDGAlgebra 𝒜 d} (hM : IsDGLeftModule hDG ℳ dM) : IsCurvedDGLeftModule ⋯ ℳ dM

An ordinary differential graded left module is a curved one with curvature zero.

theorem TauCeti.isCurvedDGLeftModule_zero_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] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {ℳ : ℤ → Submodule R M} [SetLike.GradedSMul 𝒜 ℳ] [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} {hDG : IsDGAlgebra 𝒜 d} : IsCurvedDGLeftModule ⋯ ℳ dM ↔ IsDGLeftModule hDG ℳ dM

Zero curvature. Curved differential graded left modules over an algebra of curvature zero are exactly ordinary differential graded left modules.