Commit 2024-05-15 12:02 c5f6c2d6

View on Github →

feat(CategoryTheory/Limits): add classes ReflectsFiniteLimits and friends (#12909) This PR adds classes ReflectsFiniteLimits, ReflectsFiniteProducts and their duals, and relates them to existing classes. It also cleans up the file CategoryTheory.Limits.Preserves.Finite a bit and removes some porting notes that are no longer relevant.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/Finite.lean

added def CategoryTheory.Limits.preservesFiniteColimitsOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesFiniteCoproductsOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesFiniteLimitsOfReflectsOfPreserves

added def CategoryTheory.Limits.preservesFiniteProductsOfReflectsOfPreserves