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
.