Basic

📁 Source: Mathlib/CategoryTheory/CopyDiscardCategory/Basic.lean

Statistics

Metric	Count
Definitions CopyDiscardCategory, comonObj, toSymmetricCategory	3
Theorems copy_tensor, copy_unit, discard_tensor, discard_unit, isCommComonObj	5
Total	8

CategoryTheory

Definitions

Name	Category	Theorems
CopyDiscardCategory 📖	CompData	—

CategoryTheory.CopyDiscardCategory

Definitions

Name	Category	Theorems
comonObj 📖	CompOp	10 math math: CategoryTheory.Deterministic.discard_natural, CategoryTheory.MarkovCategory.eq_discard, copy_unit, copy_tensor, discard_unit, CategoryTheory.MarkovCategory.discard_natural, CategoryTheory.MarkovCategory.discard_natural_assoc, isCommComonObj, discard_tensor, CategoryTheory.Deterministic.copy_natural
toSymmetricCategory 📖	CompOp	2 math math: copy_tensor, isCommComonObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
copy_tensor 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comonObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.SymmetricCategory.toBraidedCategory toSymmetricCategory	—	—
copy_unit 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comonObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
discard_tensor 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comonObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
discard_unit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comonObj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
isCommComonObj 📖	mathematical	—	CategoryTheory.IsCommComonObj CategoryTheory.SymmetricCategory.toBraidedCategory toSymmetricCategory comonObj	—	—

---

← Back to Index