Finite biproducts of curved differential graded right modules

The zero right module and componentwise products carry curved differentials of the same curvature. Their closed maps give a zero object and binary biproducts in the existing closed category. These constructions will also supply the finite sums used by mapping cones. The additive quotient functor sends the componentwise bicones to biproduct bicones in the existing curved homotopy category, which therefore also has a zero object and finite biproducts.

@[implicit_reducible]

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

The zero curved right module, with all homogeneous pieces and differential zero.

instance TauCeti.CurvedDGRightModuleCat.instSubsingletonCarrierZero {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) : Subsingleton (zero h).carrier

@[implicit_reducible]

noncomputable def TauCeti.CurvedDGRightModuleCat.prod {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} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) : CurvedDGRightModuleCat h

The product curved right module has componentwise grading, action and differential.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.prod_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} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) (p : ℤ) : (M.prod N).grading p = (M.grading p).prod (N.grading p)

The product grading is componentwise.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.prod_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} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) (x : M.carrier × N.carrier) : (M.prod N).differential x = (M.differential x.1, N.differential x.2)

The product differential is componentwise.

theorem TauCeti.CurvedDGRightModuleCat.isZero_closed_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} : CategoryTheory.Limits.IsZero (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (zero h))

The zero curved module is a zero object in the closed category.

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

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

The first projection of the product is a closed morphism.

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

The second projection of the product is a closed morphism.

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

The first inclusion in the product is a closed morphism.

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

The second inclusion in the product is a closed morphism.

@[simp]

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

The first closed projection is the usual linear projection.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedProdSnd {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) : closedHom (M.closedProdSnd N) = LinearMap.snd Aᵐᵒᵖ M.carrier N.carrier

The second closed projection is the usual linear projection.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedProdInl {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) : closedHom (M.closedProdInl N) = LinearMap.inl Aᵐᵒᵖ M.carrier N.carrier

The first closed inclusion is the usual linear inclusion.

@[simp]

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

The second closed inclusion is the usual linear inclusion.

noncomputable def TauCeti.CurvedDGRightModuleCat.closedProdBicone {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) : CategoryTheory.Limits.BinaryBicone (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M) (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N)

The four componentwise maps form a binary bicone in the closed category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedProdBicone_pt {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) : (M.closedProdBicone N).pt = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M.prod N)

The point of the closed product bicone is the componentwise product.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedProdBicone_fst {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) : (M.closedProdBicone N).fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (M.closedProdFst N)

The first projection of the closed bicone is the componentwise closed map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedProdBicone_snd {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) : (M.closedProdBicone N).snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (M.closedProdSnd N)

The second projection of the closed bicone is the componentwise closed map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedProdBicone_inl {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) : (M.closedProdBicone N).inl = CategoryTheory.CategoryStruct.comp (M.closedProdInl N) (CategoryTheory.eqToHom ⋯)

The first inclusion of the closed bicone is the componentwise closed map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedProdBicone_inr {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) : (M.closedProdBicone N).inr = CategoryTheory.CategoryStruct.comp (M.closedProdInr N) (CategoryTheory.eqToHom ⋯)

The second inclusion of the closed bicone is the componentwise closed map.

noncomputable def TauCeti.CurvedDGRightModuleCat.closedProdBiconeIsBilimit {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) : (M.closedProdBicone N).IsBilimit

The componentwise bicone is both a limit and a colimit.

instance TauCeti.CurvedDGRightModuleCat.instHasBinaryBiproductForgetEnrichmentCochainComplexModuleCatInt {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} (X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) : CategoryTheory.Limits.HasBinaryBiproduct X Y

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

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

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

theorem TauCeti.CurvedDGRightModuleCat.isZero_homotopy_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} : CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R (zero h))

The class of the zero curved module is a zero object.

instance TauCeti.CurvedDGRightModuleCat.instHasZeroObjectDGHomotopyCategory {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.HasZeroObject (DGHomotopyCategory R (CurvedDGRightModuleCat h))

noncomputable def TauCeti.CurvedDGRightModuleCat.homotopyProdBicone {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) : CategoryTheory.Limits.BinaryBicone (DGHomotopyCategory.of R M) (DGHomotopyCategory.of R N)

The componentwise product bicone in the curved homotopy category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homotopyProdBicone_pt {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) : (M.homotopyProdBicone N).pt = DGHomotopyCategory.of R (M.prod N)

The point of the product bicone is the class of the componentwise product.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homotopyProdBicone_fst {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) : (M.homotopyProdBicone N).fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((dgClosedToHomotopy R).map (M.closedProdFst N))

The first homotopy projection is the class of the first closed projection.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homotopyProdBicone_snd {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) : (M.homotopyProdBicone N).snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((dgClosedToHomotopy R).map (M.closedProdSnd N))

The second homotopy projection is the class of the second closed projection.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homotopyProdBicone_inl {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) : (M.homotopyProdBicone N).inl = CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map (M.closedProdInl N)) (CategoryTheory.eqToHom ⋯)

The first homotopy inclusion is the class of the first closed inclusion.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homotopyProdBicone_inr {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) : (M.homotopyProdBicone N).inr = CategoryTheory.CategoryStruct.comp ((dgClosedToHomotopy R).map (M.closedProdInr N)) (CategoryTheory.eqToHom ⋯)

The second homotopy inclusion is the class of the second closed inclusion.

noncomputable def TauCeti.CurvedDGRightModuleCat.homotopyProdBiconeIsBilimit {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) : (M.homotopyProdBicone N).IsBilimit

The componentwise bicone is a biproduct in the homotopy category.

instance TauCeti.CurvedDGRightModuleCat.instHasBinaryBiproductDGHomotopyCategory {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} (X Y : DGHomotopyCategory R (CurvedDGRightModuleCat h)) : CategoryTheory.Limits.HasBinaryBiproduct X Y

instance TauCeti.CurvedDGRightModuleCat.instHasBinaryBiproductsDGHomotopyCategory {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.HasBinaryBiproducts (DGHomotopyCategory R (CurvedDGRightModuleCat h))

instance TauCeti.CurvedDGRightModuleCat.instHasFiniteProductsDGHomotopyCategory {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.HasFiniteProducts (DGHomotopyCategory R (CurvedDGRightModuleCat h))

instance TauCeti.CurvedDGRightModuleCat.instHasFiniteBiproductsDGHomotopyCategory {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.HasFiniteBiproducts (DGHomotopyCategory R (CurvedDGRightModuleCat h))