PathObject

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

Statistics

Metric	Count
Definitions PathObject, IsGood, IsVeryGood, ofFactorizationData, toPrepathObject, trans, PrepathObject, P, p, p₀, p₁, trans, ι	13
Theorems fibration_p, cofibration_ι, toIsGood, exists_very_good, instFibrationP₀, instFibrationP₁, instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations, instIsCofibrantPOfIsVeryGood, instIsFibrantP, instIsGoodSymmOfRespectsIsoFibrations, instIsGoodTrans, instIsVeryGoodOfFactorizationData, instIsVeryGoodSymmOfRespectsIsoFibrations, instNonempty, instWeakEquivalenceP₀, instWeakEquivalenceP₁, ofFactorizationData_P, ofFactorizationData_p, ofFactorizationData_p₀, ofFactorizationData_p₁, ofFactorizationData_ι, symm_P, symm_p, symm_p_assoc, symm_p₀, symm_p₁, symm_ι, trans_P, trans_p₀, trans_p₁, trans_ι, weakEquivalence_ι, p_fst, p_fst_assoc, p_snd, p_snd_assoc, symm_P, symm_p, symm_p_assoc, symm_p₀, symm_p₁, symm_ι, trans_P, trans_p₀, trans_p₁, trans_ι, ι_p₀, ι_p₀_assoc, ι_p₁, ι_p₁_assoc	50
Total	63

HomotopicalAlgebra

Definitions

Name	Category	Theorems
PathObject 📖	CompData	1 math math: PathObject.instNonempty
PrepathObject 📖	CompData	—

HomotopicalAlgebra.PathObject

Definitions

