Closed boundaries of odd homotopies of curved right modules

An odd right-linear homotopy has a closed boundary dN ∘ k + k ∘ dM. Its class in the existing curved homotopy category is zero, and two closed maps have the same class precisely when their difference is such a boundary. The construction reuses the zero-cocycle equivalence and square-zero Hom differential of curved modules of the same curvature. An object is zero in this quotient exactly when its identity admits a contraction.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 6.2.
• The Tau Ceti contributors, TauCeti.Algebra.Homology.Curved.Frobenius: the contractibility characterization follows the corresponding componentwise split construction.

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

The boundary of an odd homotopy is a closed morphism of curved right modules.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedHomotopyBoundary_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} (k : ↥(dgRightModuleCochains (-1))) (x : M.carrier) : (closedHom (closedHomotopyBoundary k)) x = N.differential (↑k x) + ↑k (M.differential x)

The underlying map of the closed boundary is dN ∘ k + k ∘ dM.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homOf_closedHomotopyBoundary {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} (k : ↥(dgRightModuleCochains (-1))) : DGHomotopyCategory.homOf R (dgClosedHom R (closedHomotopyBoundary k)) ⋯ = 0

The class of a closed homotopy boundary is zero.

theorem TauCeti.CurvedDGRightModuleCat.quotient_map_eq_iff_exists_homotopy {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 g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : (dgClosedToHomotopy R).map f = (dgClosedToHomotopy R).map g ↔ ∃ (k : ↥(dgRightModuleCochains (-1))), ∀ (x : M.carrier), (closedHom f) x - (closedHom g) x = N.differential (↑k x) + ↑k (M.differential x)

Two closed maps have the same homotopy class exactly when an odd homotopy gives their pointwise difference as a boundary.

theorem TauCeti.CurvedDGRightModuleCat.isZero_homotopy_iff_exists_contraction {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} (P : CurvedDGRightModuleCat h) : CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R P) ↔ ∃ (k : ↥(dgRightModuleCochains (-1))), ∀ (x : P.carrier), P.differential (↑k x) + ↑k (P.differential x) = x

A curved module is zero in the homotopy category exactly when it admits a contraction.