Mapping cones of curved differential graded right modules

The cone of a closed map f : M ⟶ N has underlying graded right module M[1] × N and differential (x, y) ↦ (-dM x, f x + dN y). The two off-diagonal terms in its square cancel because f commutes with the differentials. Its curvature is therefore the same as the curvature of M and N, without a centrality assumption.

The right action is unchanged. The canonical inclusion of N and projection to M[1] are closed maps, and the adjacent composites vanish in the existing homotopy category. A closed map g : N ⟶ P with f ≫ g = 0 induces the closed map coneDesc f g hfg : cone(f) ⟶ P. A null-homotopic closed map factors through its source's identity cone via the inclusion.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Sections 6.2 and 7.6. His curvature is the negative of the right-module curvature stored here.
• The Tau Ceti contributors, TauCeti.Algebra.Homology.Curved.Cone.Basic: the curved-duplex cone formalization is the precedent for the cone, its maps and its contraction interface.
• The Tau Ceti contributors, TauCeti.Algebra.Homology.Curved.Frobenius: the identity-cone factorization adapts the corresponding componentwise split construction.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneDifferential {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) : M.carrier × N.carrier →ₗ[R] M.carrier × N.carrier

The cone differential uses the linear mapping-cone construction on the ground-ring maps.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneDifferential_apply {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) (x : M.carrier × N.carrier) : (coneDifferential f) x = (-M.differential x.1, (closedHom f) x.1 + N.differential x.2)

The cone differential has diagonal entries -dM and dN and lower-left entry f.

@[implicit_reducible]

noncomputable def TauCeti.CurvedDGRightModuleCat.cone {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) : CurvedDGRightModuleCat h

The cone of a closed map, with grading M[1] × N and the original curvature.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.cone_grading {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) (p : ℤ) : (cone f).grading p = (M.grading (p + 1)).prod (N.grading p)

The degree-p part of the cone is Mᵖ⁺¹ × Nᵖ.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.cone_differential_apply {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) (x : M.carrier × N.carrier) : (cone f).differential x = (-M.differential x.1, (closedHom f) x.1 + N.differential x.2)

The differential on the cone acts by the usual block formula.

noncomputable def TauCeti.CurvedDGRightModuleCat.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) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f)

The closed inclusion of the codomain into its cone.

noncomputable def TauCeti.CurvedDGRightModuleCat.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) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M.shift 1)

The closed projection from the cone to the cohomological shift of its domain.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_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) : closedHom (coneInclusion f) = LinearMap.inr Aᵐᵒᵖ M.carrier N.carrier

The cone inclusion is the usual second linear inclusion.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_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) : closedHom (coneProjection f) = LinearMap.fst Aᵐᵒᵖ M.carrier N.carrier

The cone projection is the usual first linear projection.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneInclusion_comp_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) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (coneProjection f) = 0

