Documentation

Mathlib.Algebra.Category.ModuleCat.Products

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

source
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.

Instances For
    source
    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.

    Instances For
      source
      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
        source
        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
        source
        @[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
        source
        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
        source
        @[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