Curved differential graded right modules #
A curved differential graded right module over a curved differential graded algebra has a degree-one differential satisfying the graded Leibniz rule
dM (x * a) = dM x * a + (-1) ^ |x| * (x * d a)
and the curvature equation dM (dM x) = x * w. The latter replaces the square-zero axiom of an
ordinary differential graded module. The algebra curvature convention
d (d a) = a * w - w * a is exactly the one compatible with this right-module equation.
In Lean, a right A-module is represented as a left module over Aᵐᵒᵖ, so x * a is written
MulOpposite.op a • x. The grading on Aᵐᵒᵖ is transported from the internal grading of A;
the module action itself has no extra sign.
Unlike ordinary differential graded modules, curved modules do not generally have cohomology: the image of their differential need not lie in its kernel. The zero-curvature comparison below therefore returns the existing ordinary DG-module structure before any cohomology is formed.
Main definitions #
TauCeti.IsCurvedDGRightModule: the curved differential graded right-module axioms.TauCeti.CurvedDGRightModuleCat: bundled curved differential graded right modules, the objects of the differential graded category of curved modules.
Main results #
TauCeti.IsCurvedDGRightModule.map_decompose: the differential commutes with homogeneous projections up to its degree-one shift.TauCeti.IsCurvedDGRightModule.leibniz_of_map_eq_zero: cycles of the algebra act compatibly with the module differential, without a homogeneity assumption on the module element.TauCeti.IsCurvedDGRightModule.toIsDGRightModule_of_curvature_eq_zero: zero curvature turns a curved right module into an ordinary differential graded right module.TauCeti.isCurvedDGRightModule_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.
A curved differential graded right module over the curved differential graded algebra
(𝒜, d, w). Its differential raises degree by one, obeys the right graded Leibniz rule, and
squares to right multiplication by the curvature.
- isHomogeneous : LinearMap.IsHomogeneous dM ℳ ℳ 1
The differential raises degree by one.
- leibniz {q : ℤ} {x : M} : x ∈ ℳ q → ∀ (a : A), dM (MulOpposite.op a • x) = MulOpposite.op a • dM x + q.negOnePow • MulOpposite.op (d a) • x
The graded right Leibniz rule for a module element of degree
q. The differential squares to right multiplication by the curvature.
Instances For
The differential of a curved differential graded right module commutes with homogeneous projections, up to its degree-one shift.
The right Leibniz rule against a cycle of the algebra. The signed term vanishes, so the module element need not be homogeneous.
The curvature action commutes with the module differential.
A curved differential graded right module whose curvature is zero is an ordinary differential graded right module.
An ordinary differential graded right module is a curved one with curvature zero.
Zero curvature. Curved differential graded right modules over an algebra of curvature zero are exactly ordinary differential graded right modules.
Bundled curved modules #
A bundled curved differential graded right module over the curved differential graded
algebra h.
- carrier : Type uM
The underlying module.
- addCommGroup : AddCommGroup self.carrier
- scalarTower : IsScalarTower R Aᵐᵒᵖ self.carrier
The internal grading of the module.
- decomposition : DirectSum.Decomposition self.grading
- gradedSMul : SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece self.grading
The module differential.
- isCurvedDGRightModule : IsCurvedDGRightModule h self.grading self.differential
The differential and action satisfy the curved DG right-module laws.
Instances For
Bundle a curved differential graded right module with its existing structures.
Equations
- One or more equations did not get rendered due to their size.