The concrete products in the category of modules are products in the categorical sense.

def ModuleCat.productCone {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCatMax R) : CategoryTheory.Limits.Fan Z

The product cone induced by the concrete product.

Equations

• ModuleCat.productCone Z = CategoryTheory.Limits.Fan.mk (ModuleCat.of R ((i : ι) → ↑(Z i))) fun (i : ι) => LinearMap.proj i

def ModuleCat.productConeIsLimit {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCatMax R) : CategoryTheory.Limits.IsLimit (ModuleCat.productCone Z)

The concrete product cone is limiting.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• ModuleCat.piIsoPi Z = CategoryTheory.Limits.limit.isoLimitCone { cone := ModuleCat.productCone Z, isLimit := ModuleCat.productConeIsLimit Z }

@[simp]

theorem ModuleCat.piIsoPi_inv_kernel_ι {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCatMax R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).inv (CategoryTheory.Limits.Pi.π Z i) = LinearMap.proj i

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 (ModuleCat.of R ((i : ι) → ↑(Z i)))) : (CategoryTheory.Limits.Pi.π Z i) ((ModuleCat.piIsoPi Z).inv x) = (LinearMap.proj i) x

@[simp]

theorem ModuleCat.piIsoPi_hom_ker_subtype {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCatMax R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (ModuleCat.piIsoPi Z).hom (LinearMap.proj i) = CategoryTheory.Limits.Pi.π 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 (∏ᶜ Z)) : (LinearMap.proj i) ((ModuleCat.piIsoPi Z).hom x) = (CategoryTheory.Limits.Pi.π Z i) x