Coproducts of curved differential graded right modules #
The external direct sum of a family of curved right modules over one curved DG algebra, with the componentwise grading, right action and differential, is again a curved right module of the same curvature. Its summand inclusions are closed morphisms, and it is the coproduct of the family in the closed degree-zero category.
The quotient functor to the curved homotopy category carries this coproduct to a coproduct. A
morphism out of the direct sum in the homotopy category lifts to a closed morphism by fullness of
the quotient functor. For uniqueness, odd homotopies chosen on the summands glue, through the
direct-sum universal property, to an odd homotopy on the direct sum. Hence the curved homotopy
category has all coproducts indexed by Type u. These are the coproducts under which the
coacyclic objects of the second kind are closed.
Main definitions #
TauCeti.CurvedDGRightModuleCat.directSum: the direct sum of a family of curved right modules.TauCeti.CurvedDGRightModuleCat.closedDirectSumCofan: the cofan of closed summand inclusions.TauCeti.CurvedDGRightModuleCat.homotopyDirectSumCofan: its image in the curved homotopy category.
Main results #
TauCeti.CurvedDGRightModuleCat.closedDirectSumCofanIsColimit: the direct sum is a coproduct in the closed degree-zero category.TauCeti.CurvedDGRightModuleCat.dgClosedToHomotopy_map_directSum_ext: closed maps out of a direct sum are homotopic as soon as their restrictions to all summands are.TauCeti.CurvedDGRightModuleCat.homotopyDirectSumCofanIsColimit: the direct sum is a coproduct in the curved homotopy category.- The
HasCoproductsinstances on the closed and homotopy categories, and the preservation of all coproducts indexed byType uby the quotient functor.
References #
- L. Positselski, Differential graded Koszul duality: an introductory survey, Bull. Lond. Math. Soc. 55 (2023), 1553–1640, Section 7.6.
- The Tau Ceti contributors,
TauCeti.Algebra.Category.GradedModuleCat.Coproducts.Basic: the direct-sum universal property follows the corresponding construction for graded modules.
@[implicit_reducible]
noncomputable def
TauCeti.CurvedDGRightModuleCat.directSum
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{w : A}
{h : IsCurvedDGAlgebra 𝒜 d w}
{J : Type uJ}
(M : J → CurvedDGRightModuleCat h)
:
The direct sum of a family of curved right modules, with componentwise grading, right action and differential.
Instances For
theorem
TauCeti.CurvedDGRightModuleCat.directSum_grading
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{w : A}
{h : IsCurvedDGAlgebra 𝒜 d w}
{J : Type uJ}
(M : J → CurvedDGRightModuleCat h)
:
(directSum M).grading = InternalGrading.directSumPiece fun (j : J) => InternalGrading.ofDecomposition (M j).grading
The homogeneous pieces of the direct sum are those of the direct-sum grading.
@[simp]
theorem
TauCeti.CurvedDGRightModuleCat.mem_directSum_grading_iff
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{w : A}
{h : IsCurvedDGAlgebra 𝒜 d w}
{J : Type uJ}
(M : J → CurvedDGRightModuleCat h)
(p : ℤ)
(x : DirectSum J fun (j : J) => (M j).carrier)
:
Membership in a homogeneous piece of the direct sum is componentwise.
theorem
TauCeti.CurvedDGRightModuleCat.directSum_differential
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{w : A}
{h : IsCurvedDGAlgebra 𝒜 d w}
{J : Type uJ}
(M : J → CurvedDGRightModuleCat h)
:
The differential of the direct sum is componentwise.
@[simp]
theorem
TauCeti.CurvedDGRightModuleCat.directSum_differential_apply
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{w : A}
{h : IsCurvedDGAlgebra 𝒜 d w}
{J : Type uJ}
(M : J → CurvedDGRightModuleCat h)
(x : DirectSum J fun (j : J) => (M j).carrier)
(j : J)
:
Each component of the direct-sum differential is the differential of that summand. The
coercion to functions is written out because the carrier of directSum M is not syntactically a
function type; it is the one DirectSum.ext produces.
@[simp]
theorem
TauCeti.CurvedDGRightModuleCat.directSum_differential_of
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{w : A}
{h : IsCurvedDGAlgebra 𝒜 d w}
{J : Type uJ}
(M : J → CurvedDGRightModuleCat h)
[DecidableEq J]
(j : J)
(x : (M j).carrier)
:
(directSum M).differential ((DirectSum.of (fun (j : J) => (M j).carrier) j) x) = (DirectSum.of (fun (j : J) => (M j).carrier) j) ((M j).differential x)
The differential of the direct sum preserves each summand.
theorem
TauCeti.CurvedDGRightModuleCat.toModule_comp_directSum_differential
{R : Type uR}
{A : Type uA}
[CommRing R]
[Ring A]
[Algebra R A]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{w : A}
{h : IsCurvedDGAlgebra 𝒜 d w}
{J : Type uJ}
(M : J → CurvedDGRightModuleCat h)
[DecidableEq J]
{N : Type uN}
[AddCommGroup N]
[Module R N]
[Module Aᵐᵒᵖ N]
[IsScalarTower R Aᵐᵒᵖ N]
(φ : (j : J) → (M j).carrier →ₗ[Aᵐᵒᵖ] N)
:
↑R (DirectSum.toModule Aᵐᵒᵖ J N φ) ∘ₗ (directSum M).differential = DirectSum.toModule R J N fun (j : J) => ↑R (φ j) ∘ₗ (M j).differential
Precomposing a direct-sum universal map with the differential of the direct sum gives the universal map of the summand maps precomposed with the summand differentials.
noncomputable def
TauCeti.CurvedDGRightModuleCat.closedDirectSumι
{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)
:
The inclusion of a summand into the direct sum, as a closed morphism.
Instances For
@[simp]
theorem
TauCeti.CurvedDGRightModuleCat.closedHom_closedDirectSumι
{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)
[hJ : DecidableEq J]
(j : J)
:
The closed summand inclusion is the direct-sum inclusion.
noncomputable def
TauCeti.CurvedDGRightModuleCat.closedDirectSumDesc
{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) ℤ) (M j) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N)
:
The closed morphism out of the direct sum restricting to a prescribed family of closed morphisms on the summands.
Instances For
@[simp]
theorem
TauCeti.CurvedDGRightModuleCat.closedHom_closedDirectSumDesc
{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)
[hJ : DecidableEq J]
{N : CurvedDGRightModuleCat h}
(f :
(j : J) →
CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N)
:
closedHom (closedDirectSumDesc f) = DirectSum.toModule Aᵐᵒᵖ J N.carrier fun (j : J) => closedHom (f j)
The closed morphism out of the direct sum is the direct-sum universal map.
@[simp]
theorem
TauCeti.CurvedDGRightModuleCat.closedDirectSumι_desc
{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) ℤ) (M j) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N)
(j : J)
:
The closed morphism out of the direct sum restricts to the prescribed morphisms.
@[simp]
theorem
TauCeti.CurvedDGRightModuleCat.closedDirectSumι_desc_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) ℤ) (M j) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N)
(j : J)
{Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)}
(h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ Z)
:
The closed morphism out of the direct sum restricts to the prescribed morphisms.
theorem
TauCeti.CurvedDGRightModuleCat.closedDirectSum_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) ℤ) (directSum M) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N}
(hfg :
∀ (j : J),
CategoryTheory.CategoryStruct.comp (closedDirectSumι M j) f = CategoryTheory.CategoryStruct.comp (closedDirectSumι M j) g)
:
Closed morphisms out of the direct sum are determined by their restrictions to the summands.
@[reducible, inline]
noncomputable abbrev
TauCeti.CurvedDGRightModuleCat.closedDirectSumCofan
{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.Cofan fun (j : J) => CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j)
The cofan of closed summand inclusions into the direct sum.
Instances For
noncomputable def
TauCeti.CurvedDGRightModuleCat.closedDirectSumCofanIsColimit
{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)
:
The direct sum is the coproduct in the closed degree-zero category.
Instances For
instance
TauCeti.CurvedDGRightModuleCat.instHasCoproductForgetEnrichmentCochainComplexModuleCatInt
{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))
:
instance
TauCeti.CurvedDGRightModuleCat.instHasCoproductsForgetEnrichmentCochainComplexModuleCatInt
{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}
:
theorem
TauCeti.CurvedDGRightModuleCat.dgClosedToHomotopy_map_directSum_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) ℤ) (directSum M) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N}
(hfg :
∀ (j : J),
(dgClosedToHomotopy R).map (CategoryTheory.CategoryStruct.comp (closedDirectSumι M j) f) = (dgClosedToHomotopy R).map (CategoryTheory.CategoryStruct.comp (closedDirectSumι M j) g))
:
Two closed morphisms out of a direct sum are homotopic as soon as their restrictions to all summands are: odd homotopies on the summands glue to an odd homotopy on the direct sum.
@[reducible, inline]
noncomputable abbrev
TauCeti.CurvedDGRightModuleCat.homotopyDirectSumCofan
{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.Cofan fun (j : J) => DGHomotopyCategory.of R (M j)
The cofan of homotopy classes of the summand inclusions into the direct sum.
Instances For
noncomputable def
TauCeti.CurvedDGRightModuleCat.homotopyDirectSumCofanIsColimit
{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)
:
The direct sum is the coproduct in the curved homotopy category.
Instances For
instance
TauCeti.CurvedDGRightModuleCat.instPreservesColimitForgetEnrichmentCochainComplexModuleCatIntDGHomotopyCategoryDiscreteFunctorOfDgClosedToHomotopy
{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.PreservesColimit
(CategoryTheory.Discrete.functor fun (j : J) =>
CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M j))
(dgClosedToHomotopy R)
The quotient functor to the curved homotopy category preserves the direct-sum coproducts.
instance
TauCeti.CurvedDGRightModuleCat.instPreservesColimitsOfShapeForgetEnrichmentCochainComplexModuleCatIntDGHomotopyCategoryDiscreteDgClosedToHomotopy
{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}
:
The quotient functor to the curved homotopy category preserves all coproducts indexed by
J.
instance
TauCeti.CurvedDGRightModuleCat.instHasCoproductDGHomotopyCategory
{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))
:
instance
TauCeti.CurvedDGRightModuleCat.instHasCoproductsDGHomotopyCategory
{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}
: