Documentation Verification Report

CommSq

📁 Source: Mathlib/CategoryTheory/CommSq.lean

Statistics

Metric	Count
Definitions `HasLift`, `LiftStruct`, `l`, `op`, `opEquiv`, `unop`, `unopEquiv`	7
Theorems `exists_lift`, `iff`, `iff_op`, `iff_unop`, `mk'`, `ext`, `ext_iff`, `fac_left`, `fac_right`, `opEquiv_apply`, `opEquiv_symm_apply`, `op_l`, `unop_l`, `eq_of_epi`, `eq_of_mono`, `fac_left`, `fac_left_assoc`, `fac_right`, `fac_right_assoc`, `flip`, `horiz_comp`, `horiz_inv`, `map`, `of_arrow`, `op`, `subsingleton_liftStruct_of_epi`, `subsingleton_liftStruct_of_mono`, `unop`, `vert_comp`, `vert_inv`, `w`, `w_assoc`, `map_commSq`	33
Total	40

CategoryTheory.CommSq

Definitions

Name	Category	Theorems
`HasLift` 📖	CompData	12 math math: `CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift`, `instHasLift`, `HasLift.over`, `HasLift.mk'`, `CategoryTheory.sq_hasLift_of_hasLiftingProperty`, `HasLift.iff_op`, `right_adjoint_hasLift_iff`, `left_adjoint_hasLift_iff`, `CategoryTheory.HasLiftingProperty.sq_hasLift`, `instHasLift_1`, `HasLift.iff_unop`, `HasLift.iff`
`LiftStruct` 📖	CompData	6 math math: `HasLift.exists_lift`, `LiftStruct.opEquiv_symm_apply`, `subsingleton_liftStruct_of_mono`, `subsingleton_liftStruct_of_epi`, `LiftStruct.opEquiv_apply`, `HasLift.iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_epi` 📖	—	`CategoryTheory.CommSq`	—	—	`CategoryTheory.cancel_epi` `w`
`eq_of_mono` 📖	—	`CategoryTheory.CommSq`	—	—	`CategoryTheory.cancel_mono` `w`
`fac_left` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift`	—	`LiftStruct.fac_left` `HasLift.exists_lift`
`fac_left_assoc` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac_left`
`fac_right` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift`	—	`LiftStruct.fac_right` `HasLift.exists_lift`
`fac_right_assoc` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac_right`
`flip` 📖	—	`CategoryTheory.CommSq`	—	—	`w`
`horiz_comp` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Category.assoc` `w`
`horiz_inv` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Iso.hom`	`CategoryTheory.Iso.inv`	—	`flip` `vert_inv`
`map` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	`CategoryTheory.Functor.map_commSq`
`of_arrow` 📖	mathematical	—	`CategoryTheory.CommSq` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Comma.right` `CategoryTheory.Comma.hom` `CategoryTheory.CommaMorphism.left` `CategoryTheory.CommaMorphism.right`	—	`CategoryTheory.CommaMorphism.w`
`op` 📖	mathematical	`CategoryTheory.CommSq`	`Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`w`
`subsingleton_liftStruct_of_epi` 📖	mathematical	`CategoryTheory.CommSq`	`LiftStruct`	—	`LiftStruct.ext` `CategoryTheory.cancel_epi` `LiftStruct.fac_left`
`subsingleton_liftStruct_of_mono` 📖	mathematical	`CategoryTheory.CommSq`	`LiftStruct`	—	`LiftStruct.ext` `CategoryTheory.cancel_mono` `LiftStruct.fac_right`
`unop` 📖	mathematical	`CategoryTheory.CommSq` `Opposite` `CategoryTheory.Category.opposite`	`Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	`w`
`vert_comp` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`flip` `horiz_comp`
`vert_inv` 📖	mathematical	`CategoryTheory.CommSq` `CategoryTheory.Iso.hom`	`CategoryTheory.Iso.inv`	—	`CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.eq_inv_comp` `w`
`w` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`w_assoc` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

CategoryTheory.CommSq.HasLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lift` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CommSq.LiftStruct`	—	—
`iff` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CommSq.HasLift` `CategoryTheory.CommSq.LiftStruct`	—	`exists_lift`
`iff_op` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CommSq.HasLift` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CommSq.op`	—	`CategoryTheory.CommSq.op` `iff` `Nonempty.congr`
`iff_unop` 📖	mathematical	`CategoryTheory.CommSq` `Opposite` `CategoryTheory.Category.opposite`	`CategoryTheory.CommSq.HasLift` `Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CommSq.unop`	—	`CategoryTheory.CommSq.unop` `iff` `Nonempty.congr`
`mk'` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CommSq.HasLift`	—	—

CategoryTheory.CommSq.LiftStruct

Definitions

Name	Category	Theorems
`l` 📖	CompOp	5 math math: `op_l`, `fac_left`, `fac_right`, `unop_l`, `ext_iff`
`op` 📖	CompOp	2 math math: `op_l`, `opEquiv_apply`
`opEquiv` 📖	CompOp	2 math math: `opEquiv_symm_apply`, `opEquiv_apply`
`unop` 📖	CompOp	2 math math: `opEquiv_symm_apply`, `unop_l`
`unopEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.CommSq` `l`	—	—	—
`ext_iff` 📖	mathematical	`CategoryTheory.CommSq`	`l`	—	`ext`
`fac_left` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `l`	—	—
`fac_right` 📖	mathematical	`CategoryTheory.CommSq`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `l`	—	—
`opEquiv_apply` 📖	mathematical	`CategoryTheory.CommSq`	`DFunLike.coe` `Equiv` `CategoryTheory.CommSq.LiftStruct` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CommSq.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `opEquiv` `op`	—	`CategoryTheory.CommSq.op`
`opEquiv_symm_apply` 📖	mathematical	`CategoryTheory.CommSq`	`DFunLike.coe` `Equiv` `CategoryTheory.CommSq.LiftStruct` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CommSq.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv` `unop`	—	`CategoryTheory.CommSq.op` `CategoryTheory.CommSq.unop`
`op_l` 📖	mathematical	`CategoryTheory.CommSq`	`l` `Opposite` `CategoryTheory.Category.opposite` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CommSq.op` `op`	—	`CategoryTheory.CommSq.op`
`unop_l` 📖	mathematical	`CategoryTheory.CommSq` `Opposite` `CategoryTheory.Category.opposite`	`l` `Opposite.unop` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CommSq.unop` `unop`	—	`CategoryTheory.CommSq.unop`

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_commSq` 📖	mathematical	`CategoryTheory.CommSq`	`obj` `map`	—	`map_comp` `CategoryTheory.CommSq.w`

---

← Back to Index