Cocartesian Monoidal Categories

This file defines cocartesian monoidal categories (dual of cartesian monoidal) and proves that KlSPComp is cocartesian with Sum as coproduct and Empty as initial object.

Main definitions

• SemiCocartesianMonoidalCategory — monoidal category with initial tensor unit
• CocartesianMonoidalCategory — tensor is the categorical coproduct
• KlSPComp instance of CocartesianMonoidalCategory

class CategoryTheory.SemiCocartesianMonoidalCategory (C : Type u) [Category.{v, u} C] extends CategoryTheory.MonoidalCategory C : Type (max u v)

A monoidal category is semicocartesian if the unit for the tensor product is an initial object. Dual of SemiCartesianMonoidalCategory.

• tensorObj : C → C → C
• whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
• tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂
• tensorUnit : C
• associator (X Y Z : C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
• leftUnitor (X : C) : tensorObj (tensorUnit C) X ≅ X
• rightUnitor (X : C) : tensorObj X (tensorUnit C) ≅ X
• tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorHom f g = CategoryStruct.comp (whiskerRight f X₂) (whiskerLeft Y₁ g)
• id_tensorHom_id (X₁ X₂ : C) : tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (tensorObj X₁ X₂)
• tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)
• whiskerLeft_id (X Y : C) : whiskerLeft X (CategoryStruct.id Y) = CategoryStruct.id (tensorObj X Y)
• id_whiskerRight (X Y : C) : whiskerRight (CategoryStruct.id X) Y = CategoryStruct.id (tensorObj X Y)
• associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))
• leftUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f
• rightUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerRight f (tensorUnit C)) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f
• pentagon (W X Y Z : C) : CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom
• triangle (X Y : C) : CategoryStruct.comp (associator X (tensorUnit C) Y).hom (whiskerLeft X (leftUnitor Y).hom) = whiskerRight (rightUnitor X).hom Y
• isInitialTensorUnit : Limits.IsInitial (MonoidalCategoryStruct.tensorUnit C)

  The tensor unit is an initial object.

• inl (X Y : C) : X ⟶ MonoidalCategoryStruct.tensorObj X Y

  The first coprojection into the coproduct.

• inr (X Y : C) : Y ⟶ MonoidalCategoryStruct.tensorObj X Y

  The second coprojection into the coproduct.

• inl_def (X Y : C) : inl X Y = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (MonoidalCategoryStruct.whiskerLeft X (isInitialTensorUnit.to Y))
• inr_def (X Y : C) : inr X Y = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv (MonoidalCategoryStruct.whiskerRight (isInitialTensorUnit.to X) Y)

def CategoryTheory.SemiCocartesianMonoidalCategory.fromUnit {C : Type u} [Category.{v, u} C] [SemiCocartesianMonoidalCategory C] (X : C) : MonoidalCategoryStruct.tensorUnit C ⟶ X

The unique morphism from the initial tensor unit to any object.

Equations

• CategoryTheory.SemiCocartesianMonoidalCategory.fromUnit X = CategoryTheory.SemiCocartesianMonoidalCategory.isInitialTensorUnit.to X

@[simp]

