Coproducts of internally graded modules

The existing degreewise direct sum is a coproduct in GradedModuleCat. Its injections and universal map have internal degree zero, so the underlying direct-sum universal property lifts from modules to graded modules. The forgetful functor to modules preserves these coproducts.

The universal property follows ModuleCat.coproductCoconeIsColimit in Mathlib.Algebra.Category.ModuleCat.Products. The grading argument is InternalGrading.toModule_mem_of_mem_directSumPiece, as in GradedModuleCat.freeLift.

These coproducts provide the sums required for Mathlib's totalization of cochain bifunctors, including balanced tensor composition of graded bimodule complexes.

@[reducible, inline]

noncomputable abbrev TauCeti.GradedModuleCat.coproductCofan {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) : CategoryTheory.Limits.Cofan M

The cofan of the direct-sum injections, each of internal degree zero. The abbreviation retains the concrete point for computations with direct-sum elements.

@[simp]

theorem TauCeti.GradedModuleCat.hom_coproductCofan_inj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) [hJ : DecidableEq J] (j : J) : ((coproductCofan M).inj j).hom = DirectSum.lof A J (fun (j : J) => (M j).carrier) j

The underlying map of a coproduct injection is the direct-sum inclusion.

theorem TauCeti.GradedModuleCat.mem_coproductCofan_pt_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) {p : ℤ} {x : (coproductCofan M).pt.carrier} : x ∈ (coproductCofan M).pt.grading.piece ℤ p ↔ ∀ (j : J), x j ∈ (M j).grading.piece ℤ p

Membership in a degree piece of the coproduct is componentwise.

noncomputable def TauCeti.GradedModuleCat.coproductDesc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) (s : CategoryTheory.Limits.Cofan M) : (coproductCofan M).pt ⟶ s.pt

Extend a cofan of graded maps along the direct-sum universal property.

@[simp]

theorem TauCeti.GradedModuleCat.hom_coproductDesc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) [hJ : DecidableEq J] (s : CategoryTheory.Limits.Cofan M) : (coproductDesc M s).hom = DirectSum.toModule A J s.pt.carrier fun (j : J) => (s.inj j).hom

The underlying universal map is the direct-sum universal linear map.

@[simp]

theorem TauCeti.GradedModuleCat.coproductCofan_inj_desc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) (s : CategoryTheory.Limits.Cofan M) (j : J) : CategoryTheory.CategoryStruct.comp ((coproductCofan M).inj j) (coproductDesc M s) = s.inj j

The universal map restricts to the prescribed map on each summand.

@[simp]

theorem TauCeti.GradedModuleCat.coproductCofan_inj_desc_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) (s : CategoryTheory.Limits.Cofan M) (j : J) {Z : GradedModuleCat 𝒜} (h : s.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((coproductCofan M).inj j) (CategoryTheory.CategoryStruct.comp (coproductDesc M s) h) = CategoryTheory.CategoryStruct.comp (s.inj j) h

The universal map restricts to the prescribed map on each summand.

noncomputable def TauCeti.GradedModuleCat.coproductCofanIsColimit {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) : CategoryTheory.Limits.IsColimit (coproductCofan M)

The direct sum of internally graded modules is their categorical coproduct.

instance TauCeti.GradedModuleCat.instHasCoproduct {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) : CategoryTheory.Limits.HasCoproduct M

instance TauCeti.GradedModuleCat.instHasCoproducts {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} : CategoryTheory.Limits.HasCoproducts (GradedModuleCat 𝒜)

instance TauCeti.GradedModuleCat.instPreservesColimitModuleCatDiscreteFunctorToModuleCat {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor M) toModuleCat

instance TauCeti.GradedModuleCat.projective_directSumObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) [∀ (j : J), CategoryTheory.Projective (M j)] : CategoryTheory.Projective (directSumObj M)

A degreewise direct sum of projective graded modules is projective, with no finiteness assumption on the index type.

theorem TauCeti.GradedModuleCat.finrank_hom_directSumObj {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {J : Type w} (M : J → GradedModuleCat 𝒜) [Fintype J] [StrongRankCondition k] (N : GradedModuleCat 𝒜) [∀ (j : J), Module.Free k (M j ⟶ N)] [∀ (j : J), Module.Finite k (M j ⟶ N)] : Module.finrank k (directSumObj M ⟶ N) = ∑ j : J, Module.finrank k (M j ⟶ N)

The dimension of graded maps from a finite degreewise direct sum is the sum of the Hom dimensions of its summands. The Hom modules must be finite and free over k.