The graded-split cone sequence

The canonical inclusion and projection of a cone form a conflation of the graded-split exact structure. Its graded splitting is given by the second projection and first inclusion. These maps need not commute with the differentials.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneShortComplex {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : CategoryTheory.ShortComplex (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))

The short complex N → Cone(f) → M[1] of closed cone maps.

theorem TauCeti.CurvedDGRightModuleCat.coneShortComplex_eq_mk {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : coneShortComplex f = { X₁ := CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N, X₂ := CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f), X₃ := CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M.shift 1), f := coneInclusion f, g := coneProjection f, zero := ⋯ }

The cone sequence has the canonical inclusion and projection as its two arrows.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneShortComplex_X₁ {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : (coneShortComplex f).X₁ = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N

The first object of the cone sequence is its target module.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneShortComplex_X₂ {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : (coneShortComplex f).X₂ = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f)

The middle object of the cone sequence is the cone.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneShortComplex_X₃ {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : (coneShortComplex f).X₃ = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M.shift 1)

The last object of the cone sequence is the shifted source.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneShortComplex_f {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (coneShortComplex f).f (CategoryTheory.eqToHom ⋯)) = coneInclusion f

After identifying its endpoints, the first map is the cone inclusion.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneShortComplex_g {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (coneShortComplex f).g (CategoryTheory.eqToHom ⋯)) = coneProjection f

After identifying its endpoints, the second map is the cone projection.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneGradedSplitting {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : ((coneShortComplex f).map forgetDifferential).Splitting

The cone sequence splits after forgetting the differential.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneGradedSplitting_r {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (coneGradedSplitting f).r (CategoryTheory.eqToHom ⋯))).hom = LinearMap.snd Aᵐᵒᵖ M.carrier N.carrier

The graded retraction is the second product projection on the identified objects.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneGradedSplitting_s {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (coneGradedSplitting f).s (CategoryTheory.eqToHom ⋯))).hom = LinearMap.inl Aᵐᵒᵖ M.carrier N.carrier

The graded section is the first product inclusion on the identified objects.

theorem TauCeti.CurvedDGRightModuleCat.coneShortComplex_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} {M N : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : gradedSplitExact.Conflation (coneShortComplex f)

The cone sequence is a graded-split conflation.

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isInflation_coneInclusion {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : gradedSplitExact.IsInflation (coneInclusion f)

The closed cone inclusion is an inflation of the graded-split exact structure.

theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isDeflation_coneProjection {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 : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : gradedSplitExact.IsDeflation (coneProjection f)

The closed cone projection is a deflation of the graded-split exact structure.