Documentation

TauCeti.Algebra.Homology.DG.Module.Defs

Differential graded left modules #

Let d be a differential on an internally โ„ค-graded R-algebra ๐’œ on a carrier A, in the sense of TauCeti.IsDGAlgebra. A differential graded left module over it is an A-module M with an internal โ„ค-grading โ„ณ for which the action adds degrees, together with an R-linear differential dM of degree +1, in the sense of TauCeti.LinearMap.IsHomogeneous, which squares to zero and satisfies the graded Leibniz rule

dM (a โ€ข x) = d a โ€ข x + (-1) ^ |a| โ€ข (a โ€ข dM x).

Only a homogeneous scalar a is constrained by the Leibniz axiom, because the sign depends on its degree alone; this is the exact shape of TauCeti.IsDGAlgebra.leibniz, and indeed a differential graded algebra is a differential graded left module over itself. Decomposing a scalar into homogeneous components removes the hypothesis whenever the sign is multiplied by something that vanishes: the differential of a โ€ข x is d a โ€ข x as soon as x is a cycle, so a cycle acts on cycles and the cycles of A carry the boundaries of M into themselves.

The grading is stored internally, as a family โ„ณ : โ„ค โ†’ Submodule R M with Mathlib's DirectSum.Decomposition โ„ณ and SetLike.GradedSMul ๐’œ โ„ณ. This matches the presentation of TauCeti.IsDGAlgebra, so the action is the given A-action on M and no signed totalization intervenes. The ground ring acts through the algebra, IsScalarTower R A M: the R-module structure which carries the grading and the linearity of dM is the restriction of the A-action along algebraMap R A, so there is only one action of R in play.

Handedness #

The handedness is part of the name: this file defines the left interface and says nothing about the right one, whose Leibniz rule dM (x โ€ข a) = dM x โ€ข a + (-1) ^ |x| โ€ข (x โ€ข d a) is a separate axiom system, on an Aแตแต’แต–-module. Turning one into the other needs the sign-twisted graded opposite a *แต’แต– b = (-1) ^ (|a| * |b|) โ€ข (b * a). The unsigned MulOpposite will not do: with a *แต’แต– b = b * a the Leibniz rule for *แต’แต– asks for d (b * a) = b * d a + (-1) ^ |a| โ€ข (d b * a), while the rule in A gives d (b * a) = d b * a + (-1) ^ |b| โ€ข (b * d a). So no reduction between the two handednesses is claimed here. The left handedness is the one Mathlib's Module A M gives directly, and the one whose Leibniz sign depends on the same factor as TauCeti.IsDGAlgebra.leibniz, which is what lets a differential graded algebra be a module over itself with no twist.

Main definitions #

Main results #

Read through TauCeti.IsDGAlgebra.isDGLeftModule, these results are the homogeneous consequences of the algebra axioms used by TauCeti.Algebra.Homology.DG.Algebra.Cohomology; the cycles, boundaries and cohomology module of a module are built on this file in TauCeti.Algebra.Homology.DG.Module.Cohomology.

References #

source
structure TauCeti.IsDGLeftModule {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} [IsScalarTower R A M] (h : IsDGAlgebra ๐’œ d) (โ„ณ : โ„ค โ†’ Submodule R M) [SetLike.GradedSMul ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] (dM : M โ†’โ‚—[R] M) :
Prop

A differential graded left module over the differential graded algebra (๐’œ, d): an internally โ„ค-graded A-module โ„ณ on a carrier M, whose action adds degrees, with an R-linear map dM which raises degree by one, squares to zero, and satisfies the graded Leibniz rule on a homogeneous scalar. The sign (-1) ^ p is Int.negOnePow p, acting through the units of โ„ค.

Instances For
    source
    theorem TauCeti.IsDGAlgebra.isDGLeftModule {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} (h : IsDGAlgebra ๐’œ d) :
    IsDGLeftModule h ๐’œ d

    A differential graded algebra is a differential graded left module over itself. The Leibniz rule is the one of the algebra, read through smul_eq_mul.

    source
    theorem TauCeti.IsDGLeftModule.map_decompose {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) (p : โ„ค) (x : M) :
    dM โ†‘(((DirectSum.decompose โ„ณ) x) p) = โ†‘(((DirectSum.decompose โ„ณ) (dM x)) (p + 1))

    The differential of a differential graded left module commutes with the homogeneous projections of the grading, up to the shift by one that it applies to degrees.

    source
    theorem TauCeti.IsDGLeftModule.decompose_mem_range {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) {x : M} (hx : x โˆˆ dM.range) (p : โ„ค) :
    โ†‘(((DirectSum.decompose โ„ณ) x) p) โˆˆ dM.range

    Every homogeneous projection of a boundary is again a boundary.

    source
    theorem TauCeti.IsDGLeftModule.map_decompose_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) {x : M} (hx : dM x = 0) (p : โ„ค) :
    dM โ†‘(((DirectSum.decompose โ„ณ) x) p) = 0

    The homogeneous components of a cycle are cycles.

    source
    theorem TauCeti.IsDGLeftModule.leibniz_of_map_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) (a : A) {x : M} (hx : dM x = 0) :
    dM (a โ€ข x) = d a โ€ข x

    The Leibniz rule against a cycle: the sign disappears with the term it multiplies, so the scalar need not be homogeneous.

    source
    theorem TauCeti.IsDGLeftModule.map_smul_eq_zero_of_map_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) {a : A} {x : M} (ha : d a = 0) (hx : dM x = 0) :
    dM (a โ€ข x) = 0

    A cycle of the algebra acts on a cycle of the module to give a cycle.

    source
    theorem TauCeti.IsDGLeftModule.smul_map_eq_negOnePow_smul_map_smul {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) {p : โ„ค} {a : A} (ha : a โˆˆ ๐’œ p) (hda : d a = 0) (x : M) :
    a โ€ข dM x = p.negOnePow โ€ข dM (a โ€ข x)

    A homogeneous cycle of the algebra acting on a differential is, up to the sign of its degree, the differential of the action.

    source
    theorem TauCeti.IsDGLeftModule.smul_mem_range_of_map_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) {a : A} (ha : d a = 0) {y : M} (hy : y โˆˆ dM.range) :
    a โ€ข y โˆˆ dM.range

    A cycle of the algebra carries a boundary of the module to a boundary. Componentwise this is the Leibniz rule read backwards: a โ€ข dM x = (-1) ^ |a| * dM (a โ€ข x) for a homogeneous cycle a.

    source
    theorem TauCeti.IsDGLeftModule.map_smul_mem_range_of_map_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [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 ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (hM : IsDGLeftModule h โ„ณ dM) (a : A) {x : M} (hx : dM x = 0) :
    d a โ€ข x โˆˆ dM.range

    A boundary of the algebra carries a cycle of the module to a boundary: d a โ€ข x is the differential of a โ€ข x.

    source
    theorem TauCeti.isDGLeftModule_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] (๐’œ : โ„ค โ†’ Submodule R A) [GradedAlgebra ๐’œ] (โ„ณ : โ„ค โ†’ Submodule R M) [SetLike.GradedSMul ๐’œ โ„ณ] [DirectSum.Decomposition โ„ณ] :
    IsDGLeftModule โ‹ฏ โ„ณ 0

    A graded module with zero differential over a graded algebra with zero differential is a differential graded left module.