Small products of curved differential graded right modules

The product is formed degreewise in the category of graded right modules. Its elements are families with common finite degree support. The differential and right action are componentwise, so the right Leibniz rule and the common-curvature identity hold in every component. This is the graded product rather than the unrestricted product of the underlying total modules.

Closed maps into this product have the expected universal property. The homotopy quotient preserves it: a family of odd homotopies into the factors has a common degree of minus one, so the finite degree support of a source element also controls the family of its homotopy images. Consequently the component homotopies lift into the graded product and prove uniqueness in the quotient. Existence uses fullness of the closed-to-homotopy quotient functor.

No centrality or zero-curvature hypothesis is imposed.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.
• The Tau Ceti contributors, Curved.Module.Right.Coproduct: the quotient universal-property proof is dualized, using homogeneous product lifts in place of direct-sum descent.

theorem TauCeti.CurvedDGRightModuleCat.instGradedMonoidIntSubmodulePieceOfDecomposition {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] : SetLike.GradedMonoid ((InternalGrading.ofDecomposition 𝒜).piece ℤ)

noncomputable def TauCeti.CurvedDGRightModuleCat.productDifferential {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : (GradedModuleCat.product fun (j : J) => (M j).toGradedModuleCat).carrier →ₗ[R] (GradedModuleCat.product fun (j : J) => (M j).toGradedModuleCat).carrier

The componentwise differential on the underlying degreewise graded product.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.productDifferential_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} {J : Type u} (M : J → CurvedDGRightModuleCat h) (x : (GradedModuleCat.product fun (j : J) => (M j).toGradedModuleCat).carrier) (j : J) : ↑((productDifferential M) x) j = (M j).differential (↑x j)

The differential of the graded product is computed in each factor.

@[implicit_reducible]

noncomputable def TauCeti.CurvedDGRightModuleCat.product {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : CurvedDGRightModuleCat h

The degreewise product with componentwise curved differential.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.mem_product_grading_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} {J : Type u} (M : J → CurvedDGRightModuleCat h) (p : ℤ) (x : (product M).carrier) : x ∈ (product M).grading p ↔ ∀ (j : J), ↑x j ∈ (M j).grading p

Product homogeneity is componentwise homogeneity of the family.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.product_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} {J : Type u} (M : J → CurvedDGRightModuleCat h) (x : (product M).carrier) (j : J) : ↑((product M).differential x) j = (M j).differential (↑x j)

The product differential is the differential in each factor.

noncomputable def TauCeti.CurvedDGRightModuleCat.forgetDifferentialProductIso {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : forgetDifferential.obj (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (product M)) ≅ GradedModuleCat.product fun (j : J) => (M j).toGradedModuleCat

Forgetting the product differential gives the degreewise graded product.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.forgetDifferentialProductIso_hom_hom {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : (forgetDifferentialProductIso M).hom.hom = LinearMap.id

The comparison with the graded product is the identity on underlying families.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.forgetDifferentialProductIso_inv_hom {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : (forgetDifferentialProductIso M).inv.hom = LinearMap.id

The inverse comparison is also the identity on underlying families.

noncomputable def TauCeti.CurvedDGRightModuleCat.closedProductπ {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) (j : J) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (product M) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)

The closed projection to one factor of the product.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedProductπ_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} {J : Type u} (M : J → CurvedDGRightModuleCat h) (j : J) (x : (product M).carrier) : (closedHom (closedProductπ M j)) x = ↑x j

On elements the closed projection is coordinate evaluation.

noncomputable def TauCeti.CurvedDGRightModuleCat.closedProductLift {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) {N : CurvedDGRightModuleCat h} (f : (j : J) → CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (product M)

A family of closed maps lifts into the degreewise product.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedProductLift_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} {J : Type u} (M : J → CurvedDGRightModuleCat h) {N : CurvedDGRightModuleCat h} (f : (j : J) → CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)) (x : N.carrier) (j : J) : ↑((closedHom (closedProductLift M f)) x) j = (closedHom (f j)) x

The lifted closed map has the prescribed components.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedProductLift_π {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) {N : CurvedDGRightModuleCat h} (f : (j : J) → CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)) (j : J) : CategoryTheory.CategoryStruct.comp (closedProductLift M f) (closedProductπ M j) = f j

