The cohomology module of a differential graded left module #
Let dM be a differential on a module ℳ over the differential graded algebra (𝒜, d), in the
sense of TauCeti.IsDGLeftModule. Its cycles are the kernel of dM and its boundaries
are the image of dM. This file shows that the cycles are a module over the algebra of cycles
TauCeti.IsDGAlgebra.cycles of A, that the boundaries are a submodule of it, and that the
resulting quotient -- the cohomology module H(M) -- is a module over the cohomology algebra
H(A).
Both halves of the descent come from the Leibniz rule with one factor killed. A cycle of
A acting on a cycle of M gives a cycle, because the differential of a • x is d a • x as
soon as x is a cycle; a cycle of A acting on a boundary gives a boundary, because for a
homogeneous cycle a the Leibniz rule read backwards says a • dM x = (-1) ^ |a| * dM (a • x).
Finally a boundary of A acting on a cycle of M is a boundary, again because d a • x is
dM (a • x). The last statement says exactly that the boundary ideal of A annihilates H(M),
which is what descends the action along H(A) = cycles(A) / boundaries(A).
The cycles also inherit the grading: dM commutes with the homogeneous projections, so the
homogeneous components of a cycle are cycles, and the degree pieces of the cycles of M form an
internal direct sum on which the degree pieces of the cycles of A act additively in the degree.
Main definitions #
TauCeti.IsDGLeftModule.cycles: the kernel of the differential, as a module over the algebra of cycles ofA.TauCeti.IsDGLeftModule.cyclesDeg: the homogeneous cycles of a fixed degree.TauCeti.IsDGLeftModule.boundaries: the image of the differential, as a submodule of the cycles.TauCeti.IsDGLeftModule.Cohomology: the cohomology module, the cycles modulo the boundaries.
Main results #
TauCeti.IsDGLeftModule.iSup_cyclesDeg_eq_topandTauCeti.IsDGLeftModule.isInternal_cyclesDeg: every cycle is a sum of homogeneous ones, and the homogeneous cycles form an internal direct sum.TauCeti.IsDGLeftModule.instGradedSMulCyclesDeg: the cycles of a differential graded left module are a graded module over the graded algebra of cycles.TauCeti.IsDGLeftModule.isTorsionBySet_boundaries: the boundaries ofAannihilate the cohomology module.TauCeti.IsDGLeftModule.instModuleCohomology: the cohomology of a differential graded left module is a module over the cohomology algebra, withTauCeti.IsDGLeftModule.quotientMk_smulcomputing the action through a representing cycle.
This supplies for modules what TauCeti.Algebra.Homology.DG.Algebra.Cohomology supplies for
algebras. The descent of the action along the boundary ideal is Mathlib's
Module.IsTorsionBySet.module.
References #
- B. Keller, Deriving DG categories, Sections 1 and 2.
- B. Keller, Introduction to A-infinity algebras and modules, Sections 3.1 and 4.1.
The cycles of a differential graded left module: the kernel of the differential. It is a
module over the algebra of cycles of A because a cycle acting on a cycle is a cycle.
Instances For
The differential of every element is a cycle, by the square-zero axiom.
The boundaries of a differential graded left module: the image of the differential, viewed
inside the cycles. A cycle of A carries a boundary to a boundary, so this is a submodule over
the algebra of cycles.
Equations
- hM.boundaries = { toAddSubmonoid := AddSubmonoid.comap hM.cycles.subtype.toAddMonoidHom dM.range.toAddSubmonoid, smul_mem' := ⋯ }
Instances For
The cycle represented by a differential is a boundary.
The cohomology module H(M) of a differential graded left module: the cycles modulo the
boundaries.
Equations
- hM.Cohomology = (↥hM.cycles ⧸ hM.boundaries)
Instances For
A cohomology class vanishes exactly when the cycle representing it is a boundary.
The class of a differential vanishes in cohomology.
The boundaries of the algebra annihilate the cohomology module: a boundary d a carries a
cycle x to the boundary dM (a • x).
The cohomology of a differential graded left module is a module over the cohomology algebra.
The action of a cycle of A on a cycle of M descends, because the boundaries of A annihilate
the cohomology module.
Equations
- hM.instModuleCohomology = ⋯.module
The action of the cohomology algebra on the cohomology module is the action of a representing cycle.
The degree-p homogeneous cycles, as a submodule of the module of cycles.
Equations
- hM.cyclesDeg p = Submodule.comap (↑R hM.cycles.subtype) (ℳ p)
Instances For
The cycles are closed under every homogeneous projection of the ambient grading.
The cycles inherit the grading of the ambient differential graded left module.
Equations
- hM.instDecompositionCyclesDeg = TauCeti.DirectSum.Decomposition.restrict ℳ hM.cyclesDeg (↑R hM.cycles.subtype) ⋯ ⋯ ⋯
Every cycle is a sum of homogeneous cycles: the homogeneous components of a cycle are cycles, and they add up to it.
The homogeneous cycle spaces are independent, as subspaces of the independent grading of the ambient module.
The homogeneous cycle spaces form an internal direct sum.
Under the inherited grading of the cycles, homogeneous projection agrees with homogeneous projection in the ambient module.
The cycles of a differential graded left module are a graded module over the graded algebra of
cycles: a homogeneous cycle of degree p carries a homogeneous cycle of degree q to one of
degree p + q.