Colimits

📁 Source: Mathlib/CategoryTheory/Monoidal/Limits/Colimits.lean

Statistics

Metric	Count
Definitions tensor, tensor₂, tensor, tensor₂	4
Theorems tensor_pt, tensor_ι_app	2
Total	6

CategoryTheory.Limits.Cocone

Definitions

Name	Category	Theorems
tensor 📖	CompOp	2 math math: tensor_ι_app, tensor_pt
tensor₂ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor_pt 📖	mathematical	—	pt CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct tensor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensor_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Monoidal.functorCategoryMonoidalStruct CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct pt ι tensor CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—

CategoryTheory.Limits.IsColimit

Definitions

Name	Category	Theorems
tensor 📖	CompOp	—
tensor₂ 📖	CompOp	—

---

← Back to Index