Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `LiftStruct`, `HasLiftingProperty`, `HasLiftingPropertyFixedBot`, `HasLiftingPropertyFixedTop`	4
Theorems `hasLiftingProperty_iff`, `iff_of_arrow_iso_left`, `iff_of_arrow_iso_right`, `iff_op`, `iff_unop`, `of_arrow_iso_left`, `of_arrow_iso_right`, `of_comp_left`, `of_comp_right`, `of_left_iso`, `of_right_iso`, `op`, `sq_hasLift`, `unop`, `leftLiftingProperty`, `rightLiftingProperty`, `sq_hasLift_of_hasLiftingProperty`	17
Total	21

CategoryTheory

Definitions

Name	Category	Theorems
`HasLiftingProperty` 📖	CompData	35 math math: `instHasLiftingPropertyInl`, `HasLiftingProperty.unop`, `HomotopicalAlgebra.ModelCategory.cm4b`, `HasLiftingProperty.op`, `Injective.instHasLiftingPropertyOfMono`, `HasLiftingProperty.of_left_iso`, `StrongMono.rlp`, `Adjunction.hasLiftingProperty_iff`, `ParametrizedAdjunction.hasLiftingProperty_iff`, `SSet.modelCategoryQuillen.instHasLiftingPropertyιHornHAddNatOfNatOfFibration`, `MorphismProperty.hasLiftingProperty_of_wfs`, `HasLiftingProperty.iff_of_arrow_iso_right`, `Projective.hasLiftingProperty_of_isZero`, `RetractArrow.rightLiftingProperty`, `HasLiftingProperty.of_comp_left`, `HasLiftingProperty.iff_of_arrow_iso_left`, `SmallObject.hasRightLiftingProperty_πObj`, `Injective.hasLiftingProperty_of_isZero`, `instHasLiftingPropertyFst`, `HasLiftingProperty.over`, `instHasLiftingPropertyInr`, `instHasLiftingPropertySnd`, `IsPullback.hasLiftingProperty`, `HasLiftingProperty.iff_op`, `HasLiftingProperty.iff_unop`, `HasLiftingProperty.of_arrow_iso_right`, `HasLiftingProperty.of_arrow_iso_left`, `IsPushout.hasLiftingProperty`, `HasLiftingProperty.of_right_iso`, `Projective.instHasLiftingPropertyOfEpi`, `StrongEpi.llp`, `RetractArrow.leftLiftingProperty`, `HomotopicalAlgebra.ModelCategory.cm4a`, `Arrow.hasLiftingProperty_iff`, `HasLiftingProperty.of_comp_right`
`HasLiftingPropertyFixedBot` 📖	MathDef	—
`HasLiftingPropertyFixedTop` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sq_hasLift_of_hasLiftingProperty` 📖	mathematical	`CommSq`	`CommSq.HasLift`	—	`HasLiftingProperty.sq_hasLift`

CategoryTheory.Arrow

Definitions

Name	Category	Theorems
`LiftStruct` 📖	CompOp	1 math math: `hasLiftingProperty_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLiftingProperty_iff` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `LiftStruct`	—	`CategoryTheory.CommaMorphism.w` `CategoryTheory.sq_hasLift_of_hasLiftingProperty` `CategoryTheory.CommSq.fac_left` `CategoryTheory.CommSq.fac_right` `CategoryTheory.CommSq.w`

CategoryTheory.HasLiftingProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_of_arrow_iso_left` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`of_arrow_iso_left`
`iff_of_arrow_iso_right` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`of_arrow_iso_right`
`iff_op` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`op` `unop`
`iff_unop` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `Opposite` `CategoryTheory.Category.opposite` `Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`unop` `op`
`of_arrow_iso_left` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`CategoryTheory.Arrow.iso_w'` `of_comp_left` `of_left_iso` `CategoryTheory.Arrow.isIso_left` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Arrow.isIso_right` `CategoryTheory.Iso.isIso_hom`
`of_arrow_iso_right` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`CategoryTheory.Arrow.iso_w'` `of_comp_right` `of_right_iso` `CategoryTheory.Arrow.isIso_left` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Arrow.isIso_right` `CategoryTheory.Iso.isIso_hom`
`of_comp_left` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.CommSq.w` `CategoryTheory.CommSq.HasLift.mk'` `CategoryTheory.Category.assoc` `CategoryTheory.sq_hasLift_of_hasLiftingProperty` `CategoryTheory.CommSq.fac_right` `CategoryTheory.CommSq.fac_left`
`of_comp_right` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.CommSq.w` `CategoryTheory.Category.assoc` `CategoryTheory.sq_hasLift_of_hasLiftingProperty` `CategoryTheory.CommSq.fac_left` `CategoryTheory.CommSq.HasLift.mk'` `CategoryTheory.CommSq.fac_right_assoc` `CategoryTheory.CommSq.fac_right`
`of_left_iso` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`CategoryTheory.CommSq.HasLift.mk'` `CategoryTheory.IsIso.hom_inv_id_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.CommSq.w` `CategoryTheory.IsIso.inv_hom_id_assoc`
`of_right_iso` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`CategoryTheory.CommSq.HasLift.mk'` `CategoryTheory.CommSq.w_assoc` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc` `CategoryTheory.IsIso.inv_hom_id`
`op` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.CommSq.unop` `CategoryTheory.sq_hasLift_of_hasLiftingProperty`
`sq_hasLift` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CommSq.HasLift`	—	—
`unop` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty` `Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.CommSq.op` `CategoryTheory.CommSq.HasLift.iff_op` `CategoryTheory.sq_hasLift_of_hasLiftingProperty`

CategoryTheory.RetractArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftLiftingProperty` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`CategoryTheory.Category.assoc` `CategoryTheory.CommSq.w` `CategoryTheory.Arrow.w_mk_right_assoc` `CategoryTheory.sq_hasLift_of_hasLiftingProperty` `i_w_assoc` `CategoryTheory.CommSq.fac_left` `retract_left_assoc` `CategoryTheory.Category.id_comp` `CategoryTheory.CommSq.fac_right` `retract_right_assoc`
`rightLiftingProperty` 📖	mathematical	—	`CategoryTheory.HasLiftingProperty`	—	`CategoryTheory.Category.assoc` `CategoryTheory.CommSq.w` `i_w` `CategoryTheory.sq_hasLift_of_hasLiftingProperty` `CategoryTheory.CommSq.fac_left_assoc` `retract_left` `CategoryTheory.Category.comp_id` `CategoryTheory.Arrow.w_mk_right` `CategoryTheory.CommSq.fac_right_assoc` `retract_right`

---

← Back to Index