Name	Category	Theorems
IsGood 📖	CompData	5 math math: instIsGoodTrans, HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject, RightHomotopy.exists_good_pathObject, IsVeryGood.toIsGood, instIsGoodSymmOfRespectsIsoFibrations
IsVeryGood 📖	CompData	4 math math: exists_very_good, HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject, instIsVeryGoodSymmOfRespectsIsoFibrations, instIsVeryGoodOfFactorizationData
ofFactorizationData 📖	CompOp	7 math math: ofFactorizationData_p, instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations, ofFactorizationData_p₁, instIsVeryGoodOfFactorizationData, ofFactorizationData_P, ofFactorizationData_p₀, ofFactorizationData_ι
toPrepathObject 📖	CompOp	26 math math: weakEquivalence_ι, symm_p₁, instFibrationP₀, symm_p₀, ofFactorizationData_p, symm_p_assoc, symm_p, IsVeryGood.cofibration_ι, instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations, ofFactorizationData_p₁, instIsFibrantP, trans_p₀, instFibrationP₁, symm_ι, ofFactorizationData_P, trans_ι, symm_P, ofFactorizationData_p₀, instIsCofibrantPOfIsVeryGood, instWeakEquivalenceP₁, ofFactorizationData_ι, IsGood.fibration_p, RightHomotopy.homotopy_extension, instWeakEquivalenceP₀, trans_p₁, trans_P
trans 📖	CompOp	5 math math: instIsGoodTrans, trans_p₀, trans_ι, trans_p₁, trans_P

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_very_good 📖	mathematical	—	IsVeryGood HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5a instIsVeryGoodOfFactorizationData
instFibrationP₀ 📖	mathematical	—	HomotopicalAlgebra.Fibration HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.PrepathObject.p₀	—	HomotopicalAlgebra.PrepathObject.p_fst HomotopicalAlgebra.instFibrationCompOfIsStableUnderCompositionFibrations IsGood.fibration_p HomotopicalAlgebra.instFibrationFstOfIsFibrant
instFibrationP₁ 📖	mathematical	—	HomotopicalAlgebra.Fibration HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.PrepathObject.p₁	—	HomotopicalAlgebra.PrepathObject.p_snd HomotopicalAlgebra.instFibrationCompOfIsStableUnderCompositionFibrations IsGood.fibration_p HomotopicalAlgebra.instFibrationSndOfIsFibrant
instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.isCofibrant_of_cofibration IsVeryGood.cofibration_ι instIsVeryGoodOfFactorizationData
instIsCofibrantPOfIsVeryGood 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant HomotopicalAlgebra.PrepathObject.P toPrepathObject	—	HomotopicalAlgebra.isCofibrant_of_cofibration IsVeryGood.cofibration_ι
instIsFibrantP 📖	mathematical	—	HomotopicalAlgebra.IsFibrant HomotopicalAlgebra.PrepathObject.P toPrepathObject	—	HomotopicalAlgebra.isFibrant_of_fibration instFibrationP₀
instIsGoodSymmOfRespectsIsoFibrations 📖	mathematical	—	IsGood symm CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape HomotopicalAlgebra.fibration_iff IsGood.fibration_p symm_p CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.Category.id_comp CategoryTheory.Limits.prod.comp_lift HomotopicalAlgebra.PrepathObject.p_snd HomotopicalAlgebra.PrepathObject.p_fst CategoryTheory.Limits.limit.lift_π
instIsGoodTrans 📖	mathematical	—	IsGood HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair HomotopicalAlgebra.ModelCategory.categoryWithFibrations	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.prod.lift_map CategoryTheory.Category.comp_id CategoryTheory.Limits.prod.hom_ext CategoryTheory.Limits.pullback.condition CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.assoc HomotopicalAlgebra.PrepathObject.p_fst HomotopicalAlgebra.PrepathObject.p_snd CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.IsPullback.of_hasPullback HomotopicalAlgebra.fibration_iff CategoryTheory.MorphismProperty.of_isPullback HomotopicalAlgebra.instIsStableUnderBaseChangeFibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_right CategoryTheory.IsPullback.of_prod_fst_with_id IsGood.fibration_p HomotopicalAlgebra.instFibrationCompOfIsStableUnderCompositionFibrations CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeFibrations HomotopicalAlgebra.instFibrationMapOfIsWeakFactorizationSystemTrivialCofibrationsFibrations_1 instFibrationP₀ HomotopicalAlgebra.instFibrationOfIsWeakFactorizationSystemCofibrationsTrivialFibrationsOfIsIso HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations CategoryTheory.IsIso.id
instIsVeryGoodOfFactorizationData 📖	mathematical	—	IsVeryGood HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype ofFactorizationData_p HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations
instIsVeryGoodSymmOfRespectsIsoFibrations 📖	mathematical	—	IsVeryGood symm CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instIsGoodSymmOfRespectsIsoFibrations IsVeryGood.toIsGood IsVeryGood.cofibration_ι
instNonempty 📖	mathematical	—	HomotopicalAlgebra.PathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype exists_very_good
instWeakEquivalenceP₀ 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.PrepathObject.p₀	—	HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac HomotopicalAlgebra.PrepathObject.ι_p₀ weakEquivalence_ι HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences
instWeakEquivalenceP₁ 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.PrepathObject.p₁	—	HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac HomotopicalAlgebra.PrepathObject.ι_p₁ weakEquivalence_ι HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences
ofFactorizationData_P 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.prod CategoryTheory.Limits.diag	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
ofFactorizationData_p 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.MorphismProperty.MapFactorizationData.p HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.prod CategoryTheory.Limits.diag	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.prod.hom_ext HomotopicalAlgebra.PrepathObject.p_fst HomotopicalAlgebra.PrepathObject.p_snd
ofFactorizationData_p₀ 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p₀ toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.prod CategoryTheory.Limits.diag CategoryTheory.MorphismProperty.MapFactorizationData.p CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
ofFactorizationData_p₁ 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p₁ toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.prod CategoryTheory.Limits.diag CategoryTheory.MorphismProperty.MapFactorizationData.p CategoryTheory.Limits.prod.snd	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
ofFactorizationData_ι 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.ι toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.i HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.prod CategoryTheory.Limits.diag	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
symm_P 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.P toPrepathObject symm	—	—
symm_p 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p toPrepathObject symm CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.PrepathObject.P CategoryTheory.Limits.prod CategoryTheory.Iso.hom CategoryTheory.Limits.prod.braiding	—	HomotopicalAlgebra.PrepathObject.symm_p
symm_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.PrepathObject.P toPrepathObject symm CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair HomotopicalAlgebra.PrepathObject.p CategoryTheory.Iso.hom CategoryTheory.Limits.prod.braiding	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' symm_p
symm_p₀ 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p₀ toPrepathObject symm HomotopicalAlgebra.PrepathObject.p₁	—	—
symm_p₁ 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p₁ toPrepathObject symm HomotopicalAlgebra.PrepathObject.p₀	—	—
symm_ι 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.ι toPrepathObject symm	—	—
trans_P 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.Limits.pullback HomotopicalAlgebra.PrepathObject.p₁ HomotopicalAlgebra.PrepathObject.p₀	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
trans_p₀ 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p₀ toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PrepathObject.p₁ CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
trans_p₁ 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.p₁ toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PrepathObject.p₀ CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
trans_ι 📖	mathematical	—	HomotopicalAlgebra.PrepathObject.ι toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.Limits.pullback.lift HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PrepathObject.p₁ HomotopicalAlgebra.PrepathObject.p₀	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
weakEquivalence_ι 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.PrepathObject.P toPrepathObject HomotopicalAlgebra.PrepathObject.ι	—	—

