Documentation Verification Report

IsKan

📁 Source: Mathlib/CategoryTheory/Bicategory/Kan/IsKan.lean

Statistics

Metric	Count
Definitions `IsAbsKan`, `desc`, `isKan`, `ofIsoAbsKan`, `IsKan`, `desc`, `mk`, `ofCompId`, `ofIsoKan`, `uniqueUpToIso`, `whiskerOfCommute`, `IsAbsKan`, `desc`, `isKan`, `ofIsoAbsKan`, `IsKan`, `desc`, `mk`, `ofIdComp`, `ofIsoKan`, `uniqueUpToIso`, `whiskerOfCommute`, `IsKan`, `IsKan`	24
Theorems `fac`, `fac_assoc`, `hom_ext`, `uniqueUpToIso_hom_right`, `uniqueUpToIso_inv_right`, `fac`, `fac_assoc`, `hom_ext`, `uniqueUpToIso_hom_right`, `uniqueUpToIso_inv_right`	10
Total	34

CategoryTheory.Bicategory.LeftExtension

Definitions

Name	Category	Theorems
`IsAbsKan` 📖	CompOp	—
`IsKan` 📖	CompOp	1 math math: `CategoryTheory.Bicategory.Lan.CommuteWith.commute`

CategoryTheory.Bicategory.LeftExtension.IsAbsKan

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	—
`isKan` 📖	CompOp	—
`ofIsoAbsKan` 📖	CompOp	—

CategoryTheory.Bicategory.LeftExtension.IsKan

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	7 math math: `CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_inv`, `fac_assoc`, `uniqueUpToIso_hom_right`, `CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_inv_right`, `CategoryTheory.Bicategory.lanIsKan_desc`, `uniqueUpToIso_inv_right`, `fac`
`mk` 📖	CompOp	—
`ofCompId` 📖	CompOp	—
`ofIsoKan` 📖	CompOp	—
`uniqueUpToIso` 📖	CompOp	2 math math: `uniqueUpToIso_hom_right`, `uniqueUpToIso_inv_right`
`whiskerOfCommute` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.LeftExtension.extension` `CategoryTheory.Bicategory.LeftExtension.unit` `CategoryTheory.Bicategory.whiskerLeft` `desc`	—	`CategoryTheory.StructuredArrow.IsUniversal.fac`
`fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.LeftExtension.extension` `CategoryTheory.Bicategory.LeftExtension.unit` `CategoryTheory.Bicategory.whiskerLeft` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.LeftExtension.extension` `CategoryTheory.Bicategory.LeftExtension.unit` `CategoryTheory.Bicategory.whiskerLeft`	—	—	`CategoryTheory.StructuredArrow.IsUniversal.hom_ext`
`uniqueUpToIso_hom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `uniqueUpToIso` `desc`	—	—
`uniqueUpToIso_inv_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `uniqueUpToIso` `desc`	—	—

CategoryTheory.Bicategory.LeftLift

Definitions

Name	Category	Theorems
`IsAbsKan` 📖	CompOp	—
`IsKan` 📖	CompOp	1 math math: `CategoryTheory.Bicategory.LanLift.CommuteWith.commute`

CategoryTheory.Bicategory.LeftLift.IsAbsKan

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	—
`isKan` 📖	CompOp	—
`ofIsoAbsKan` 📖	CompOp	—

CategoryTheory.Bicategory.LeftLift.IsKan

Definitions

Name	Category	Theorems
`desc` 📖	CompOp	7 math math: `fac_assoc`, `fac`, `CategoryTheory.Bicategory.lanLiftIsKan_desc`, `uniqueUpToIso_hom_right`, `CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right`, `uniqueUpToIso_inv_right`, `CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_inv`
`mk` 📖	CompOp	—
`ofIdComp` 📖	CompOp	—
`ofIsoKan` 📖	CompOp	—
`uniqueUpToIso` 📖	CompOp	2 math math: `uniqueUpToIso_hom_right`, `uniqueUpToIso_inv_right`
`whiskerOfCommute` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.LeftLift.lift` `CategoryTheory.Bicategory.LeftLift.unit` `CategoryTheory.Bicategory.whiskerRight` `desc`	—	`CategoryTheory.StructuredArrow.IsUniversal.fac`
`fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.LeftLift.lift` `CategoryTheory.Bicategory.LeftLift.unit` `CategoryTheory.Bicategory.whiskerRight` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fac`
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.LeftLift.lift` `CategoryTheory.Bicategory.LeftLift.unit` `CategoryTheory.Bicategory.whiskerRight`	—	—	`CategoryTheory.StructuredArrow.IsUniversal.hom_ext`
`uniqueUpToIso_hom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `uniqueUpToIso` `desc`	—	—
`uniqueUpToIso_inv_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `uniqueUpToIso` `desc`	—	—

CategoryTheory.Bicategory.RightExtension

Definitions

Name	Category	Theorems
`IsKan` 📖	CompOp	—

CategoryTheory.Bicategory.RightLift

Definitions

Name	Category	Theorems
`IsKan` 📖	CompOp	—

---

← Back to Index