Homotopy

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

Statistics

Metric	Count
Definitions rightHomotopy, leftHomotopy, leftHomotopyClassEquivRightHomotopyClass	3
Theorems postcomp_bijective_of_fibration_of_weakEquivalence, postcomp_bijective_of_weakEquivalence, whitehead, rightHomotopyRel, precomp_bijective_of_cofibration_of_weakEquivalence, precomp_bijective_of_weakEquivalence, whitehead, leftHomotopyRel, leftHomotopyClassEquivRightHomotopyClass_mk, leftHomotopyClassEquivRightHomotopyClass_symm_mk, leftHomotopyRel_iff_rightHomotopyRel	11
Total	14

HomotopicalAlgebra

Definitions

Name	Category	Theorems
leftHomotopyClassEquivRightHomotopyClass 📖	CompOp	2 math math: leftHomotopyClassEquivRightHomotopyClass_symm_mk, leftHomotopyClassEquivRightHomotopyClass_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftHomotopyClassEquivRightHomotopyClass_mk 📖	mathematical	—	DFunLike.coe Equiv LeftHomotopyClass ModelCategory.categoryWithWeakEquivalences RightHomotopyClass EquivLike.toFunLike Equiv.instEquivLike leftHomotopyClassEquivRightHomotopyClass	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits ModelCategory.cm1a
leftHomotopyClassEquivRightHomotopyClass_symm_mk 📖	mathematical	—	DFunLike.coe Equiv RightHomotopyClass ModelCategory.categoryWithWeakEquivalences LeftHomotopyClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm leftHomotopyClassEquivRightHomotopyClass	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits ModelCategory.cm1a
leftHomotopyRel_iff_rightHomotopyRel 📖	mathematical	—	LeftHomotopyRel ModelCategory.categoryWithWeakEquivalences RightHomotopyRel	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits ModelCategory.cm1a LeftHomotopyRel.rightHomotopyRel RightHomotopyRel.leftHomotopyRel

HomotopicalAlgebra.LeftHomotopyClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
postcomp_bijective_of_fibration_of_weakEquivalence 📖	mathematical	—	Function.Bijective HomotopicalAlgebra.LeftHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences postcomp	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype mk_surjective CategoryTheory.Limits.hasColimitOfHasColimitsOfShape HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder CategoryTheory.Limits.coprod.desc_comp CategoryTheory.Limits.coprod.hom_ext CategoryTheory.Limits.colimit.ι_desc HomotopicalAlgebra.Precylinder.inl_i_assoc HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ HomotopicalAlgebra.Precylinder.inr_i_assoc HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁ mk_eq_mk_iff CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4b HomotopicalAlgebra.Cylinder.IsGood.cofibration_i CategoryTheory.whisker_eq CategoryTheory.CommSq.fac_left CategoryTheory.Limits.coprod.inl_desc CategoryTheory.Limits.coprod.inr_desc CategoryTheory.Limits.initial.to_comp CategoryTheory.CommSq.fac_right
postcomp_bijective_of_weakEquivalence 📖	mathematical	—	Function.Bijective HomotopicalAlgebra.LeftHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences postcomp	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.FibrantBrownFactorization.instNonemptyOfIsFibrant Function.Bijective.of_comp_iff' postcomp_bijective_of_fibration_of_weakEquivalence HomotopicalAlgebra.FibrantBrownFactorization.fibration_r HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR mk_surjective CategoryTheory.Category.assoc HomotopicalAlgebra.FibrantBrownFactorization.i_r CategoryTheory.Category.comp_id Function.bijective_id CategoryTheory.MorphismProperty.MapFactorizationData.fac Function.Bijective.comp HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations
whitehead 📖	mathematical	—	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.RightHomotopyClass.whitehead

HomotopicalAlgebra.LeftHomotopyRel

Definitions

Name	Category	Theorems
rightHomotopy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rightHomotopyRel 📖	mathematical	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	HomotopicalAlgebra.RightHomotopyRel	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.PathObject.exists_very_good HomotopicalAlgebra.PathObject.IsVeryGood.toIsGood

HomotopicalAlgebra.RightHomotopyClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
precomp_bijective_of_cofibration_of_weakEquivalence 📖	mathematical	—	Function.Bijective HomotopicalAlgebra.RightHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences precomp	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype mk_surjective CategoryTheory.Limits.hasLimitOfHasLimitsOfShape HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject CategoryTheory.Limits.prod.comp_lift CategoryTheory.Limits.prod.hom_ext CategoryTheory.Category.assoc HomotopicalAlgebra.PrepathObject.p_fst HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ CategoryTheory.Limits.limit.lift_π HomotopicalAlgebra.PrepathObject.p_snd HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁ mk_eq_mk_iff CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4a HomotopicalAlgebra.PathObject.IsGood.fibration_p CategoryTheory.eq_whisker CategoryTheory.CommSq.fac_right CategoryTheory.Limits.prod.lift_fst CategoryTheory.Limits.prod.lift_snd CategoryTheory.Limits.terminal.comp_from CategoryTheory.CommSq.fac_left
precomp_bijective_of_weakEquivalence 📖	mathematical	—	Function.Bijective HomotopicalAlgebra.RightHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences precomp	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b HomotopicalAlgebra.CofibrantBrownFactorization.instNonemptyOfIsCofibrant Function.Bijective.of_comp_iff' precomp_bijective_of_cofibration_of_weakEquivalence HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS mk_surjective HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc Function.bijective_id CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc Function.Bijective.comp HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations
whitehead 📖	mathematical	—	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a precomp_bijective_of_weakEquivalence mk_surjective mk_eq_mk_iff CategoryTheory.Category.comp_id HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel CategoryTheory.Category.assoc CategoryTheory.Category.id_comp HomotopicalAlgebra.LeftHomotopyRel.postcomp

HomotopicalAlgebra.RightHomotopyRel

Definitions

Name	Category	Theorems
leftHomotopy 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftHomotopyRel 📖	mathematical	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	HomotopicalAlgebra.LeftHomotopyRel	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b HomotopicalAlgebra.Cylinder.exists_very_good HomotopicalAlgebra.Cylinder.IsVeryGood.toIsGood

---

← Back to Index