Differential graded right modules #
A differential graded right module over an internally graded differential graded algebra has a degree-one, square-zero differential satisfying
dM (x * a) = dM x * a + (-1) ^ |x| * (x * d a)
for homogeneous x. In Lean a right A-module is represented as a left module over Aᵐᵒᵖ, so
the action x * a is written MulOpposite.op a • x. The source grading on Aᵐᵒᵖ is obtained by
transporting the grading of A along MulOpposite.op; no sign is inserted into the action itself.
The homogeneous Leibniz rule extends to useful statements on arbitrary elements. In particular, cycles act on cycles, cycles of the algebra preserve module boundaries, and differentials in the algebra act by boundaries on module cycles. These are the facts needed to make the cohomology of a right DG module into a right module over the cohomology algebra.
Main definitions #
TauCeti.IsDGRightModule: the differential graded right-module axioms on an internally graded module over a differential graded algebra.
Main results #
TauCeti.IsDGRightModule.leibniz_of_map_eq_zero: the Leibniz rule against an algebra cycle, without a homogeneity assumption on the module element.TauCeti.IsDGRightModule.op_smul_mem_range_of_map_eq_zero: an algebra cycle preserves module boundaries.TauCeti.IsDGRightModule.op_map_smul_mem_range_of_map_eq_zero: the differential of an algebra element acts by a boundary on a module cycle.TauCeti.isDGRightModule_zero: a graded right module with zero differential is a DG right module over a graded algebra with zero differential.TauCeti.IsDGAlgebra.isDGRightModule: a differential graded algebra is a differential graded right module over itself, the free rank-one right module.
References #
- B. Keller, Deriving DG categories, Sections 1 and 2.
- B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.
A differential graded right module over the differential graded algebra (𝒜, d). The
right action by a : A is written op a • x. The differential raises degree by one, squares to
zero, and obeys the right graded Leibniz rule on homogeneous module elements.
- isHomogeneous : LinearMap.IsHomogeneous dM ℳ ℳ 1
The differential raises the degree by one.
The differential squares to zero.
- 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.
Instances For
The differential of a differential graded right module commutes with homogeneous projections, up to the shift by one that it applies to degrees.
Every homogeneous projection of a boundary is again a boundary.
The homogeneous components of a cycle are cycles.
The right Leibniz rule against a cycle of the algebra. The sign disappears with the term it multiplies, so the module element need not be homogeneous.
A cycle of the algebra acts on a cycle of the right module to give a cycle.
A homogeneous module element multiplied by the differential of an algebra element is, up to the sign of its degree, the difference between the differential of the product and the product of the module differential.
A cycle of the algebra preserves boundaries of the right module.
The differential of an algebra element acts by a boundary on every cycle of the right module. The witness is assembled degreewise because the sign depends on the degree of the module element.
A differential graded algebra is a differential graded right module over itself, the free rank-one right module. Its Leibniz rule is the algebra Leibniz rule, whose sign is carried by the module element because that is the left-hand factor of the product.
A graded right module with zero differential over a graded algebra with zero differential is a differential graded right module.