RightHomotopy

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

Statistics

Metric	Count
Definitions RightHomotopy, precomp, refl, trans, RightHomotopy, h, precomp, refl, trans, RightHomotopyClass, mk, precomp, RightHomotopyRel	13
Theorems exists_good_pathObject, homotopy_extension, rightHomotopyRel, weakEquivalence_iff, h₀, h₀_assoc, h₁, h₁_assoc, precomp_h, refl_h, symm_h, trans_h, mk_eq_mk_iff, mk_surjective, precomp_mk, sound, equivalence, exists_good_pathObject, exists_very_good_pathObject, factorsThroughLocalization, postcomp, precomp, refl, trans	24
Total	37

HomotopicalAlgebra

Definitions

Name	Category	Theorems
RightHomotopyClass 📖	CompOp	8 math math: BifibrantObject.HoCat.homEquivRight_apply, BifibrantObject.HoCat.homEquivLeft_symm_apply, leftHomotopyClassEquivRightHomotopyClass_symm_mk, RightHomotopyClass.mk_surjective, BifibrantObject.HoCat.homEquivRight_symm_apply, RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence, RightHomotopyClass.precomp_bijective_of_weakEquivalence, leftHomotopyClassEquivRightHomotopyClass_mk
RightHomotopyRel 📖	CompOp	10 math math: PathObject.RightHomotopy.rightHomotopyRel, RightHomotopyRel.factorsThroughLocalization, RightHomotopyRel.equivalence, RightHomotopyClass.whitehead, leftHomotopyRel_iff_rightHomotopyRel, RightHomotopyClass.mk_eq_mk_iff, BifibrantObject.homRel_iff_rightHomotopyRel, LeftHomotopyRel.rightHomotopyRel, RightHomotopyRel.refl, CofibrantObject.homRel_iff_rightHomotopyRel

HomotopicalAlgebra.PathObject

Definitions

Name	Category	Theorems
RightHomotopy 📖	CompOp	3 math math: HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject, HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject, RightHomotopy.exists_good_pathObject

HomotopicalAlgebra.PathObject.RightHomotopy

Definitions

Name	Category	Theorems
precomp 📖	CompOp	—
refl 📖	CompOp	—
trans 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_good_pathObject 📖	mathematical	—	HomotopicalAlgebra.PathObject.IsGood 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.PathObject.RightHomotopy	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5a CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc HomotopicalAlgebra.PrepathObject.p_fst HomotopicalAlgebra.PrepathObject.ι_p₀ HomotopicalAlgebra.PrepathObject.p_snd HomotopicalAlgebra.PrepathObject.ι_p₁ HomotopicalAlgebra.instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition HomotopicalAlgebra.ModelCategory.cm2 HomotopicalAlgebra.PathObject.weakEquivalence_ι HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations HomotopicalAlgebra.fibration_iff CategoryTheory.Limits.prod.hom_ext CategoryTheory.MorphismProperty.MapFactorizationData.hp HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
homotopy_extension 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PathObject.toPrepathObject HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.PrepathObject.RightHomotopy.h	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4b HomotopicalAlgebra.PathObject.instFibrationP₀ CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeFibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.instIsStableUnderBaseChangeFibrations HomotopicalAlgebra.PathObject.instWeakEquivalenceP₀ HomotopicalAlgebra.ModelCategory.cm2 CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition HomotopicalAlgebra.ModelCategory.cm3a CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition CategoryTheory.CommSq.fac_right CategoryTheory.CommSq.fac_left
rightHomotopyRel 📖	mathematical	—	HomotopicalAlgebra.RightHomotopyRel	—	—
weakEquivalence_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence	—	HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ HomotopicalAlgebra.PathObject.instWeakEquivalenceP₀ HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁ HomotopicalAlgebra.instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition HomotopicalAlgebra.PathObject.instWeakEquivalenceP₁

HomotopicalAlgebra.PrepathObject

Definitions

Name	Category	Theorems
RightHomotopy 📖	CompData	—

HomotopicalAlgebra.PrepathObject.RightHomotopy

Definitions

Name	Category	Theorems
h 📖	CompOp	9 math math: refl_h, precomp_h, h₀, h₀_assoc, h₁, h₁_assoc, symm_h, HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension, trans_h
precomp 📖	CompOp	1 math math: precomp_h
refl 📖	CompOp	1 math math: refl_h
trans 📖	CompOp	1 math math: trans_h

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
h₀ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.PrepathObject.P h HomotopicalAlgebra.PrepathObject.p₀	—	—
h₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.PrepathObject.P h HomotopicalAlgebra.PrepathObject.p₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₀
h₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.PrepathObject.P h HomotopicalAlgebra.PrepathObject.p₁	—	—
h₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.PrepathObject.P h HomotopicalAlgebra.PrepathObject.p₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₁
precomp_h 📖	mathematical	—	h CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct precomp HomotopicalAlgebra.PrepathObject.P	—	—
refl_h 📖	mathematical	—	h refl CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PrepathObject.ι	—	—
symm_h 📖	mathematical	—	h HomotopicalAlgebra.PrepathObject.symm symm	—	—
trans_h 📖	mathematical	—	h HomotopicalAlgebra.PrepathObject.trans trans CategoryTheory.Limits.pullback.lift HomotopicalAlgebra.PrepathObject.P HomotopicalAlgebra.PrepathObject.p₁ HomotopicalAlgebra.PrepathObject.p₀	—	—

