Cylinder

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

Statistics

Metric	Count
Definitions Cylinder, IsGood, IsVeryGood, ofFactorizationData, toPrecylinder, trans, Precylinder, I, i, i₀, i₁, trans, π	13
Theorems cofibration_i, fibration_π, toIsGood, exists_very_good, instCofibrationI₀, instCofibrationI₁, instIsCofibrantI, instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations, instIsFibrantIOfIsVeryGood, instIsGoodSymmOfRespectsIsoCofibrations, instIsGoodTrans, instIsVeryGoodOfFactorizationData, instIsVeryGoodSymmOfRespectsIsoCofibrations, instNonempty, instWeakEquivalenceI₀, instWeakEquivalenceI₁, ofFactorizationData_I, ofFactorizationData_i, ofFactorizationData_i₀, ofFactorizationData_i₁, ofFactorizationData_π, symm_I, symm_i, symm_i_assoc, symm_i₀, symm_i₁, symm_π, trans_I, trans_i₀, trans_i₁, trans_π, weakEquivalence_π, inl_i, inl_i_assoc, inr_i, inr_i_assoc, i₀_π, i₀_π_assoc, i₁_π, i₁_π_assoc, symm_I, symm_i, symm_i_assoc, symm_i₀, symm_i₁, symm_π, trans_I, trans_i₀, trans_i₁, trans_π	50
Total	63

HomotopicalAlgebra

Definitions

Name	Category	Theorems
Cylinder 📖	CompData	1 math math: Cylinder.instNonempty
Precylinder 📖	CompData	—

HomotopicalAlgebra.Cylinder

Definitions