The inclusion followed by the projection vanishes already in the closed category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneInclusion_comp_coneProjection_assoc {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) {Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M.shift 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (CategoryTheory.CategoryStruct.comp (coneProjection f) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The inclusion followed by the projection vanishes already in the closed category.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneDesc {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) {P : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P

A closed map g killing the closed map f induces the closed map cone(f) ⟶ P sending (x, y) to g y.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_coneDesc {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) {P : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) : closedHom (coneDesc f g hfg) = closedHom g ∘ₗ LinearMap.snd Aᵐᵒᵖ M.carrier N.carrier

The map out of the cone applies g to the second component.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneInclusion_comp_coneDesc {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) {P : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (coneDesc f g hfg) = g

The cone inclusion followed by the induced map out of the cone is the original map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneInclusion_comp_coneDesc_assoc {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) {P : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P) (hfg : CategoryTheory.CategoryStruct.comp f g = 0) {Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (CategoryTheory.CategoryStruct.comp (coneDesc f g hfg) h✝) = CategoryTheory.CategoryStruct.comp g h✝

The cone inclusion followed by the induced map out of the cone is the original map.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneInclusionHomotopy {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) : ↥(dgRightModuleCochains (-1))

The first linear inclusion, viewed as a degree-minus-one homotopy into the cone.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneInclusionHomotopy_apply {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) (x : M.carrier) : ↑(coneInclusionHomotopy f) x = (x, 0)

The homotopy for the first adjacent composite sends x to (x, 0).

theorem TauCeti.CurvedDGRightModuleCat.comp_coneInclusion_boundary {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) (x : M.carrier) : (closedHom (CategoryTheory.CategoryStruct.comp f (coneInclusion f))) x = (cone f).differential (↑(coneInclusionHomotopy f) x) + ↑(coneInclusionHomotopy f) (M.differential x)

The first adjacent composite is the boundary of the first inclusion homotopy.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneProjectionHomotopy {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) : ↥(dgRightModuleCochains (-1))

The second projection, viewed as a degree-minus-one homotopy to the shifted codomain.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneProjectionHomotopy_apply {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) (x : M.carrier × N.carrier) : ↑(coneProjectionHomotopy f) x = x.2

The homotopy for the third adjacent composite sends (x, y) to y.

theorem TauCeti.CurvedDGRightModuleCat.coneProjection_comp_shift_boundary {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) (x : M.carrier × N.carrier) : (closedHom (CategoryTheory.CategoryStruct.comp (coneProjection f) ((closedShiftFunctor 1).map f))) x = (N.shift 1).differential (↑(coneProjectionHomotopy f) x) + ↑(coneProjectionHomotopy f) ((cone f).differential x)

The projection followed by the shifted map is the boundary of the second projection.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.quotient_map_comp_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) : CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map f) ((dgClosedToHomotopy R).map (coneInclusion f)) = 0

The first adjacent composite vanishes in the curved homotopy category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.quotient_map_comp_coneInclusion_assoc {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) {Z : DGHomotopyCategory R (CurvedDGRightModuleCat h)} (h✝ : (dgClosedToHomotopy R).obj (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map f) (CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map (coneInclusion f)) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The first adjacent composite vanishes in the curved homotopy category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.quotient_map_coneProjection_comp_shift {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 ((dgClosedToHomotopy R).map (coneProjection f)) ((dgClosedToHomotopy R).map ((closedShiftFunctor 1).map f)) = 0

The third adjacent composite also vanishes in the curved homotopy category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.quotient_map_coneProjection_comp_shift_assoc {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) {Z : DGHomotopyCategory R (CurvedDGRightModuleCat h)} (h✝ : (dgClosedToHomotopy R).obj ((closedShiftFunctor 1).obj (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map (coneProjection f)) (CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map ((closedShiftFunctor 1).map f)) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The third adjacent composite also vanishes in the curved homotopy category.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneContraction {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.IsIso f] : ↥(dgRightModuleCochains (-1))

The contracting homotopy of the cone of an isomorphism applies its inverse to the second component and includes the result into the first component.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneContraction_apply {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.IsIso f] (x : M.carrier × N.carrier) : ↑(coneContraction f) x = ((closedHom (CategoryTheory.inv f)) x.2, 0)

The contraction sends (x, y) to (f⁻¹ y, 0).

noncomputable def TauCeti.CurvedDGRightModuleCat.coneHomotopyContraction {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) (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M) (α : ↥(dgRightModuleCochains (-1))) (β : ↥(dgRightModuleCochains (-1))) : ↥(dgRightModuleCochains (-1))

A corrected degree-minus-one cochain for a closed map g and cochains α, β. For t = f ∘ α - β ∘ f, its matrix is (α - g ∘ t, g; β ∘ t, -β). It is a contraction when the inverse-homotopy equations in coneHomotopyContraction_boundary hold.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneHomotopyContraction_apply {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) (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M) (α : ↥(dgRightModuleCochains (-1))) (β : ↥(dgRightModuleCochains (-1))) (x : M.carrier × N.carrier) : ↑(coneHomotopyContraction f g α β) x = (↑α x.1 - (closedHom g) ((closedHom f) (↑α x.1) - ↑β ((closedHom f) x.1)) + (closedHom g) x.2, ↑β ((closedHom f) (↑α x.1) - ↑β ((closedHom f) x.1)) - ↑β x.2)

The corrected degree-minus-one cochain has this block formula on the cone carrier.

theorem TauCeti.CurvedDGRightModuleCat.coneHomotopyContraction_boundary {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) (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M) (α : ↥(dgRightModuleCochains (-1))) (β : ↥(dgRightModuleCochains (-1))) (hα : ∀ (x : M.carrier), (closedHom g) ((closedHom f) x) - x = M.differential (↑α x) + ↑α (M.differential x)) (hβ : ∀ (x : N.carrier), (closedHom f) ((closedHom g) x) - x = N.differential (↑β x) + ↑β (N.differential x)) (x : M.carrier × N.carrier) : (cone f).differential (↑(coneHomotopyContraction f g α β) x) + ↑(coneHomotopyContraction f g α β) ((cone f).differential x) = x

Inverse homotopies make the corrected contraction a boundary of the identity. The correction uses the closed odd map t = f ∘ α - β ∘ f, so no coherence between the chosen inverse homotopies, or zero-curvature hypothesis, is required.

theorem TauCeti.CurvedDGRightModuleCat.isZero_homotopy_cone_isIso {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.IsIso ((dgClosedToHomotopy R).map f)] : CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R (cone f))

A closed map which becomes an isomorphism in the homotopy category has a contractible cone.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneHomotopyContraction_inv_zero {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.IsIso f] : coneHomotopyContraction f (CategoryTheory.inv f) 0 0 = coneContraction f

The strict inverse contraction is the zero-homotopy case of the corrected contraction.

theorem TauCeti.CurvedDGRightModuleCat.coneContraction_boundary {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.IsIso f] (x : M.carrier × N.carrier) : (cone f).differential (↑(coneContraction f) x) + ↑(coneContraction f) ((cone f).differential x) = x

The strict contraction boundary follows from the general inverse-homotopy formula.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneMap {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone g)

A square commuting up to the specified odd homotopy induces a closed map of cones.

theorem TauCeti.CurvedDGRightModuleCat.closedHom_coneMap {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) : closedHom (coneMap f g a b k hsq) = (closedHom a).prodMap (closedHom b) + LinearMap.inr Aᵐᵒᵖ M'.carrier N'.carrier ∘ₗ ↑k ∘ₗ LinearMap.fst Aᵐᵒᵖ M.carrier N.carrier

The underlying cone map has the homotopy as its lower-left entry.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_coneMap_apply {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) (x : M.carrier × N.carrier) : (closedHom (coneMap f g a b k hsq)) x = ((closedHom a) x.1, (closedHom b) x.2 + ↑k x.1)

A cone map sends (x, y) to (a x, b y + k x).

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneInclusion_comp_coneMap {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (coneMap f g a b k hsq) = CategoryTheory.CategoryStruct.comp b (coneInclusion g)

Cone maps commute with the canonical inclusions.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneInclusion_comp_coneMap_assoc {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) {Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneInclusion f) (CategoryTheory.CategoryStruct.comp (coneMap f g a b k hsq) h✝) = CategoryTheory.CategoryStruct.comp b (CategoryTheory.CategoryStruct.comp (coneInclusion g) h✝)

Cone maps commute with the canonical inclusions.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneMap_comp_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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) : CategoryTheory.CategoryStruct.comp (coneMap f g a b k hsq) (coneProjection g) = CategoryTheory.CategoryStruct.comp (coneProjection f) ((closedShiftFunctor 1).map a)

Cone maps commute with the canonical projections and the shifted domain map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneMap_comp_coneProjection_assoc {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) {Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M'.shift 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneMap f g a b k hsq) (CategoryTheory.CategoryStruct.comp (coneProjection g) h✝) = CategoryTheory.CategoryStruct.comp (coneProjection f) (CategoryTheory.CategoryStruct.comp ((closedShiftFunctor 1).map a) h✝)

Cone maps commute with the canonical projections and the shifted domain map.

noncomputable def TauCeti.CurvedDGRightModuleCat.coneMapCompHomotopy {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 M' N' : CurvedDGRightModuleCat h} (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (k : ↥(dgRightModuleCochains (-1))) {N'' : CurvedDGRightModuleCat h} (b' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (k' : ↥(dgRightModuleCochains (-1))) : ↥(dgRightModuleCochains (-1))

The homotopy for a composite of two cone-map squares is b' ∘ k + k' ∘ a.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneMapCompHomotopy_apply {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 M' N' : CurvedDGRightModuleCat h} (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (k : ↥(dgRightModuleCochains (-1))) {N'' : CurvedDGRightModuleCat h} (b' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (k' : ↥(dgRightModuleCochains (-1))) (x : M.carrier) : ↑(coneMapCompHomotopy a k b' k') x = (closedHom b') (↑k x) + ↑k' ((closedHom a) x)

The composite square homotopy evaluates by post- and precomposition.

theorem TauCeti.CurvedDGRightModuleCat.coneMapCompHomotopy_boundary {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) {M'' N'' : CurvedDGRightModuleCat h} (j : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M'' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (a' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M'') (b' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (k' : ↥(dgRightModuleCochains (-1))) (hsq' : ∀ (x : M'.carrier), (closedHom b') ((closedHom g) x) - (closedHom j) ((closedHom a') x) = N''.differential (↑k' x) + ↑k' (M'.differential x)) (x : M.carrier) : (closedHom (CategoryTheory.CategoryStruct.comp b b')) ((closedHom f) x) - (closedHom j) ((closedHom (CategoryTheory.CategoryStruct.comp a a')) x) = N''.differential (↑(coneMapCompHomotopy a k b' k') x) + ↑(coneMapCompHomotopy a k b' k') (M.differential x)

The sum of the two square homotopies witnesses the composite square.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneMap_comp {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) {M'' N'' : CurvedDGRightModuleCat h} (j : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M'' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (a' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M'') (b' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (k' : ↥(dgRightModuleCochains (-1))) (hsq' : ∀ (x : M'.carrier), (closedHom b') ((closedHom g) x) - (closedHom j) ((closedHom a') x) = N''.differential (↑k' x) + ↑k' (M'.differential x)) : CategoryTheory.CategoryStruct.comp (coneMap f g a b k hsq) (coneMap g j a' b' k' hsq') = coneMap f j (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') (coneMapCompHomotopy a k b' k') ⋯

Cone maps compose using the induced composite square homotopy.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneMap_comp_assoc {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) {M' N' : CurvedDGRightModuleCat h} (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (a : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M') (b : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N') (k : ↥(dgRightModuleCochains (-1))) (hsq : ∀ (x : M.carrier), (closedHom b) ((closedHom f) x) - (closedHom g) ((closedHom a) x) = N'.differential (↑k x) + ↑k (M.differential x)) {M'' N'' : CurvedDGRightModuleCat h} (j : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M'' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (a' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M'') (b' : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N' ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N'') (k' : ↥(dgRightModuleCochains (-1))) (hsq' : ∀ (x : M'.carrier), (closedHom b') ((closedHom g) x) - (closedHom j) ((closedHom a') x) = N''.differential (↑k' x) + ↑k' (M'.differential x)) {Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (coneMap f g a b k hsq) (CategoryTheory.CategoryStruct.comp (coneMap g j a' b' k' hsq') h✝) = CategoryTheory.CategoryStruct.comp (coneMap f j (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') (coneMapCompHomotopy a k b' k') ⋯) h✝

Cone maps compose using the induced composite square homotopy.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coneMap_id {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) : coneMap f f (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M)) (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N)) 0 ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone f))

The cone map of the identity square with zero homotopy is the identity.

theorem TauCeti.CurvedDGRightModuleCat.quotient_map_eq_zero_iff_factors_coneIdentity {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) : (dgClosedToHomotopy R).map f = 0 ↔ ∃ (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M))) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N), CategoryTheory.CategoryStruct.comp (coneInclusion (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M))) g = f

A closed map is null-homotopic exactly when it factors through the identity cone of its source via the canonical inclusion.