Documentation Verification Report

PointwiseLeftDerived

📁 Source: Mathlib/CategoryTheory/Functor/Derived/PointwiseLeftDerived.lean

Statistics

Metric	Count
Definitions `HasPointwiseLeftDerivedFunctor`, `HasPointwiseLeftDerivedFunctorAt`, `isPointwiseRightKanExtensionOfIsIsoOfIsLocalization`, `isPointwiseRightKanExtensionAtOfIsoOfIsLocalization`, `isPointwiseRightKanExtensionOfHasPointwiseLeftDerivedFunctor`, `isPointwiseRightKanExtensionOfIsoOfIsLocalization`	6
Theorems `hasLimit`, `hasLimit'`, `hasLeftDerivedFunctor_of_hasPointwiseLeftDerivedFunctor`, `hasPointwiseLeftDerivedFunctorAt_iff`, `hasPointwiseLeftDerivedFunctorAt_iff_of_mem`, `hasPointwiseLeftDerivedFunctor_of_inverts`, `hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor`, `instIsLeftDerivedFunctorLiftHomFac`, `isIso_of_isLeftDerivedFunctor_of_inverts`, `isLeftDerivedFunctor_iff_of_inverts`, `isLeftDerivedFunctor_of_inverts`	11
Total	17

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`HasPointwiseLeftDerivedFunctor` 📖	MathDef	1 math math: `hasPointwiseLeftDerivedFunctor_of_inverts`
`HasPointwiseLeftDerivedFunctorAt` 📖	CompData	2 math math: `hasPointwiseLeftDerivedFunctorAt_iff`, `hasPointwiseLeftDerivedFunctorAt_iff_of_mem`
`isPointwiseRightKanExtensionAtOfIsoOfIsLocalization` 📖	CompOp	—
`isPointwiseRightKanExtensionOfHasPointwiseLeftDerivedFunctor` 📖	CompOp	—
`isPointwiseRightKanExtensionOfIsoOfIsLocalization` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLeftDerivedFunctor_of_hasPointwiseLeftDerivedFunctor` 📖	mathematical	`HasPointwiseLeftDerivedFunctor`	`HasLeftDerivedFunctor`	—	`hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor` `q_isLocalization` `instHasRightKanExtension`
`hasPointwiseLeftDerivedFunctorAt_iff` 📖	mathematical	—	`HasPointwiseLeftDerivedFunctorAt` `HasPointwiseRightKanExtensionAt` `obj`	—	`hasPointwiseRightKanExtensionAt_iff_of_equivalence` `q_isLocalization` `HasPointwiseLeftDerivedFunctorAt.hasLimit'`
`hasPointwiseLeftDerivedFunctorAt_iff_of_mem` 📖	mathematical	—	`HasPointwiseLeftDerivedFunctorAt`	—	`hasPointwiseLeftDerivedFunctorAt_iff` `q_isLocalization` `hasPointwiseRightKanExtensionAt_iff_of_iso`
`hasPointwiseLeftDerivedFunctor_of_inverts` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`HasPointwiseLeftDerivedFunctor`	—	`hasPointwiseLeftDerivedFunctorAt_iff` `q_isLocalization` `RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension`
`hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor` 📖	mathematical	`HasPointwiseLeftDerivedFunctor`	`HasPointwiseRightKanExtension`	—	`CategoryTheory.Localization.essSurj` `hasPointwiseRightKanExtensionAt_iff_of_iso` `hasPointwiseLeftDerivedFunctorAt_iff`
`instIsLeftDerivedFunctorLiftHomFac` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`IsLeftDerivedFunctor` `CategoryTheory.Localization.lift` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `comp` `CategoryTheory.Localization.fac`	—	`isLeftDerivedFunctor_of_inverts`
`isIso_of_isLeftDerivedFunctor_of_inverts` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `category` `comp`	—	`instIsLeftDerivedFunctorLiftHomFac` `leftDerivedNatTrans_fac` `CategoryTheory.Category.comp_id` `CategoryTheory.IsIso.comp_isIso` `isIso_whiskerLeft` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Iso.isIso_hom`
`isLeftDerivedFunctor_iff_of_inverts` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`IsLeftDerivedFunctor` `CategoryTheory.IsIso` `CategoryTheory.Functor` `category` `comp`	—	`isIso_of_isLeftDerivedFunctor_of_inverts` `isLeftDerivedFunctor_of_inverts`
`isLeftDerivedFunctor_of_inverts` 📖	mathematical	—	`IsLeftDerivedFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `category` `comp`	—	`RightExtension.IsPointwiseRightKanExtension.isRightKanExtension`

CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLimit` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseRightKanExtensionAt` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_iff`
`hasLimit'` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseRightKanExtensionAt` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.Functor.RightExtension

Definitions

Name	Category	Theorems
`isPointwiseRightKanExtensionOfIsIsoOfIsLocalization` 📖	CompOp	—

---

← Back to Index