Name	Category	Theorems
IsGood 📖	CompData	5 math math: HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder, IsVeryGood.toIsGood, LeftHomotopy.exists_good_cylinder, instIsGoodSymmOfRespectsIsoCofibrations, instIsGoodTrans
IsVeryGood 📖	CompData	4 math math: HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder, exists_very_good, instIsVeryGoodOfFactorizationData, instIsVeryGoodSymmOfRespectsIsoCofibrations
ofFactorizationData 📖	CompOp	7 math math: ofFactorizationData_i₀, ofFactorizationData_i₁, ofFactorizationData_I, ofFactorizationData_i, instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations, ofFactorizationData_π, instIsVeryGoodOfFactorizationData
toPrecylinder 📖	CompOp	26 math math: instCofibrationI₁, ofFactorizationData_i₀, instIsCofibrantI, ofFactorizationData_i₁, LeftHomotopy.covering_homotopy, symm_i₁, ofFactorizationData_I, IsVeryGood.fibration_π, trans_π, ofFactorizationData_i, instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations, instIsFibrantIOfIsVeryGood, symm_i, trans_i₀, IsGood.cofibration_i, symm_π, ofFactorizationData_π, trans_I, instCofibrationI₀, trans_i₁, symm_i₀, instWeakEquivalenceI₀, symm_i_assoc, symm_I, instWeakEquivalenceI₁, weakEquivalence_π
trans 📖	CompOp	5 math math: trans_π, trans_i₀, trans_I, trans_i₁, instIsGoodTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_very_good 📖	mathematical	—	IsVeryGood HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5b instIsVeryGoodOfFactorizationData
instCofibrationI₀ 📖	mathematical	—	HomotopicalAlgebra.Cofibration HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.Precylinder.i₀	—	HomotopicalAlgebra.Precylinder.inl_i HomotopicalAlgebra.instCofibrationCompOfIsStableUnderCompositionCofibrations HomotopicalAlgebra.instCofibrationInlOfIsCofibrant IsGood.cofibration_i
instCofibrationI₁ 📖	mathematical	—	HomotopicalAlgebra.Cofibration HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.Precylinder.i₁	—	HomotopicalAlgebra.Precylinder.inr_i HomotopicalAlgebra.instCofibrationCompOfIsStableUnderCompositionCofibrations HomotopicalAlgebra.instCofibrationInrOfIsCofibrant IsGood.cofibration_i
instIsCofibrantI 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant HomotopicalAlgebra.Precylinder.I toPrecylinder	—	HomotopicalAlgebra.isCofibrant_of_cofibration instCofibrationI₀
instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations 📖	mathematical	—	HomotopicalAlgebra.IsFibrant HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.isFibrant_of_fibration IsVeryGood.fibration_π instIsVeryGoodOfFactorizationData
instIsFibrantIOfIsVeryGood 📖	mathematical	—	HomotopicalAlgebra.IsFibrant HomotopicalAlgebra.Precylinder.I toPrecylinder	—	HomotopicalAlgebra.isFibrant_of_fibration IsVeryGood.fibration_π
instIsGoodSymmOfRespectsIsoCofibrations 📖	mathematical	—	IsGood symm CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape HomotopicalAlgebra.cofibration_iff IsGood.cofibration_i symm_i CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.Limits.coprod.desc_comp HomotopicalAlgebra.Precylinder.inr_i HomotopicalAlgebra.Precylinder.inl_i CategoryTheory.Category.comp_id
instIsGoodTrans 📖	mathematical	—	IsGood HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair HomotopicalAlgebra.ModelCategory.categoryWithCofibrations	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.coprod.map_desc CategoryTheory.Category.id_comp CategoryTheory.Limits.coprod.hom_ext CategoryTheory.Limits.pushout.condition CategoryTheory.Limits.colimit.ι_desc HomotopicalAlgebra.Precylinder.inl_i_assoc HomotopicalAlgebra.Precylinder.inr_i_assoc HomotopicalAlgebra.Precylinder.inl_i CategoryTheory.IsPushout.of_hasPushout CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits HomotopicalAlgebra.cofibration_iff CategoryTheory.MorphismProperty.of_isPushout HomotopicalAlgebra.instIsStableUnderCobaseChangeCofibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations CategoryTheory.IsPushout.of_top CategoryTheory.IsPushout.flip CategoryTheory.IsPushout.of_coprod_inl_with_id IsGood.cofibration_i HomotopicalAlgebra.instCofibrationCompOfIsStableUnderCompositionCofibrations CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeCofibrations HomotopicalAlgebra.instCofibrationMapOfIsWeakFactorizationSystemCofibrationsTrivialFibrations_1 instCofibrationI₀ HomotopicalAlgebra.instCofibrationOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsIso HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations CategoryTheory.IsIso.id
instIsVeryGoodOfFactorizationData 📖	mathematical	—	IsVeryGood HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype ofFactorizationData_i HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations
instIsVeryGoodSymmOfRespectsIsoCofibrations 📖	mathematical	—	IsVeryGood symm CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instIsGoodSymmOfRespectsIsoCofibrations IsVeryGood.toIsGood IsVeryGood.fibration_π
instNonempty 📖	mathematical	—	HomotopicalAlgebra.Cylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype exists_very_good
instWeakEquivalenceI₀ 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.Precylinder.i₀	—	HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac HomotopicalAlgebra.Precylinder.i₀_π weakEquivalence_π HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences
instWeakEquivalenceI₁ 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.Precylinder.i₁	—	HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac HomotopicalAlgebra.Precylinder.i₁_π weakEquivalence_π HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences
ofFactorizationData_I 📖	mathematical	—	HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.coprod CategoryTheory.Limits.codiag	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
ofFactorizationData_i 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.MorphismProperty.MapFactorizationData.i HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.coprod CategoryTheory.Limits.codiag	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.coprod.hom_ext HomotopicalAlgebra.Precylinder.inl_i HomotopicalAlgebra.Precylinder.inr_i
ofFactorizationData_i₀ 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i₀ toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.codiag CategoryTheory.Limits.coprod.inl CategoryTheory.MorphismProperty.MapFactorizationData.i	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
ofFactorizationData_i₁ 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i₁ toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.codiag CategoryTheory.Limits.coprod.inr CategoryTheory.MorphismProperty.MapFactorizationData.i	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
ofFactorizationData_π 📖	mathematical	—	HomotopicalAlgebra.Precylinder.π toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ofFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.p HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.coprod CategoryTheory.Limits.codiag	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
symm_I 📖	mathematical	—	HomotopicalAlgebra.Precylinder.I toPrecylinder symm	—	—
symm_i 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i toPrecylinder symm CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod HomotopicalAlgebra.Precylinder.I CategoryTheory.Iso.hom CategoryTheory.Limits.coprod.braiding	—	HomotopicalAlgebra.Precylinder.symm_i
symm_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair HomotopicalAlgebra.Precylinder.I toPrecylinder symm HomotopicalAlgebra.Precylinder.i CategoryTheory.Iso.hom CategoryTheory.Limits.coprod.braiding	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' symm_i
symm_i₀ 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i₀ toPrecylinder symm HomotopicalAlgebra.Precylinder.i₁	—	—
symm_i₁ 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i₁ toPrecylinder symm HomotopicalAlgebra.Precylinder.i₀	—	—
symm_π 📖	mathematical	—	HomotopicalAlgebra.Precylinder.π toPrecylinder symm	—	—
trans_I 📖	mathematical	—	HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.Limits.pushout HomotopicalAlgebra.Precylinder.i₁ HomotopicalAlgebra.Precylinder.i₀	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
trans_i₀ 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i₀ toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.Precylinder.I CategoryTheory.Limits.pushout HomotopicalAlgebra.Precylinder.i₁ CategoryTheory.Limits.pushout.inl	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
trans_i₁ 📖	mathematical	—	HomotopicalAlgebra.Precylinder.i₁ toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.Precylinder.I CategoryTheory.Limits.pushout HomotopicalAlgebra.Precylinder.i₀ CategoryTheory.Limits.pushout.inr	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
trans_π 📖	mathematical	—	HomotopicalAlgebra.Precylinder.π toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences trans CategoryTheory.Limits.pushout.desc HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Precylinder.i₁ HomotopicalAlgebra.Precylinder.i₀	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
weakEquivalence_π 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.Precylinder.I toPrecylinder HomotopicalAlgebra.Precylinder.π	—	—

