LeftHomotopy

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

Statistics

Metric	Count
Definitions LeftHomotopy, postcomp, refl, trans, LeftHomotopyClass, mk, postcomp, LeftHomotopyRel, LeftHomotopy, h, postcomp, refl, trans	13
Theorems covering_homotopy, exists_good_cylinder, leftHomotopyRel, weakEquivalence_iff, mk_eq_mk_iff, mk_surjective, postcomp_mk, sound, equivalence, exists_good_cylinder, exists_very_good_cylinder, factorsThroughLocalization, postcomp, precomp, refl, trans, h₀, h₀_assoc, h₁, h₁_assoc, postcomp_h, refl_h, symm_h, trans_h	24
Total	37

HomotopicalAlgebra

Definitions

Name	Category	Theorems
LeftHomotopyClass 📖	CompOp	6 math math: BifibrantObject.HoCat.homEquivLeft_apply, leftHomotopyClassEquivRightHomotopyClass_symm_mk, LeftHomotopyClass.postcomp_bijective_of_weakEquivalence, LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence, LeftHomotopyClass.mk_surjective, leftHomotopyClassEquivRightHomotopyClass_mk
LeftHomotopyRel 📖	CompOp	10 math math: LeftHomotopyClass.mk_eq_mk_iff, LeftHomotopyClass.whitehead, Cylinder.LeftHomotopy.leftHomotopyRel, FibrantObject.homRel_iff_leftHomotopyRel, LeftHomotopyRel.factorsThroughLocalization, BifibrantObject.homRel_iff_leftHomotopyRel, leftHomotopyRel_iff_rightHomotopyRel, RightHomotopyRel.leftHomotopyRel, LeftHomotopyRel.equivalence, LeftHomotopyRel.refl

HomotopicalAlgebra.Cylinder

Definitions

Name	Category	Theorems
LeftHomotopy 📖	CompOp	3 math math: HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder, LeftHomotopy.exists_good_cylinder, HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder

HomotopicalAlgebra.Cylinder.LeftHomotopy

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
covering_homotopy 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp	HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Cylinder.toPrecylinder HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.Precylinder.LeftHomotopy.h	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4a HomotopicalAlgebra.Cylinder.instCofibrationI₀ CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeCofibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations HomotopicalAlgebra.instIsStableUnderCobaseChangeCofibrations HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₀ HomotopicalAlgebra.ModelCategory.cm2 CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.ModelCategory.cm3a CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition CategoryTheory.CommSq.fac_left CategoryTheory.CommSq.fac_right
exists_good_cylinder 📖	mathematical	—	HomotopicalAlgebra.Cylinder.IsGood 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.Cylinder.LeftHomotopy	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5b CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.MapFactorizationData.fac_assoc HomotopicalAlgebra.Precylinder.inl_i_assoc HomotopicalAlgebra.Precylinder.i₀_π HomotopicalAlgebra.Precylinder.inr_i_assoc HomotopicalAlgebra.Precylinder.i₁_π HomotopicalAlgebra.instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition HomotopicalAlgebra.ModelCategory.cm2 HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations HomotopicalAlgebra.Cylinder.weakEquivalence_π HomotopicalAlgebra.cofibration_iff CategoryTheory.Limits.coprod.hom_ext HomotopicalAlgebra.Precylinder.inl_i HomotopicalAlgebra.Precylinder.inr_i CategoryTheory.MorphismProperty.MapFactorizationData.hi HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁
leftHomotopyRel 📖	mathematical	—	HomotopicalAlgebra.LeftHomotopyRel	—	—
weakEquivalence_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence	—	HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₀ HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁ HomotopicalAlgebra.instWeakEquivalenceCompOfIsStableUnderCompositionWeakEquivalences CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition HomotopicalAlgebra.Cylinder.instWeakEquivalenceI₁

HomotopicalAlgebra.LeftHomotopyClass

Definitions

Name	Category	Theorems
mk 📖	CompOp	—
postcomp 📖	CompOp	3 math math: postcomp_mk, postcomp_bijective_of_weakEquivalence, postcomp_bijective_of_fibration_of_weakEquivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_eq_mk_iff 📖	mathematical	—	HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.LeftHomotopyRel	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Equivalence.eqvGen_iff HomotopicalAlgebra.LeftHomotopyRel.equivalence Quot.eq
mk_surjective 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.LeftHomotopyClass	—	Quot.mk_surjective
postcomp_mk 📖	mathematical	—	postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
sound 📖	—	HomotopicalAlgebra.LeftHomotopyRel	—	—	—

