feat(CategoryTheory/SmallObject): llp is stable under transfinite composition (#21682)

We deduce from previous results (#20119) that if `W : MorphismProperty C`, then the class `W.llp` of morphisms which satisfy the left lifting property with respect to `W` is stable under transfinite composition.

Author: joelriou

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -72,7 +72,7 @@ lemma sSup_iff (S : Set (MorphismProperty C)) {X Y : C} (f : X ⟶ Y) :
     exact ⟨_, ⟨⟨_, ⟨_, ⟨⟨W, hW⟩, rfl⟩⟩, rfl⟩, rfl⟩, hf⟩
 
 @[simp]
-lemma iSup_iff {ι : Type*} (W : ι → MorphismProperty C) {X Y : C} (f : X ⟶ Y) :
+lemma iSup_iff {ι : Sort*} (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

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

@@ -136,6 +136,11 @@ of morphisms in `W`. -/
 def transfiniteCompositionsOfShape : MorphismProperty C :=
   fun _ _ f ↦ Nonempty (W.TransfiniteCompositionOfShape J f)
 
+lemma transfiniteCompositionsOfShape_monotone :
+    Monotone (transfiniteCompositionsOfShape (C := C) (J := J)) := by
+  rintro _ _ h _ _ _ ⟨t⟩
+  exact ⟨t.ofLE h⟩
+
 variable {J} in
 lemma transfiniteCompositionsOfShape_eq_of_orderIso (e : J ≃o J') :
     W.transfiniteCompositionsOfShape J =
@@ -214,6 +219,26 @@ instance : W.IsMultiplicative where
 
 end IsStableUnderTransfiniteComposition
 
+/-- The class of transfinite compositions (for arbitrary well-ordered types `J : Type w`)
+of a class of morphisms `W`. -/
+@[pp_with_univ]
+def transfiniteCompositions : MorphismProperty C :=
+  ⨆ (J : Type w) (_ : LinearOrder J) (_ : SuccOrder J) (_ : OrderBot J)
+    (_ : WellFoundedLT J), W.transfiniteCompositionsOfShape J
+
+lemma transfiniteCompositions_iff {X Y : C} (f : X ⟶ Y) :
+    transfiniteCompositions.{w} W f ↔
+      ∃ (J : Type w) (_ : LinearOrder J) (_ : SuccOrder J) (_ : OrderBot J)
+        (_ : WellFoundedLT J), W.transfiniteCompositionsOfShape J f := by
+  simp only [transfiniteCompositions, iSup_iff]
+
+lemma transfiniteCompositionsOfShape_le_transfiniteCompositions
+    (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] :
+    W.transfiniteCompositionsOfShape J ≤ transfiniteCompositions.{w} W := by
+  intro A B f hf
+  rw [transfiniteCompositions_iff]
+  exact ⟨_, _, _, _, _, hf⟩
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

@@ -4,15 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
+import Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
+import Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
 import Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
 
 /-!
 # The left lifting property is stable under transfinite composition
 
-Let `C` be a category, and `p : X ⟶ Y` be a morphism in `C`. In this file,
-we show that a transfinite composition of morphisms that have the left
-lifting property with respect to `p` also has the left lifting property with
-respect to `p`, see `HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot`.
+In this file, we show that if `W : MorphismProperty C`, then
+`W.llp.IsStableUnderTransfiniteCompositionOfShape J`, i.e.
+the class of morphisms which have the left lifting property with
+respect to `W` is stable under transfinite composition.
+
+The main technical lemma is
+`HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot`.
+It corresponds to the particular case `W` contains only one morphism `p : X ⟶ Y`:
+it shows that a transfinite composition of morphisms that have the left
+lifting property with respect to `p` also has the left lifting property
+with respect to `p`.
 
 About the proof, given a colimit cocone `c` for a well-order-continuous
 functor `F : J ⥤ C` from a well-ordered type `J`, we introduce a projective
@@ -39,10 +48,6 @@ This is constructed by transfinite induction on `j`:
 `F.obj j ⟶ F.obj (Order.succ j)` has the left lifting property with respect to `p`;
 * When `j` is a limit element, we use the "continuity" of `F`.
 
-TODO: Given `P : MorphismProperty C`, deduce that the class of morphisms
-that have the left lifting property with respect to `P` is stable
-by transfinite composition.
-
 -/
 
 universe w v u
@@ -221,4 +226,34 @@ end transfiniteComposition
 
 end HasLiftingProperty
 
+namespace MorphismProperty
+
+variable (W : MorphismProperty C)
+  (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J]
+
+instance isStableUnderTransfiniteCompositionOfShape_llp :
+    W.llp.IsStableUnderTransfiniteCompositionOfShape J := by
+  rw [isStableUnderTransfiniteCompositionOfShape_iff]
+  rintro X Y f ⟨h⟩
+  have : W.llp (h.incl.app ⊥) := fun _ _ p hp ↦
+    HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot
+      (hc := h.isColimit) (fun j hj ↦ h.map_mem j hj _ hp)
+  exact (MorphismProperty.arrow_mk_iso_iff _
+    (Arrow.isoMk h.isoBot.symm (Iso.refl _))).2 this
+
+lemma transfiniteCompositionsOfShape_le_llp_rlp :
+    W.transfiniteCompositionsOfShape J ≤ W.rlp.llp := by
+  have := W.rlp.isStableUnderTransfiniteCompositionOfShape_llp J
+  rw [isStableUnderTransfiniteCompositionOfShape_iff] at this
+  exact le_trans (transfiniteCompositionsOfShape_monotone J W.le_llp_rlp) this
+
+lemma transfiniteCompositions_le_llp_rlp :
+    transfiniteCompositions.{w} W ≤ W.rlp.llp := by
+  intro _ _ f hf
+  rw [transfiniteCompositions_iff] at hf
+  obtain ⟨_, _, _, _, _, hf⟩ := hf
+  exact W.transfiniteCompositionsOfShape_le_llp_rlp _ _ hf
+
+end MorphismProperty
+
 end CategoryTheory