feat(CategoryTheory): the retract argument

Mathlib.lean

@@ -2103,6 +2103,7 @@ import Mathlib.CategoryTheory.MorphismProperty.Limits
 import Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
 import Mathlib.CategoryTheory.MorphismProperty.Representable
 import Mathlib.CategoryTheory.MorphismProperty.Retract
+import Mathlib.CategoryTheory.MorphismProperty.RetractArgument
 import Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans

Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean

@@ -115,6 +115,11 @@ lemma mem_trivialFibrations [Fibration f] [WeakEquivalence f] :
     trivialFibrations C f :=
   ⟨mem_fibrations f, mem_weakEquivalences f⟩
 
+lemma mem_trivialFibrations_iff :
+    trivialFibrations C f ↔ Fibration f ∧ WeakEquivalence f := by
+  rw [fibration_iff, weakEquivalence_iff]
+  rfl
+
 end TrivFib
 
 section TrivCof
@@ -137,6 +142,11 @@ lemma mem_trivialCofibrations [Cofibration f] [WeakEquivalence f] :
     trivialCofibrations C f :=
   ⟨mem_cofibrations f, mem_weakEquivalences f⟩
 
+lemma mem_trivialCofibrations_iff :
+    trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f := by
+  rw [cofibration_iff, weakEquivalence_iff]
+  rfl
+
 end TrivCof
 
 end HomotopicalAlgebra

Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

@@ -6,6 +6,7 @@ Authors: Jack McKoen
 import Mathlib.CategoryTheory.MorphismProperty.Limits
 import Mathlib.CategoryTheory.MorphismProperty.Retract
 import Mathlib.CategoryTheory.LiftingProperties.Limits
+import Mathlib.Order.GaloisConnection.Defs
 
 /-!
 # Left and right lifting properties
@@ -35,6 +36,14 @@ right lifting property (rlp) with respect to `T`. -/
 def rlp : MorphismProperty C := fun _ _ f ↦
   ∀ ⦃X Y : C⦄ (g : X ⟶ Y) (_ : T g), HasLiftingProperty g f
 
+lemma llp_of_isIso {A B : C} (i : A ⟶ B) [IsIso i] :
+    T.llp i :=
+  fun _ _ _ _ ↦ inferInstance
+
+lemma rlp_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] :
+    T.rlp f :=
+  fun _ _ _ _ ↦ inferInstance
+
 lemma llp_isStableUnderRetracts : T.llp.IsStableUnderRetracts where
   of_retract h hg _ _ f hf :=
     letI := hg _ hf
@@ -84,6 +93,16 @@ lemma rlp_IsStableUnderProductsOfShape (J : Type*) :
   have := fun j ↦ hf j _ hp
   infer_instance
 
+lemma le_llp_iff_le_rlp (T' : MorphismProperty C) :
+    T ≤ T'.llp ↔ T' ≤ T.rlp :=
+  ⟨fun h _ _ _ hp _ _ _ hi ↦ h _ hi _ hp,
+    fun h _ _ _ hi _ _ _ hp ↦ h _ hp _ hi⟩
+
+lemma gc_llp_rlp :
+    GaloisConnection (OrderDual.toDual (α := MorphismProperty C) ∘ llp)
+      (rlp ∘ OrderDual.ofDual) :=
+  fun _ _ ↦ le_llp_iff_le_rlp _ _
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/MorphismProperty/Retract.lean

@@ -47,6 +47,11 @@ instance IsStableUnderRetracts.isomorphisms : (isomorphisms C).IsStableUnderRetr
     · rw [← h.i_w_assoc, IsIso.hom_inv_id_assoc, h.retract_left]
     · rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]
 
+instance (P₁ P₂ : MorphismProperty C)
+    [P₁.IsStableUnderRetracts] [P₂.IsStableUnderRetracts] :
+    (P₁ ⊓ P₂).IsStableUnderRetracts where
+  of_retract := fun h ⟨h₁, h₂⟩ ↦ ⟨of_retract h h₁, of_retract h h₂⟩
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/MorphismProperty/RetractArgument.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.MorphismProperty.Factorization
+import Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
+
+/-!
+# The retract argument
+
+Let `W₁` and `W₂` be classes of morphisms in a category `C` such that
+any morphism can be factored as a morphism in `W₁` followed by
+a morphism in `W₂` (this is `HasFactorization W₁ W₂`).
+If `W₁` has the left lifting property with respect to `W₂`
+(i.e. `W₁ ≤ W₂.llp`, or equivalently `W₂ ≤ W₁.rlp`),
+then `W₂.llp = W₁` if `W₁` is stable under retracts,
+and `W₁.rlp = W₂` if `W₂` is.
+
+## Reference
+- https://ncatlab.org/nlab/show/weak+factorization+system#retract_argument
+
+-/
+
+namespace CategoryTheory
+
+variable {C : Type*} [Category C]
+
+/-- If `i ≫ p = f`, and `f` has the left lifting property with respect to `p`,
+then `f` is a retract of `i`. -/
+noncomputable def RetractArrow.ofLeftLiftingProperty
+    {X Y Z : C} {f : X ⟶ Z} {i : X ⟶ Y} {p : Y ⟶ Z} (h : i ≫ p = f)
+    [HasLiftingProperty f p] : RetractArrow f i :=
+  have sq : CommSq i f p (𝟙 _) := ⟨by simp [h]⟩
+  { i := Arrow.homMk (𝟙 X) sq.lift
+    r := Arrow.homMk (𝟙 X) p }
+
+/-- If `i ≫ p = f`, and `f` has the right lifting property with respect to `i`,
+then `f` is a retract of `p`. -/
+noncomputable def RetractArrow.ofRightLiftingProperty
+    {X Y Z : C} {f : X ⟶ Z} {i : X ⟶ Y} {p : Y ⟶ Z} (h : i ≫ p = f)
+    [HasLiftingProperty i f] : RetractArrow f p :=
+  have sq : CommSq (𝟙 _) i f p := ⟨by simp [h]⟩
+  { i := Arrow.homMk i (𝟙 _)
+    r := Arrow.homMk sq.lift (𝟙 _) }
+
+namespace MorphismProperty
+
+variable {W₁ W₂ : MorphismProperty C}
+
+lemma llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts
+    [HasFactorization W₁ W₂] [W₁.IsStableUnderRetracts] (h₁ : W₁ ≤ W₂.llp) :
+    W₂.llp = W₁ :=
+  le_antisymm (fun A B i hi ↦ by
+    have h := factorizationData W₁ W₂ i
+    have := hi _ h.hp
+    simpa using of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi) h₁
+
+lemma rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts
+    [HasFactorization W₁ W₂] [W₂.IsStableUnderRetracts] (h₂ : W₂ ≤ W₁.rlp) :
+    W₁.rlp = W₂ :=
+  le_antisymm (fun X Y p hp ↦ by
+    have h := factorizationData W₁ W₂ p
+    have := hp _ h.hi
+    simpa using of_retract (RetractArrow.ofRightLiftingProperty h.fac) h.hp) h₂
+
+end MorphismProperty
+
+end CategoryTheory