FundamentalLemma

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

Statistics

Metric	Count
Definitions leftHomotopyClassToHom, rightHomotopyClassToHom	2
Theorems iff_map_eq, iff_map_eq, bijective_leftHomotopyClassToHom, bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom, bijective_rightHomotopyClassToHom, leftHomotopyClassToHom_mk, map_surjective_of_isLocalization, rightHomotopyClassToHom_mk	8
Total	10

HomotopicalAlgebra

Definitions

Name	Category	Theorems
leftHomotopyClassToHom 📖	CompOp	3 math math: bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom, bijective_leftHomotopyClassToHom, leftHomotopyClassToHom_mk
rightHomotopyClassToHom 📖	CompOp	3 math math: bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom, bijective_rightHomotopyClassToHom, rightHomotopyClassToHom_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijective_leftHomotopyClassToHom 📖	mathematical	—	Function.Bijective LeftHomotopyClass ModelCategory.categoryWithWeakEquivalences Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj leftHomotopyClassToHom	—	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 bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom bijective_rightHomotopyClassToHom
bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom 📖	mathematical	—	Function.Bijective LeftHomotopyClass ModelCategory.categoryWithWeakEquivalences Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj leftHomotopyClassToHom RightHomotopyClass rightHomotopyClassToHom	—	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 LeftHomotopyClass.mk_surjective
bijective_rightHomotopyClassToHom 📖	mathematical	—	Function.Bijective RightHomotopyClass ModelCategory.categoryWithWeakEquivalences Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj rightHomotopyClassToHom	—	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 BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences BifibrantObject.instIsLocalizationCompιWeakEquivalences RightHomotopyClass.mk_surjective CategoryTheory.NatIso.naturality_1 Equiv.bijective FibrantObject.instCofibrationIResolutionObj FibrantObject.instWeakEquivalenceIResolutionObj FibrantObject.instIsFibrantResolutionObj isCofibrant_of_cofibration CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeCofibrations ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations CategoryTheory.Localization.inverts weakEquivalence_iff Function.Bijective.of_comp_iff RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id Function.Bijective.comp CofibrantObject.HoCat.exists_resolution isFibrant_of_fibration instIsMultiplicativeFibrations ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence LeftHomotopyClass.mk_surjective CategoryTheory.Category.id_comp
leftHomotopyClassToHom_mk 📖	mathematical	—	leftHomotopyClassToHom ModelCategory.categoryWithWeakEquivalences CategoryTheory.Functor.map	—	—
map_surjective_of_isLocalization 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	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 bijective_leftHomotopyClassToHom
rightHomotopyClassToHom_mk 📖	mathematical	—	rightHomotopyClassToHom ModelCategory.categoryWithWeakEquivalences CategoryTheory.Functor.map	—	—

HomotopicalAlgebra.LeftHomotopyRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_map_eq 📖	mathematical	—	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.Functor.map	—	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 CategoryTheory.AreEqualizedByLocalization.map_eq factorsThroughLocalization HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff HomotopicalAlgebra.bijective_leftHomotopyClassToHom

HomotopicalAlgebra.RightHomotopyRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_map_eq 📖	mathematical	—	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.Functor.map	—	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 CategoryTheory.AreEqualizedByLocalization.map_eq factorsThroughLocalization HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff HomotopicalAlgebra.bijective_rightHomotopyClassToHom

---

← Back to Index