The graded-split exact structure on curved right modules

A short complex of closed maps is a conflation when it splits after forgetting the differentials. The graded forgetful functor preserves finite limits and colimits and reflects isomorphisms, so these sequences are kernel-cokernel pairs. Its preservation of pushouts and pullbacks transfers the Quillen axioms from the split exact structure on graded right modules.

These splittings are graded right-linear maps; they need not be closed maps. Thus this exact structure records the underlying graded-module splittings used to identify its relatively projective and injective objects with the contractible curved modules.

References

• The Tau Ceti contributors, TauCeti.Algebra.Homology.Curved.Exact: the inflation and deflation recognition arguments adapt its componentwise exact-structure construction.
• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.

noncomputable def TauCeti.CurvedDGRightModuleCat.gradedSplitExact {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} : ExactStructure (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))

The exact structure whose conflations split as short complexes of graded right modules.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_conflation_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} (S : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))) : gradedSplitExact.Conflation S ↔ (ExactStructure.split (GradedModuleCat ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ))).Conflation (S.map forgetDifferential)

A graded-split conflation is exactly a split sequence after forgetting the differentials.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isInflation_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} {M N : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (f : M ⟶ N) : gradedSplitExact.IsInflation f ↔ (ExactStructure.split (GradedModuleCat ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ))).IsInflation (forgetDifferential.map f)

An inflation is recognized by the underlying graded split inflation.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isDeflation_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} {M N : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (f : M ⟶ N) : gradedSplitExact.IsDeflation f ↔ (ExactStructure.split (GradedModuleCat ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ))).IsDeflation (forgetDifferential.map f)

A deflation is recognized by the underlying graded split deflation.

theorem TauCeti.CurvedDGRightModuleCat.forgetDifferential_isConflationExact {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} : gradedSplitExact.IsConflationExact (ExactStructure.split (GradedModuleCat ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ))) forgetDifferential

Forgetting the differential preserves graded-split conflations.