Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.Arrow.pushoutProduct

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasPushouts C] →
      [CategoryTheory.MonoidalCategory C] →
        CategoryTheory.Functor (CategoryTheory.Arrow C)
          (CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C))

The Leibniz functor associated to the tensor product on a monoidal category. This is the bifunctor of arrow categories that sends f : A ⟶ B and g : X ⟶ Y to the canonical map from the pushout of f ◁ X and A ▷ g to B ⊗ Y, induced by the following diagram: `` A ⊗ X --> B ⊗ X | | v v A ⊗ Y --> B ⊗ Y ``

Defined in

Mathlib.CategoryTheory.Monoidal.PushoutProduct

Cited by

64 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPushoutsCategoryTheory.MonoidalCategory