mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(category_theory/concrete): representably concrete

Open b-mehta opened this issue 4 years ago • 2 comments
trafficstars

Representably concrete categories: This makes it easier to talk about elements of (specific) limit objects in most concrete categories that are useful in practice. It should work for any limit (not colimit) in most of the algebraic categories we have as well as some of the topological and order categories; this PR also adds instances for many of these, though some are missing.

I also added the fact that monomorphisms are the same as injections in representably concrete categories, as mentioned already: https://github.com/leanprover-community/mathlib/pull/7405#discussion_r624944721

Open in Gitpod

b-mehta avatar May 01 '21 16:05 b-mehta

I'm reverting this back to WIP - it's probably easier to review as a series of PRs rather than one monolithic one, especially since I keep thinking of things to add to it.

b-mehta avatar Jun 15 '21 19:06 b-mehta

It would be nice not to lose this one to the dustbin of history!

kim-em avatar May 02 '22 09:05 kim-em