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`.



Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: mckoen

Mathlib/CategoryTheory/Localization/FiniteProducts.lean

@@ -38,7 +38,7 @@ include hW
 
 lemma inverts :
     (W.functorCategory (Discrete J)).IsInvertedBy (lim ⋙ L) :=
-  fun _ _ f hf => Localization.inverts L W _ (hW.lim_map f hf)
+  fun _ _ f hf => Localization.inverts L W _ (hW.limMap f hf)
 
 variable [W.ContainsIdentities] [Finite J]
 

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -61,6 +61,26 @@ lemma ext (W W' : MorphismProperty C) (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f
 lemma top_apply {X Y : C} (f : X ⟶ Y) : (⊤ : MorphismProperty C) f := by
   simp only [top_eq]
 
+@[simp]
+lemma sSup_iff (S : Set (MorphismProperty C)) {X Y : C} (f : X ⟶ Y) :
+    sSup S f ↔ ∃ (W : S), W.1 f := by
+  dsimp [sSup, iSup]
+  constructor
+  · rintro ⟨_, ⟨⟨_, ⟨⟨_, ⟨_, h⟩, rfl⟩, rfl⟩⟩, rfl⟩, hf⟩
+    exact ⟨⟨_, h⟩, hf⟩
+  · rintro ⟨⟨W, hW⟩, hf⟩
+    exact ⟨_, ⟨⟨_, ⟨_, ⟨⟨W, hW⟩, rfl⟩⟩, rfl⟩, rfl⟩, hf⟩
+
+@[simp]
+lemma iSup_iff {ι : Type*} (W : ι → MorphismProperty C) {X Y : C} (f : X ⟶ Y) :
+    iSup W f ↔ ∃ i, W i f := by
+  apply (sSup_iff (Set.range W) f).trans
+  constructor
+  · rintro ⟨⟨_, i, rfl⟩, hf⟩
+    exact ⟨i, hf⟩
+  · rintro ⟨i, hf⟩
+    exact ⟨⟨_, i, rfl⟩, hf⟩
+
 /-- The morphism property in `Cᵒᵖ` associated to a morphism property in `C` -/
 @[simp]
 def op (P : MorphismProperty C) : MorphismProperty Cᵒᵖ := fun _ _ f => P f.unop