Consequences of model category axioms #

In this file, we deduce basic properties of fibrations, cofibrations, and weak equivalences from the axioms of model categories.

source

instance HomotopicalAlgebra.instIsStableUnderRetractsTrivialCofibrationsOfCofibrationsOfWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [(cofibrations C).IsStableUnderRetracts] [(weakEquivalences C).IsStableUnderRetracts] :

(trivialCofibrations C).IsStableUnderRetracts

source

instance HomotopicalAlgebra.instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithFibrations C] [(fibrations C).IsStableUnderRetracts] [(weakEquivalences C).IsStableUnderRetracts] :

(trivialFibrations C).IsStableUnderRetracts

source

instance HomotopicalAlgebra.instCofibrationCompOfIsStableUnderCompositionCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryWithCofibrations C] [(cofibrations C).IsStableUnderComposition] [hf : Cofibration f] [hg : Cofibration g] :

Cofibration (CategoryTheory.CategoryStruct.comp f g)

source

instance HomotopicalAlgebra.instFibrationCompOfIsStableUnderCompositionFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryWithFibrations C] [(fibrations C).IsStableUnderComposition] [hf : Fibration f] [hg : Fibration g] :

Fibration (CategoryTheory.CategoryStruct.comp f g)

source

instance HomotopicalAlgebra.instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryWithWeakEquivalences C] [(weakEquivalences C).IsStableUnderComposition] [hf : WeakEquivalence f] [hg : WeakEquivalence g] :

WeakEquivalence (CategoryTheory.CategoryStruct.comp f g)

source

theorem HomotopicalAlgebra.weakEquivalence_of_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [hg : WeakEquivalence g] [hfg : WeakEquivalence (CategoryTheory.CategoryStruct.comp f g)] :

WeakEquivalence f

source

theorem HomotopicalAlgebra.weakEquivalence_of_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : WeakEquivalence f] [hfg : WeakEquivalence (CategoryTheory.CategoryStruct.comp f g)] :

WeakEquivalence g

source

theorem HomotopicalAlgebra.weakEquivalence_postcomp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [WeakEquivalence g] :

WeakEquivalence (CategoryTheory.CategoryStruct.comp f g) ↔ WeakEquivalence f

source

theorem HomotopicalAlgebra.weakEquivalence_precomp_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [WeakEquivalence f] :

WeakEquivalence (CategoryTheory.CategoryStruct.comp f g) ↔ WeakEquivalence g

source

theorem HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {fg : X ⟶ Z} (fac : CategoryTheory.CategoryStruct.comp f g = fg) [WeakEquivalence g] [hfg : WeakEquivalence fg] :

WeakEquivalence f

source

theorem HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {fg : X ⟶ Z} (fac : CategoryTheory.CategoryStruct.comp f g = fg) [WeakEquivalence f] [WeakEquivalence fg] :

WeakEquivalence g

source

theorem HomotopicalAlgebra.fibrations_llp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] :

(fibrations C).llp = trivialCofibrations C

source

theorem HomotopicalAlgebra.trivialCofibrations_rlp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] :

(trivialCofibrations C).rlp = fibrations C

source

instance HomotopicalAlgebra.instIsStableUnderCobaseChangeTrivialCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] :

(trivialCofibrations C).IsStableUnderCobaseChange

source

instance HomotopicalAlgebra.instIsStableUnderBaseChangeFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] :

(fibrations C).IsStableUnderBaseChange

source

instance HomotopicalAlgebra.instIsMultiplicativeTrivialCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] :

(trivialCofibrations C).IsMultiplicative

source

instance HomotopicalAlgebra.instIsMultiplicativeFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] :

(fibrations C).IsMultiplicative

source

instance HomotopicalAlgebra.isStableUnderCoproductsOfShape_trivialCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] (J : Type w) :

(trivialCofibrations C).IsStableUnderCoproductsOfShape J

source

instance HomotopicalAlgebra.isStableUnderProductsOfShape_fibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] (J : Type w) :

(fibrations C).IsStableUnderProductsOfShape J

source

theorem HomotopicalAlgebra.trivialFibrations_llp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] :

(trivialFibrations C).llp = cofibrations C

source

theorem HomotopicalAlgebra.cofibrations_rlp (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] :

(cofibrations C).rlp = trivialFibrations C

source

instance HomotopicalAlgebra.instIsStableUnderCobaseChangeCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] :

(cofibrations C).IsStableUnderCobaseChange

source

instance HomotopicalAlgebra.instIsStableUnderBaseChangeTrivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] :

(trivialFibrations C).IsStableUnderBaseChange

source

instance HomotopicalAlgebra.instIsMultiplicativeCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] :

(cofibrations C).IsMultiplicative

source

instance HomotopicalAlgebra.instIsMultiplicativeTrivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] :

(trivialFibrations C).IsMultiplicative

source

instance HomotopicalAlgebra.isStableUnderCoproductsOfShape_cofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] (J : Type w) :

(cofibrations C).IsStableUnderCoproductsOfShape J

source

instance HomotopicalAlgebra.isStableUnderProductsOfShape_trivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] (J : Type w) :

(trivialFibrations C).IsStableUnderProductsOfShape J

source

instance HomotopicalAlgebra.instCofibrationInlOfIsStableUnderCobaseChangeCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] [(cofibrations C).IsStableUnderCobaseChange] [hg : Cofibration g] :

