LiftingProperties

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

Statistics

Metric	Count
Definitions	0
Theorems hasLiftingProperty_of_isZero, instHasLiftingPropertyOfMono, injective_iff_rlp_monomorphisms_of_isZero, injective_iff_rlp_monomorphisms_zero	4
Total	4

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_iff_rlp_monomorphisms_of_isZero 📖	mathematical	Limits.IsZero	Injective MorphismProperty.rlp MorphismProperty.monomorphisms	—	Injective.hasLiftingProperty_of_isZero Limits.comp_zero sq_hasLift_of_hasLiftingProperty CommSq.fac_left Limits.IsZero.eq_of_tgt
injective_iff_rlp_monomorphisms_zero 📖	mathematical	—	Injective MorphismProperty.rlp MorphismProperty.monomorphisms Limits.HasZeroObject.zero' Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Limits.HasZeroMorphisms.zero	—	injective_iff_rlp_monomorphisms_of_isZero Limits.isZero_zero

CategoryTheory.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLiftingProperty_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero	CategoryTheory.HasLiftingProperty	—	comp_factorThru CategoryTheory.Limits.IsZero.eq_of_tgt
instHasLiftingPropertyOfMono 📖	mathematical	—	CategoryTheory.HasLiftingProperty CategoryTheory.Limits.HasZeroObject.zero'	—	hasLiftingProperty_of_isZero CategoryTheory.Limits.isZero_zero

---

← Back to Index