Theorems · Definition · category theory

HomotopicalAlgebra.ModelCategory.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {P : Sort u_1} →
      {categoryWithFibrations :
          autoParam (HomotopicalAlgebra.CategoryWithFibrations C)
            HomotopicalAlgebra.ModelCategory.categoryWithFibrations._autoParam} →
        {categoryWithCofibrations :
            autoParam (HomotopicalAlgebra.CategoryWithCofibrations C)
              HomotopicalAlgebra.ModelCategory.categoryWithCofibrations._autoParam} →
          {categoryWithWeakEquivalences :
              autoParam (HomotopicalAlgebra.CategoryWithWeakEquivalences C)
                HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences._autoParam} →
            {cm1a :
                autoParam (CategoryTheory.Limits.HasFiniteLimits C) HomotopicalAlgebra.ModelCategory.cm1a._autoParam} →
              {cm1b :
                  autoParam (CategoryTheory.Limits.HasFiniteColimits C)
                    HomotopicalAlgebra.ModelCategory.cm1b._autoParam} →
                {cm2 :
                    autoParam (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty
                      HomotopicalAlgebra.ModelCategory.cm2._autoParam} →
                  {cm3a :
                      autoParam (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts
                        HomotopicalAlgebra.ModelCategory.cm3a._autoParam} →
                    {cm3b :
                        autoParam (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts
                          HomotopicalAlgebra.ModelCategory.cm3b._autoParam} →
                      {cm3c :
                          autoParam (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts
                            HomotopicalAlgebra.ModelCategory.cm3c._autoParam} →
                        {cm4a :
                            autoParam
                              (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i]
                                [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p],
                                CategoryTheory.HasLiftingProperty i p)
                              HomotopicalAlgebra.ModelCategory.cm4a._autoParam} →
                          {cm4b :
                              autoParam
                                (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i]
                                  [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p],
                                  CategoryTheory.HasLiftingProperty i p)
                                HomotopicalAlgebra.ModelCategory.cm4b._autoParam} →
                            {cm5a :
                                autoParam
                                  ((HomotopicalAlgebra.trivialCofibrations C).HasFactorization
                                    (HomotopicalAlgebra.fibrations C))
                                  HomotopicalAlgebra.ModelCategory.cm5a._autoParam} →
                              {cm5b :
                                  autoParam
                                    ((HomotopicalAlgebra.cofibrations C).HasFactorization
                                      (HomotopicalAlgebra.trivialFibrations C))
                                    HomotopicalAlgebra.ModelCategory.cm5b._autoParam} →
                                {categoryWithFibrations' :
                                    autoParam (HomotopicalAlgebra.CategoryWithFibrations C)
                                      HomotopicalAlgebra.ModelCategory.categoryWithFibrations._autoParam} →
                                  {categoryWithCofibrations' :
                                      autoParam (HomotopicalAlgebra.CategoryWithCofibrations C)
                                        HomotopicalAlgebra.ModelCategory.categoryWithCofibrations._autoParam} →
                                    {categoryWithWeakEquivalences' :
                                        autoParam (HomotopicalAlgebra.CategoryWithWeakEquivalences C)
                                          HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences._autoParam} →
                                      {cm1a' :
                                          autoParam (CategoryTheory.Limits.HasFiniteLimits C)
                                            HomotopicalAlgebra.ModelCategory.cm1a._autoParam} →
                                        {cm1b' :
                                            autoParam (CategoryTheory.Limits.HasFiniteColimits C)
                                              HomotopicalAlgebra.ModelCategory.cm1b._autoParam} →
                                          {cm2' :
                                              autoParam (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty
                                                HomotopicalAlgebra.ModelCategory.cm2._autoParam} →
                                            {cm3a' :
                                                autoParam (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts
                                                  HomotopicalAlgebra.ModelCategory.cm3a._autoParam} →
                                              {cm3b' :
                                                  autoParam (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts
                                                    HomotopicalAlgebra.ModelCategory.cm3b._autoParam} →
                                                {cm3c' :
                                                    autoParam (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts
                                                      HomotopicalAlgebra.ModelCategory.cm3c._autoParam} →
                                                  {cm4a' :
                                                      autoParam
                                                        (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y)
                                                          [HomotopicalAlgebra.Cofibration i]
                                                          [HomotopicalAlgebra.WeakEquivalence i]
                                                          [HomotopicalAlgebra.Fibration p],
                                                          CategoryTheory.HasLiftingProperty i p)
                                                        HomotopicalAlgebra.ModelCategory.cm4a._autoParam} →
                                                    {cm4b' :
                                                        autoParam
                                                          (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y)
                                                            [HomotopicalAlgebra.Cofibration i]
                                                            [HomotopicalAlgebra.Fibration p]
                                                            [HomotopicalAlgebra.WeakEquivalence p],
                                                            CategoryTheory.HasLiftingProperty i p)
                                                          HomotopicalAlgebra.ModelCategory.cm4b._autoParam} →
                                                      {cm5a' :
                                                          autoParam
                                                            ((HomotopicalAlgebra.trivialCofibrations C).HasFactorization
                                                              (HomotopicalAlgebra.fibrations C))
                                                            HomotopicalAlgebra.ModelCategory.cm5a._autoParam} →
                                                        {cm5b' :
                                                            autoParam
                                                              ((HomotopicalAlgebra.cofibrations C).HasFactorization
                                                                (HomotopicalAlgebra.trivialFibrations C))
                                                              HomotopicalAlgebra.ModelCategory.cm5b._autoParam} →
                                                          { categoryWithFibrations := categoryWithFibrations,
                                                                categoryWithCofibrations := categoryWithCofibrations,
                                                                categoryWithWeakEquivalences :=
                                                                  categoryWithWeakEquivalences,
                                                                cm1a := cm1a, cm1b := cm1b, cm2 := cm2, cm3a := cm3a,
                                                                cm3b := cm3b, cm3c := cm3c, cm4a := cm4a, cm4b := cm4b,
                                                                cm5a := cm5a, cm5b := cm5b } =
                                                              { categoryWithFibrations := categoryWithFibrations',
                                                                categoryWithCofibrations := categoryWithCofibrations',
                                                                categoryWithWeakEquivalences :=
                                                                  categoryWithWeakEquivalences',
                                                                cm1a := cm1a', cm1b := cm1b', cm2 := cm2',
                                                                cm3a := cm3a', cm3b := cm3b', cm3c := cm3c',
                                                                cm4a := cm4a', cm4b := cm4b', cm5a := cm5a',
                                                                cm5b := cm5b' } →
                                                            (categoryWithFibrations ≍ categoryWithFibrations' →
                                                                categoryWithCofibrations ≍ categoryWithCofibrations' →
                                                                  categoryWithWeakEquivalences ≍
                                                                      categoryWithWeakEquivalences' →
                                                                    P) →
                                                              P

Defined in: Mathlib.AlgebraicTopology.ModelCategory.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Quiver.Homstatement and proof · cited by 32,603
HomotopicalAlgebra.ModelCategorystatement · cited by 141
HomotopicalAlgebra.CategoryWithWeakEquivalencesstatement and proof · cited by 77
CategoryTheory.HasLiftingPropertystatement and proof · cited by 50
HomotopicalAlgebra.CategoryWithFibrationsstatement and proof · cited by 46
HomotopicalAlgebra.CategoryWithCofibrationsstatement and proof · cited by 46
HomotopicalAlgebra.WeakEquivalencestatement and proof · cited by 45
HomotopicalAlgebra.weakEquivalencesstatement and proof · cited by 44
HomotopicalAlgebra.fibrationsstatement and proof · cited by 40
HomotopicalAlgebra.cofibrationsstatement and proof · cited by 37
CategoryTheory.Limits.HasFiniteLimitsstatement and proof · cited by 36

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.