Documentation

Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Tensor products of cokernels #

Let c₁ and c₂ be cokernel coforks for morphisms f₁ : X₁ ⟶ Y₁ and f₂ : X₂ ⟶ Y₂ in a monoidal preadditive category. We define a cokernel cofork for (X₁ ⊗ Y₂) ⨿ (Y₁ ⊗ X₂) ⟶ Y₁ ⊗ Y₂ with point c₁.pt ⊗ c₂.pt, and show that it is colimit if c₁ and c₂ are colimit, and the cokernels of f₁ and f₂ are preserved by suitable tensor products.

source
🔸 coverage
@[reducible, inline]
noncomputable abbrev CategoryTheory.Limits.CokernelCofork.tensor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} (c₁ : CokernelCofork f₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} (c₂ : CokernelCofork f₂) [HasBinaryCoproduct (MonoidalCategoryStruct.tensorObj X₁ Y₂) (MonoidalCategoryStruct.tensorObj Y₁ X₂)] :
CokernelCofork (coprod.desc (MonoidalCategoryStruct.whiskerRight f₁ Y₂) (MonoidalCategoryStruct.whiskerLeft Y₁ f₂))

Given two cokernel coforks c₁ and c₂ for f₁ : X₁ ⟶ Y₁ and f₂ : X₂ ⟶ Y₂, this is the cokernel cofork for (X₁ ⊗ Y₂) ⨿ (Y₁ ⊗ X₂) ⟶ Y₁ ⊗ Y₂ with point c₁.pt ⊗ c₂.pt.

Instances For
    source
    🔸 coverage
    noncomputable def CategoryTheory.Limits.CokernelCofork.isColimitTensor {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] [MonoidalCategory C] [MonoidalPreadditive C] {X₁ Y₁ : C} {f₁ : X₁ ⟶ Y₁} {c₁ : CokernelCofork f₁} (hc₁ : IsColimit c₁) {X₂ Y₂ : C} {f₂ : X₂ ⟶ Y₂} {c₂ : CokernelCofork f₂} (hc₂ : IsColimit c₂) [HasBinaryCoproduct (MonoidalCategoryStruct.tensorObj X₁ Y₂) (MonoidalCategoryStruct.tensorObj Y₁ X₂)] [PreservesColimit (parallelPair f₂ 0) (MonoidalCategory.tensorLeft c₁.pt)] [PreservesColimit (parallelPair f₁ 0) (MonoidalCategory.tensorRight Y₂)] [PreservesColimit (parallelPair f₁ 0) (MonoidalCategory.tensorRight X₂)] :
    IsColimit (c₁.tensor c₂)

    Given two colimit cokernel coforks c₁ and c₂ for f₁ : X₁ ⟶ Y₁ and f₂ : X₂ ⟶ Y₂, if the cokernels of f₁ and f₂ are preserves by suitable tensor products, then c₁.pt ⊗ c₂.pt is the cokernel of the morphism (X₁ ⊗ Y₂) ⨿ (Y₁ ⊗ X₂) ⟶ Y₁ ⊗ Y₂.

    Instances For