The lifted closed map followed by a projection is the prescribed component.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedProductLift_π_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} {J : Type u} (M : J → CurvedDGRightModuleCat h) {N : CurvedDGRightModuleCat h} (f : (j : J) → CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)) (j : J) {Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (closedProductLift M f) (CategoryTheory.CategoryStruct.comp (closedProductπ M j) h✝) = CategoryTheory.CategoryStruct.comp (f j) h✝

The lifted closed map followed by a projection is the prescribed component.

theorem TauCeti.CurvedDGRightModuleCat.closedProduct_hom_ext {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) {N : CurvedDGRightModuleCat h} {f g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (product M)} (hfg : ∀ (j : J), CategoryTheory.CategoryStruct.comp f (closedProductπ M j) = CategoryTheory.CategoryStruct.comp g (closedProductπ M j)) : f = g

Closed maps into the product are determined by their projections.

@[reducible, inline]

noncomputable abbrev TauCeti.CurvedDGRightModuleCat.closedProductFan {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : CategoryTheory.Limits.Fan fun (j : J) => CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)

The fan of closed projections from the degreewise product.

noncomputable def TauCeti.CurvedDGRightModuleCat.closedProductFanIsLimit {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : CategoryTheory.Limits.IsLimit (closedProductFan M)

The degreewise product is a product in the closed degree-zero category.

instance TauCeti.CurvedDGRightModuleCat.instHasProductForgetEnrichmentCochainComplexModuleCatInt {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} {J : Type u} (X : J → CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) : CategoryTheory.Limits.HasProduct X

instance TauCeti.CurvedDGRightModuleCat.instHasProductsForgetEnrichmentCochainComplexModuleCatInt {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.Limits.HasProducts (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))

theorem TauCeti.CurvedDGRightModuleCat.dgClosedToHomotopy_map_product_ext {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) {N : CurvedDGRightModuleCat h} {f g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (product M)} (hfg : ∀ (j : J), (dgClosedToHomotopy R).map (CategoryTheory.CategoryStruct.comp f (closedProductπ M j)) = (dgClosedToHomotopy R).map (CategoryTheory.CategoryStruct.comp g (closedProductπ M j))) : (dgClosedToHomotopy R).map f = (dgClosedToHomotopy R).map g

Componentwise homotopies glue to a homotopy into the product. Their common degree of minus one gives a uniform finite degree support on each source element.

@[reducible, inline]

noncomputable abbrev TauCeti.CurvedDGRightModuleCat.homotopyProductFan {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : CategoryTheory.Limits.Fan fun (j : J) => DGHomotopyCategory.of R (M j)

The fan of homotopy classes of the product projections.

noncomputable def TauCeti.CurvedDGRightModuleCat.homotopyProductFanIsLimit {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : CategoryTheory.Limits.IsLimit (homotopyProductFan M)

The degreewise product is a product in the curved homotopy category.

instance TauCeti.CurvedDGRightModuleCat.instPreservesLimitForgetEnrichmentCochainComplexModuleCatIntDGHomotopyCategoryDiscreteFunctorOfDgClosedToHomotopy {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} {J : Type u} (M : J → CurvedDGRightModuleCat h) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun (j : J) => CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)) (dgClosedToHomotopy R)

The quotient functor preserves the degreewise products.

instance TauCeti.CurvedDGRightModuleCat.instPreservesLimitsOfShapeForgetEnrichmentCochainComplexModuleCatIntDGHomotopyCategoryDiscreteDgClosedToHomotopy {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} {J : Type u} : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) (dgClosedToHomotopy R)

The quotient functor preserves all products indexed by J.

instance TauCeti.CurvedDGRightModuleCat.instHasProductDGHomotopyCategory {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} {J : Type u} (X : J → DGHomotopyCategory R (CurvedDGRightModuleCat h)) : CategoryTheory.Limits.HasProduct X

instance TauCeti.CurvedDGRightModuleCat.instHasProductsDGHomotopyCategory {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.Limits.HasProducts (DGHomotopyCategory R (CurvedDGRightModuleCat h))