Documentation

LeanPool.RegtsSevenster.RS.Classical.CatTheory.WhiskerAdditive

Whiskering against negation, zero and binary biproducts #

Mathlib records that whiskering in a preadditive monoidal category is additive (MonoidalPreadditive.whiskerLeft_add, MonoidalPreadditive.add_whiskerRight) and that it kills the zero morphism, but not the consequences the development uses everywhere: whiskering commutes with negation, a tensor product with a zero object is a zero object, and tensoring distributes over a binary biproduct on either side. All hold in any preadditive monoidal category, so they live here rather than in any of the files that consume them.

Mathlib's Limits.Functor.mapBiprod at tensorLeft B is the same isomorphism, but its PreservesBinaryBiproduct hypothesis is not an instance for tensorLeft, so the distributors are built here directly.

source
@[simp]
theorem RS.whiskerLeft_neg {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (X : C) {Y Z : C} (f : Y ⟶ Z) :
CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (-f) = -CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f

Whiskering on the left commutes with negation.

source
@[simp]
theorem RS.neg_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X Y : C} (f : X ⟶ Y) (Z : C) :
CategoryTheory.MonoidalCategoryStruct.whiskerRight (-f) Z = -CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z

Whiskering on the right commutes with negation.

source
theorem RS.isZero_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] {X : C} (h : CategoryTheory.Limits.IsZero X) (V : C) :
CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj X V)

Tensoring a zero object on the right with any object gives a zero object.

source
theorem RS.isZero_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] (V : C) {Y : C} (h : CategoryTheory.Limits.IsZero Y) :
CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj V Y)

Tensoring any object with a zero object on the right gives a zero object.

Distributivity over a binary biproduct #

source
noncomputable def RS.tensorBiprodIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) :
CategoryTheory.MonoidalCategoryStruct.tensorObj B (X ⊞ Y) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj B X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj B Y

Tensoring on the left distributes over a binary biproduct.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def RS.biprodTensorIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⊞ Y) B ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj X B ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj Y B

    Tensoring on the right distributes over a binary biproduct.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem RS.inl_tensorBiprodIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inl) (tensorBiprodIso B X Y).hom = CategoryTheory.Limits.biprod.inl
      source
      @[simp]
      theorem RS.inl_tensorBiprodIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj B X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj B Y ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inl) (CategoryTheory.CategoryStruct.comp (tensorBiprodIso B X Y).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
      source
      @[simp]
      theorem RS.inr_tensorBiprodIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inr) (tensorBiprodIso B X Y).hom = CategoryTheory.Limits.biprod.inr
      source
      @[simp]
      theorem RS.inr_tensorBiprodIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj B X ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj B Y ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inr) (CategoryTheory.CategoryStruct.comp (tensorBiprodIso B X Y).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
      source
      @[simp]
      theorem RS.inl_tensorBiprodIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (tensorBiprodIso B X Y).inv = CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inl
      source
      @[simp]
      theorem RS.inl_tensorBiprodIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj B (X ⊞ Y) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (tensorBiprodIso B X Y).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inl) h
      source
      @[simp]
      theorem RS.inr_tensorBiprodIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (tensorBiprodIso B X Y).inv = CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inr
      source
      @[simp]
      theorem RS.inr_tensorBiprodIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (B X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj B (X ⊞ Y) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (tensorBiprodIso B X Y).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft B CategoryTheory.Limits.biprod.inr) h
      source
      @[simp]
      theorem RS.inl_biprodTensorIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl B) (biprodTensorIso X Y B).hom = CategoryTheory.Limits.biprod.inl
      source
      @[simp]
      theorem RS.inl_biprodTensorIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X B ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj Y B ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl B) (CategoryTheory.CategoryStruct.comp (biprodTensorIso X Y B).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
      source
      @[simp]
      theorem RS.inr_biprodTensorIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr B) (biprodTensorIso X Y B).hom = CategoryTheory.Limits.biprod.inr
      source
      @[simp]
      theorem RS.inr_biprodTensorIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X B ⊞ CategoryTheory.MonoidalCategoryStruct.tensorObj Y B ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr B) (CategoryTheory.CategoryStruct.comp (biprodTensorIso X Y B).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h
      source
      @[simp]
      theorem RS.inl_biprodTensorIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (biprodTensorIso X Y B).inv = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl B
      source
      @[simp]
      theorem RS.inl_biprodTensorIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⊞ Y) B ⟶ Z) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp (biprodTensorIso X Y B).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inl B) h
      source
      @[simp]
      theorem RS.inr_biprodTensorIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (biprodTensorIso X Y B).inv = CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr B
      source
      @[simp]
      theorem RS.inr_biprodTensorIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (X Y B : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⊞ Y) B ⟶ Z) :
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp (biprodTensorIso X Y B).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Limits.biprod.inr B) h