HomotopicalAlgebra.Cylinder.IsGood

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofibration_i 📖	mathematical	—	HomotopicalAlgebra.Cofibration CategoryTheory.Limits.coprod HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Cylinder.toPrecylinder HomotopicalAlgebra.Precylinder.i	—	—

HomotopicalAlgebra.Cylinder.IsVeryGood

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fibration_π 📖	mathematical	—	HomotopicalAlgebra.Fibration HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Cylinder.toPrecylinder HomotopicalAlgebra.Precylinder.π	—	—
toIsGood 📖	mathematical	—	HomotopicalAlgebra.Cylinder.IsGood	—	—

HomotopicalAlgebra.Precylinder

Definitions

Name	Category	Theorems
I 📖	CompOp	41 math math: HomotopicalAlgebra.Cylinder.instCofibrationI₁, trans_π, i₁_π_assoc, inr_i, inr_i_assoc, LeftHomotopy.h₀_assoc, HomotopicalAlgebra.Cylinder.instIsCofibrantI, HomotopicalAlgebra.Cylinder.LeftHomotopy.covering_homotopy, HomotopicalAlgebra.Cylinder.ofFactorizationData_I, symm_i_assoc, HomotopicalAlgebra.Cylinder.IsVeryGood.fibration_π, i₀_π, HomotopicalAlgebra.Cylinder.trans_π, LeftHomotopy.refl_h, HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations, HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood, LeftHomotopy.trans_h, trans_I, symm_I, LeftHomotopy.h₁_assoc, LeftHomotopy.h₀, HomotopicalAlgebra.Cylinder.symm_i, HomotopicalAlgebra.Cylinder.trans_i₀, inl_i_assoc, HomotopicalAlgebra.Cylinder.IsGood.cofibration_i, LeftHomotopy.h₁, HomotopicalAlgebra.Cylinder.trans_I, HomotopicalAlgebra.Cylinder.instCofibrationI₀, HomotopicalAlgebra.Cylinder.trans_i₁, HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₀, i₀_π_assoc, symm_i, LeftHomotopy.postcomp_h, i₁_π, HomotopicalAlgebra.Cylinder.symm_i_assoc, trans_i₁, HomotopicalAlgebra.Cylinder.symm_I, trans_i₀, inl_i, HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₁, HomotopicalAlgebra.Cylinder.weakEquivalence_π
i 📖	CompOp	10 math math: inr_i, inr_i_assoc, symm_i_assoc, HomotopicalAlgebra.Cylinder.ofFactorizationData_i, HomotopicalAlgebra.Cylinder.symm_i, inl_i_assoc, HomotopicalAlgebra.Cylinder.IsGood.cofibration_i, symm_i, HomotopicalAlgebra.Cylinder.symm_i_assoc, inl_i
i₀ 📖	CompOp	22 math math: trans_π, LeftHomotopy.h₀_assoc, symm_i₀, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀, HomotopicalAlgebra.Cylinder.symm_i₁, i₀_π, HomotopicalAlgebra.Cylinder.trans_π, symm_i₁, LeftHomotopy.trans_h, trans_I, LeftHomotopy.h₀, HomotopicalAlgebra.Cylinder.trans_i₀, inl_i_assoc, HomotopicalAlgebra.Cylinder.trans_I, HomotopicalAlgebra.Cylinder.instCofibrationI₀, HomotopicalAlgebra.Cylinder.trans_i₁, HomotopicalAlgebra.Cylinder.symm_i₀, HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₀, i₀_π_assoc, trans_i₁, trans_i₀, inl_i
i₁ 📖	CompOp	22 math math: HomotopicalAlgebra.Cylinder.instCofibrationI₁, trans_π, i₁_π_assoc, inr_i, inr_i_assoc, symm_i₀, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁, HomotopicalAlgebra.Cylinder.symm_i₁, HomotopicalAlgebra.Cylinder.trans_π, symm_i₁, LeftHomotopy.trans_h, trans_I, LeftHomotopy.h₁_assoc, HomotopicalAlgebra.Cylinder.trans_i₀, LeftHomotopy.h₁, HomotopicalAlgebra.Cylinder.trans_I, HomotopicalAlgebra.Cylinder.trans_i₁, HomotopicalAlgebra.Cylinder.symm_i₀, i₁_π, trans_i₁, trans_i₀, HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₁
trans 📖	CompOp	5 math math: trans_π, LeftHomotopy.trans_h, trans_I, trans_i₁, trans_i₀
π 📖	CompOp	12 math math: trans_π, i₁_π_assoc, HomotopicalAlgebra.Cylinder.IsVeryGood.fibration_π, i₀_π, HomotopicalAlgebra.Cylinder.trans_π, LeftHomotopy.refl_h, symm_π, HomotopicalAlgebra.Cylinder.symm_π, HomotopicalAlgebra.Cylinder.ofFactorizationData_π, i₀_π_assoc, i₁_π, HomotopicalAlgebra.Cylinder.weakEquivalence_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod I CategoryTheory.Limits.coprod.inl i i₀	—	CategoryTheory.Limits.colimit.ι_desc
inl_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.inl I i i₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_i
inr_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod I CategoryTheory.Limits.coprod.inr i i₁	—	CategoryTheory.Limits.colimit.ι_desc
inr_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.inr I i i₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_i
i₀_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I i₀ π CategoryTheory.CategoryStruct.id	—	—
i₀_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I i₀ π	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' i₀_π
i₁_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I i₁ π CategoryTheory.CategoryStruct.id	—	—
i₁_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I i₁ π	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' i₁_π
symm_I 📖	mathematical	—	I symm	—	—
symm_i 📖	mathematical	—	i symm CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod I CategoryTheory.Iso.hom CategoryTheory.Limits.coprod.braiding	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.coprod.desc_comp inr_i inl_i
symm_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair I symm i CategoryTheory.Iso.hom CategoryTheory.Limits.coprod.braiding	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' symm_i
symm_i₀ 📖	mathematical	—	i₀ symm i₁	—	—
symm_i₁ 📖	mathematical	—	i₁ symm i₀	—	—
symm_π 📖	mathematical	—	π symm	—	—
trans_I 📖	mathematical	—	I trans CategoryTheory.Limits.pushout i₁ i₀	—	—
trans_i₀ 📖	mathematical	—	i₀ trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.Limits.pushout i₁ CategoryTheory.Limits.pushout.inl	—	—
trans_i₁ 📖	mathematical	—	i₁ trans CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct I CategoryTheory.Limits.pushout i₀ CategoryTheory.Limits.pushout.inr	—	—
trans_π 📖	mathematical	—	π trans CategoryTheory.Limits.pushout.desc I i₁ i₀	—	—

---

← Back to Index