From 61a45b35952d9ecf88b836310026d86087b8d392 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 13:42:14 +0200 Subject: [PATCH 1/6] feat(AlgebraicTopology): transport a model category structure by an equivalence --- Mathlib.lean | 1 + .../ModelCategory/Transport.lean | 74 +++++++++++++++++++ .../MorphismProperty/Factorization.lean | 18 +++++ .../MorphismProperty/LiftingProperty.lean | 24 ++++++ 4 files changed, 117 insertions(+) create mode 100644 Mathlib/AlgebraicTopology/ModelCategory/Transport.lean diff --git a/Mathlib.lean b/Mathlib.lean index 8cb401a7c26386..f15ef5014052c0 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean new file mode 100644 index 00000000000000..eef5bb61e5c2c0 --- /dev/null +++ b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean @@ -0,0 +1,74 @@ +/- +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 + +@[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 + rw [cofibration_iff] at hf ⊢ + rwa [h₁] at hf + have {X Y : C} (f : X ⟶ Y) [hf : Fibration f] : Fibration (e.functor.map f) := by + rw [fibration_iff] at hf ⊢ + rwa [h₂] at hf + have {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f] : WeakEquivalence (e.functor.map f) := by + rw [weakEquivalence_iff] at hf ⊢ + rwa [h₃] at 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 diff --git a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean index 2f07fd2269e5b9..b425c278e80a3b 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean @@ -245,6 +245,24 @@ instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category* J] : HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) := ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩ +instance {D : Type*} [Category D] (F : D ⥤ C) [F.IsEquivalence] + [W₁.RespectsIso] [W₂.RespectsIso] + [HasFactorization W₁ W₂] : + HasFactorization (W₁.inverseImage F) (W₂.inverseImage F) where + nonempty_mapFactorizationData {X Y} f := by + let h := factorizationData W₁ W₂ (F.map f) + exact ⟨{ + 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) }⟩ + end MorphismProperty end CategoryTheory diff --git a/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean b/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean index 63c7882673c4f6..8d323c9cf812ce 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean +++ b/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 From 13db256635a29c7699fda06fe811c0e9b5be1df9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 13:46:50 +0200 Subject: [PATCH 2/6] cleaning up --- Mathlib/AlgebraicTopology/ModelCategory/Transport.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean index eef5bb61e5c2c0..1adc26afe11a8e 100644 --- a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean +++ b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean @@ -43,14 +43,11 @@ def ModelCategory.transport 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 - rw [cofibration_iff] at hf ⊢ - rwa [h₁] at hf + simpa [cofibration_iff, h₁] using hf have {X Y : C} (f : X ⟶ Y) [hf : Fibration f] : Fibration (e.functor.map f) := by - rw [fibration_iff] at hf ⊢ - rwa [h₂] at hf + simpa [fibration_iff, h₂] using hf have {X Y : C} (f : X ⟶ Y) [hf : WeakEquivalence f] : WeakEquivalence (e.functor.map f) := by - rw [weakEquivalence_iff] at hf ⊢ - rwa [h₃] at hf + simpa [weakEquivalence_iff, h₃] using hf exact { cm1a := ⟨fun _ _ _ ↦ Adjunction.hasLimitsOfShape_of_equivalence e.functor⟩ cm1b := ⟨fun _ _ _ ↦ Adjunction.hasColimitsOfShape_of_equivalence e.functor⟩ From 3a8ee3937359f65ff44967632cfce1f55f89db60 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 13:47:33 +0200 Subject: [PATCH 3/6] cleaning up --- Mathlib/AlgebraicTopology/ModelCategory/Transport.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean index 1adc26afe11a8e..41ce0ceab83fca 100644 --- a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean +++ b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean @@ -61,11 +61,7 @@ def ModelCategory.transport 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 } + cm5a := by rw [h₁', h₂]; infer_instance + cm5b := by rw [h₁, h₂']; infer_instance } end HomotopicalAlgebra From b2afef2c573acea7e1880a1a05b0c755a879a7c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 14:37:06 +0200 Subject: [PATCH 4/6] docstring --- Mathlib/AlgebraicTopology/ModelCategory/Transport.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean index 41ce0ceab83fca..dfec613beef5f6 100644 --- a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean +++ b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean @@ -29,6 +29,7 @@ namespace HomotopicalAlgebra open CategoryTheory Limits +/-- Transport of a model category structure via an equivalence of categories. -/ @[implicit_reducible] def ModelCategory.transport {C D : Type*} [Category* C] [Category* D] [ModelCategory D] From 33fdc19afa7970f4a9800cd308cb4c614131e267 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Thu, 7 May 2026 20:56:56 +0200 Subject: [PATCH 5/6] Update Mathlib/CategoryTheory/MorphismProperty/Factorization.lean Co-authored-by: Dagur Asgeirsson --- .../MorphismProperty/Factorization.lean | 33 ++++++++++--------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean index b425c278e80a3b..e35348177b8e20 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean @@ -245,23 +245,26 @@ instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category* J] : HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) := ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩ +noncomputable def mapFactorizationDataOfEquivalence {D : Type*} [Category D] (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 {D : Type*} [Category D] (F : D ⥤ C) [F.IsEquivalence] - [W₁.RespectsIso] [W₂.RespectsIso] - [HasFactorization W₁ W₂] : + [W₁.RespectsIso] [W₂.RespectsIso] [HasFactorization W₁ W₂] : HasFactorization (W₁.inverseImage F) (W₂.inverseImage F) where - nonempty_mapFactorizationData {X Y} f := by - let h := factorizationData W₁ W₂ (F.map f) - exact ⟨{ - 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) }⟩ + nonempty_mapFactorizationData f := + ⟨mapFactorizationDataOfEquivalence W₁ W₂ F f <| factorizationData W₁ W₂ (F.map f)⟩ end MorphismProperty From d6d9cd831ebbe1e69e9898a4de0b1d47e2ff3bd5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 21:07:27 +0200 Subject: [PATCH 6/6] better docstring --- .../AlgebraicTopology/ModelCategory/Transport.lean | 7 ++++++- .../MorphismProperty/Factorization.lean | 14 +++++++++----- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean index dfec613beef5f6..b644d80c29d975 100644 --- a/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean +++ b/Mathlib/AlgebraicTopology/ModelCategory/Transport.lean @@ -29,7 +29,12 @@ namespace HomotopicalAlgebra open CategoryTheory Limits -/-- Transport of a model category structure via an equivalence of categories. -/ +/-- 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] diff --git a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean index e35348177b8e20..1c755e174dcfe5 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean +++ b/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,9 +245,13 @@ instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category* J] : HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) := ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩ -noncomputable def mapFactorizationDataOfEquivalence {D : Type*} [Category D] (F : D ⥤ C) +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)) : + {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) @@ -260,11 +264,11 @@ noncomputable def mapFactorizationDataOfEquivalence {D : Type*} [Category D] (F exact Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _) fac := F.map_injective (by simp) -instance {D : Type*} [Category D] (F : D ⥤ C) [F.IsEquivalence] +instance (F : D ⥤ C) [F.IsEquivalence] [W₁.RespectsIso] [W₂.RespectsIso] [HasFactorization W₁ W₂] : HasFactorization (W₁.inverseImage F) (W₂.inverseImage F) where nonempty_mapFactorizationData f := - ⟨mapFactorizationDataOfEquivalence W₁ W₂ F f <| factorizationData W₁ W₂ (F.map f)⟩ + ⟨(factorizationData W₁ W₂ (F.map f)).ofIsEquivalence⟩ end MorphismProperty