BrownLemma

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

Statistics

Metric	Count
Definitions CofibrantBrownFactorization, mk', s, toMapFactorizationData, FibrantBrownFactorization, mk', r, toMapFactorizationData	8
Theorems cofibration_s, instNonemptyOfIsCofibrant, instWeakEquivalenceICofibrationsTrivialFibrations, instWeakEquivalenceS, mk'_Z, mk'_i, mk'_p, mk'_s, s_p, s_p_assoc, fibration_r, i_r, i_r_assoc, instNonemptyOfIsFibrant, instWeakEquivalencePTrivialCofibrationsFibrations, instWeakEquivalenceR, mk'_Z, mk'_i, mk'_p, mk'_r	20
Total	28

HomotopicalAlgebra

Definitions

Name	Category	Theorems
CofibrantBrownFactorization 📖	CompData	1 math math: CofibrantBrownFactorization.instNonemptyOfIsCofibrant
FibrantBrownFactorization 📖	CompData	1 math math: FibrantBrownFactorization.instNonemptyOfIsFibrant

HomotopicalAlgebra.CofibrantBrownFactorization

Definitions

Name	Category	Theorems
mk' 📖	CompOp	4 math math: mk'_s, mk'_p, mk'_Z, mk'_i
s 📖	CompOp	5 math math: s_p, cofibration_s, mk'_s, s_p_assoc, instWeakEquivalenceS
toMapFactorizationData 📖	CompOp	8 math math: instWeakEquivalenceICofibrationsTrivialFibrations, s_p, cofibration_s, mk'_p, s_p_assoc, mk'_Z, instWeakEquivalenceS, mk'_i

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofibration_s 📖	mathematical	—	HomotopicalAlgebra.Cofibration CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData s	—	—
instNonemptyOfIsCofibrant 📖	mathematical	—	HomotopicalAlgebra.CofibrantBrownFactorization	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5b CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instWeakEquivalenceICofibrationsTrivialFibrations 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.i	—	HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac HomotopicalAlgebra.ModelCategory.cm2 CategoryTheory.MorphismProperty.MapFactorizationData.fac HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations
instWeakEquivalenceS 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData s	—	HomotopicalAlgebra.weakEquivalence_of_postcomp_of_fac HomotopicalAlgebra.ModelCategory.cm2 s_p HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.ModelCategory.cm3a CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition
mk'_Z 📖	mathematical	—	CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData mk' CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.desc CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
mk'_i 📖	mathematical	—	CategoryTheory.MorphismProperty.MapFactorizationData.i HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData mk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.MorphismProperty.MapFactorizationData.Z CategoryTheory.Limits.coprod.desc CategoryTheory.CategoryStruct.id CategoryTheory.Limits.coprod.inl	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
mk'_p 📖	mathematical	—	CategoryTheory.MorphismProperty.MapFactorizationData.p HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData mk' CategoryTheory.Limits.coprod CategoryTheory.Limits.coprod.desc CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
mk'_s 📖	mathematical	—	s mk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.coprod CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.Limits.coprod.desc CategoryTheory.CategoryStruct.id CategoryTheory.Limits.coprod.inr CategoryTheory.MorphismProperty.MapFactorizationData.i	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
s_p 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData s CategoryTheory.MorphismProperty.MapFactorizationData.p CategoryTheory.CategoryStruct.id	—	—
s_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.cofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.trivialFibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences toMapFactorizationData s CategoryTheory.MorphismProperty.MapFactorizationData.p	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' s_p

HomotopicalAlgebra.FibrantBrownFactorization

Definitions

Name	Category	Theorems
mk' 📖	CompOp	4 math math: mk'_i, mk'_Z, mk'_r, mk'_p
r 📖	CompOp	5 math math: i_r_assoc, instWeakEquivalenceR, fibration_r, mk'_r, i_r
toMapFactorizationData 📖	CompOp	8 math math: i_r_assoc, instWeakEquivalenceR, mk'_i, instWeakEquivalencePTrivialCofibrationsFibrations, mk'_Z, fibration_r, mk'_p, i_r

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fibration_r 📖	mathematical	—	HomotopicalAlgebra.Fibration CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData r	—	—
i_r 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.i r CategoryTheory.CategoryStruct.id	—	—
i_r_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.i r	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' i_r
instNonemptyOfIsFibrant 📖	mathematical	—	HomotopicalAlgebra.FibrantBrownFactorization	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5a CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instWeakEquivalencePTrivialCofibrationsFibrations 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData CategoryTheory.MorphismProperty.MapFactorizationData.p	—	HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac HomotopicalAlgebra.ModelCategory.cm2 CategoryTheory.MorphismProperty.MapFactorizationData.fac HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations
instWeakEquivalenceR 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData r	—	HomotopicalAlgebra.weakEquivalence_of_precomp_of_fac HomotopicalAlgebra.ModelCategory.cm2 i_r HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations HomotopicalAlgebra.instWeakEquivalenceIdOfContainsIdentitiesWeakEquivalences CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.ModelCategory.cm3a CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition
mk'_Z 📖	mathematical	—	CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData mk' CategoryTheory.Limits.prod CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
mk'_i 📖	mathematical	—	CategoryTheory.MorphismProperty.MapFactorizationData.i HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData mk' CategoryTheory.Limits.prod CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
mk'_p 📖	mathematical	—	CategoryTheory.MorphismProperty.MapFactorizationData.p HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations toMapFactorizationData mk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z CategoryTheory.Limits.prod CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.Limits.prod.fst	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
mk'_r 📖	mathematical	—	r mk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.MapFactorizationData.Z HomotopicalAlgebra.trivialCofibrations HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.fibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.prod CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.MorphismProperty.MapFactorizationData.p CategoryTheory.Limits.prod.snd	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape

---

← Back to Index