Cofibration (CategoryTheory.Limits.pushout.inl f g)

source

instance HomotopicalAlgebra.instCofibrationInrOfIsStableUnderCobaseChangeCofibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithCofibrations C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] [(cofibrations C).IsStableUnderCobaseChange] [hf : Cofibration f] :

Cofibration (CategoryTheory.Limits.pushout.inr f g)

source

instance HomotopicalAlgebra.instWeakEquivalenceInlOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] [(trivialCofibrations C).IsStableUnderCobaseChange] [Cofibration g] [WeakEquivalence g] :

WeakEquivalence (CategoryTheory.Limits.pushout.inl f g)

source

instance HomotopicalAlgebra.instWeakEquivalenceInrOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] [(trivialCofibrations C).IsStableUnderCobaseChange] [Cofibration f] [WeakEquivalence f] :

WeakEquivalence (CategoryTheory.Limits.pushout.inr f g)

source

instance HomotopicalAlgebra.instFibrationSndOfIsStableUnderBaseChangeFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(fibrations C).IsStableUnderBaseChange] [hf : Fibration f] :

Fibration (CategoryTheory.Limits.pullback.snd f g)

source

instance HomotopicalAlgebra.instFibrationFstOfIsStableUnderBaseChangeFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(fibrations C).IsStableUnderBaseChange] [hg : Fibration g] :

Fibration (CategoryTheory.Limits.pullback.fst f g)

source

instance HomotopicalAlgebra.instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(trivialFibrations C).IsStableUnderBaseChange] [Fibration f] [WeakEquivalence f] :

WeakEquivalence (CategoryTheory.Limits.pullback.snd f g)

source

instance HomotopicalAlgebra.instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithFibrations C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [(trivialFibrations C).IsStableUnderBaseChange] [Fibration g] [WeakEquivalence g] :

WeakEquivalence (CategoryTheory.Limits.pullback.fst f g)

source

instance HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), Cofibration (f i)] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] :

Cofibration (CategoryTheory.Limits.Sigma.map f)

source

instance HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct Y] [h : ∀ (i : J), Cofibration (f i)] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] [∀ (i : J), WeakEquivalence (f i)] :

WeakEquivalence (CategoryTheory.Limits.Sigma.map f)

source

instance HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), Fibration (f i)] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] :

Fibration (CategoryTheory.Limits.Pi.map f)

source

instance HomotopicalAlgebra.instWeakEquivalenceMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {J : Type u_1} {X Y : J → C} (f : (i : J) → X i ⟶ Y i) [CategoryTheory.Limits.HasProduct X] [CategoryTheory.Limits.HasProduct Y] [h : ∀ (i : J), Fibration (f i)] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] [∀ (i : J), WeakEquivalence (f i)] :

WeakEquivalence (CategoryTheory.Limits.Pi.map f)

source

instance HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] [h₁ : Cofibration f₁] [h₂ : Cofibration f₂] [CategoryTheory.Limits.HasBinaryCoproduct X₁ X₂] [CategoryTheory.Limits.HasBinaryCoproduct Y₁ Y₂] :

Cofibration (CategoryTheory.Limits.coprod.map f₁ f₂)

source

instance HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1 (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] [h₁ : Fibration f₁] [h₂ : Fibration f₂] [CategoryTheory.Limits.HasBinaryProduct X₁ X₂] [CategoryTheory.Limits.HasBinaryProduct Y₁ Y₂] :

Fibration (CategoryTheory.Limits.prod.map f₁ f₂)

source

instance HomotopicalAlgebra.instCofibrationOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] [CategoryTheory.IsIso f] :

Cofibration f

source

instance HomotopicalAlgebra.instFibrationOfIsWeakFactorizationSystemCofibrationsTrivialFibrationsOfIsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] [CategoryTheory.IsIso f] :

Fibration f

source

instance HomotopicalAlgebra.instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] [(weakEquivalences C).IsStableUnderRetracts] [CategoryTheory.IsIso f] :

WeakEquivalence f

source

instance HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] [(weakEquivalences C).IsStableUnderRetracts] [(weakEquivalences C).IsStableUnderComposition] :

(weakEquivalences C).IsMultiplicative

source

instance HomotopicalAlgebra.instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] [(weakEquivalences C).IsStableUnderRetracts] [(weakEquivalences C).IsStableUnderComposition] :

(weakEquivalences C).RespectsIso

source

instance HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).ContainsIdentities] (X : C) :

WeakEquivalence (CategoryTheory.CategoryStruct.id X)

source

instance HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (cofibrations C).MapFactorizationData (trivialFibrations C) f) :

Cofibration h.i

source

instance HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (cofibrations C).MapFactorizationData (trivialFibrations C) f) :

Fibration h.p

source

instance HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (cofibrations C).MapFactorizationData (trivialFibrations C) f) :

WeakEquivalence h.p

source

instance HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (trivialCofibrations C).MapFactorizationData (fibrations C) f) :

Cofibration h.i

source

instance HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (trivialCofibrations C).MapFactorizationData (fibrations C) f) :

WeakEquivalence h.i

source

instance HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] {X Y : C} (f : X ⟶ Y) (h : (trivialCofibrations C).MapFactorizationData (fibrations C) f) :

Fibration h.p

Documentation

Mathlib.AlgebraicTopology.ModelCategory.Instances

Consequences of model category axioms #