theorem CategoryTheory.SemiCocartesianMonoidalCategory.fromUnit_comp {C : Type u} [Category.{v, u} C] [SemiCocartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (fromUnit X) f = fromUnit Y

@[simp]

theorem CategoryTheory.SemiCocartesianMonoidalCategory.fromUnit_comp_assoc {C : Type u} [Category.{v, u} C] [SemiCocartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (fromUnit X) (CategoryStruct.comp f h) = CategoryStruct.comp (fromUnit Y) h

@[simp]

theorem CategoryTheory.SemiCocartesianMonoidalCategory.fromUnit_unit {C : Type u} [Category.{v, u} C] [SemiCocartesianMonoidalCategory C] : fromUnit (MonoidalCategoryStruct.tensorUnit C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.SemiCocartesianMonoidalCategory.isInitialTensorUnit_to {C : Type u} [Category.{v, u} C] [SemiCocartesianMonoidalCategory C] (X : C) : isInitialTensorUnit.to X = fromUnit X

Bridge lemma: isInitialTensorUnit.to X is the same as fromUnit X.

class CategoryTheory.CocartesianMonoidalCategory (C : Type u) [Category.{v, u} C] extends CategoryTheory.SemiCocartesianMonoidalCategory C : Type (max u v)

A monoidal category is cocartesian if the tensor product is the categorical coproduct and the unit is initial. Dual of CartesianMonoidalCategory.

• tensorObj : C → C → C
• whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
• tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂
• tensorUnit : C
• associator (X Y Z : C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
• leftUnitor (X : C) : tensorObj (tensorUnit C) X ≅ X
• rightUnitor (X : C) : tensorObj X (tensorUnit C) ≅ X
• tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorHom f g = CategoryStruct.comp (whiskerRight f X₂) (whiskerLeft Y₁ g)
• id_tensorHom_id (X₁ X₂ : C) : tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (tensorObj X₁ X₂)
• tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)
• whiskerLeft_id (X Y : C) : whiskerLeft X (CategoryStruct.id Y) = CategoryStruct.id (tensorObj X Y)
• id_whiskerRight (X Y : C) : whiskerRight (CategoryStruct.id X) Y = CategoryStruct.id (tensorObj X Y)
• associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))
• leftUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f
• rightUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerRight f (tensorUnit C)) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f
• pentagon (W X Y Z : C) : CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom
• triangle (X Y : C) : CategoryStruct.comp (associator X (tensorUnit C) Y).hom (whiskerLeft X (leftUnitor Y).hom) = whiskerRight (rightUnitor X).hom Y
• isInitialTensorUnit : Limits.IsInitial (MonoidalCategoryStruct.tensorUnit C)
• inl (X Y : C) : X ⟶ MonoidalCategoryStruct.tensorObj X Y
• inr (X Y : C) : Y ⟶ MonoidalCategoryStruct.tensorObj X Y
• inl_def (X Y : C) : inl X Y = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (MonoidalCategoryStruct.whiskerLeft X (isInitialTensorUnit.to Y))
• inr_def (X Y : C) : inr X Y = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).inv (MonoidalCategoryStruct.whiskerRight (isInitialTensorUnit.to X) Y)
• tensorCoproductIsBinaryCoproduct (X Y : C) : Limits.IsColimit (Limits.BinaryCofan.mk (SemiCocartesianMonoidalCategory.inl X Y) (SemiCocartesianMonoidalCategory.inr X Y))

  The monoidal product is the categorical coproduct.

def CategoryTheory.CocartesianMonoidalCategory.desc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : MonoidalCategoryStruct.tensorObj X Y ⟶ Z

The copairing (universal map from coproduct).

Equations

• CategoryTheory.CocartesianMonoidalCategory.desc f g = (CategoryTheory.CocartesianMonoidalCategory.tensorCoproductIsBinaryCoproduct X Y).desc (CategoryTheory.Limits.BinaryCofan.mk f g)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_desc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) (desc f g) = f

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_desc_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) (CategoryStruct.comp (desc f g) h) = CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_desc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) (desc f g) = g

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_desc_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) (CategoryStruct.comp (desc f g) h) = CategoryStruct.comp g h

theorem CategoryTheory.CocartesianMonoidalCategory.hom_ext {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} {f g : MonoidalCategoryStruct.tensorObj X Y ⟶ Z} (hl : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) f = CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) g) (hr : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) f = CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) g) : f = g

theorem CategoryTheory.CocartesianMonoidalCategory.hom_ext_iff {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} {f g : MonoidalCategoryStruct.tensorObj X Y ⟶ Z} : f = g ↔ CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) f = CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) g ∧ CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) f = CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) g

theorem CategoryTheory.CocartesianMonoidalCategory.desc_unique {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {h : MonoidalCategoryStruct.tensorObj X Y ⟶ Z} (hl : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) h = f) (hr : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) h = g) : h = desc f g

