The homotopy category of curved right modules is triangulated #

Let A be a right-convention curved DG algebra. The graded-split exact structure on curved right A-modules is Frobenius, and its stable category is identified with the curved homotopy category by gradedSplitStableToHomotopy, compatibly with the shifts by ℤ (stable suspension on one side, the coherent cohomological shift on the other). This file transports Happel's triangulation of the stable category along this equivalence. The curved homotopy category thereby becomes a triangulated category whose shift by one is the cohomological shift, although individual curved modules have no homology.

No centrality of the curvature is assumed. The distinguished triangles are, up to isomorphism, the images of Happel's standard triangles of graded-split conflations: short sequences of closed maps of curved modules which split after forgetting the differentials.

Main definitions #

TauCeti.CurvedDGRightModuleCat.homotopyPretriangulated: the pretriangulated structure on the curved homotopy category.

Main results #

TauCeti.CurvedDGRightModuleCat.homotopyIsTriangulated: the curved homotopy category is triangulated.
TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopy_isTriangulated: the comparison from the graded-split stable category is a triangle functor.
TauCeti.CurvedDGRightModuleCat.map_stableConflationTriangle_mem_distTriang: graded-split conflations give distinguished triangles.
TauCeti.CurvedDGRightModuleCat.mk_distinguished_of_conflation: an identity-cone extension computes the positive connecting arrow of any graded-split conflation.
TauCeti.CurvedDGRightModuleCat.homotopy_mem_distTriang_iff: every distinguished triangle is isomorphic to the image of the standard triangle of a graded-split conflation.
TauCeti.CurvedDGRightModuleCat.prop_cone, TauCeti.CurvedDGRightModuleCat.prop_target_of_prop_cone, TauCeti.CurvedDGRightModuleCat.prop_source_of_prop_cone: the two-out-of-three property for the source, target and cone of a closed map, in isomorphism-closed triangulated subcategories.

References #

L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6: the homotopy category of curved DG modules is triangulated.
D. Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2, Theorem 2.6: the stable category of a Frobenius category is triangulated.
The Tau Ceti contributors, TauCeti.Algebra.Homology.Periodic.Triangulated: the transport follows the corresponding statements for periodic homotopy categories.

source

@[instance_reducible]

noncomputable instance TauCeti.CurvedDGRightModuleCat.homotopyPretriangulated {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :

CategoryTheory.Pretriangulated (DGHomotopyCategory R (CurvedDGRightModuleCat h))

The curved homotopy category is pretriangulated: its distinguished triangles are the triangles isomorphic to images of Happel's distinguished triangles under the equivalence with the graded-split stable category.

source

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitStableToHomotopy_isTriangulated {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :

gradedSplitStableToHomotopy.IsTriangulated

The comparison from the graded-split stable category of curved right modules to their homotopy category is a triangle functor.

source

instance TauCeti.CurvedDGRightModuleCat.homotopyIsTriangulated {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} :

CategoryTheory.IsTriangulated (DGHomotopyCategory R (CurvedDGRightModuleCat h))

The homotopy category of curved right modules is triangulated, with the shift by one given by the cohomological shift.

source

theorem TauCeti.CurvedDGRightModuleCat.map_stableConflationTriangle_mem_distTriang {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))) (hS : gradedSplitExact.Conflation S) :

gradedSplitStableToHomotopy.mapTriangle.obj (⋯.stableConflationTriangle S hS) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

Graded-split conflations give distinguished triangles. The image of the standard stable triangle of a graded-split conflation of curved right modules is distinguished in the curved homotopy category.

source

theorem TauCeti.CurvedDGRightModuleCat.mk_distinguished_of_conflation {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))} (hS : gradedSplitExact.Conflation S) (a : S.X₂ ⟶ (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.I) (δ : S.X₃ ⟶ (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.K) (ha : CategoryTheory.CategoryStruct.comp S.f a = (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.i) (hδ : CategoryTheory.CategoryStruct.comp S.g δ = CategoryTheory.CategoryStruct.comp a (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) S.X₁).coneIdentityInjectivePresentation.p) :

CategoryTheory.Pretriangulated.Triangle.mk ((dgClosedToHomotopy R).map S.f) ((dgClosedToHomotopy R).map S.g) (CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map δ) (CategoryTheory.eqToHom ⋯)) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

A graded-split conflation gives a distinguished triangle whose third arrow is the class of the cokernel map induced by an extension to the first object's identity cone. The canonical suspension comparison gives this connecting arrow with positive sign.

source

theorem TauCeti.CurvedDGRightModuleCat.homotopy_mem_distTriang_iff {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (T : CategoryTheory.Pretriangulated.Triangle (DGHomotopyCategory R (CurvedDGRightModuleCat h))) :

T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ (S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))) (hS : gradedSplitExact.Conflation S), Nonempty (T ≅ gradedSplitStableToHomotopy.mapTriangle.obj (⋯.stableConflationTriangle S hS))

A triangle in the curved homotopy category is distinguished exactly when it is isomorphic to the image of the standard stable triangle of a graded-split conflation.