Documentation Verification Report

KanExtension

📁 Source: Mathlib/CategoryTheory/GuitartExact/KanExtension.lean

Statistics

Metric	Count
Definitions `compTwoSquare`, `compTwoSquare`, `isPointwiseLeftKanExtensionAtCompTwoSquareEquiv`, `isPointwiseLeftKanExtensionEquivOfGuitartExact`, `isPointwiseLeftKanExtensionOfCompTwoSquare`, `lanBaseChange`	6
Theorems `nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff`, `hasLeftKanExtension`, `hasPointwiseLeftKanExtension`, `hasPointwiseLeftKanExtensionAt_iff`, `hasPointwiseLeftKanExtension_iff`, `instIsIsoFunctorLanBaseChangeOfGuitartExact`, `isIso_lanBaseChange_app`, `isIso_lanBaseChange_app_iff`, `lanBaseChange_app`	9
Total	15

CategoryTheory.Functor.LeftExtension

Definitions

Name	Category	Theorems
`compTwoSquare` 📖	CompOp	3 math math: `nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff`, `CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff`, `CategoryTheory.TwoSquare.lanBaseChange_app`
`isPointwiseLeftKanExtensionAtCompTwoSquareEquiv` 📖	CompOp	—
`isPointwiseLeftKanExtensionEquivOfGuitartExact` 📖	CompOp	—
`isPointwiseLeftKanExtensionOfCompTwoSquare` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff` 📖	mathematical	—	`IsPointwiseLeftKanExtensionAt` `CategoryTheory.Functor.comp` `compTwoSquare` `CategoryTheory.Functor.obj`	—	`Equiv.nonempty_congr`

CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension

Definitions

Name	Category	Theorems
`compTwoSquare` 📖	CompOp	—

CategoryTheory.TwoSquare

Definitions

Name	Category	Theorems
`lanBaseChange` 📖	CompOp	4 math math: `isIso_lanBaseChange_app`, `isIso_lanBaseChange_app_iff`, `instIsIsoFunctorLanBaseChangeOfGuitartExact`, `lanBaseChange_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLeftKanExtension` 📖	mathematical	`CategoryTheory.Functor.HasPointwiseLeftKanExtension`	`CategoryTheory.Functor.HasLeftKanExtension` `CategoryTheory.Functor.comp`	—	`hasPointwiseLeftKanExtension` `CategoryTheory.Functor.instHasLeftKanExtension`
`hasPointwiseLeftKanExtension` 📖	mathematical	`CategoryTheory.Functor.HasPointwiseLeftKanExtension`	`CategoryTheory.Functor.comp`	—	`CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension`
`hasPointwiseLeftKanExtensionAt_iff` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.Final.hasColimit_comp_iff`
`hasPointwiseLeftKanExtension_iff` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseLeftKanExtension` `CategoryTheory.Functor.comp`	—	`hasPointwiseLeftKanExtensionAt_iff` `instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact` `CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso`
`instIsIsoFunctorLanBaseChangeOfGuitartExact` 📖	mathematical	`CategoryTheory.Functor.HasLeftKanExtension` `CategoryTheory.Functor.HasPointwiseLeftKanExtension`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.lan` `CategoryTheory.Functor.instHasLeftKanExtension` `lanBaseChange`	—	`CategoryTheory.Functor.instHasLeftKanExtension` `CategoryTheory.NatTrans.isIso_iff_isIso_app` `isIso_lanBaseChange_app`
`isIso_lanBaseChange_app` 📖	mathematical	`CategoryTheory.Functor.HasLeftKanExtension` `CategoryTheory.Functor.HasPointwiseLeftKanExtension`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.lan` `CategoryTheory.NatTrans.app` `lanBaseChange`	—	`isIso_lanBaseChange_app_iff` `CategoryTheory.Functor.instIsLeftKanExtensionObjLanAppLanUnit` `CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension`
`isIso_lanBaseChange_app_iff` 📖	mathematical	`CategoryTheory.Functor.HasLeftKanExtension`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.lan` `CategoryTheory.NatTrans.app` `lanBaseChange` `CategoryTheory.Functor.IsLeftKanExtension` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.Functor.LeftExtension.compTwoSquare` `CategoryTheory.Functor.lanUnit` `CategoryTheory.Comma.left` `CategoryTheory.Comma.hom`	—	`lanBaseChange_app` `CategoryTheory.Functor.isIso_lanAdjunction_homEquiv_symm_iff`
`lanBaseChange_app` 📖	mathematical	`CategoryTheory.Functor.HasLeftKanExtension`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringLeft` `CategoryTheory.Functor.lan` `lanBaseChange` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.Adjunction.homEquiv` `CategoryTheory.Functor.lanAdjunction` `CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Functor.id` `CategoryTheory.Functor.LeftExtension.compTwoSquare` `CategoryTheory.Functor.lanUnit`	—	—

---

← Back to Index