Simp library for CocartesianMonoidalCategory

Dual of Mathlib's CartesianMonoidalCategory simp library.

Core desc identities

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.desc_inl_inr {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y : C} : desc (SemiCocartesianMonoidalCategory.inl X Y) (SemiCocartesianMonoidalCategory.inr X Y) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.desc_comp_inl_inr {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z : C} (f : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : desc (CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) f) (CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) f) = f

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.desc_comp {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ W) : CategoryStruct.comp (desc f g) h = desc (CategoryStruct.comp f h) (CategoryStruct.comp g h)

theorem CategoryTheory.CocartesianMonoidalCategory.desc_comp_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Z) (g : Y ⟶ Z) (h : Z ⟶ W) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryStruct.comp (desc f g) (CategoryStruct.comp h h✝) = CategoryStruct.comp (desc (CategoryStruct.comp f h) (CategoryStruct.comp g h)) h✝

Coprojections and whiskering

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_whiskerLeft {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) (MonoidalCategoryStruct.whiskerLeft X f) = SemiCocartesianMonoidalCategory.inl X Z

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) h) = CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Z) h

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_whiskerLeft {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) (MonoidalCategoryStruct.whiskerLeft X f) = CategoryStruct.comp f (SemiCocartesianMonoidalCategory.inr X Z)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Y) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) h) = CategoryStruct.comp f (CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Z) h)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_whiskerRight {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Z) (MonoidalCategoryStruct.whiskerRight f Z) = CategoryStruct.comp f (SemiCocartesianMonoidalCategory.inl Y Z)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Y Z ⟶ Z✝) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) h) = CategoryStruct.comp f (CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl Y Z) h)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_whiskerRight {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Z) (MonoidalCategoryStruct.whiskerRight f Z) = SemiCocartesianMonoidalCategory.inr Y Z

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Y Z ⟶ Z✝) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X Z) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) h) = CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr Y Z) h

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_tensorHom {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X₁ Y₁) (MonoidalCategoryStruct.tensorHom f g) = CategoryStruct.comp f (SemiCocartesianMonoidalCategory.inl X₂ Y₂)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_tensorHom_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X₁ Y₁) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) h) = CategoryStruct.comp f (CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X₂ Y₂) h)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_tensorHom {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X₁ Y₁) (MonoidalCategoryStruct.tensorHom f g) = CategoryStruct.comp g (SemiCocartesianMonoidalCategory.inr X₂ Y₂)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_tensorHom_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X₁ Y₁) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) h) = CategoryStruct.comp g (CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr X₂ Y₂) h)

