[Merged by Bors] - feat(AlgebraicTopology): transport a model category structure by an equivalence

Mathlib.lean

@@ -1488,6 +1488,7 @@ public import Mathlib.AlgebraicTopology.ModelCategory.Opposite
 public import Mathlib.AlgebraicTopology.ModelCategory.Over
 public import Mathlib.AlgebraicTopology.ModelCategory.PathObject
 public import Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
+public import Mathlib.AlgebraicTopology.ModelCategory.Transport
 public import Mathlib.AlgebraicTopology.MooreComplex
 public import Mathlib.AlgebraicTopology.Quasicategory.Basic
 public import Mathlib.AlgebraicTopology.Quasicategory.Nerve

Mathlib/AlgebraicTopology/ModelCategory/Transport.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2026 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.AlgebraicTopology.ModelCategory.Basic
+public import Mathlib.CategoryTheory.Adjunction.Limits
+
+/-!
+# Transport a model category via an equivalence
+
+Given an equivalence of categories `e : C ≌ D`, we transport
+a model category structure on `D` in order to obtain a model
+category structure on `C`. More precisely, we assume
+that `C` has been equipped with notions of cofibrations, fibrations
+and weak equivalences and that these properties of morphisms
+are the inverse images of the corresponding properties of
+morphisms by the functor `e.functor : C ⥤ D`. Under these
+assumptions, we show that the model category axioms for `C`
+hold if they hold for `D`.
+
+-/
+
+@[expose] public section
+
+namespace HomotopicalAlgebra
+
+open CategoryTheory Limits
+
+/-- Transport of a model category structure on a category `D` via an equivalence of
+categories `e : C ≌ D`. We assume that the category `C` is already endowed
+with a `CategoryWithFibrations` instance (and similarly for cofibrations and weak
+equivalences), and that the three properties of morphisms (fibrations, cofibrations,
+weak equivalences) in `C` coincide with the inverse images by `e.functor : C ⥤ D`
+of the corresponding properties of morphisms in `D`. -/
+@[implicit_reducible]
+def ModelCategory.transport
+    {C D : Type*} [Category* C] [Category* D] [ModelCategory D]
+    [CategoryWithCofibrations C] [CategoryWithFibrations C]
+    [CategoryWithWeakEquivalences C] (e : C ≌ D)
+    (h₁ : cofibrations C = (cofibrations D).inverseImage e.functor)
+    (h₂ : fibrations C = (fibrations D).inverseImage e.functor)
+    (h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor) :
+    ModelCategory C := by
+  have h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor := by
+    simp [trivialCofibrations, h₁, h₃]
+  have h₂' : trivialFibrations C = (trivialFibrations D).inverseImage e.functor := by
+    simp [trivialFibrations, h₂, h₃]
+  have {X Y : C} (f : X ⟶ Y) [hf : Cofibration f] : Cofibration (e.functor.map f) := by
+    simpa [cofibration_iff, h₁] using hf
+  have {X Y : C} (f : X ⟶ Y) [hf : Fibration f] : Fibration (e.functor.map f) := by
+    simpa [fibration_iff, h₂] using hf
+  have {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f] : WeakEquivalence (e.functor.map f) := by
+    simpa [weakEquivalence_iff, h₃] using hf
+  exact {
+    cm1a := ⟨fun _ _ _ ↦ Adjunction.hasLimitsOfShape_of_equivalence e.functor⟩
+    cm1b := ⟨fun _ _ _ ↦ Adjunction.hasColimitsOfShape_of_equivalence e.functor⟩
+    cm2 := by rw [h₃]; infer_instance
+    cm3a := by rw [h₃]; infer_instance
+    cm3b := by rw [h₂]; infer_instance
+    cm3c := by rw [h₁]; infer_instance
+    cm4a _ _ _ _ _ := by
+      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
+      infer_instance
+    cm4b _ _ _ _ _ := by
+      rw [← e.functor.hasLiftingProperty_iff_of_isEquivalence]
+      infer_instance
+    cm5a := by rw [h₁', h₂]; infer_instance
+    cm5b := by rw [h₁, h₂']; infer_instance }
+
+end HomotopicalAlgebra

Mathlib/CategoryTheory/MorphismProperty/Factorization.lean

@@ -39,7 +39,7 @@ namespace CategoryTheory
 
 namespace MorphismProperty
 
-variable {C : Type*} [Category* C] (W₁ W₂ : MorphismProperty C)
+variable {C D : Type*} [Category* C] [Category* D] (W₁ W₂ : MorphismProperty C)
 
 /-- Given two classes of morphisms `W₁` and `W₂` on a category `C`, this is
 the data of the factorization of a morphism `f : X ⟶ Y` as `i ≫ p` with
@@ -245,6 +245,31 @@ instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category* J] :
     HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) :=
   ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩
 
+variable {W₁ W₂} in
+/-- The term in `MapFactorizationData (W₁.inverseImage F) (W₂.inverseImage F) f`
+deduced from `h : MapFactorizationData W₁ W₂ (F.map f)` when `F` is an equivalence
+of categories and both `W₁` and `W₂` respect isomorphisms. -/
+noncomputable def MapFactorizationData.ofIsEquivalence {F : D ⥤ C}
+    [F.IsEquivalence] [W₁.RespectsIso] [W₂.RespectsIso]
+    {X Y : D} {f : X ⟶ Y} (h : MapFactorizationData W₁ W₂ (F.map f)) :
+    MapFactorizationData (W₁.inverseImage F) (W₂.inverseImage F) f where
+  Z := F.objPreimage h.Z
+  i := F.preimage (h.i ≫ (F.objObjPreimageIso h.Z).inv)
+  p := F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)
+  hi := by
+    refine (W₁.arrow_mk_iso_iff ?_).1 h.hi
+    exact Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm
+  hp := by
+    refine (W₂.arrow_mk_iso_iff ?_).1 h.hp
+    exact Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _)
+  fac := F.map_injective (by simp)
+
+instance (F : D ⥤ C) [F.IsEquivalence]
+    [W₁.RespectsIso] [W₂.RespectsIso] [HasFactorization W₁ W₂] :
+    HasFactorization (W₁.inverseImage F) (W₂.inverseImage F) where
+  nonempty_mapFactorizationData f :=
+    ⟨(factorizationData W₁ W₂ (F.map f)).ofIsEquivalence⟩
+
 end MorphismProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

