Documentation

TauCeti.CategoryTheory.Exact.Graded.Projective

Projectives and projective resolutions in a graded exact category #

The grading shift of a graded exact category is a conflation-exact autoequivalence. Relative projectivity is therefore invariant under shifting: an object is projective precisely when its shift, or its inverse shift, is projective. This supplies the shift stability of the canonical projective class rather than requiring it as an extra hypothesis.

The same equivalence shifts projective presentations and finite projective resolutions term by term. In particular, the objects of finite projective dimension form a shift-stable property. These facts are the projective input to graded comparison and horseshoe constructions and to the graded resolution theorem.

The comparison maps between finite projective resolutions are compatible with the shift: the complex of a shifted resolution is the shifted complex, and under this identification the lift of f{1} is homotopic to the shift of the lift of f. This is the graded comparison theorem; as in the ungraded case it holds only up to homotopy, since the lift itself is a choice.

Main results #

References #

source
@[simp]
theorem TauCeti.GradedExactStructure.isProjective_shift_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (Q : C) :
E.isProjective (E.shift.functor.obj Q) ↔ E.isProjective Q

An object is projective relative to a graded exact structure exactly when its grading shift is projective.

source
@[simp]
theorem TauCeti.GradedExactStructure.isProjective_inverseShift_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) (Q : C) :
E.isProjective (E.shift.inverse.obj Q) ↔ E.isProjective Q

An object is projective relative to a graded exact structure exactly when its inverse grading shift is projective.

source
@[simp]
theorem TauCeti.GradedExactStructure.isProjective_inverseImage_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) :
E.isProjective.inverseImage E.shift.functor = E.isProjective

The relative projectives form a shift-stable object property.

source
@[simp]
theorem TauCeti.GradedExactStructure.isProjective_inverseImage_inverseShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) :
E.isProjective.inverseImage E.shift.inverse = E.isProjective

The relative projectives are also stable under the inverse grading shift.

source
@[simp]
theorem TauCeti.GradedExactStructure.admitsFiniteProjectiveResolution_inverseImage_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) :
(E.admitsFiniteResolution E.isProjective).inverseImage E.shift.functor = E.admitsFiniteResolution E.isProjective

The objects of finite projective dimension form a shift-stable property.

source
@[simp]
theorem TauCeti.GradedExactStructure.admitsFiniteProjectiveResolution_inverseImage_inverseShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) :
(E.admitsFiniteResolution E.isProjective).inverseImage E.shift.inverse = E.admitsFiniteResolution E.isProjective

The objects of finite projective dimension are also stable under the inverse grading shift.

source
def TauCeti.ExactStructure.ProjectivePresentation.shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
E.ProjectivePresentation (E.shift.functor.obj X)

Shift every object and morphism in a relative projective presentation.

