Commit 2024-01-09 09:24 420479f2

View on Github →

feat(CategoryTheory): define countable categories and countable limits (#8674) We define a class CountableCategory analogous to FinCategory, and provide some API for countable limits. This will be necessary to develop the theory of light condensed sets.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Countable.lean

added def CategoryTheory.CountableCategory.HomAsType

Created Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

added theorem CategoryTheory.Limits.sequentialFunctor_initial_aux

added theorem CategoryTheory.Limits.sequentialFunctor_map