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 : ι → ModuleCat 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 : ι) => ModuleCat.ofHom (LinearMap.proj i)

def ModuleCat.productConeIsLimit {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) : CategoryTheory.Limits.IsLimit (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 : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] : ∏ᶜ Z ≅ 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 : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (piIsoPi Z).inv (CategoryTheory.Limits.Pi.π Z i) = ofHom (LinearMap.proj i)

theorem ModuleCat.piIsoPi_inv_kernel_ι_apply {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : CategoryTheory.ToType (of R ((i : ι) → ↑(Z i)))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) ((CategoryTheory.ConcreteCategory.hom (piIsoPi Z).inv) x) = x i

@[simp]

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

theorem ModuleCat.piIsoPi_hom_ker_subtype_apply {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [CategoryTheory.Limits.HasProduct Z] (i : ι) (x : CategoryTheory.ToType (∏ᶜ Z)) : (CategoryTheory.ConcreteCategory.hom (piIsoPi Z).hom) x i = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) x

def ModuleCat.coproductCocone {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] : CategoryTheory.Limits.Cofan Z

The coproduct cone induced by the concrete product.

Equations

• ModuleCat.coproductCocone Z = CategoryTheory.Limits.Cofan.mk (ModuleCat.of R (DirectSum ι fun (i : ι) => ↑(Z i))) fun (i : ι) => ModuleCat.ofHom (DirectSum.lof R ι (fun (i : ι) => ↑(Z i)) i)

def ModuleCat.coproductCoconeIsColimit {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] : CategoryTheory.Limits.IsColimit (coproductCocone Z)

The concrete coproduct cone is limiting.

Equations

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

noncomputable def ModuleCat.coprodIsoDirectSum {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] [CategoryTheory.Limits.HasCoproduct Z] : ∐ Z ≅ of R (DirectSum ι fun (i : ι) => ↑(Z i))

The categorical coproduct of a family of objects in ModuleCat agrees with direct sum.

Equations

• ModuleCat.coprodIsoDirectSum Z = CategoryTheory.Limits.colimit.isoColimitCocone { cocone := ModuleCat.coproductCocone Z, isColimit := ModuleCat.coproductCoconeIsColimit Z }

@[simp]

theorem ModuleCat.ι_coprodIsoDirectSum_hom {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] [CategoryTheory.Limits.HasCoproduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι Z i) (coprodIsoDirectSum Z).hom = ofHom (DirectSum.lof R ι (fun (i : ι) => ↑(Z i)) i)

theorem ModuleCat.ι_coprodIsoDirectSum_hom_apply {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] [CategoryTheory.Limits.HasCoproduct Z] (i : ι) (x : CategoryTheory.ToType (Z i)) : (CategoryTheory.ConcreteCategory.hom (coprodIsoDirectSum Z).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι Z i)) x) = (DirectSum.lof R ι (fun (i : ι) => ↑(Z i)) i) x

@[simp]

theorem ModuleCat.lof_coprodIsoDirectSum_inv {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] [CategoryTheory.Limits.HasCoproduct Z] (i : ι) : CategoryTheory.CategoryStruct.comp (ofHom (DirectSum.lof R ι (fun (i : ι) => ↑(Z i)) i)) (coprodIsoDirectSum Z).inv = CategoryTheory.Limits.Sigma.ι Z i

theorem ModuleCat.lof_coprodIsoDirectSum_inv_apply {R : Type u} [Ring R] {ι : Type v} (Z : ι → ModuleCat R) [DecidableEq ι] [CategoryTheory.Limits.HasCoproduct Z] (i : ι) (x : CategoryTheory.ToType (of R ↑(Z i))) : (CategoryTheory.ConcreteCategory.hom (coprodIsoDirectSum Z).inv) ((DirectSum.lof R ι (fun (i : ι) => ↑(Z i)) i) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι Z i)) x