Equations
Instances For
    source
    def TauCeti.ExactStructure.ProjectivePresentation.inverseShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
    E.ProjectivePresentation (E.shift.inverse.obj X)

    Apply the inverse grading shift to every object and morphism in a relative projective presentation.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.shift_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.shift.K = E.shift.functor.obj P.K
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.shift_P {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.shift.P = E.shift.functor.obj P.P
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.shift_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.shift.i ≍ E.shift.functor.map P.i
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.shift_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.shift.p ≍ E.shift.functor.map P.p
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.inverseShift_K {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.inverseShift.K = E.shift.inverse.obj P.K
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.inverseShift_P {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.inverseShift.P = E.shift.inverse.obj P.P
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.inverseShift_i {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.inverseShift.i ≍ E.shift.inverse.map P.i
      source
      @[simp]
      theorem TauCeti.ExactStructure.ProjectivePresentation.inverseShift_p {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (P : E.ProjectivePresentation X) :
      P.inverseShift.p ≍ E.shift.inverse.map P.p
      source
      def TauCeti.ExactStructure.FiniteResolution.shiftProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
      E.FiniteResolution E.isProjective (E.shift.functor.obj X)

      Shift every term and conflation of a finite projective resolution.

      Equations
      Instances For
        source
        def TauCeti.ExactStructure.FiniteResolution.inverseShiftProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
        E.FiniteResolution E.isProjective (E.shift.inverse.obj X)

        Apply the inverse grading shift to every term and conflation of a finite projective resolution.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.ExactStructure.FiniteResolution.shiftProjective_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (hX : E.isProjective X) :
          (base hX).shiftProjective = base ⋯
          source
          @[simp]
          theorem TauCeti.ExactStructure.FiniteResolution.shiftProjective_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {K Q X : C} (hQ : E.isProjective Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution E.isProjective K) :
          (step hQ i p zero hp r).shiftProjective = step ⋯ (E.shift.functor.map i) (E.shift.functor.map p) ⋯ ⋯ r.shiftProjective
          source
          @[simp]
          theorem TauCeti.ExactStructure.FiniteResolution.inverseShiftProjective_base {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (hX : E.isProjective X) :
          (base hX).inverseShiftProjective = base ⋯
          source
          @[simp]
          theorem TauCeti.ExactStructure.FiniteResolution.inverseShiftProjective_step {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {K Q X : C} (hQ : E.isProjective Q) (i : K ⟶ Q) (p : Q ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hp : E.Conflation { X₁ := K, X₂ := Q, X₃ := X, f := i, g := p, zero := zero }) (r : E.FiniteResolution E.isProjective K) :
          (step hQ i p zero hp r).inverseShiftProjective = step ⋯ (E.shift.inverse.map i) (E.shift.inverse.map p) ⋯ ⋯ r.inverseShiftProjective
          source
          @[simp]
          theorem TauCeti.ExactStructure.FiniteResolution.length_shiftProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
          r.shiftProjective.length = r.length
          source
          @[simp]
          theorem TauCeti.ExactStructure.FiniteResolution.length_inverseShiftProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
          r.inverseShiftProjective.length = r.length
          source
          noncomputable def TauCeti.ExactStructure.FiniteResolution.toChainComplexShiftProjectiveIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
          r.shiftProjective.toChainComplex ≅ (E.shift.functor.mapHomologicalComplex (ComplexShape.down ℕ)).obj r.toChainComplex

          The complex of the shift of a finite projective resolution is the shift of its complex.

          Equations
          Instances For
            source
            noncomputable def TauCeti.ExactStructure.FiniteResolution.toChainComplexInverseShiftProjectiveIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
            r.inverseShiftProjective.toChainComplex ≅ (E.shift.inverse.mapHomologicalComplex (ComplexShape.down ℕ)).obj r.toChainComplex

            The complex of the inverse shift of a finite projective resolution is the inverse shift of its complex.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexShiftProjectiveIso_hom_f_zero_comp_map_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
              CategoryTheory.CategoryStruct.comp (r.toChainComplexShiftProjectiveIso.hom.f 0) (E.shift.functor.map r.aug) = r.shiftProjective.aug

              The identification of the complex of a shifted resolution with the shifted complex is compatible with the augmentations.

              source
              @[simp]
              theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexShiftProjectiveIso_hom_f_zero_comp_map_aug_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) {Z : C} (h : E.shift.functor.obj X ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (r.toChainComplexShiftProjectiveIso.hom.f 0) (CategoryTheory.CategoryStruct.comp (E.shift.functor.map r.aug) h) = CategoryTheory.CategoryStruct.comp r.shiftProjective.aug h

              The identification of the complex of a shifted resolution with the shifted complex is compatible with the augmentations.

              source
              @[simp]
              theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexInverseShiftProjectiveIso_hom_f_zero_comp_map_aug {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) :
              CategoryTheory.CategoryStruct.comp (r.toChainComplexInverseShiftProjectiveIso.hom.f 0) (E.shift.inverse.map r.aug) = r.inverseShiftProjective.aug

              The identification of the complex of an inversely shifted resolution with the inversely shifted complex is compatible with the augmentations.

              source
              @[simp]
              theorem TauCeti.ExactStructure.FiniteResolution.toChainComplexInverseShiftProjectiveIso_hom_f_zero_comp_map_aug_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X : C} (r : E.FiniteResolution E.isProjective X) {Z : C} (h : E.shift.inverse.obj X ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (r.toChainComplexInverseShiftProjectiveIso.hom.f 0) (CategoryTheory.CategoryStruct.comp (E.shift.inverse.map r.aug) h) = CategoryTheory.CategoryStruct.comp r.inverseShiftProjective.aug h

              The identification of the complex of an inversely shifted resolution with the inversely shifted complex is compatible with the augmentations.

              source
              noncomputable def TauCeti.ExactStructure.FiniteResolution.liftShiftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X Y : C} (f : X ⟶ Y) (r : E.FiniteResolution E.isProjective X) (r' : E.FiniteResolution E.isProjective Y) :
              Homotopy (lift ⋯ (E.shift.functor.map f) r.shiftProjective r'.shiftProjective) (CategoryTheory.CategoryStruct.comp r.toChainComplexShiftProjectiveIso.hom (CategoryTheory.CategoryStruct.comp ((E.shift.functor.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift ⋯ f r r')) r'.toChainComplexShiftProjectiveIso.inv))

              The graded comparison theorem. The comparison map between two finite projective resolutions commutes with the grading shift up to homotopy: the lift of f{1} between the shifted resolutions is homotopic to the shift of the lift of f.

              Equations
              Instances For
                source
                noncomputable def TauCeti.ExactStructure.FiniteResolution.liftInverseShiftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : GradedExactStructure C} {X Y : C} (f : X ⟶ Y) (r : E.FiniteResolution E.isProjective X) (r' : E.FiniteResolution E.isProjective Y) :
                Homotopy (lift ⋯ (E.shift.inverse.map f) r.inverseShiftProjective r'.inverseShiftProjective) (CategoryTheory.CategoryStruct.comp r.toChainComplexInverseShiftProjectiveIso.hom (CategoryTheory.CategoryStruct.comp ((E.shift.inverse.mapHomologicalComplex (ComplexShape.down ℕ)).map (lift ⋯ f r r')) r'.toChainComplexInverseShiftProjectiveIso.inv))

                The comparison map between two finite projective resolutions commutes with the inverse grading shift up to homotopy.

                Equations
                Instances For