HomotopicalAlgebra.RightHomotopyClass

Definitions

Name	Category	Theorems
mk 📖	CompOp	—
precomp 📖	CompOp	3 math math: precomp_mk, precomp_bijective_of_cofibration_of_weakEquivalence, precomp_bijective_of_weakEquivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_eq_mk_iff 📖	mathematical	—	HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.RightHomotopyRel	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Equivalence.eqvGen_iff HomotopicalAlgebra.RightHomotopyRel.equivalence Quot.eq
mk_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.RightHomotopyClass	—	Quot.mk_surjective
precomp_mk 📖	mathematical	—	precomp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
sound 📖	—	HomotopicalAlgebra.RightHomotopyRel	—	—	—

HomotopicalAlgebra.RightHomotopyRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalence 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype refl symm trans
exists_good_pathObject 📖	mathematical	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	HomotopicalAlgebra.PathObject.IsGood 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.PathObject.RightHomotopy	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObject
exists_very_good_pathObject 📖	mathematical	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	HomotopicalAlgebra.PathObject.IsVeryGood 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 HomotopicalAlgebra.PathObject.RightHomotopy	—	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 exists_good_pathObject HomotopicalAlgebra.ModelCategory.cm5b CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc HomotopicalAlgebra.PrepathObject.ι_p₀ HomotopicalAlgebra.PrepathObject.ι_p₁ HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac HomotopicalAlgebra.ModelCategory.cm2 CategoryTheory.MorphismProperty.MapFactorizationData.fac HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations HomotopicalAlgebra.PathObject.weakEquivalence_ι CategoryTheory.Limits.prod.hom_ext HomotopicalAlgebra.PrepathObject.p_fst CategoryTheory.Category.assoc HomotopicalAlgebra.PrepathObject.p_snd HomotopicalAlgebra.instFibrationCompOfIsStableUnderCompositionFibrations CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeFibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations HomotopicalAlgebra.PathObject.IsGood.fibration_p CategoryTheory.Limits.initial.to_comp HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4b CategoryTheory.CommSq.fac_right_assoc HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
factorsThroughLocalization 📖	mathematical	—	HomRel.FactorsThroughLocalization HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.weakEquivalences	—	CategoryTheory.areEqualizedByLocalization_iff CategoryTheory.Functor.q_isLocalization CategoryTheory.Localization.inverts HomotopicalAlgebra.weakEquivalence_iff HomotopicalAlgebra.PathObject.weakEquivalence_ι CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Functor.map_comp HomotopicalAlgebra.PrepathObject.ι_p₀ CategoryTheory.Functor.map_id HomotopicalAlgebra.PrepathObject.ι_p₁ HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
postcomp 📖	mathematical	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	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 exists_very_good_pathObject HomotopicalAlgebra.PathObject.exists_very_good CategoryTheory.Category.assoc CategoryTheory.Limits.prod.comp_lift HomotopicalAlgebra.PrepathObject.ι_p₀_assoc HomotopicalAlgebra.PrepathObject.ι_p₁_assoc CategoryTheory.Limits.prod.hom_ext HomotopicalAlgebra.PrepathObject.p_fst HomotopicalAlgebra.PrepathObject.ι_p₀ CategoryTheory.Category.comp_id CategoryTheory.Limits.limit.lift_π HomotopicalAlgebra.PrepathObject.p_snd HomotopicalAlgebra.PrepathObject.ι_p₁ CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4a HomotopicalAlgebra.PathObject.IsVeryGood.cofibration_ι HomotopicalAlgebra.PathObject.weakEquivalence_ι HomotopicalAlgebra.PathObject.IsGood.fibration_p HomotopicalAlgebra.PathObject.IsVeryGood.toIsGood CategoryTheory.eq_whisker CategoryTheory.CommSq.fac_right CategoryTheory.Limits.prod.lift_fst HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀_assoc CategoryTheory.Limits.prod.lift_snd HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁_assoc
precomp 📖	mathematical	HomotopicalAlgebra.RightHomotopyRel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel
refl 📖	mathematical	—	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	HomotopicalAlgebra.PathObject.instNonempty
trans 📖	—	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape exists_good_pathObject HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits

---

← Back to Index