Documentation Verification Report

PointwiseRightDerived

📁 Source: Mathlib/CategoryTheory/Localization/DerivabilityStructure/PointwiseRightDerived.lean

Statistics

Metric	Count
Definitions `rightDerivedFunctorComparison`	1
Theorems `hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure`, `hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure`, `instIsIsoFunctorRightDerivedFunctorComparison`, `isIso_iff_of_isRightDerivabilityStructure`, `isIso_α_iff_of_isRightDerivabilityStructure`, `rightDerivedFunctorComparison_fac`, `rightDerivedFunctorComparison_fac_app`, `rightDerivedFunctorComparison_fac_app_assoc`, `rightDerivedFunctorComparison_fac_assoc`	9
Total	10

CategoryTheory.LocalizerMorphism

Definitions

Name	Category	Theorems
`rightDerivedFunctorComparison` 📖	CompOp	5 math math: `rightDerivedFunctorComparison_fac_app_assoc`, `rightDerivedFunctorComparison_fac`, `rightDerivedFunctorComparison_fac_app`, `rightDerivedFunctorComparison_fac_assoc`, `instIsIsoFunctorRightDerivedFunctorComparison`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt` `CategoryTheory.Functor.comp` `functor` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.q_isLocalization` `CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff` `CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff` `CategoryTheory.TwoSquare.instFinalCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact` `IsRightDerivabilityStructure.guitartExact'` `CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso`
`hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure` 📖	mathematical	—	`CategoryTheory.Functor.HasPointwiseRightDerivedFunctor` `CategoryTheory.Functor.comp` `functor`	—	`hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure` `IsRightDerivabilityStructure.hasRightResolutions` `CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff_of_mem` `RightResolution.hw`
`instIsIsoFunctorRightDerivedFunctorComparison` 📖	mathematical	`CategoryTheory.Functor.HasPointwiseRightDerivedFunctor` `CategoryTheory.Functor.comp` `functor`	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `localizedFunctor` `rightDerivedFunctorComparison`	—	`hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure` `CategoryTheory.Functor.isRightDerivedFunctor_iff_isIso_rightDerivedDesc` `CategoryTheory.Functor.isRightDerivedFunctor_iff_isLeftKanExtension` `CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension` `guitartExact_of_isRightDerivabilityStructure`
`isIso_iff_of_isRightDerivabilityStructure` 📖	mathematical	`CategoryTheory.Functor.HasPointwiseRightDerivedFunctor` `CategoryTheory.Functor.comp` `functor`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app`	—	`CategoryTheory.isIso_comp_right_iff` `CategoryTheory.NatIso.isIso_app_of_isIso` `instIsIsoFunctorRightDerivedFunctorComparison` `rightDerivedFunctorComparison_fac_app` `CategoryTheory.Functor.map_isIso` `CategoryTheory.NatIso.hom_app_isIso`
`isIso_α_iff_of_isRightDerivabilityStructure` 📖	mathematical	`CategoryTheory.Functor.HasPointwiseRightDerivedFunctor` `CategoryTheory.Functor.comp` `functor`	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app`	—	`isIso_iff_of_isRightDerivabilityStructure`
`rightDerivedFunctorComparison_fac` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `functor` `localizedFunctor` `CategoryTheory.Functor.whiskerLeft` `rightDerivedFunctorComparison` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.CatCommSq.iso` `catCommSq`	—	`CategoryTheory.Functor.rightDerived_fac`
`rightDerivedFunctorComparison_fac_app` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `functor` `localizedFunctor` `CategoryTheory.NatTrans.app` `rightDerivedFunctorComparison` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.CatCommSq.iso` `catCommSq`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.congr_app` `rightDerivedFunctorComparison_fac`
`rightDerivedFunctorComparison_fac_app_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `functor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `localizedFunctor` `rightDerivedFunctorComparison` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.CatCommSq.iso` `catCommSq`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `rightDerivedFunctorComparison_fac_app`
`rightDerivedFunctorComparison_fac_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `functor` `localizedFunctor` `CategoryTheory.Functor.whiskerLeft` `rightDerivedFunctorComparison` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.associator` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.CatCommSq.iso` `catCommSq`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `rightDerivedFunctorComparison_fac`

---

← Back to Index