The cohomology of a differential graded right module #
Let M be a differential graded right module over a differential graded algebra A. Its cycles
are the kernel of the module differential and its boundaries are the image. The cycles form a
right module over the algebra cycles, the boundaries form a right submodule, and the resulting
quotient H(M) is a right module over the cohomology algebra H(A).
Right modules are represented as left modules over the opposite ring. Thus the scalar ring of the
cycle module is cycles(A)ᵐᵒᵖ, while that of the cohomology module is H(A)ᵐᵒᵖ. The latter action
is obtained by descending the former through the boundary ideal. This keeps the handedness visible
in types and ensures that multiplication in the opposite ring encodes the usual right-module
associativity law.
The cycles inherit the grading of M. Their homogeneous pieces form an internal direct sum and
make them a graded right module over the graded algebra of cycles.
This development adapts the left-module construction in
TauCeti.Algebra.Homology.DG.Module.Cohomology to right modules via opposite rings.
Main definitions #
TauCeti.IsDGRightModule.cycles: module cycles, as a right module over algebra cycles.TauCeti.IsDGRightModule.boundaries: module boundaries inside the cycles.TauCeti.IsDGRightModule.Cohomology: cycles modulo boundaries.TauCeti.IsDGRightModule.cyclesDeg: the homogeneous cycles of a fixed degree.
Main results #
TauCeti.IsDGRightModule.instModuleCohomology:H(M)is a right module overH(A).TauCeti.IsDGRightModule.op_quotientMk_smul: the descended action is computed on cycle representatives.TauCeti.IsDGRightModule.instGradedSMulCyclesDeg: the cycles are a graded right module over the graded algebra of cycles.TauCeti.IsDGRightModule.isInternal_cyclesDeg: the homogeneous cycle spaces form an internal direct sum.
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.
@[instance_reducible]
noncomputable instance
TauCeti.IsDGAlgebra.instModuleOppositeCycles
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module Aᵐᵒᵖ M]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
(h : IsDGAlgebra 𝒜 d)
:
Restriction of the right A-action to the opposite of the algebra of cycles.
Equations
instance
TauCeti.IsDGAlgebra.instIsScalarTowerOppositeCycles
{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}
(h : IsDGAlgebra 𝒜 d)
:
IsScalarTower R (↥h.cycles)ᵐᵒᵖ M
The restricted cycle action is compatible with the action of the ground ring.
def
TauCeti.IsDGRightModule.cycles
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The cycles of a differential graded right module, as a right module over the algebra cycles.
Instances For
@[simp]
theorem
TauCeti.IsDGRightModule.mem_cycles
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
{x : M}
:
An element is a module cycle exactly when its differential vanishes.
theorem
TauCeti.IsDGRightModule.map_mem_cycles
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
(x : M)
:
The differential of every module element is a cycle.
noncomputable def
TauCeti.IsDGRightModule.boundaries
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The boundaries of a differential graded right module, as a right submodule of its cycles.
Equations
- hM.boundaries = { toAddSubmonoid := AddSubmonoid.comap hM.cycles.subtype.toAddMonoidHom dM.range.toAddSubmonoid, smul_mem' := ⋯ }
Instances For
@[simp]
theorem
TauCeti.IsDGRightModule.mem_boundaries
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
{z : ↥hM.cycles}
:
A module cycle is a boundary exactly when its underlying element lies in the differential's range.
theorem
TauCeti.IsDGRightModule.map_mem_boundaries
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
(x : M)
:
The cycle represented by a differential is a boundary.
@[reducible, inline]
abbrev
TauCeti.IsDGRightModule.Cohomology
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
Type uM
The cohomology H(M) of a differential graded right module: cycles modulo boundaries.
Equations
- hM.Cohomology = (↥hM.cycles ⧸ hM.boundaries)
Instances For
theorem
TauCeti.IsDGRightModule.quotientMk_eq_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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
{z : ↥hM.cycles}
:
A module cohomology class vanishes exactly when its cycle representative is a boundary.
@[simp]
theorem
TauCeti.IsDGRightModule.quotientMk_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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
(x : M)
:
The class of a differential vanishes in module cohomology.
theorem
TauCeti.IsDGRightModule.isTorsionBySet_boundaries
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The opposite boundary ideal of the algebra annihilates module cohomology.
@[instance_reducible]
noncomputable instance
TauCeti.IsDGRightModule.instModuleQuotientOpBoundaries
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
Module ((↥h.cycles)ᵐᵒᵖ ⧸ TwoSidedIdeal.asIdeal h.boundaries.op) hM.Cohomology
Module cohomology is a module over the opposite algebra of cycles modulo the opposite boundary
ideal, since by isTorsionBySet_boundaries that ideal annihilates it. This is the intermediate
scalar ring through which the action of the cohomology algebra is defined.
Equations
@[instance_reducible]
noncomputable instance
TauCeti.IsDGRightModule.instModuleCohomology
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The cohomology of a differential graded right module is a right module over the cohomology algebra.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
TauCeti.IsDGRightModule.op_quotientMk_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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
(z : ↥h.cycles)
(x : hM.Cohomology)
:
MulOpposite.op ((Ideal.Quotient.mk (TwoSidedIdeal.asIdeal h.boundaries)) z) • x = MulOpposite.op z • x
The action on module cohomology is computed by acting with a cycle representative.
noncomputable def
TauCeti.IsDGRightModule.cyclesDeg
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
:
The degree-p homogeneous module cycles.
Equations
- hM.cyclesDeg p = Submodule.comap (↑R hM.cycles.subtype) (ℳ p)
Instances For
@[simp]
theorem
TauCeti.IsDGRightModule.mem_cyclesDeg
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
{p : ℤ}
{z : ↥hM.cycles}
:
A cycle belongs to degree p exactly when its underlying module element does.
theorem
TauCeti.IsDGRightModule.isHomogeneous_cycles
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
Module cycles are closed under every homogeneous projection of the ambient grading.
@[instance_reducible]
noncomputable instance
TauCeti.IsDGRightModule.instDecompositionCyclesDeg
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
Module cycles inherit the grading of the ambient differential graded right module.
Equations
- hM.instDecompositionCyclesDeg = TauCeti.DirectSum.Decomposition.restrict ℳ hM.cyclesDeg (↑R hM.cycles.subtype) ⋯ ⋯ ⋯
theorem
TauCeti.IsDGRightModule.iSup_cyclesDeg_eq_top
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
Every module cycle is a sum of homogeneous module cycles.
theorem
TauCeti.IsDGRightModule.iSupIndep_cyclesDeg
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The homogeneous module cycle spaces are independent.
theorem
TauCeti.IsDGRightModule.isInternal_cyclesDeg
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The homogeneous module cycle spaces form an internal direct sum.
@[simp]
theorem
TauCeti.IsDGRightModule.coe_decompose_cyclesDeg
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
(z : ↥hM.cycles)
:
Homogeneous projection of a module cycle agrees with projection in the ambient module.
instance
TauCeti.IsDGRightModule.instGradedSMulCyclesDeg
{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}
{h : IsDGAlgebra 𝒜 d}
{ℳ : ℤ → Submodule R M}
[SetLike.GradedSMul (InternalGrading.ofDecomposition 𝒜).opposite.piece ℳ]
[DirectSum.Decomposition ℳ]
{dM : M →ₗ[R] M}
(hM : IsDGRightModule h ℳ dM)
:
The cycles of a differential graded right module are a graded right module over the graded algebra of cycles.