Documentation Verification Report

PointwiseRightDerived

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

Statistics

Metric	Count
Definitions `HasPointwiseRightDerivedFunctor`, `HasPointwiseRightDerivedFunctorAt`, `isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization`, `isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization`, `isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor`, `isPointwiseLeftKanExtensionOfIsoOfIsLocalization`	6
Theorems `hasColimit`, `hasColimit'`, `hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor`, `hasPointwiseRightDerivedFunctorAt_iff`, `hasPointwiseRightDerivedFunctorAt_iff_of_mem`, `hasPointwiseRightDerivedFunctor_of_inverts`, `hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor`, `instIsRightDerivedFunctorLiftInvFac`, `isIso_of_isRightDerivedFunctor_of_inverts`, `isRightDerivedFunctor_iff_of_inverts`, `isRightDerivedFunctor_of_inverts`	11
Total	17

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`HasPointwiseRightDerivedFunctor` 📖	MathDef	3 math math: `CategoryTheory.LocalizerMorphism.Derives.hasPointwiseRightDerivedFunctor`, `CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure`, `hasPointwiseRightDerivedFunctor_of_inverts`
`HasPointwiseRightDerivedFunctorAt` 📖	CompData	3 math math: `CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure`, `hasPointwiseRightDerivedFunctorAt_iff_of_mem`, `hasPointwiseRightDerivedFunctorAt_iff`
`isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization` 📖	CompOp	—
`isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor` 📖	CompOp	—
`isPointwiseLeftKanExtensionOfIsoOfIsLocalization` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor` 📖	mathematical	`HasPointwiseRightDerivedFunctor`	`HasPointwiseLeftKanExtension`	—	`CategoryTheory.Localization.essSurj` `hasPointwiseLeftKanExtensionAt_iff_of_iso` `hasPointwiseRightDerivedFunctorAt_iff`
`hasPointwiseRightDerivedFunctorAt_iff` 📖	mathematical	—	`HasPointwiseRightDerivedFunctorAt` `HasPointwiseLeftKanExtensionAt` `obj`	—	`hasPointwiseLeftKanExtensionAt_iff_of_equivalence` `q_isLocalization` `HasPointwiseRightDerivedFunctorAt.hasColimit'`
`hasPointwiseRightDerivedFunctorAt_iff_of_mem` 📖	mathematical	—	`HasPointwiseRightDerivedFunctorAt`	—	`hasPointwiseRightDerivedFunctorAt_iff` `q_isLocalization` `hasPointwiseLeftKanExtensionAt_iff_of_iso`
`hasPointwiseRightDerivedFunctor_of_inverts` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`HasPointwiseRightDerivedFunctor`	—	`hasPointwiseRightDerivedFunctorAt_iff` `q_isLocalization` `LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension`
`hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor` 📖	mathematical	`HasPointwiseRightDerivedFunctor`	`HasRightDerivedFunctor`	—	`hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor` `q_isLocalization` `instHasLeftKanExtension`
`instIsRightDerivedFunctorLiftInvFac` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`IsRightDerivedFunctor` `CategoryTheory.Localization.lift` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `comp` `CategoryTheory.Localization.fac`	—	`isRightDerivedFunctor_of_inverts`
`isIso_of_isRightDerivedFunctor_of_inverts` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `category` `comp`	—	`instIsRightDerivedFunctorLiftInvFac` `rightDerivedNatTrans_fac` `CategoryTheory.Category.id_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_inv` `isIso_whiskerLeft` `CategoryTheory.Iso.isIso_hom`
`isRightDerivedFunctor_iff_of_inverts` 📖	mathematical	`CategoryTheory.MorphismProperty.IsInvertedBy`	`IsRightDerivedFunctor` `CategoryTheory.IsIso` `CategoryTheory.Functor` `category` `comp`	—	`isIso_of_isRightDerivedFunctor_of_inverts` `isRightDerivedFunctor_of_inverts`
`isRightDerivedFunctor_of_inverts` 📖	mathematical	—	`IsRightDerivedFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `category` `comp`	—	`LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension`

CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimit` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff`
`hasColimit'` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt` `CategoryTheory.MorphismProperty.Localization` `CategoryTheory.MorphismProperty.instCategoryLocalization` `CategoryTheory.MorphismProperty.Q` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.Functor.LeftExtension

Definitions

Name	Category	Theorems
`isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization` 📖	CompOp	—

---

← Back to Index