WeakFactorizationSystem

📁 Source: Mathlib/CategoryTheory/MorphismProperty/WeakFactorizationSystem.lean

Statistics

Metric	Count
Definitions IsWeakFactorizationSystem	1
Theorems hasFactorization, llp, mk', rlp, hasLiftingProperty_of_wfs, llp_eq_of_wfs, rlp_eq_of_wfs	7
Total	8

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
IsWeakFactorizationSystem 📖	CompData	3 math math: IsWeakFactorizationSystem.mk', HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations, HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLiftingProperty_of_wfs 📖	mathematical	—	CategoryTheory.HasLiftingProperty	—	llp_eq_of_wfs
llp_eq_of_wfs 📖	mathematical	—	llp	—	IsWeakFactorizationSystem.llp
rlp_eq_of_wfs 📖	mathematical	—	rlp	—	IsWeakFactorizationSystem.rlp

CategoryTheory.MorphismProperty.IsWeakFactorizationSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasFactorization 📖	mathematical	—	CategoryTheory.MorphismProperty.HasFactorization	—	—
llp 📖	mathematical	—	CategoryTheory.MorphismProperty.llp	—	—
mk' 📖	mathematical	CategoryTheory.HasLiftingProperty	CategoryTheory.MorphismProperty.IsWeakFactorizationSystem	—	CategoryTheory.MorphismProperty.rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts CategoryTheory.MorphismProperty.llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts
rlp 📖	mathematical	—	CategoryTheory.MorphismProperty.rlp	—	—

---

← Back to Index