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..b644d80c29d975 --- /dev/null +++ b/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 diff --git a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean index 2f07fd2269e5b9..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,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 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