HomotopicalAlgebra.LeftHomotopyRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalence 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype refl symm trans
exists_good_cylinder 📖	mathematical	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	HomotopicalAlgebra.Cylinder.IsGood 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.Cylinder.LeftHomotopy	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder
exists_very_good_cylinder 📖	mathematical	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	HomotopicalAlgebra.Cylinder.IsVeryGood 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 HomotopicalAlgebra.Cylinder.LeftHomotopy	—	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 exists_good_cylinder HomotopicalAlgebra.ModelCategory.cm5a CategoryTheory.Category.assoc CategoryTheory.MorphismProperty.MapFactorizationData.fac HomotopicalAlgebra.Precylinder.i₀_π HomotopicalAlgebra.Precylinder.i₁_π HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac HomotopicalAlgebra.ModelCategory.cm2 HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations HomotopicalAlgebra.Cylinder.weakEquivalence_π CategoryTheory.Limits.coprod.hom_ext HomotopicalAlgebra.Precylinder.inl_i HomotopicalAlgebra.Precylinder.inl_i_assoc HomotopicalAlgebra.Precylinder.inr_i HomotopicalAlgebra.Precylinder.inr_i_assoc HomotopicalAlgebra.instCofibrationCompOfIsStableUnderCompositionCofibrations CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeCofibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations HomotopicalAlgebra.Cylinder.IsGood.cofibration_i HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations CategoryTheory.Limits.terminal.comp_from HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4a CategoryTheory.CommSq.fac_left HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁
factorsThroughLocalization 📖	mathematical	—	HomRel.FactorsThroughLocalization HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.weakEquivalences	—	CategoryTheory.areEqualizedByLocalization_iff CategoryTheory.Functor.q_isLocalization CategoryTheory.Localization.inverts HomotopicalAlgebra.weakEquivalence_iff HomotopicalAlgebra.Cylinder.weakEquivalence_π CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Functor.map_comp HomotopicalAlgebra.Precylinder.i₀_π CategoryTheory.Functor.map_id HomotopicalAlgebra.Precylinder.i₁_π HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁
postcomp 📖	mathematical	HomotopicalAlgebra.LeftHomotopyRel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel
precomp 📖	mathematical	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	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 exists_very_good_cylinder HomotopicalAlgebra.Cylinder.exists_very_good CategoryTheory.Limits.coprod.desc_comp CategoryTheory.Category.assoc HomotopicalAlgebra.Precylinder.i₀_π CategoryTheory.Category.comp_id HomotopicalAlgebra.Precylinder.i₁_π CategoryTheory.Limits.coprod.hom_ext CategoryTheory.Limits.colimit.ι_desc HomotopicalAlgebra.Precylinder.inl_i_assoc HomotopicalAlgebra.Precylinder.i₀_π_assoc HomotopicalAlgebra.Precylinder.inr_i_assoc HomotopicalAlgebra.Precylinder.i₁_π_assoc CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4b HomotopicalAlgebra.Cylinder.IsGood.cofibration_i HomotopicalAlgebra.Cylinder.IsVeryGood.toIsGood HomotopicalAlgebra.Cylinder.IsVeryGood.fibration_π HomotopicalAlgebra.Cylinder.weakEquivalence_π CategoryTheory.whisker_eq CategoryTheory.CommSq.fac_left Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.coprod.inl_desc HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ CategoryTheory.Limits.coprod.inr_desc HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁
refl 📖	mathematical	—	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	HomotopicalAlgebra.Cylinder.instNonempty
trans 📖	—	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape exists_good_cylinder HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits

HomotopicalAlgebra.Precylinder

Definitions

Name	Category	Theorems
LeftHomotopy 📖	CompData	—

HomotopicalAlgebra.Precylinder.LeftHomotopy

Definitions

Name	Category	Theorems
h 📖	CompOp	9 math math: h₀_assoc, HomotopicalAlgebra.Cylinder.LeftHomotopy.covering_homotopy, refl_h, trans_h, symm_h, h₁_assoc, h₀, h₁, postcomp_h
postcomp 📖	CompOp	1 math math: postcomp_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.Precylinder.I HomotopicalAlgebra.Precylinder.i₀ h	—	—
h₀_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Precylinder.i₀ h	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₀
h₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Precylinder.i₁ h	—	—
h₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Precylinder.i₁ h	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' h₁
postcomp_h 📖	mathematical	—	h CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct postcomp HomotopicalAlgebra.Precylinder.I	—	—
refl_h 📖	mathematical	—	h refl CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Precylinder.π	—	—
symm_h 📖	mathematical	—	h HomotopicalAlgebra.Precylinder.symm symm	—	—
trans_h 📖	mathematical	—	h HomotopicalAlgebra.Precylinder.trans trans CategoryTheory.Limits.pushout.desc HomotopicalAlgebra.Precylinder.I HomotopicalAlgebra.Precylinder.i₁ HomotopicalAlgebra.Precylinder.i₀	—	—

---

← Back to Index