Documentation

TauCeti.Algebra.Category.GradedModuleCat.Resolution

Concrete graded resolutions as categorical projective resolutions #

A TauCeti.GradedProjectiveResolution records projective modules, homogeneous differentials, and an exact augmentation as linear maps. This file turns that data into a CategoryTheory.ProjectiveResolution in TauCeti.GradedModuleCat. Its terms retain their internal gradings, and its differentials and augmentation are the original maps.

The resulting resolution can be used directly with Mathlib's comparison maps, uniqueness up to chain homotopy, and computation of Ext from projective resolutions. No enough-projectives hypothesis is needed to bundle a given resolution. The construction imposes neither linearity, minimality, finite generation, nor boundedness.

References #

source
@[reducible, inline]
abbrev TauCeti.GradedProjectiveResolution.termObj {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) (n : β„•) :
GradedModuleCat π’œ

A term of a concrete graded resolution, with its specified internal grading.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.GradedProjectiveResolution.differential {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) (n : β„•) :
    r.termObj (n + 1) ⟢ r.termObj n

    The differential of a concrete graded resolution as a morphism of graded modules.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.GradedProjectiveResolution.augmentation {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) :
      r.termObj 0 ⟢ M

      The augmentation of a concrete graded resolution as a morphism of graded modules.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.GradedProjectiveResolution.differential_comp_differential {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) (n : β„•) :
        CategoryTheory.CategoryStruct.comp (r.differential (n + 1)) (r.differential n) = 0
        source
        @[simp]
        theorem TauCeti.GradedProjectiveResolution.differential_comp_differential_assoc {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) (n : β„•) {Z : GradedModuleCat π’œ} (h : r.termObj n ⟢ Z) :
        CategoryTheory.CategoryStruct.comp (r.differential (n + 1)) (CategoryTheory.CategoryStruct.comp (r.differential n) h) = CategoryTheory.CategoryStruct.comp 0 h
        source
        @[simp]
        theorem TauCeti.GradedProjectiveResolution.differential_zero_comp_augmentation {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) :
        CategoryTheory.CategoryStruct.comp (r.differential 0) r.augmentation = 0
        source
        @[simp]
        theorem TauCeti.GradedProjectiveResolution.differential_zero_comp_augmentation_assoc {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) {Z : GradedModuleCat π’œ} (h : M ⟢ Z) :
        CategoryTheory.CategoryStruct.comp (r.differential 0) (CategoryTheory.CategoryStruct.comp r.augmentation h) = CategoryTheory.CategoryStruct.comp 0 h
        source
        noncomputable def TauCeti.GradedProjectiveResolution.toProjectiveResolution {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) [DirectSum.Decomposition π’œ] :
        CategoryTheory.ProjectiveResolution M

        A concrete graded projective resolution is a categorical projective resolution in the category of graded modules. The quasi-isomorphism is its original augmentation.

        Equations
        Instances For
          source
          noncomputable def TauCeti.GradedProjectiveResolution.toProjectiveResolutionXIso {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) [DirectSum.Decomposition π’œ] (n : β„•) :
          r.toProjectiveResolution.complex.X n β‰… r.termObj n

          The terms of the categorical resolution are the original graded modules.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.GradedProjectiveResolution.toProjectiveResolution_complex_d {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) [DirectSum.Decomposition π’œ] (n : β„•) :
            r.toProjectiveResolution.complex.d (n + 1) n = CategoryTheory.CategoryStruct.comp (r.toProjectiveResolutionXIso (n + 1)).hom (CategoryTheory.CategoryStruct.comp (r.differential n) (r.toProjectiveResolutionXIso n).inv)

            The categorical differential is the original differential, through the term identifications.

            source
            @[simp]
            theorem TauCeti.GradedProjectiveResolution.toProjectiveResolution_Ο€_f_zero {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {π’œ : β„€ β†’ Submodule k A} {M : GradedModuleCat π’œ} (r : GradedProjectiveResolution π’œ M.grading) [DirectSum.Decomposition π’œ] :
            r.toProjectiveResolution.Ο€.f 0 = CategoryTheory.CategoryStruct.comp (r.toProjectiveResolutionXIso 0).hom r.augmentation

            The categorical augmentation is the original augmentation, through the term identification.