Documentation

TauCeti.Algebra.Module.GradedModule.Resolution

Linear graded projective resolutions #

Let π’œ be a β„€-graded k-algebra and M a graded π’œ-module. A graded projective resolution of M is an exact sequence

β‹― ⟢ Pβ‚‚ ⟢ P₁ ⟢ Pβ‚€ ⟢ M ⟢ 0

of graded π’œ-modules and degree-zero homogeneous π’œ-linear maps, whose terms are projective π’œ-modules. It is linear when its nth term is generated by its homogeneous piece of internal degree n. This is the notion in which Koszulity is stated: a nonnegatively graded algebra with semisimple degree-zero part Aβ‚€ is Koszul when Aβ‚€, as a graded module, has a linear resolution.

Write Aβ‚Š for the sum of the pieces of π’œ of positive degree. A graded projective resolution is minimal when every differential takes values in Aβ‚Š Pβ‚™, the standard notion of minimality for graded resolutions over a nonnegatively graded algebra. The main result of this file is that, over a nonnegatively graded algebra, a linear resolution is minimal: the differential Pβ‚™β‚Šβ‚ ⟢ Pβ‚™ is homogeneous of degree zero, its source lives in degrees β‰₯ n + 1, and every homogeneous element of Pβ‚™ of degree > n already lies in Aβ‚Š Pβ‚™, because Pβ‚™ is generated in degree n. A linear resolution also forces the resolved module to be generated in degree zero.

Main definitions #

Main results #

Implementation notes #

The terms are graded modules in the sense of TauCeti.InternalGrading: total π’œ-modules with an internal direct-sum decomposition into k-submodules, on which π’œ acts by SetLike.GradedSMul. Mathlib has no category of graded modules, so the resolution is recorded by its terms, differentials and augmentation, with exactness stated by Function.Exact. Projectivity is projectivity of the underlying π’œ-module; for β„€-graded rings a graded module is projective in the category of graded modules exactly when it is projective as an ungraded module (NΔƒstΔƒsescu--Van Oystaeyen).

References #

source
structure TauCeti.GradedProjectiveResolution {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] (π’œ : β„€ β†’ Submodule k A) {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] (G : InternalGrading k M) :
Type (max (max (max uA uM) uk) (w + 1))

A graded projective resolution of the graded π’œ-module (M, G): projective graded π’œ-modules X n, degree-zero homogeneous π’œ-linear differentials d n : X (n + 1) ⟢ X n and a degree-zero homogeneous augmentation Ο€ : X 0 ⟢ M, such that β‹― ⟢ X 1 ⟢ X 0 ⟢ M ⟢ 0 is exact.

Instances For
    source
    def TauCeti.GradedProjectiveResolution.IsLinear {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M} (r : GradedProjectiveResolution π’œ G) :
    Prop

    A graded projective resolution is linear if its term in homological degree n is generated by its homogeneous piece of internal degree n.

    Equations
    Instances For
      source
      def TauCeti.GradedProjectiveResolution.IsMinimal {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M} (r : GradedProjectiveResolution π’œ G) :
      Prop

      A graded projective resolution is minimal if each differential X (n + 1) ⟢ X n takes values in Aβ‚Š (X n), the products of elements of positive degree of π’œ with elements of X n.

      Equations
      Instances For
        source
        theorem TauCeti.GradedProjectiveResolution.isLinear_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M} {r : GradedProjectiveResolution π’œ G} :
        r.IsLinear ↔ βˆ€ (n : β„•), (r.grading n).IsGeneratedInDegree A ↑n

        Linearity of a resolution, unfolded: each term is generated in its homological degree.

        source
        theorem TauCeti.GradedProjectiveResolution.isMinimal_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M} {r : GradedProjectiveResolution π’œ G} :
        r.IsMinimal ↔ βˆ€ (n : β„•) (x : r.X (n + 1)), (r.d n) x ∈ (⨆ (i : β„€), ⨆ (_ : 0 < i), π’œ i) β€’ ⊀

        Minimality of a resolution, unfolded: each differential takes values in Aβ‚Š (X n).

        source
        theorem TauCeti.GradedProjectiveResolution.IsLinear.piece_eq_bot_of_lt {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M} {r : GradedProjectiveResolution π’œ G} (hπ’œ : βˆ€ i < 0, π’œ i = βŠ₯) (hr : r.IsLinear) {n : β„•} {p : β„€} (hp : p < ↑n) :
        (r.grading n).piece p = βŠ₯

        Over a nonnegatively graded algebra, the term in homological degree n of a linear resolution has no nonzero homogeneous elements of internal degree below n.

        source
        theorem TauCeti.GradedProjectiveResolution.IsLinear.isMinimal {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} [GradedAlgebra π’œ] {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M} {r : GradedProjectiveResolution π’œ G} (hπ’œ : βˆ€ i < 0, π’œ i = βŠ₯) (hr : r.IsLinear) :
        r.IsMinimal

        A linear resolution is minimal, over a nonnegatively graded algebra: each differential goes from a module generated in degree n + 1 to one generated in degree n, so it takes values in Aβ‚Š (X n).

        source
        theorem TauCeti.GradedProjectiveResolution.IsLinear.isGeneratedInDegree_zero {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : Type uM} [AddCommGroup M] [Module k M] [Module A M] {G : InternalGrading k M} {r : GradedProjectiveResolution π’œ G} (hr : r.IsLinear) :
        G.IsGeneratedInDegree A 0

        A graded module with a linear resolution is generated in degree zero: the augmentation is surjective and preserves degree, and its source is generated in degree zero.