Commit 2025-02-06 15:22 e4712116

View on Github →

feat(CategoryTheory): equivalence between Ind C and left exact functors from C to Type (#21430)

Estimated changes

Modified Mathlib/CategoryTheory/Equivalence.lean

added def CategoryTheory.Equivalence.ofFullSubcategory

Modified Mathlib/CategoryTheory/Limits/Indization/Category.lean

Modified Mathlib/CategoryTheory/Limits/Indization/IndObject.lean

added theorem CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimits

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