mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(CategoryTheory): triangulated subcategories

Open joelriou opened this issue 1 year ago • 0 comments

This PR defines the type Triangulated.Subcategory C when C is a pretriangulated category. It also introduces a type class Set.RespectsIso for set of objects in a category C that is stable under isomorphisms.

Open in Gitpod

joelriou avatar Mar 28 '24 11:03 joelriou