Small products of graded modules

The categorical product has the degreewise product grading. Its total module is the submodule of the Cartesian product consisting of finite sums of homogeneous families, as constructed by InternalGrading.product. A degree-zero family of maps has values in this submodule because the finite degree support of a source element controls all of its images simultaneously.

The finite direct-sum product fan in GradedModuleCat.Abelian also applies when the scalar pieces do not decompose the algebra. The degreewise fan here allows arbitrary index types and uses the graded-algebra decomposition to keep the total product stable under scalars.

@[implicit_reducible]

noncomputable def TauCeti.GradedModuleCat.product {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) : GradedModuleCat 𝒜

The degreewise product of graded modules, with finite total degree support.

@[simp]

theorem TauCeti.GradedModuleCat.mem_product_piece_iff {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) (p : ℤ) (x : (product M).carrier) : x ∈ (product M).grading.piece ℤ p ↔ ∀ (j : J), ↑x j ∈ (M j).grading.piece ℤ p

The product grading is checked in every component.

noncomputable def TauCeti.GradedModuleCat.productπ {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) (j : J) : product M ⟶ M j

The graded projection to one factor.

@[simp]

theorem TauCeti.GradedModuleCat.productπ_apply {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) (j : J) (x : (product M).carrier) : (productπ M j).hom x = ↑x j

The projection is the corresponding coordinate of the family.

noncomputable def TauCeti.GradedModuleCat.productLift {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) {N : GradedModuleCat 𝒜} (f : (j : J) → N ⟶ M j) : N ⟶ product M

A family of degree-zero maps lifts into the degreewise product.

@[simp]

theorem TauCeti.GradedModuleCat.productLift_apply {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) {N : GradedModuleCat 𝒜} (f : (j : J) → N ⟶ M j) (x : N.carrier) (j : J) : ↑((productLift M f).hom x) j = (f j).hom x

The lift has the prescribed components.

@[simp]

theorem TauCeti.GradedModuleCat.productLift_π {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) {N : GradedModuleCat 𝒜} (f : (j : J) → N ⟶ M j) (j : J) : CategoryTheory.CategoryStruct.comp (productLift M f) (productπ M j) = f j

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

@[simp]

theorem TauCeti.GradedModuleCat.productLift_π_assoc {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) {N : GradedModuleCat 𝒜} (f : (j : J) → N ⟶ M j) (j : J) {Z : GradedModuleCat 𝒜} (h : M j ⟶ Z) : CategoryTheory.CategoryStruct.comp (productLift M f) (CategoryTheory.CategoryStruct.comp (productπ M j) h) = CategoryTheory.CategoryStruct.comp (f j) h

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

theorem TauCeti.GradedModuleCat.product_hom_ext {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) {N : GradedModuleCat 𝒜} {f g : N ⟶ product M} (hfg : ∀ (j : J), CategoryTheory.CategoryStruct.comp f (productπ M j) = CategoryTheory.CategoryStruct.comp g (productπ M j)) : f = g

Maps into the product are determined by their projections.

@[reducible, inline]

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

The fan of graded product projections.

noncomputable def TauCeti.GradedModuleCat.degreewiseProductFanIsLimit {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (M : J → GradedModuleCat 𝒜) : CategoryTheory.Limits.IsLimit (degreewiseProductFan M)

The degreewise product satisfies the categorical product universal property.

instance TauCeti.GradedModuleCat.hasProductDegreewise {k : Type uk} {A : Type uA} [CommRing k] [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] {J : Type v} (X : J → GradedModuleCat 𝒜) : CategoryTheory.Limits.HasProduct X

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