Commit 2024-10-27 15:49 5532a724

View on Github →

feat(CategoryTheory/SmallObject): very basic API for the iteration of functors (#18115) This PR adds some very basic API for the iteration of functors and fixes the notation for intervals (Set.Iic and Set.Iio are now used).

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/CategoryTheory/SmallObject/Iteration.lean to Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

added theorem CategoryTheory.Functor.Iteration.Hom.congr_app

added def CategoryTheory.Functor.Iteration.eval

added theorem CategoryTheory.Functor.Iteration.natTrans_comp

added theorem CategoryTheory.Functor.Iteration.natTrans_id

added theorem CategoryTheory.Functor.Iteration.natTrans_naturality

added def CategoryTheory.Functor.Iteration.restrictionLE

added theorem CategoryTheory.Functor.Iteration.restrictionLE_map

added theorem CategoryTheory.Functor.Iteration.restrictionLE_obj

modified def CategoryTheory.Functor.Iteration.restrictionLT

modified theorem CategoryTheory.Functor.Iteration.restrictionLT_map

added def CategoryTheory.Functor.Iteration.trunc

added def CategoryTheory.Functor.Iteration.truncFunctor

added theorem CategoryTheory.Functor.Iteration.truncFunctor_map_natTrans_app