@@ -166,6 +166,30 @@ lemma rlp_retracts : T.retracts.rlp = T.rlp := by
   · rw [← le_llp_iff_le_rlp]
     exact T.retracts_le_llp_rlp
 
+lemma rlp_ofHoms_iff_hasLiftingProperty (ι : Type*) [Nonempty ι] {A B X Y : C}
+    (i : A ⟶ B) (p : X ⟶ Y) :
+    (MorphismProperty.ofHoms (fun (_ : ι) ↦ i)).rlp p ↔ HasLiftingProperty i p :=
+  ⟨fun hp ↦ hp _ ⟨Classical.arbitrary ι⟩,
+    by rintro _ _ _ _ ⟨⟩; assumption⟩
+
+lemma llp_ofHoms_iff_hasLiftingProperty (ι : Type*) [Nonempty ι] {A B X Y : C}
+    (i : A ⟶ B) (p : X ⟶ Y) :
+    (MorphismProperty.ofHoms (fun (_ : ι) ↦ p)).llp i ↔ HasLiftingProperty i p :=
+  ⟨fun hp ↦ hp _ ⟨Classical.arbitrary ι⟩,
+    by rintro _ _ _ _ ⟨⟩; assumption⟩
+
 end MorphismProperty
 
+lemma Functor.hasLiftingProperty_iff_of_isEquivalence
+    {D : Type*} [Category* D] (G : C ⥤ D) [G.IsEquivalence]
+    {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) :
+    HasLiftingProperty (G.map i) (G.map p) ↔
+      HasLiftingProperty i p := by
+  simp only [dsimp% G.asEquivalence.toAdjunction.hasLiftingProperty_iff,
+    ← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
+  exact MorphismProperty.arrow_mk_iso_iff _
+    (Arrow.isoMk (G.asEquivalence.unitIso.symm.app _)
+      (G.asEquivalence.unitIso.symm.app _)
+      (G.asEquivalence.unitIso.inv.naturality p).symm)
+
 end CategoryTheory