desc + tensor

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.map_desc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : X ⟶ Y) (h : W ⟶ Z) (k : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (desc h k) = desc (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.map_desc_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : X ⟶ Y) (h : W ⟶ Z) (k : Y ⟶ Z) {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (CategoryStruct.comp (desc h k) h✝) = CategoryStruct.comp (desc (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.whiskerLeft_desc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ W) (g : Y ⟶ Z) (h : Z ⟶ W) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X g) (desc f h) = desc f (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.whiskerLeft_desc_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ W) (g : Y ⟶ Z) (h : Z ⟶ W) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X g) (CategoryStruct.comp (desc f h) h✝) = CategoryStruct.comp (desc f (CategoryStruct.comp g h)) h✝

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.whiskerRight_desc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ W) (h : Z ⟶ W) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) (desc g h) = desc (CategoryStruct.comp f g) h

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.whiskerRight_desc_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ W) (h : Z ⟶ W) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) (CategoryStruct.comp (desc g h) h✝) = CategoryStruct.comp (desc (CategoryStruct.comp f g) h) h✝

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.desc_inl_comp_inr_comp {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : desc (CategoryStruct.comp f (SemiCocartesianMonoidalCategory.inl X Z)) (CategoryStruct.comp g (SemiCocartesianMonoidalCategory.inr X Z)) = MonoidalCategoryStruct.tensorHom f g

Unitor projections

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_leftUnitor_hom {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr (MonoidalCategoryStruct.tensorUnit C) X) (MonoidalCategoryStruct.leftUnitor X).hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inr_leftUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inr (MonoidalCategoryStruct.tensorUnit C) X) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom h) = h

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_rightUnitor_hom {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X (MonoidalCategoryStruct.tensorUnit C)) (MonoidalCategoryStruct.rightUnitor X).hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.CocartesianMonoidalCategory.inl_rightUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [CocartesianMonoidalCategory C] (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (SemiCocartesianMonoidalCategory.inl X (MonoidalCategoryStruct.tensorUnit C)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom h) = h

Concrete instance: KlSPComp is cocartesian

IsInitial for Empty

noncomputable def CatCrypt.Core.KlSPComp.emptyIsInitial : CategoryTheory.Limits.IsInitial (have this := Empty; this)

Empty is initial in KlSPComp: there is a unique morphism from Empty to any type.

Equations

• CatCrypt.Core.KlSPComp.emptyIsInitial = CategoryTheory.Limits.IsInitial.ofUnique (have this := Empty; this)

Coprojections

noncomputable def CatCrypt.Core.KlSPComp.klInl (α β : KlSPComp) : α ⟶ have this := α ⊕ β; this

Left coprojection: embed into the left summand via pure.

Equations

• α.klInl β a = CatCrypt.Core.SPComp.pure (Sum.inl a)

noncomputable def CatCrypt.Core.KlSPComp.klInr (α β : KlSPComp) : β ⟶ have this := α ⊕ β; this

Right coprojection: embed into the right summand via pure.

Equations

• α.klInr β b = CatCrypt.Core.SPComp.pure (Sum.inr b)

Copairing

noncomputable def CatCrypt.Core.KlSPComp.klDesc {α β γ : KlSPComp} (f : α ⟶ γ) (g : β ⟶ γ) : (have this := α ⊕ β; this) ⟶ γ

Copairing: given morphisms from each summand, produce a morphism from the coproduct.

Equations

• CatCrypt.Core.KlSPComp.klDesc f g (Sum.inl a) = f a
• CatCrypt.Core.KlSPComp.klDesc f g (Sum.inr b) = g b

theorem CatCrypt.Core.KlSPComp.klInl_klDesc {α β γ : KlSPComp} (f : α ⟶ γ) (g : β ⟶ γ) : CategoryTheory.CategoryStruct.comp (α.klInl β) (klDesc f g) = f

theorem CatCrypt.Core.KlSPComp.klInr_klDesc {α β γ : KlSPComp} (f : α ⟶ γ) (g : β ⟶ γ) : CategoryTheory.CategoryStruct.comp (α.klInr β) (klDesc f g) = g

theorem CatCrypt.Core.KlSPComp.klDesc_unique {α β γ : KlSPComp} {f : α ⟶ γ} {g : β ⟶ γ} {h : (have this := α ⊕ β; this) ⟶ γ} (hl : CategoryTheory.CategoryStruct.comp (α.klInl β) h = f) (hr : CategoryTheory.CategoryStruct.comp (α.klInr β) h = g) : h = klDesc f g

Coproduct is colimit

noncomputable def CatCrypt.Core.KlSPComp.binaryCoproductIsColimit (α β : KlSPComp) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (α.klInl β) (α.klInr β))

Equations

• α.binaryCoproductIsColimit β = CategoryTheory.Limits.BinaryCofan.isColimitMk (fun (s : CategoryTheory.Limits.BinaryCofan α β) => CatCrypt.Core.KlSPComp.klDesc s.inl s.inr) ⋯ ⋯ ⋯

inl_def / inr_def compatibility

CocartesianMonoidalCategory instance

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instSemiCocartesianMonoidalCategory : CategoryTheory.SemiCocartesianMonoidalCategory KlSPComp

Equations

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

@[implicit_reducible]

noncomputable instance CatCrypt.Core.KlSPComp.instCocartesianMonoidalCategory : CategoryTheory.CocartesianMonoidalCategory KlSPComp

Equations

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