Limits

📁 Source: Mathlib/CategoryTheory/LiftingProperties/Limits.lean

Statistics

Metric	Count
Definitions	0
Theorems hasLiftingProperty, hasLiftingProperty, instHasLiftingPropertyFst, instHasLiftingPropertyInl, instHasLiftingPropertyInr, instHasLiftingPropertyMap, instHasLiftingPropertyMap_1, instHasLiftingPropertySnd	8
Total	8

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasLiftingPropertyFst 📖	mathematical	—	HasLiftingProperty Limits.pullback Limits.pullback.fst	—	IsPullback.hasLiftingProperty IsPullback.flip IsPullback.of_hasPullback
instHasLiftingPropertyInl 📖	mathematical	—	HasLiftingProperty Limits.pushout Limits.pushout.inl	—	IsPushout.hasLiftingProperty IsPushout.of_hasPushout
instHasLiftingPropertyInr 📖	mathematical	—	HasLiftingProperty Limits.pushout Limits.pushout.inr	—	IsPushout.hasLiftingProperty IsPushout.flip IsPushout.of_hasPushout
instHasLiftingPropertyMap 📖	mathematical	HasLiftingProperty	Limits.piObj Limits.Pi.map	—	Category.assoc CommSq.w Limits.Pi.map_π sq_hasLift_of_hasLiftingProperty Limits.Pi.hom_ext Limits.limit.lift_π CommSq.fac_left Limits.limit.lift_map CommSq.fac_right
instHasLiftingPropertyMap_1 📖	mathematical	HasLiftingProperty	Limits.sigmaObj Limits.Sigma.map	—	Category.assoc CommSq.w Limits.Sigma.ι_map_assoc sq_hasLift_of_hasLiftingProperty Limits.Sigma.hom_ext Limits.colimit.ι_desc CommSq.fac_left Limits.colimit.ι_desc_assoc CommSq.fac_right
instHasLiftingPropertySnd 📖	mathematical	—	HasLiftingProperty Limits.pullback Limits.pullback.snd	—	IsPullback.hasLiftingProperty IsPullback.of_hasPullback

CategoryTheory.IsPullback

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLiftingProperty 📖	mathematical	CategoryTheory.IsPullback	CategoryTheory.HasLiftingProperty	—	CategoryTheory.Category.assoc CategoryTheory.CommSq.w toCommSq CategoryTheory.sq_hasLift_of_hasLiftingProperty CategoryTheory.CommSq.fac_right hom_ext lift_fst CategoryTheory.CommSq.fac_left lift_snd

CategoryTheory.IsPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLiftingProperty 📖	mathematical	CategoryTheory.IsPushout	CategoryTheory.HasLiftingProperty	—	CategoryTheory.Category.assoc CategoryTheory.CommSq.w toCommSq CategoryTheory.sq_hasLift_of_hasLiftingProperty CategoryTheory.CommSq.fac_left inl_desc hom_ext inl_desc_assoc inr_desc_assoc CategoryTheory.CommSq.fac_right

---

← Back to Index