LiftingProperties

📁 Source: Mathlib/CategoryTheory/Preadditive/Projective/LiftingProperties.lean

Statistics

Metric	Count
Definitions	0
Theorems hasLiftingProperty_of_isZero, instHasLiftingPropertyOfEpi, projective_iff_llp_epimorphisms_of_isZero, projective_iff_llp_epimorphisms_zero	4
Total	4

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective_iff_llp_epimorphisms_of_isZero 📖	mathematical	Limits.IsZero	Projective MorphismProperty.llp MorphismProperty.epimorphisms	—	Projective.hasLiftingProperty_of_isZero Limits.zero_comp sq_hasLift_of_hasLiftingProperty CommSq.fac_right Limits.IsZero.eq_of_src
projective_iff_llp_epimorphisms_zero 📖	mathematical	—	Projective MorphismProperty.llp MorphismProperty.epimorphisms Limits.HasZeroObject.zero' Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasZeroMorphisms.zero	—	projective_iff_llp_epimorphisms_of_isZero Limits.isZero_zero

CategoryTheory.Projective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLiftingProperty_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero	CategoryTheory.HasLiftingProperty	—	CategoryTheory.Limits.IsZero.eq_of_src factorThru_comp
instHasLiftingPropertyOfEpi 📖	mathematical	—	CategoryTheory.HasLiftingProperty CategoryTheory.Limits.HasZeroObject.zero'	—	hasLiftingProperty_of_isZero CategoryTheory.Limits.isZero_zero

---

← Back to Index