Commit 2025-01-22 14:26 72bf52f2

View on Github →

feat(CategoryTheory): pullbacks/pushouts/limits/colimits of a class of morphisms (#20157) Given P : MorphismProperty C and J a category, we introduce morphisms properties P.pullbacks, P.pushouts, P.limitsOfShape J and P.colimitsOfShape J which are obtained from P by taking these type of (co)limits. We obtain results like P.isStableUnderBaseChange_iff_pullbacks_le : P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P.

Estimated changes