Instances

📁 Source: Mathlib/AlgebraicTopology/ModelCategory/Instances.lean

Statistics

Metric	Count
Definitions	0
Theorems cofibrations_rlp, fibrations_llp, instCofibrationCompOfIsStableUnderCompositionCofibrations, instCofibrationICofibrationsTrivialFibrations, instCofibrationITrivialCofibrationsFibrations, instCofibrationInlOfIsStableUnderCobaseChangeCofibrations, instCofibrationInrOfIsStableUnderCobaseChangeCofibrations, instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations, instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1, instCofibrationOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsIso, instFibrationCompOfIsStableUnderCompositionFibrations, instFibrationFstOfIsStableUnderBaseChangeFibrations, instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations, instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1, instFibrationOfIsWeakFactorizationSystemCofibrationsTrivialFibrationsOfIsIso, instFibrationPCofibrationsTrivialFibrations, instFibrationPTrivialCofibrationsFibrations, instFibrationSndOfIsStableUnderBaseChangeFibrations, instIsMultiplicativeCofibrations, instIsMultiplicativeFibrations, instIsMultiplicativeTrivialCofibrations, instIsMultiplicativeTrivialFibrations, instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition, instIsStableUnderBaseChangeFibrations, instIsStableUnderBaseChangeTrivialFibrations, instIsStableUnderCobaseChangeCofibrations, instIsStableUnderCobaseChangeTrivialCofibrations, instIsStableUnderRetractsTrivialCofibrationsOfCofibrationsOfWeakEquivalences, instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences, instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition, instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences, instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, instWeakEquivalenceITrivialCofibrationsFibrations, instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences, instWeakEquivalenceInlOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, instWeakEquivalenceInrOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration, instWeakEquivalenceMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations, instWeakEquivalenceMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations, instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso, instWeakEquivalencePCofibrationsTrivialFibrations, instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration, isStableUnderCoproductsOfShape_cofibrations, isStableUnderCoproductsOfShape_trivialCofibrations, isStableUnderProductsOfShape_fibrations, isStableUnderProductsOfShape_trivialFibrations, trivialCofibrations_rlp, trivialFibrations_llp, weakEquivalence_of_postcomp, weakEquivalence_of_postcomp_of_fac, weakEquivalence_of_precomp, weakEquivalence_of_precomp_of_fac, weakEquivalence_postcomp_iff, weakEquivalence_precomp_iff	53
Total	53

HomotopicalAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofibrations_rlp 📖	mathematical	—	CategoryTheory.MorphismProperty.rlp cofibrations trivialFibrations	—	CategoryTheory.MorphismProperty.rlp_eq_of_wfs
fibrations_llp 📖	mathematical	—	CategoryTheory.MorphismProperty.llp fibrations trivialCofibrations	—	CategoryTheory.MorphismProperty.llp_eq_of_wfs
instCofibrationCompOfIsStableUnderCompositionCofibrations 📖	mathematical	—	Cofibration CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	cofibration_iff CategoryTheory.MorphismProperty.comp_mem Cofibration.mem
instCofibrationICofibrationsTrivialFibrations 📖	mathematical	—	Cofibration CategoryTheory.MorphismProperty.MapFactorizationData.Z cofibrations trivialFibrations CategoryTheory.MorphismProperty.MapFactorizationData.i	—	CategoryTheory.MorphismProperty.MapFactorizationData.hi
instCofibrationITrivialCofibrationsFibrations 📖	mathematical	—	Cofibration CategoryTheory.MorphismProperty.MapFactorizationData.Z trivialCofibrations fibrations CategoryTheory.MorphismProperty.MapFactorizationData.i	—	CategoryTheory.MorphismProperty.MapFactorizationData.hi
instCofibrationInlOfIsStableUnderCobaseChangeCofibrations 📖	mathematical	—	Cofibration CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inl	—	cofibration_iff CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPushout.of_hasPushout
instCofibrationInrOfIsStableUnderCobaseChangeCofibrations 📖	mathematical	—	Cofibration CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr	—	cofibration_iff CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.of_hasPushout
instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations 📖	mathematical	Cofibration	CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.map	—	CategoryTheory.MorphismProperty.colimMap isStableUnderCoproductsOfShape_cofibrations
instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1 📖	mathematical	—	Cofibration CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.map	—	cofibration_iff CategoryTheory.MorphismProperty.colimMap isStableUnderCoproductsOfShape_cofibrations
instCofibrationOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsIso 📖	mathematical	—	Cofibration	—	CategoryTheory.MorphismProperty.llp_of_isIso fibrations_llp
instFibrationCompOfIsStableUnderCompositionFibrations 📖	mathematical	—	Fibration CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	fibration_iff CategoryTheory.MorphismProperty.comp_mem Fibration.mem
instFibrationFstOfIsStableUnderBaseChangeFibrations 📖	mathematical	—	Fibration CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	—	fibration_iff CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback
instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations 📖	mathematical	Fibration	CategoryTheory.Limits.piObj CategoryTheory.Limits.Pi.map	—	CategoryTheory.MorphismProperty.limMap isStableUnderProductsOfShape_fibrations
instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1 📖	mathematical	—	Fibration CategoryTheory.Limits.prod CategoryTheory.Limits.prod.map	—	fibration_iff CategoryTheory.MorphismProperty.limMap isStableUnderProductsOfShape_fibrations
instFibrationOfIsWeakFactorizationSystemCofibrationsTrivialFibrationsOfIsIso 📖	mathematical	—	Fibration	—	CategoryTheory.MorphismProperty.rlp_of_isIso cofibrations_rlp
instFibrationPCofibrationsTrivialFibrations 📖	mathematical	—	Fibration CategoryTheory.MorphismProperty.MapFactorizationData.Z cofibrations trivialFibrations CategoryTheory.MorphismProperty.MapFactorizationData.p	—	CategoryTheory.MorphismProperty.MapFactorizationData.hp
instFibrationPTrivialCofibrationsFibrations 📖	mathematical	—	Fibration CategoryTheory.MorphismProperty.MapFactorizationData.Z trivialCofibrations fibrations CategoryTheory.MorphismProperty.MapFactorizationData.p	—	CategoryTheory.MorphismProperty.MapFactorizationData.hp
instFibrationSndOfIsStableUnderBaseChangeFibrations 📖	mathematical	—	Fibration CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd	—	fibration_iff CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.of_hasPullback
instIsMultiplicativeCofibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative cofibrations	—	trivialFibrations_llp CategoryTheory.MorphismProperty.llp_isMultiplicative
instIsMultiplicativeFibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative fibrations	—	trivialCofibrations_rlp CategoryTheory.MorphismProperty.rlp_isMultiplicative
instIsMultiplicativeTrivialCofibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative trivialCofibrations	—	fibrations_llp CategoryTheory.MorphismProperty.llp_isMultiplicative
instIsMultiplicativeTrivialFibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative trivialFibrations	—	cofibrations_rlp CategoryTheory.MorphismProperty.rlp_isMultiplicative
instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative weakEquivalences	—	weakEquivalence_iff instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso CategoryTheory.IsIso.id
instIsStableUnderBaseChangeFibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange fibrations	—	trivialCofibrations_rlp CategoryTheory.MorphismProperty.rlp_isStableUnderBaseChange
instIsStableUnderBaseChangeTrivialFibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange trivialFibrations	—	cofibrations_rlp CategoryTheory.MorphismProperty.rlp_isStableUnderBaseChange
instIsStableUnderCobaseChangeCofibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange cofibrations	—	trivialFibrations_llp CategoryTheory.MorphismProperty.llp_isStableUnderCobaseChange
instIsStableUnderCobaseChangeTrivialCofibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange trivialCofibrations	—	fibrations_llp CategoryTheory.MorphismProperty.llp_isStableUnderCobaseChange
instIsStableUnderRetractsTrivialCofibrationsOfCofibrationsOfWeakEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts trivialCofibrations	—	CategoryTheory.MorphismProperty.instIsStableUnderRetractsMin
instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts trivialFibrations	—	CategoryTheory.MorphismProperty.instIsStableUnderRetractsMin
instRespectsIsoWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso weakEquivalences	—	CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition weakEquivalence_iff instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso
instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences 📖	mathematical	—	WeakEquivalence CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	weakEquivalence_iff CategoryTheory.MorphismProperty.comp_mem WeakEquivalence.mem
instWeakEquivalenceFstOfIsStableUnderBaseChangeTrivialFibrationsOfFibration 📖	mathematical	—	WeakEquivalence CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst	—	weakEquivalence_iff CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback mem_trivialFibrations
instWeakEquivalenceITrivialCofibrationsFibrations 📖	mathematical	—	WeakEquivalence CategoryTheory.MorphismProperty.MapFactorizationData.Z trivialCofibrations fibrations CategoryTheory.MorphismProperty.MapFactorizationData.i	—	CategoryTheory.MorphismProperty.MapFactorizationData.hi
instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences 📖	mathematical	—	WeakEquivalence CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	weakEquivalence_iff CategoryTheory.MorphismProperty.id_mem
instWeakEquivalenceInlOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration 📖	mathematical	—	WeakEquivalence CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inl	—	weakEquivalence_iff CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPushout.of_hasPushout mem_trivialCofibrations
instWeakEquivalenceInrOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration 📖	mathematical	—	WeakEquivalence CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr	—	weakEquivalence_iff CategoryTheory.MorphismProperty.of_isPushout CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.of_hasPushout mem_trivialCofibrations
instWeakEquivalenceMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations 📖	mathematical	Fibration WeakEquivalence	CategoryTheory.Limits.piObj CategoryTheory.Limits.Pi.map	—	weakEquivalence_iff CategoryTheory.MorphismProperty.limMap isStableUnderProductsOfShape_trivialFibrations mem_trivialFibrations
instWeakEquivalenceMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations 📖	mathematical	Cofibration WeakEquivalence	CategoryTheory.Limits.sigmaObj CategoryTheory.Limits.Sigma.map	—	weakEquivalence_iff CategoryTheory.MorphismProperty.colimMap isStableUnderCoproductsOfShape_trivialCofibrations mem_trivialCofibrations
instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso 📖	mathematical	—	WeakEquivalence	—	CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.hasFactorization weakEquivalence_iff CategoryTheory.MorphismProperty.of_retract CategoryTheory.MorphismProperty.MapFactorizationData.fac CategoryTheory.HasLiftingProperty.of_left_iso CategoryTheory.MorphismProperty.MapFactorizationData.hi
instWeakEquivalencePCofibrationsTrivialFibrations 📖	mathematical	—	WeakEquivalence CategoryTheory.MorphismProperty.MapFactorizationData.Z cofibrations trivialFibrations CategoryTheory.MorphismProperty.MapFactorizationData.p	—	CategoryTheory.MorphismProperty.MapFactorizationData.hp
instWeakEquivalenceSndOfIsStableUnderBaseChangeTrivialFibrationsOfFibration 📖	mathematical	—	WeakEquivalence CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd	—	weakEquivalence_iff CategoryTheory.MorphismProperty.of_isPullback CategoryTheory.IsPullback.of_hasPullback mem_trivialFibrations
isStableUnderCoproductsOfShape_cofibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape cofibrations	—	trivialFibrations_llp CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape
isStableUnderCoproductsOfShape_trivialCofibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape trivialCofibrations	—	fibrations_llp CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape
isStableUnderProductsOfShape_fibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape fibrations	—	trivialCofibrations_rlp CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape
isStableUnderProductsOfShape_trivialFibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape trivialFibrations	—	cofibrations_rlp CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape
trivialCofibrations_rlp 📖	mathematical	—	CategoryTheory.MorphismProperty.rlp trivialCofibrations fibrations	—	CategoryTheory.MorphismProperty.rlp_eq_of_wfs
trivialFibrations_llp 📖	mathematical	—	CategoryTheory.MorphismProperty.llp trivialFibrations cofibrations	—	CategoryTheory.MorphismProperty.llp_eq_of_wfs
weakEquivalence_of_postcomp 📖	mathematical	—	WeakEquivalence	—	weakEquivalence_iff CategoryTheory.MorphismProperty.of_postcomp CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPostcompProperty
weakEquivalence_of_postcomp_of_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	WeakEquivalence	—	weakEquivalence_of_postcomp
weakEquivalence_of_precomp 📖	mathematical	—	WeakEquivalence	—	weakEquivalence_iff CategoryTheory.MorphismProperty.of_precomp CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPrecompProperty
weakEquivalence_of_precomp_of_fac 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	WeakEquivalence	—	weakEquivalence_of_precomp
weakEquivalence_postcomp_iff 📖	mathematical	—	WeakEquivalence CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	weakEquivalence_of_postcomp instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition
weakEquivalence_precomp_iff 📖	mathematical	—	WeakEquivalence CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	weakEquivalence_of_precomp instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition

---

← Back to Index