Commit 2026-10-30 15:08 21f7d1b5

chore(CategoryTheory): deprecate leftExactFunctor (#45418) The property of objects leftExactFunctor in functor categories is deprecated in favour of ObjectProperty.preservesFiniteLimits. The definition of the typeclass HasExactColimitsOfShape is moved to a separate file Mathlib/CategoryTheory/Limits/HasExactLimitsOfShape.lean with reduced imports in order to avoid a cycle of imports. Results about exact colimits are moved out of Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/PreservesLimits.lean to a new file ExactColimits.lean. A new file Mathlib/CategoryTheory/ObjectProperty/BinaryProductsClosure.lean is also added by part of the content of FiniteProducts.lean in order to avoid importing set theory definitions in some algebra files.