HomotopicalAlgebra.PathObject.IsGood

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fibration_p 📖	mathematical	—	HomotopicalAlgebra.Fibration HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PathObject.toPrepathObject CategoryTheory.Limits.prod HomotopicalAlgebra.PrepathObject.p	—	—

HomotopicalAlgebra.PathObject.IsVeryGood

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofibration_ι 📖	mathematical	—	HomotopicalAlgebra.Cofibration HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PathObject.toPrepathObject HomotopicalAlgebra.PrepathObject.ι	—	—
toIsGood 📖	mathematical	—	HomotopicalAlgebra.PathObject.IsGood	—	—

HomotopicalAlgebra.PrepathObject

Definitions

Name	Category	Theorems
P 📖	CompOp	41 math math: HomotopicalAlgebra.PathObject.weakEquivalence_ι, p_fst_assoc, p_snd, trans_p₀, trans_P, HomotopicalAlgebra.PathObject.instFibrationP₀, ι_p₁_assoc, symm_p, p_fst, trans_p₁, RightHomotopy.refl_h, HomotopicalAlgebra.PathObject.symm_p_assoc, HomotopicalAlgebra.PathObject.symm_p, HomotopicalAlgebra.PathObject.IsVeryGood.cofibration_ι, HomotopicalAlgebra.PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations, RightHomotopy.precomp_h, HomotopicalAlgebra.PathObject.instIsFibrantP, HomotopicalAlgebra.PathObject.trans_p₀, symm_P, HomotopicalAlgebra.PathObject.instFibrationP₁, HomotopicalAlgebra.PathObject.ofFactorizationData_P, symm_p_assoc, HomotopicalAlgebra.PathObject.trans_ι, RightHomotopy.h₀, HomotopicalAlgebra.PathObject.symm_P, p_snd_assoc, RightHomotopy.h₀_assoc, ι_p₀, HomotopicalAlgebra.PathObject.instIsCofibrantPOfIsVeryGood, HomotopicalAlgebra.PathObject.instWeakEquivalenceP₁, HomotopicalAlgebra.PathObject.IsGood.fibration_p, RightHomotopy.h₁, RightHomotopy.h₁_assoc, HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension, HomotopicalAlgebra.PathObject.instWeakEquivalenceP₀, ι_p₁, ι_p₀_assoc, HomotopicalAlgebra.PathObject.trans_p₁, RightHomotopy.trans_h, HomotopicalAlgebra.PathObject.trans_P, trans_ι
p 📖	CompOp	10 math math: p_fst_assoc, p_snd, symm_p, p_fst, HomotopicalAlgebra.PathObject.ofFactorizationData_p, HomotopicalAlgebra.PathObject.symm_p_assoc, HomotopicalAlgebra.PathObject.symm_p, symm_p_assoc, p_snd_assoc, HomotopicalAlgebra.PathObject.IsGood.fibration_p
p₀ 📖	CompOp	22 math math: p_fst_assoc, HomotopicalAlgebra.PathObject.symm_p₁, trans_p₀, trans_P, HomotopicalAlgebra.PathObject.instFibrationP₀, HomotopicalAlgebra.PathObject.symm_p₀, p_fst, trans_p₁, symm_p₁, HomotopicalAlgebra.PathObject.trans_p₀, HomotopicalAlgebra.PathObject.trans_ι, RightHomotopy.h₀, symm_p₀, RightHomotopy.h₀_assoc, HomotopicalAlgebra.PathObject.ofFactorizationData_p₀, ι_p₀, HomotopicalAlgebra.PathObject.instWeakEquivalenceP₀, ι_p₀_assoc, HomotopicalAlgebra.PathObject.trans_p₁, RightHomotopy.trans_h, HomotopicalAlgebra.PathObject.trans_P, trans_ι
p₁ 📖	CompOp	22 math math: HomotopicalAlgebra.PathObject.symm_p₁, p_snd, trans_p₀, trans_P, HomotopicalAlgebra.PathObject.symm_p₀, ι_p₁_assoc, trans_p₁, symm_p₁, HomotopicalAlgebra.PathObject.ofFactorizationData_p₁, HomotopicalAlgebra.PathObject.trans_p₀, HomotopicalAlgebra.PathObject.instFibrationP₁, HomotopicalAlgebra.PathObject.trans_ι, p_snd_assoc, symm_p₀, HomotopicalAlgebra.PathObject.instWeakEquivalenceP₁, RightHomotopy.h₁, RightHomotopy.h₁_assoc, ι_p₁, HomotopicalAlgebra.PathObject.trans_p₁, RightHomotopy.trans_h, HomotopicalAlgebra.PathObject.trans_P, trans_ι
trans 📖	CompOp	5 math math: trans_p₀, trans_P, trans_p₁, RightHomotopy.trans_h, trans_ι
ι 📖	CompOp	12 math math: HomotopicalAlgebra.PathObject.weakEquivalence_ι, ι_p₁_assoc, symm_ι, RightHomotopy.refl_h, HomotopicalAlgebra.PathObject.IsVeryGood.cofibration_ι, HomotopicalAlgebra.PathObject.symm_ι, HomotopicalAlgebra.PathObject.trans_ι, ι_p₀, HomotopicalAlgebra.PathObject.ofFactorizationData_ι, ι_p₁, ι_p₀_assoc, trans_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
p_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P CategoryTheory.Limits.prod p CategoryTheory.Limits.prod.fst p₀	—	CategoryTheory.Limits.limit.lift_π
p_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P CategoryTheory.Limits.prod p CategoryTheory.Limits.prod.fst p₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_fst
p_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P CategoryTheory.Limits.prod p CategoryTheory.Limits.prod.snd p₁	—	CategoryTheory.Limits.limit.lift_π
p_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P CategoryTheory.Limits.prod p CategoryTheory.Limits.prod.snd p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_snd
symm_P 📖	mathematical	—	P symm	—	—
symm_p 📖	mathematical	—	p symm CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P CategoryTheory.Limits.prod CategoryTheory.Iso.hom CategoryTheory.Limits.prod.braiding	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.prod.comp_lift p_snd p_fst
symm_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P symm CategoryTheory.Limits.prod CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair p CategoryTheory.Iso.hom CategoryTheory.Limits.prod.braiding	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' symm_p
symm_p₀ 📖	mathematical	—	p₀ symm p₁	—	—
symm_p₁ 📖	mathematical	—	p₁ symm p₀	—	—
symm_ι 📖	mathematical	—	ι symm	—	—
trans_P 📖	mathematical	—	P trans CategoryTheory.Limits.pullback p₁ p₀	—	—
trans_p₀ 📖	mathematical	—	p₀ trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback P p₁ CategoryTheory.Limits.pullback.fst	—	—
trans_p₁ 📖	mathematical	—	p₁ trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback P p₀ CategoryTheory.Limits.pullback.snd	—	—
trans_ι 📖	mathematical	—	ι trans CategoryTheory.Limits.pullback.lift P p₁ p₀	—	—
ι_p₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P ι p₀ CategoryTheory.CategoryStruct.id	—	—
ι_p₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P ι p₀	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι_p₀
ι_p₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P ι p₁ CategoryTheory.CategoryStruct.id	—	—
ι_p₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct P ι p₁	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι_p₁

---

← Back to Index