The cochain complex of a family of submodules with a differential #
A ℤ-indexed family ℳ of submodules of an R-module M, together with an R-linear
endomorphism dM which carries ℳ p into ℳ (p + 1) and squares to zero on each ℳ p,
assembles into a cochain complex of R-modules: the degree-p term is the submodule ℳ p and
the differential is the restriction of dM. This file performs that assembly. No decomposition
or exhaustiveness hypothesis on ℳ is required, and the differential is not assumed to come
from a module action.
In practice ℳ is the internal grading in which the differential graded algebras and modules of
TauCeti.Algebra.Homology.DG store their structure, because a product or an action is easier to
write on one carrier than on a family of summands. Statements which compare such an object with
a genuine complex — quasi-isomorphisms, Hom complexes, cohomology computed by Mathlib's
homological algebra — need the complex on the other side, and that is what this construction
supplies: it serves the underlying complex of a DG algebra and of a DG module on either side.
Main definitions #
TauCeti.gradedCochainComplex: the cochain complex whose degree-pterm is the submoduleℳ pand whose differential is the restriction ofdM.TauCeti.gradedCochainComplexLift: the same complex with its terms lifted to a larger module universe.TauCeti.gradedCochainComplexMap: the induced map in a common module universe.
Implementation notes #
The component, differential, and element-level differential lemmas below are the intended public
interface to gradedCochainComplex.
The cochain complex of R-modules assembled from a ℤ-indexed family ℳ of submodules of
M and an R-linear endomorphism dM carrying ℳ p into ℳ (p + 1) and square-zero on
each ℳ p.
Equations
- TauCeti.gradedCochainComplex ℳ dM hdeg hsq = CochainComplex.of (fun (p : ℤ) => ↧↥(ℳ p)) (fun (p : ℤ) => ModuleCat.ofHom (dM.restrict ⋯)) ⋯
Instances For
The differential of gradedCochainComplex on an element. This is intentionally not a simp
lemma: gradedCochainComplex_d already simplifies its left-hand side, so registering both rules
would fail the simpNF linter.
The graded cochain complex in a common module universe. Its degree-p term is
ULift (ℳ p), and its differential is the lifted restriction of dM.
Equations
- TauCeti.gradedCochainComplexLift ℳ dM hdeg hsq = ((ModuleCat.uliftFunctor.{?u.1, ?u.2, ?u.3} R).mapHomologicalComplex (ComplexShape.up ℤ)).obj (TauCeti.gradedCochainComplex ℳ dM hdeg hsq)
Instances For
The degree-p term of the lifted complex is the lifted homogeneous submodule.
The degree-p differential of the lifted complex is the lifted restriction of dM,
transported along the identifications of its source and target terms.
The differential of the lifted complex acts by the original differential on homogeneous elements.
A degree-preserving linear map commuting with differentials induces a map between the cochain complexes assembled from graded modules, even when their carriers have different universes.
Equations
- TauCeti.gradedCochainComplexMap f hf hcomm = CochainComplex.ofHom (fun (n : ℤ) => id (ModuleCat.ofHom (↑ULift.moduleEquiv.symm ∘ₗ f.restrict ⋯ ∘ₗ ↑ULift.moduleEquiv))) ⋯
Instances For
On a homogeneous element, the induced cochain map is the original linear map.
The induced cochain map depends only on the underlying linear map.
The cochain map induced by the identity linear map is the identity.
Cochain maps assembled from graded linear maps preserve composition.