Consequences of model category axioms

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

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

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

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)

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)

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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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₂)

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₂)

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

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

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

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

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

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