The concrete products in the category of modules are products in the categorical sense. #
The product cone induced by the concrete product.
Instances For
The concrete product cone is limiting.
Instances For
noncomputable def
ModuleCat.piIsoPi
{R : Type u}
[Ring R]
{ι : Type v}
(Z : ι → ModuleCatMax R)
[CategoryTheory.Limits.HasProduct Z]
:
∏ Z ≅ ModuleCat.of R ((i : ι) → ↑(Z i))
The categorical product of a family of objects in ModuleCat
agrees with the usual module-theoretical product.
Instances For
theorem
ModuleCat.piIsoPi_inv_kernel_ι_apply
{R : Type u}
[Ring R]
{ι : Type v}
(Z : ι → ModuleCatMax R)
[CategoryTheory.Limits.HasProduct Z]
(i : ι)
(x : (CategoryTheory.forget (ModuleCatMax R)).obj
{ cone := ModuleCat.productCone Z, isLimit := ModuleCat.productConeIsLimit Z }.cone.pt)
:
↑(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor Z) { as := i })
(↑(CategoryTheory.Limits.limit.isoLimitCone
{ cone := ModuleCat.productCone Z, isLimit := ModuleCat.productConeIsLimit Z }).inv
x) = ↑((ModuleCat.productCone Z).π.app { as := i }) x
@[simp]
theorem
ModuleCat.piIsoPi_inv_kernel_ι
{R : Type u}
[Ring R]
{ι : Type v}
(Z : ι → ModuleCatMax R)
[CategoryTheory.Limits.HasProduct Z]
(i : ι)
:
theorem
ModuleCat.piIsoPi_hom_ker_subtype_apply
{R : Type u}
[Ring R]
{ι : Type v}
(Z : ι → ModuleCatMax R)
[CategoryTheory.Limits.HasProduct Z]
(i : ι)
(x : (CategoryTheory.forget (ModuleCatMax R)).obj (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor Z)).pt)
:
↑((ModuleCat.productCone Z).π.app { as := i })
(↑(CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (ModuleCat.productConeIsLimit Z)
(CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor Z))).inv
x) = ↑(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor Z) { as := i }) x
@[simp]
theorem
ModuleCat.piIsoPi_hom_ker_subtype
{R : Type u}
[Ring R]
{ι : Type v}
(Z : ι → ModuleCatMax R)
[CategoryTheory.Limits.HasProduct Z]
(i : ι)
: